Add `set_fold_union_strong` and similarly for map
This discussion at Mattermost nerdsniped me to add the lemma set_fold_union
and the stronger lemma set_fold_union_strong
that only requires idempotence/associativity/commutativity for the elements in the sets.
Interestingly, the already existing "disjoint" versions of the lemma can be derived.
The proofs are pretty long/tricky, so I tried to add some comments what's going on.
Merge request reports
Activity
added 1 commit
- aa287975 - Add lemmas `set_fold_union_strong` and `set_fold_union`.
- Resolved by Robbert Krebbers
- Resolved by Robbert Krebbers
I noticed there's an inconsistency in naming between the fold lemmas for maps and sets.
- For maps we use no suffix for the "strong" version, and
_L
for the=
version. See e.g.,map_fold_insert
andmap_fold_insert_L
. - For sets we use suffix
_strong
for the "strong" version, and no suffix for the=
version. See e.g.,set_fold_disj_union_strong
andset_fold_disj_union
.
I would be in favor of using the convention for sets also for maps.
Also it appears lemmas for fold + (disjoint)union are missing for maps.
- For maps we use no suffix for the "strong" version, and
- Resolved by Robbert Krebbers
how about I open a new MR where we can bikeshed about renamings?
Or an issue? I am not sure we have consensus yet so don't spend time adjusting all the names quite yet.^^
I think for distinguishing general relation vs
=
I would prefer names ending in_gen(eral)
vs_eq
, or something like that.We do have
gen_proper
lemmas in Iris for a similar situation.Edited by Ralf Jung
added S-waiting-for-author label
added 533 commits
-
4f656cac...d37b5e70 - 531 commits from branch
master
- 5c4a203e - Add lemma `foldr_idemp`.
- 754c7a6e - Add lemmas `set_fold_union_strong` and `set_fold_union`.
-
4f656cac...d37b5e70 - 531 commits from branch
mentioned in issue #215
mentioned in merge request !573 (merged)