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

Add cardinal_Add_In to FMapFacts #12096

Merged
merged 4 commits into from Nov 9, 2023
Merged

Add cardinal_Add_In to FMapFacts #12096

merged 4 commits into from Nov 9, 2023

Commits on Nov 6, 2023

  1. Add cardinal_3 to FMapFacts 

    cardinal_3 asserts that updating a key already present in a map does not
change the number of keys in the map. This complements cardinal_2, which
makes the similar statement for if the key is not present.

It uses a new lemma, Add_transpose_neqkey, which states that it is
possible to transpose two map updates provided they are for different
keys. Since of course `add x e (add y f m) <> add y f (add x e m)`
necessarily, even if `x <> y`, this uses `Add` instead.
    @ivanbakel
    ivanbakel committed Nov 6, 2023
    Configuration menu
    Copy the full SHA
    31a777f View commit details
    Browse the repository at this point in the history

  2. Rename new lemma, compress proofs of new lemmas 

    Rename cardinal_3 -> cardinal_Add_In

Compress and structure proofs for both cardinal_Add_In and
Add_transpose_neqkey using feedback from the PR (coq#12096).
This includes
  * using commas to simplify multiple lines of rewrites, especially when
    using add_eq_o and add_neq_o repeatedly.
  * using `now` and `auto` more to solve trivial goals instead of ending
    proofs with trivial `reflexivity` or `assumption`.
  * split subgoals into bulleted points where relevant, as well as
    indent subgoals for enough/assert.
    @ivanbakel
    ivanbakel committed Nov 6, 2023
    Configuration menu
    Copy the full SHA
    e96de89 View commit details
    Browse the repository at this point in the history

  3. Update cardinal_Add_In proof to shorter version 

    This shorter version was written by Jean-Christophe Léchenet in the
feedback on coq#12096, as a proposed alternative to my longer and
unwieldier proof.

The only change I've made is to inline `remove_In_Add`, which is a lemma
we don't want to expose immediately. Morever, I've had to adjust the
proof slightly because a use of `subst` didn't work on my end - perhaps
this is a Coq change.

Co-authored-by: Jean-Christophe Léchenet <eponier@via.ecp.fr>
    @ivanbakel
    ivanbakel and Jean-Christophe Léchenet committed Nov 6, 2023
    Configuration menu
    Copy the full SHA
    a9c2235 View commit details
    Browse the repository at this point in the history

  4. Add changelog for coq#12096

    @ivanbakel
    ivanbakel committed Nov 6, 2023
    Configuration menu
    Copy the full SHA
    76aab14 View commit details
    Browse the repository at this point in the history