Add cardinal_Add_In to FMapFacts

[ivanbakel]

Kind: feature.

• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

cardinal_Add_In 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.

My proofs are very messy, because I am a relative Coq novice. I'll happily take advice or patches to improve them.

[herbelin]

The two theorems look fully relevant to me. I would however give a more appealing name to cardinal_3, even if @letouzey already used himself names like cardinal_1 and cardinal_3.

What about e.g. cardinal_Add_same?

I must however confess that I don't feel competent to evaluate the proofs done in the PR. They look pretty long and I suspect they could be made a bit more compact, by using e.g. now to close trivial subgoals, or commas to chain rewrite's. I would also recommend using bullets whenever several goals are produced.

Side question: isn't there a stronger theorem we could state? For instance, would it be true that In x m -> Add x e m m' -> m' = m??

In any case, thanks a lot for contributing. There are so many results worth to be provided!

[ivanbakel]

Side question: isn't there a stronger theorem we could state? For instance, would it be true that In x m -> Add x e m m' -> m' = m?

Equality of the map key sets, perhaps? I'm sure that would be provable, but the definitions and mechanisms for map key sets doesn't exist (to my knowledge). Actual map equality isn't possible, (even using Equal or Equiv) because what if find x m = Some e' and e' <> e?

I suspect they could be made a bit more compact, by using e.g. now to close trivial subgoals, or commas to chain rewrite's.

I'll look into making these improvements. As I said, I don't know anything about what constitutes good proof style or technique in Coq, so I'm happy to take any advice.

[eponier]

We could try to prove something like:

Definition Same_keys {A} (m1 m2 : t A) := forall k, In k m1 <-> In k m2.

