From 0c2f6db1aed4f51d3b1820d45f306fc9d2af3986 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 6 Sep 2017 11:58:37 +0200 Subject: [PATCH] Add some useful lemmas about `difference` and `delete` --- theories/collections.v | 21 +++++++++++++++++++++ theories/fin_maps.v | 9 +++++++++ 2 files changed, 30 insertions(+) diff --git a/theories/collections.v b/theories/collections.v index c5d8cc8..37ce45f 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -609,6 +609,8 @@ Section collection. Proof. set_solver. Qed. Lemma difference_diag X : X ∖ X ≡ ∅. Proof. set_solver. Qed. + Lemma difference_empty X : X ∖ ∅ ≡ X. + Proof. set_solver. Qed. Lemma difference_union_distr_l X Y Z : (X ∪ Y) ∖ Z ≡ X ∖ Z ∪ Y ∖ Z. Proof. set_solver. Qed. Lemma difference_union_distr_r X Y Z : Z ∖ (X ∪ Y) ≡ (Z ∖ X) ∩ (Z ∖ Y). @@ -671,6 +673,8 @@ Section collection. Proof. unfold_leibniz. apply subseteq_empty_difference. Qed. Lemma difference_diag_L X : X ∖ X = ∅. Proof. unfold_leibniz. apply difference_diag. Qed. + Lemma difference_empty_L X : X ∖ ∅ = X. + Proof. unfold_leibniz. apply difference_empty. Qed. Lemma difference_union_distr_l_L X Y Z : (X ∪ Y) ∖ Z = X ∖ Z ∪ Y ∖ Z. Proof. unfold_leibniz. apply difference_union_distr_l. Qed. Lemma difference_union_distr_r_L X Y Z : Z ∖ (X ∪ Y) = (Z ∖ X) ∩ (Z ∖ Y). @@ -697,6 +701,11 @@ Section collection. intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition]. destruct (decide (x ∈ X)); intuition. Qed. + Lemma difference_union X Y : X ∖ Y ∪ Y ≡ X ∪ Y. + Proof. + intros x. rewrite !elem_of_union; rewrite elem_of_difference. + split; [ | destruct (decide (x ∈ Y)) ]; intuition. + Qed. Lemma subseteq_disjoint_union X Y : X ⊆ Y ↔ ∃ Z, Y ≡ X ∪ Z ∧ X ⊥ Z. Proof. split; [|set_solver]. @@ -706,16 +715,28 @@ Section collection. Proof. intros [HXY1 HXY2] Hdiff. destruct HXY2. set_solver. Qed. Lemma empty_difference_subseteq X Y : X ∖ Y ≡ ∅ → X ⊆ Y. Proof. set_solver. Qed. + Lemma singleton_union_difference X Y x : + {[x]} ∪ (X ∖ Y) ≡ ({[x]} ∪ X) ∖ (Y ∖ {[x]}). + Proof. + intro y; split; intros Hy; [ set_solver | ]. + destruct (decide (y ∈ {[x]})); set_solver. + Qed. Context `{!LeibnizEquiv C}. Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X. Proof. unfold_leibniz. apply union_difference. Qed. + Lemma difference_union_L X Y : X ∖ Y ∪ Y = X ∪ Y. + Proof. unfold_leibniz. apply difference_union. Qed. Lemma non_empty_difference_L X Y : X ⊂ Y → Y ∖ X ≠ ∅. Proof. unfold_leibniz. apply non_empty_difference. Qed. Lemma empty_difference_subseteq_L X Y : X ∖ Y = ∅ → X ⊆ Y. Proof. unfold_leibniz. apply empty_difference_subseteq. Qed. Lemma subseteq_disjoint_union_L X Y : X ⊆ Y ↔ ∃ Z, Y = X ∪ Z ∧ X ⊥ Z. Proof. unfold_leibniz. apply subseteq_disjoint_union. Qed. + Lemma singleton_union_difference_L X Y x : + {[x]} ∪ (X ∖ Y) = ({[x]} ∪ X) ∖ (Y ∖ {[x]}). + Proof. unfold_leibniz. apply singleton_union_difference. Qed. + End dec. End collection. diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 19a8160..9cc9f21 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -409,6 +409,9 @@ Proof. intros. apply map_eq. intros j. by destruct (decide (i = j)) as [->|?]; rewrite ?lookup_delete, ?lookup_delete_ne. Qed. +Lemma delete_idemp {A} (m : M A) i : + delete i (delete i m) = delete i m. +Proof. by setoid_rewrite <-partial_alter_compose. Qed. Lemma delete_partial_alter {A} (m : M A) i f : m !! i = None → delete i (partial_alter f i m) = m. Proof. @@ -418,6 +421,9 @@ Qed. Lemma delete_insert {A} (m : M A) i x : m !! i = None → delete i (<[i:=x]>m) = m. Proof. apply delete_partial_alter. Qed. +Lemma delete_insert_delete {A} (m : M A) i x : + delete i (<[i:=x]>m) = delete i m. +Proof. by setoid_rewrite <-partial_alter_compose. Qed. Lemma insert_delete {A} (m : M A) i x : <[i:=x]>(delete i m) = <[i:=x]> m. Proof. symmetry; apply (partial_alter_compose (λ _, Some x)). Qed. Lemma delete_subseteq {A} (m : M A) i : delete i m ⊆ m. @@ -572,6 +578,9 @@ Proof. Qed. Lemma singleton_non_empty {A} i (x : A) : {[i:=x]} ≠ ∅. Proof. apply insert_non_empty. Qed. +Lemma delete_singleton_ne {A} i j (x : A) : + j ≠ i → delete i {[j := x]} = {[j := x]}. +Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed. (** ** Properties of the map operations *) Lemma fmap_empty {A B} (f : A → B) : f <\$> ∅ = ∅. -- GitLab