Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

🚧 Additional example relating tuples and vectors #8

Merged
merged 42 commits into from
Dec 15, 2023
Merged

🚧 Additional example relating tuples and vectors #8

merged 42 commits into from
Dec 15, 2023

Commits on Dec 5, 2023

  1. 🚧 Additional example relating tuples and vectors

    @ecranceMERCE
    ecranceMERCE committed Dec 5, 2023
    Configuration menu
    Copy the full SHA
    e0f55c9 View commit details
    Browse the repository at this point in the history

Commits on Dec 6, 2023

  1. 📄 License on vector ~ tuple example file

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    a9051c6 View commit details
    Browse the repository at this point in the history

  2. ♻️ Move proofs about nat in a separate file

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    661624c View commit details
    Browse the repository at this point in the history

  3. 🚧 Change relation tuple ~ vector

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    b2c098b View commit details
    Browse the repository at this point in the history

  4. 🚧 Wip parametricity proofs on vector

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    3b2e266 View commit details
    Browse the repository at this point in the history

  5. ✨ Param_trans for (4,4)

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    3381a6f View commit details
    Browse the repository at this point in the history

  6. ➕ Edit coqProject

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    6c3bd40 View commit details
    Browse the repository at this point in the history

  7. 🚧 Proof structure improvement

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    d2bdea4 View commit details
    Browse the repository at this point in the history

  8. ✨ Symmetry of witness for nat

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    93dde2c View commit details
    Browse the repository at this point in the history

  9. finish param trans

    @CohenCyril
    CohenCyril committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    74c436a View commit details
    Browse the repository at this point in the history

  10. 🚧 Non-symmetrical proof between tuple and vector

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    8870f0d View commit details
    Browse the repository at this point in the history

  11. 🚧 Explicit transports

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    acb0c9b View commit details
    Browse the repository at this point in the history

  12. 🚧 Trying a double induction principle

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    76d7c98 View commit details
    Browse the repository at this point in the history

  13. ✅ Fill last holes (append/const) with transitivity

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    1a4cbc2 View commit details
    Browse the repository at this point in the history

  14. ✅ End nat_sym

    @ecranceMERCE
    ecranceMERCE committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    1ba1e7f View commit details
    Browse the repository at this point in the history

  15. turning off debug messages

    @CohenCyril
    CohenCyril committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    3fb6569 View commit details
    Browse the repository at this point in the history

  16. finish R_in_mapK_nat

    @CohenCyril
    CohenCyril committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    fe12566 View commit details
    Browse the repository at this point in the history

  17. R_in_mapK for vector

    @CohenCyril
    CohenCyril committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    a7a17de View commit details
    Browse the repository at this point in the history

Commits on Dec 7, 2023

  1. remove some cheats from Vector

    @CohenCyril
    CohenCyril committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    fbebf5d View commit details
    Browse the repository at this point in the history

  2. Iso to Param44 via custom adjointification

    @CohenCyril
    CohenCyril committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    3242f60 View commit details
    Browse the repository at this point in the history

  3. no more cheat in vector

    @CohenCyril
    CohenCyril committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    a6433b3 View commit details
    Browse the repository at this point in the history

  4. 🚧 Arithmetic proofs for vector bool

    @ecranceMERCE
    ecranceMERCE committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    e831723 View commit details
    Browse the repository at this point in the history

  5. 🚧 Proof structure for bounded nat -> bitvector

    @ecranceMERCE
    ecranceMERCE committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    fa83ff6 View commit details
    Browse the repository at this point in the history

  6. 🚧 End 2 proofs

    @ecranceMERCE
    ecranceMERCE committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    7ff2d1a View commit details
    Browse the repository at this point in the history

  7. 🚧 WIP append cons

    @ecranceMERCE
    ecranceMERCE committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    8de6a02 View commit details
    Browse the repository at this point in the history

  8. fix

    @CohenCyril
    CohenCyril committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    b840643 View commit details
    Browse the repository at this point in the history

  9. 🚧 Setbit example

    @ecranceMERCE
    ecranceMERCE committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    0d6823d View commit details
    Browse the repository at this point in the history

  10. stuck on a timeout

    @CohenCyril
    CohenCyril committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    bd3141a View commit details
    Browse the repository at this point in the history

  11. ✨ Param_bool

    @ecranceMERCE
    ecranceMERCE committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    e220da3 View commit details
    Browse the repository at this point in the history

Commits on Dec 8, 2023

  1. 🐛 Make latest files available in the plugin

    @ecranceMERCE
    ecranceMERCE committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    a3dfbf9 View commit details
    Browse the repository at this point in the history

Commits on Dec 9, 2023

  1. ✨ Axiomatised proofs for setbit/getbit and head w/ int

    @ecranceMERCE
    ecranceMERCE committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    4f3b1b4 View commit details
    Browse the repository at this point in the history

  2. 🎨 S/cheat/axiom

    @ecranceMERCE
    ecranceMERCE committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    4ddc5ce View commit details
    Browse the repository at this point in the history

  3. use Bool instead of bool

    @CohenCyril
    CohenCyril committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    ea942c9 View commit details
    Browse the repository at this point in the history

  4. Putting Param_vector in another file

    @CohenCyril
    CohenCyril committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    39ce60f View commit details
    Browse the repository at this point in the history

  5. artifact generation

    @CohenCyril
    CohenCyril committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    ee67c50 View commit details
    Browse the repository at this point in the history

  6. adding snapshot of the artifact

    @CohenCyril
    CohenCyril committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    24ebc48 View commit details
    Browse the repository at this point in the history

  7. anonymize

    @CohenCyril
    CohenCyril committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    71f52d0 View commit details
    Browse the repository at this point in the history

Commits on Dec 10, 2023

  1. removing bug for now and silencing dev debug

    @CohenCyril
    CohenCyril committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    ed563c8 View commit details
    Browse the repository at this point in the history

  2. Comment to explain why we have axioms

    @CohenCyril
    CohenCyril committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    abedf13 View commit details
    Browse the repository at this point in the history

  3. remove last cheats

    @CohenCyril
    CohenCyril committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    0e63442 View commit details
    Browse the repository at this point in the history

Commits on Dec 11, 2023

  1. Temporary fix that enables example append_comm_cons + add cuts

    @CohenCyril
    CohenCyril committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    892d77c View commit details
    Browse the repository at this point in the history

  2. example int_to_Zp was completely wrong, fixing it

    @CohenCyril
    CohenCyril committed Dec 11, 2023
    Configuration menu
    Copy the full SHA
    7092137 View commit details
    Browse the repository at this point in the history