Make filter lemmas for maps and sets consistent + add cross split property for maps

We have the following lemmas for the combination of filter and union/disjoint for maps and sets:

Lemma map_union_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
  filter P m ∪ filter (λ v, ¬ P v) m = m.
Lemma map_disjoint_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
  filter P m ##ₘ filter (λ v, ¬ P v) m.

Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.

There are two things that are strange here:

• The naming scheme is inconsistent: union_filter vs filter_union
• The statements of the union+filter lemmas is inconsistent

This MR aims to make the set of lemmas for maps and sets consistent. Concretely:

• Sets: Add lemmas disjoint_filter, disjoint_filter_complement, and filter_union_complement.
• Maps: Rename map_disjoint_filter → map_disjoint_filter_complement and map_union_filter → map_filter_union_complement to be consistent with sets.
• Maps: Add lemmas map_disjoint_filter and map_filter_union analogous to sets.
• Maps: Use filter lemmas to prove cross split property.

changed the description

(And similarly map_union_disjoint) I think the name of the set lemma is right, as we usually use operationA_operationB for lemmas where A distributes over B.

My suggestion is to rename map_union_filter into map_union_filter_not. Or does anyone else have suggestions for a better name?

I am very confused now. Then we still have the inconsistency of union_filter vs filter_union?

Then we still have the inconsistency of union_filter vs filter_union?

Oh, I didn't even see that, also the order of the words is the wrong way around...

added 5 commits

• cc70f824 - Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and...
• d692d90f - Add `map_disjoint_filter` and `map_union_filter` similar to sets.
• ebcab097 - Add lemma `disjoint_filter` (analogous to maps).
• 64843223 - Add lemmas `disjoint_filter_complement` and `filter_union_complement` (analogous to maps).
• 26204e75 - Add lemma `map_cross_split`.

Compare with previous version

changed the description

added 1 commit

• 4fc791b3 - CHANGELOG.

Compare with previous version

I have updated the MR and the MR description.

I also added a CHANGELOG entry.

This MR should be ready.

resolved all threads

mentioned in commit fa2e2822

merged

@iris-users

• Make collection of lemmas for filter + union/disjoint consistent for sets and maps:
  • Sets: Add lemmas disjoint_filter, disjoint_filter_complement, and filter_union_complement.
  • Maps: Rename map_disjoint_filter → map_disjoint_filter_complement and map_union_filter → map_filter_union_complement to be consistent with sets.
  • Maps: Add lemmas map_disjoint_filter and map_filter_union analogous to sets.