Draft: Add law `map_fold_foldr` to `FinMap` interface.

See the discussion at https://mattermost.mpi-sws.org/iris/pl/dmdsga9stjgebfwwnjmike56do

This rule expresses a form of "parametricity": it says that regardless of A, B, f, and b, the function map_fold f b m will always traverse the map m in the same order. Namely the order of converting the map into a list.

This law holds for all instances of FinMap we currently have, and I think without weird non-constructive axioms (that allow one to define non-parametric functions) it is impossible to define a FinMap instance that does not satisfy this law.

/cc @johannes @ivanbakel

perhaps this lemma should stay, for backwards compatibility?

It was a rather obscure lemma and seemed only useful to prove the insert lemmas. (Perhaps it should have been Local to signal that...)

The new lemma with an equality and without the commutativity requirement seems to be much more useful on its own.

Do we have any uses of the old lemma in the reverse dependencies?

Do we have any uses of the old lemma in the reverse dependencies?

Not in the ones I have checked out.

marked this merge request as draft

Marked as draft, don't review, since the proposed law might not be strong enough. See discussion on Mattermost.

mentioned in merge request !566 (merged)

Closing in favor of !566 (merged).

closed