Commit cb08e14f by Robbert Krebbers

### Put `LeibnizEquiv` lemmas for `dom` in section.

parent 74649a4b
 ... ... @@ -142,32 +142,34 @@ Global Instance dom_proper_L `{!Equiv A, !LeibnizEquiv D} : Proper ((≡@{M A}) ==> (=)) (dom D) | 0. Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed. Context `{!LeibnizEquiv D}. Lemma dom_map_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X : (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) → dom D (filter P m) = X. Proof. unfold_leibniz. apply dom_map_filter. Qed. Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅. Proof. unfold_leibniz; apply dom_empty. Qed. Lemma dom_empty_inv_L {A} (m : M A) : dom D m = ∅ → m = ∅. Proof. by intros; apply dom_empty_inv; unfold_leibniz. Qed. Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m. Proof. unfold_leibniz; apply dom_alter. Qed. Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m. Proof. unfold_leibniz; apply dom_insert. Qed. Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}. Proof. unfold_leibniz; apply dom_singleton. Qed. Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m ∖ {[ i ]}. Proof. unfold_leibniz; apply dom_delete. Qed. Lemma dom_union_L {A} (m1 m2 : M A) : dom D (m1 ∪ m2) = dom D m1 ∪ dom D m2. Proof. unfold_leibniz; apply dom_union. Qed. Lemma dom_intersection_L {A} (m1 m2 : M A) : dom D (m1 ∩ m2) = dom D m1 ∩ dom D m2. Proof. unfold_leibniz; apply dom_intersection. Qed. Lemma dom_difference_L {A} (m1 m2 : M A) : dom D (m1 ∖ m2) = dom D m1 ∖ dom D m2. Proof. unfold_leibniz; apply dom_difference. Qed. Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <\$> m) = dom D m. Proof. unfold_leibniz; apply dom_fmap. Qed. Section leibniz. Context `{!LeibnizEquiv D}. Lemma dom_map_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X : (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) → dom D (filter P m) = X. Proof. unfold_leibniz. apply dom_map_filter. Qed. Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅. Proof. unfold_leibniz; apply dom_empty. Qed. Lemma dom_empty_inv_L {A} (m : M A) : dom D m = ∅ → m = ∅. Proof. by intros; apply dom_empty_inv; unfold_leibniz. Qed. Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m. Proof. unfold_leibniz; apply dom_alter. Qed. Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m. Proof. unfold_leibniz; apply dom_insert. Qed. Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}. Proof. unfold_leibniz; apply dom_singleton. Qed. Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m ∖ {[ i ]}. Proof. unfold_leibniz; apply dom_delete. Qed. Lemma dom_union_L {A} (m1 m2 : M A) : dom D (m1 ∪ m2) = dom D m1 ∪ dom D m2. Proof. unfold_leibniz; apply dom_union. Qed. Lemma dom_intersection_L {A} (m1 m2 : M A) : dom D (m1 ∩ m2) = dom D m1 ∩ dom D m2. Proof. unfold_leibniz; apply dom_intersection. Qed. Lemma dom_difference_L {A} (m1 m2 : M A) : dom D (m1 ∖ m2) = dom D m1 ∖ dom D m2. Proof. unfold_leibniz; apply dom_difference. Qed. Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <\$> m) = dom D m. Proof. unfold_leibniz; apply dom_fmap. Qed. End leibniz. End fin_map_dom. Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) : ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!