Skip to content

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

Robbert Krebbers requested to merge robbert/set_map_filter into master

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_filtermap_disjoint_filter_complement and map_union_filtermap_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.
Edited by Robbert Krebbers

Merge request reports