Lemma Same_keys_cardinal : forall elt (m m' : t elt),
  Same_keys m m' -> cardinal m = cardinal m'.

And then the theorem cardinal_Add_In would follow easily.

[ivanbakel]

Having a look at SetoidList, I think that proof would require touching more files and producing more results. Should those changes become part of this PR, or is this just a suggestion for future changes?

[ppedrot]

Actual map equality isn't possible, (even using Equal or Equiv)

This looks suspicious, if I read correctly the API, Add x e m m' is actually convertible to Equal m' (add x e m). In particular, if this is true, your theorem is a consequence of Equal_cardinal?

[ivanbakel]

In particular, if this is true, your theorem is a consequence of Equal_cardinal?

Only if you also have In x m -> cardinal (add x e m) = cardinal m, which is just a restating of the new lemma in less general terms.

[ppedrot]

Right, sorry.

[eponier]

I couldn't help giving it a try. I tried two approaches, one using remove, the other one using the predicate Same_keys I mentioned above. See here. The proofs need some polishing, though.

[Zimmi48]

@herbelin You probably forgot to self-assign this PR?

[herbelin]

@herbelin You probably forgot to self-assign this PR?

I probably missed the protocol. Is a first approving reviewer of a maintainer group supposed to self-assign?

Doing it anyway.

[ppedrot]

Can't we take @eponier's proof instead? I find it more compact.

[Zimmi48]

I probably missed the protocol. Is a first approving reviewer of a maintainer group supposed to self-assign?

In the case this is the maintainer group which the assignee should come from, then either self-assign, or re-request a review from that group. Otherwise, the PR risks being forgotten by everyone (not in anybody's review request nor assigned PR list).

[eponier]

Here is a more compact version of @ivanbakel 's proof.

In the first link I gave, I proposed two different proofs. One using remove that is rather direct and slightly smaller thant @ivanbakel 's one. Another one using the predicate Same_keys that is far longer, but I think the predicate would be a valuable addition to the library. This may be too big for this PR, though.

I let you decide, and especially @ivanbakel who initiated this PR.

[ivanbakel]

I'm happy to take a patch for improving the proof presented in this PR.

I'm personally uncomfortable with the idea of these changes being bundled with other API changes: I don't see why they would need to be part of this PR, and I wouldn't want the discussion around SameKeys to delay these changes since they are not intrinsically linked.

If someone else wants to insist on taking the SameKeys approach and incorporating these changes, I will close this particular PR and leave it to them.

[ppedrot]

I'd personally prefer the first proof, even maybe without the intermediate lemma. That is, only exporting cardinal_3 and inlining the helper lemma.

[herbelin]

Is the discussion now about three and a half different proofs?

1. current @ivanbakel's proof (a8264c3) and its shortening by @eponier (with Add_transpose_neqkey)
2. first alternative proof by @eponier (with remove_In_Add)
3. second alternative proof by @eponier (with new concept of Same_keys)

3 seems excluded for this PR. If the lemma is inlined 1 and 2 are observationally similar. So how much would it matter which one is chosen?

But why would a lemma be not advised? @ppedrot, do you find them stating too intensional properties and thus too strong constraints on the implementation?

[ppedrot]

So how much would it matter which one is chosen?

Proof style.

But why would a lemma be not advised?

Anything we export in the API is a promise to our users.

[herbelin]

Proof style.

Do you basically mean here use of bullets, indentation, explicit naming of hypotheses to which there is a reference to (which are my own basic criteria)? Or do you mean more?

Anything we export in the API is a promise to our users.

A different way to say the same as I did?

[herbelin]

Anything we export in the API is a promise to our users.

As far as I could see (I hope I'm not mistaken), the extra lemmas, whether it is remove_In_Add, Add_transpose_neqkey, Same_keys_cardinal, ... are all logical consequences of the default signature for ordered finite sets (SFun in FMapInterface). So I'm not sure why it would bind us more to provide these lemmas.

[ppedrot]

the extra lemmas are all logical consequences of the default signature for ordered finite sets

If you push this reasoning to absurd lengths, then Fermat's last theorem should be part of the stdlib since it's a consequence of CIC.

The whole point of an API is to restrict what is available to the user, and as such, anything that involves naming a lemma, writing its precise type and its implementation (when not Qed-terminated) is a piece of surface attack of the API. It's not really serious here, but since our abstraction primitives in Coq are at best primitive (pun somewhat intended), every single addition to the stdlib should be carefully thought about.

[herbelin]

I believe that we agree. We need to add lemmas which "make sense" (useful, expressing an intelligible property, ...). Here, it is about an addition in the file listing consequences of the API of finite maps over an order and I'm ok to carefully think about it.

[herbelin]

To move on, I would propose to follow @ppedrot's view, i.e. - if I followed correctly - to keep the first alternative proof by @eponier (but inlining remove_In_Add). @ivanbakel, this means following the initial goal of your PR with a modified proof, no objection to that?

@ivanbakel:

I'll look into making these improvements. As I said, I don't know anything about what constitutes good proof style or technique in Coq, so I'm happy to take any advice.

My observation is that proof styles vary a lot between people. As alluded above, what I consider important is the consistency of style, in particular a consistent indentation, the explicit naming of hypotheses which are reused later and the use of bullets to structurate the proof, all points which I believe are quite consensual. We could discuss other points, like the level of compactness, or the level of automation, or the time taken for the proof to be checked, ... but these are criteria on which opinions vary more easily. I'm remain ready to hear about more recommendations though.

[ppedrot]

What do we do with this PR? It's been basically ready for ages (minus potentially the changelog, but it's not even clear it's really needed).

[ivanbakel]

Well let me fix this quickly - we can just take the first alternative proof, which is shorter and neater. Going back over my own proof, I couldn't understand a word of it.

[ivanbakel]

Note that the new proof no longer requires Add_transpose_neqkey, so if you feel it's unnecessary I can also tear it out.

[eponier]

Thanks @ppedrot for resurrecting this PR, and thanks @ivanbakel for the work!

I'm glad to see that my proof was useful, but I'd appreciate to be cited for that. Thanks!

[ivanbakel]

Whoops, my mistake, apologies. Mentioned in the commit history but not the changelog - fixed that now.

[ppedrot]

@coqbot run full ci

[ppedrot]

I'm assigning and merging when the CI passes otherwise nothing will ever happen.

[ppedrot]

@coqbot merge now