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.