`⊆` lemmas for maps are a mess
Roughly there are four kinds of lemmas:
-
f .. m .. ⊆ m
(for examplemap_subseteq_difference_l
,map_empty_subseteq
,delete_subseteq
) -
m ⊆ f .. m ..
(for examplepartial_alter_subseteq
,insert_subseteq
,map_union_subseteq_l
,map_union_subseteq_r
) -
m1 ⊆ m2 → f .. m1 .. ⊆ f .. m2 ..
(for examplealter_mono
,delete_mono
,map_filter_strong_subseteq_ext
,map_filter_subseteq_ext
,map_filter_mono
) -
f .. m1 .. ⊆ f .. m2 .. ↔ stuff
(likemap_singleton_subseteq
).
Of kind (2), there's also variants with transitivity wired in like:
Lemma insert_subseteq_r {A} (m1 m2 : M A) i x : m1 !! i = None → m1 ⊆ m2 → m1 ⊆ <[i:=x]>m2.
Lemma insert_subseteq_l {A} (m1 m2 : M A) i x : m2 !! i = Some x → m1 ⊆ m2 → <[i:=x]> m1 ⊆ m2.
Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
Such a mess... It would be great if we could come up with a decent naming scheme.