gmultiset lemmas

Thanks for the MR. Looks good apart from the nits.

added 1 commit

• a41a00fd - [gmultiset.v] Make use of `foldr_permutation_proper`.

Compare with previous version

added 1 commit

• 90c03053 - Move out a `Proper ((≡ₚ) ==> R)` instace for `foldr`.

Compare with previous version

resolved all discussions

added 1 commit

• 87c732fc - Simplify the proof of `gmultiset_set_fold_disj_union`.

Compare with previous version

resolved all discussions

I think we should back port these lemmas to finite sets too.

Not sure if that's a job for this MR or not?

added 1 commit

• 765e544c - Add `elements_disj_union` and `set_fold` lemmas.

Compare with previous version

i've added the corresponding lemmas for finite sets. I don't really know where to put the elements_disj_union lemma. I proved it using set_ind induction. But for set_ind you need lemmas about the size function, and for those you need some elements lemmas.

revert is preferred over generalize

Why so?

changed this line in version 6 of the diff

• revert requires fewer keystrokes than generalize dependent
• revert supports multiple arguments, e.g. revert x y z; generalize dependent only supports one argument.
• generalize dependent x will also revert all hypotheses that depend on x. The order is not very well-defined, so you typically run into problems with an intros later. Better to use revert x Hx Hx' to be specific about the order in which the hypotheses that depend on x are being reverted.

i've added the corresponding lemmas for finite sets.

Thank you very much!

I don't really know where to put the elements_disj_union lemma. I proved it using set_ind induction. But for set_ind you need lemmas about the size function, and for those you need some elements lemmas

I see, that's annoying. Not sure there is a proper solution for that. I guess what you've done makes sense.

Here's a shorter proof that does not use set_ind:

Lemma elements_disj_union (X Y : C) :
  X ## Y → elements (X ∪ Y) ≡ₚ elements X ++ elements Y.
Proof.
  intros HXY. apply NoDup_Permutation.
  - apply NoDup_elements.
  - apply NoDup_app. set_solver by eauto using NoDup_elements.
  - set_solver.
Qed.

added 1 commit

• 3521f39b - Add `elements_disj_union` and `set_fold` lemmas.

Compare with previous version

LGTM! Will merge.

Thank you very much for incorporating my suggestions.

mentioned in commit a8e9b673