Add lemmas for commuting funcs with folds

These lemmas were helpful to me in recent proofs (in particular, the multiset one is used for iris/iris#923.) They allow for moving a unitary function on a fold accumulator in and out of the fold as necessary, provided the function commutes appropriately with the fold function.

The location of the multiset lemma in the file is not ideal, since it has to come after gmultiset_ind, which is well after all the other fold lemmas. However, proving it without gmultiset_ind is much harder, and moving gmultiset_ind further up the file is itself non-trivial, so I've opted not to try. Fixed by Robbert's changes.

mentioned in merge request iris!923 (merged)

Thanks for the MR. Some comments:

• It would be good to also have this lemma for sets and lists, and make sure the names are consistent
• The lemma for multisets seems weaker, it requires commutativity and associativity for all elements, and not just those in the set. I think it makes sense to have both versions (with Comm/Assoc and more general premise) for all fold functions.

The lemma for multisets seems weaker, it requires commutativity and associativity for all elements, and not just those in the set. I think it makes sense to have both versions (with Comm/Assoc and more general premise) for all fold functions.

This is in part just for consistency with the rest of the set API, which also requires Comm and Assoc when just an element-wise restriction would do.

I'm happy to try and add these, but is there a nice restatement for maps? I could make a version dropping the key inequality and lookup requirements from the commutativity condition, but maybe there's a better way to generalise it?

added 1 commit

• db3d621b - Extend fold-commuting lemmas to lists, sets

Compare with previous version

resolved all threads

added 5 commits

• 97b27e98 - Add lemmas for commuting funcs with folds
• 8f0af65f - Extend fold-commuting lemmas to lists, sets
• 35ac1b00 - Strengthen multiset disj union lemma
• 6a2cf610 - Strengthen all fold commutativity lemmas
• abf8ba35 - Rename comm_acc -> comm_accum

Compare with previous version

added 1 commit

• e005eabb - Rename comm_acc -> comm_accum

Compare with previous version

resolved all threads

added 2 commits

• 2c18e85a - Strengthen all fold commutativity lemmas
• 5f0dbcaa - Rename comm_acc -> comm_accum

Compare with previous version

added 2 commits

• a58e9316 - Strengthen all fold commutativity lemmas
• 02e829ad - Rename comm_acc -> comm_accum

Compare with previous version

All of these lemmas now have stronger variants which at least only require the commutativity properties to hold on elements of the structure, rather than all values in the type.

The lemmas are not exactly identical. Some of this is due to existing style, but the biggest issue is: the gmultiset strong variant only holds for equality. The other strong lemmas are stated for any preorder. This is due to some weaknesses in the gmultiset API, which having tried to solve, would be a bit of work - namely, there needs to be a proof that set_fold for gmultiset is at least Proper (eq ==> equiv ==> eq) (and ideally Proper (R ==> equiv ==> R) for the right R), similar to the set_fold_proper lemma for finite sets. It would also help to be able to define fold induction, but I don't think this is strictly necessary.

@robbertkrebbers Is there anything left to do for this MR?

mentioned in merge request !492 (merged)

mentioned in merge request !493 (merged)

added 31 commits

• 02e829ad...b4e387e6 - 24 commits from branch iris:master
• 1f6c9330 - Use `Proper (.. => impl)` instead of `Proper (.. => iff)` and `∀ x, Proper ..`...
• 3e68fc48 - Add lemmas for commuting funcs with folds
• aff46f6d - Extend fold-commuting lemmas to lists, sets
• f4c6218d - Strengthen multiset disj union lemma
• 445e0eb5 - Strengthen all fold commutativity lemmas
• 9d280a1d - Rename comm_acc -> comm_accum
• 890eab4f - Weaken premises and tweak proofs.

Compare with previous version

resolved all threads