Skip to content

Add lemmas about the union and intersection of filters on maps

Marijn van Wezel requested to merge marijnvanwezel/stdpp:filter_union_intersection into master

When merged, this merge request adds two new lemmas about the intersection and the union of filters on maps, as well as a supporting lemma about the intersection of lookups (such a supporting lemma already existed for unions, lookup_union). The proofs for the two primary lemmas were in part made with the help of Robbert.

To support the intersection of lookups, I had to create an instance of Intersection for the option type. This instance has the following behaviour:

  • None ∩ None → None
  • Some a ∩ None → None
  • None ∩ Some b → None
  • Some a ∩ Some b → Some a

This means that the intersection of option does not have a left identity. I am not sure if this is a problem.

Merge request reports