Commit 4b5d254e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Notation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom.

parent f41a35e8
......@@ -660,7 +660,7 @@ Arguments sig_map _ _ _ _ _ _ !_ / : assert.
(** We define operational type classes for the traditional operations and
relations on collections: the empty collection [∅], the union [(∪)],
intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
[(⊆)] and element of [(∈)] relation, and disjointess [()]. *)
[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
Class Empty A := empty: A.
Hint Mode Empty ! : typeclass_instances.
Notation "∅" := empty : C_scope.
......@@ -779,56 +779,56 @@ Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope.
Notation "(∉ X )" := (λ x, x X) (only parsing) : C_scope.
Class Disjoint A := disjoint : A A Prop.
Hint Mode Disjoint ! : typeclass_instances.
Hint Mode Disjoint ! : typeclass_instances.
Instance: Params (@disjoint) 2.
Infix "" := disjoint (at level 70) : C_scope.
Notation "()" := disjoint (only parsing) : C_scope.
Notation "( X .)" := (disjoint X) (only parsing) : C_scope.
Notation "(. X )" := (λ Y, Y X) (only parsing) : C_scope.
Infix "*" := (Forall2 ()) (at level 70) : C_scope.
Notation "(*)" := (Forall2 ()) (only parsing) : C_scope.
Infix "**" := (Forall2 (*)) (at level 70) : C_scope.
Infix "1*" := (Forall2 (λ p q, p.1 q.1)) (at level 70) : C_scope.
Infix "2*" := (Forall2 (λ p q, p.2 q.2)) (at level 70) : C_scope.
Infix "1**" := (Forall2 (λ p q, p.1 * q.1)) (at level 70) : C_scope.
Infix "2**" := (Forall2 (λ p q, p.2 * q.2)) (at level 70) : C_scope.
Hint Extern 0 (_ _) => symmetry; eassumption.
Hint Extern 0 (_ * _) => symmetry; eassumption.
Infix "##" := disjoint (at level 70) : C_scope.
Notation "(##)" := disjoint (only parsing) : C_scope.
Notation "( X ##.)" := (disjoint X) (only parsing) : C_scope.
Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : C_scope.
Infix "##*" := (Forall2 (##)) (at level 70) : C_scope.
Notation "(##*)" := (Forall2 (##)) (only parsing) : C_scope.
Infix "##**" := (Forall2 (##*)) (at level 70) : C_scope.
Infix "##1*" := (Forall2 (λ p q, p.1 ## q.1)) (at level 70) : C_scope.
Infix "##2*" := (Forall2 (λ p q, p.2 ## q.2)) (at level 70) : C_scope.
Infix "##1**" := (Forall2 (λ p q, p.1 ##* q.1)) (at level 70) : C_scope.
Infix "##2**" := (Forall2 (λ p q, p.2 ##* q.2)) (at level 70) : C_scope.
Hint Extern 0 (_ ## _) => symmetry; eassumption.
Hint Extern 0 (_ ##* _) => symmetry; eassumption.
Class DisjointE E A := disjointE : E A A Prop.
Hint Mode DisjointE - ! : typeclass_instances.
Instance: Params (@disjointE) 4.
Notation "X { Γ } Y" := (disjointE Γ X Y)
(at level 70, format "X { Γ } Y") : C_scope.
Notation "({ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : C_scope.
Notation "Xs { Γ }* Ys" := (Forall2 ({Γ}) Xs Ys)
(at level 70, format "Xs { Γ }* Ys") : C_scope.
Notation "({ Γ }* )" := (Forall2 ({Γ}))
Notation "X ##{ Γ } Y" := (disjointE Γ X Y)
(at level 70, format "X ##{ Γ } Y") : C_scope.
Notation "(##{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : C_scope.
Notation "Xs ##{ Γ }* Ys" := (Forall2 (##{Γ}) Xs Ys)
(at level 70, format "Xs ##{ Γ }* Ys") : C_scope.
Notation "(##{ Γ }* )" := (Forall2 (##{Γ}))
(only parsing, Γ at level 1) : C_scope.
Notation "X { Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
(at level 70, format "X { Γ1 , Γ2 , .. , Γ3 } Y") : C_scope.
Notation "Xs { Γ1 , Γ2 , .. , Γ3 }* Ys" :=
Notation "X ##{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
(at level 70, format "X ##{ Γ1 , Γ2 , .. , Γ3 } Y") : C_scope.
Notation "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
(Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
(at level 70, format "Xs { Γ1 , Γ2 , .. , Γ3 }* Ys") : C_scope.
Hint Extern 0 (_ {_} _) => symmetry; eassumption.
(at level 70, format "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys") : C_scope.
Hint Extern 0 (_ ##{_} _) => symmetry; eassumption.
Class DisjointList A := disjoint_list : list A Prop.
Hint Mode DisjointList ! : typeclass_instances.
Instance: Params (@disjoint_list) 2.
Notation " Xs" := (disjoint_list Xs) (at level 20, format " Xs") : C_scope.
Notation "## Xs" := (disjoint_list Xs) (at level 20, format "## Xs") : C_scope.
Section disjoint_list.
Context `{Disjoint A, Union A, Empty A}.
Implicit Types X : A.
Inductive disjoint_list_default : DisjointList A :=
| disjoint_nil_2 : (@nil A)
| disjoint_cons_2 (X : A) (Xs : list A) : X Xs Xs (X :: Xs).
| disjoint_nil_2 : ## (@nil A)
| disjoint_cons_2 (X : A) (Xs : list A) : X ## Xs ## Xs ## (X :: Xs).
Global Existing Instance disjoint_list_default.
Lemma disjoint_list_nil : @nil A True.
Lemma disjoint_list_nil : ## @nil A True.
Proof. split; constructor. Qed.
Lemma disjoint_list_cons X Xs : (X :: Xs) X Xs Xs.
Lemma disjoint_list_cons X Xs : ## (X :: Xs) X ## Xs ## Xs.
Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
End disjoint_list.
......
......@@ -186,7 +186,7 @@ Section set_unfold_simple.
Qed.
Global Instance set_unfold_disjoint (P Q : A Prop) X Y :
( x, SetUnfold (x X) (P x)) ( x, SetUnfold (x Y) (Q x))
SetUnfold (X Y) ( x, P x Q x False).
SetUnfold (X ## Y) ( x, P x Q x False).
Proof. constructor. unfold disjoint, collection_disjoint. naive_solver. Qed.
Context `{!LeibnizEquiv C}.
......@@ -371,9 +371,9 @@ Section simple_collection.
Lemma empty_union X Y : X Y X Y .
Proof. set_solver. Qed.
Lemma union_cancel_l X Y Z : Z X Z Y Z X Z Y X Y.
Lemma union_cancel_l X Y Z : Z ## X Z ## Y Z X Z Y X Y.
Proof. set_solver. Qed.
Lemma union_cancel_r X Y Z : X Z Y Z X Z Y Z X Y.
Lemma union_cancel_r X Y Z : X ## Z Y ## Z X Z Y Z X Y.
Proof. set_solver. Qed.
(** Empty *)
......@@ -405,22 +405,22 @@ Section simple_collection.
Proof. by rewrite elem_of_singleton. Qed.
(** Disjointness *)
Lemma elem_of_disjoint X Y : X Y x, x X x Y False.
Lemma elem_of_disjoint X Y : X ## Y x, x X x Y False.
Proof. done. Qed.
Global Instance disjoint_sym : Symmetric (@disjoint C _).
Proof. intros X Y. set_solver. Qed.
Lemma disjoint_empty_l Y : Y.
Lemma disjoint_empty_l Y : ## Y.
Proof. set_solver. Qed.
Lemma disjoint_empty_r X : X .
Lemma disjoint_empty_r X : X ## .
Proof. set_solver. Qed.
Lemma disjoint_singleton_l x Y : {[ x ]} Y x Y.
Lemma disjoint_singleton_l x Y : {[ x ]} ## Y x Y.
Proof. set_solver. Qed.
Lemma disjoint_singleton_r y X : X {[ y ]} y X.
Lemma disjoint_singleton_r y X : X ## {[ y ]} y X.
Proof. set_solver. Qed.
Lemma disjoint_union_l X1 X2 Y : X1 X2 Y X1 Y X2 Y.
Lemma disjoint_union_l X1 X2 Y : X1 X2 ## Y X1 ## Y X2 ## Y.
Proof. set_solver. Qed.
Lemma disjoint_union_r X Y1 Y2 : X Y1 Y2 X Y1 X Y2.
Lemma disjoint_union_r X Y1 Y2 : X ## Y1 Y2 X ## Y1 X ## Y2.
Proof. set_solver. Qed.
(** Big unions *)
......@@ -494,9 +494,9 @@ Section simple_collection.
Lemma empty_union_L X Y : X Y = X = Y = .
Proof. unfold_leibniz. apply empty_union. Qed.
Lemma union_cancel_l_L X Y Z : Z X Z Y Z X = Z Y X = Y.
Lemma union_cancel_l_L X Y Z : Z ## X Z ## Y Z X = Z Y X = Y.
Proof. unfold_leibniz. apply union_cancel_l. Qed.
Lemma union_cancel_r_L X Y Z : X Z Y Z X Z = Y Z X = Y.
Lemma union_cancel_r_L X Y Z : X ## Z Y ## Z X Z = Y Z X = Y.
Proof. unfold_leibniz. apply union_cancel_r. Qed.
(** Empty *)
......@@ -618,7 +618,7 @@ Section collection.
Proof. set_solver. Qed.
Lemma difference_intersection_distr_l X Y Z : (X Y) Z X Z Y Z.
Proof. set_solver. Qed.
Lemma difference_disjoint X Y : X Y X Y X.
Lemma difference_disjoint X Y : X ## Y X Y X.
Proof. set_solver. Qed.
Lemma difference_mono X1 X2 Y1 Y2 :
......@@ -630,7 +630,7 @@ Section collection.
Proof. set_solver. Qed.
(** Disjointness *)
Lemma disjoint_intersection X Y : X Y X Y .
Lemma disjoint_intersection X Y : X ## Y X Y .
Proof. set_solver. Qed.
Section leibniz.
......@@ -683,11 +683,11 @@ Section collection.
Lemma difference_intersection_distr_l_L X Y Z :
(X Y) Z = X Z Y Z.
Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
Lemma difference_disjoint_L X Y : X Y X Y = X.
Lemma difference_disjoint_L X Y : X ## Y X Y = X.
Proof. unfold_leibniz. apply difference_disjoint. Qed.
(** Disjointness *)
Lemma disjoint_intersection_L X Y : X Y X Y = .
Lemma disjoint_intersection_L X Y : X ## Y X Y = .
Proof. unfold_leibniz. apply disjoint_intersection. Qed.
End leibniz.
......@@ -707,7 +707,7 @@ Section collection.
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.
Lemma subseteq_disjoint_union X Y : X Y Z, Y X Z X ## Z.
Proof.
split; [|set_solver].
exists (Y X); split; [auto using union_difference|set_solver].
......@@ -732,7 +732,7 @@ Section collection.
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.
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]}).
......@@ -1052,7 +1052,7 @@ Section seq_set.
Qed.
Lemma seq_set_S_disjoint start len :
{[ start + len ]} seq_set (C:=C) start len.
{[ start + len ]} ## seq_set (C:=C) start len.
Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
Lemma seq_set_S_union start len :
......
......@@ -122,7 +122,7 @@ Proof.
- set_solver.
Qed.
Lemma size_union X Y : X Y size (X Y) = size X + size Y.
Lemma size_union X Y : X ## Y size (X Y) = size X + size Y.
Proof.
intros. unfold size, collection_size. simpl. rewrite <-app_length.
apply Permutation_length, NoDup_Permutation.
......
......@@ -81,14 +81,14 @@ Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
Lemma delete_insert_dom {A} (m : M A) i x :
i dom D m delete i (<[i:=x]>m) = m.
Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 m2 dom D m1 dom D m2.
Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ## m2 dom D m1 ## dom D m2.
Proof.
rewrite map_disjoint_spec, elem_of_disjoint.
setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
Qed.
Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 m2 dom D m1 dom D m2.
Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ## m2 dom D m1 ## dom D m2.
Proof. apply map_disjoint_dom. Qed.
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 dom D m2 m1 m2.
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ## dom D m2 m1 ## m2.
Proof. apply map_disjoint_dom. Qed.
Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 m2) dom D m1 dom D m2.
Proof.
......
......@@ -92,10 +92,10 @@ Definition map_included `{∀ A, Lookup K A (M A)} {A}
(R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
Definition map_disjoint `{ A, Lookup K A (M A)} {A} : relation (M A) :=
map_relation (λ _ _, False) (λ _, True) (λ _, True).
Infix "ₘ" := map_disjoint (at level 70) : C_scope.
Hint Extern 0 (_ _) => symmetry; eassumption.
Notation "( m ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
Notation "(.ₘ m )" := (λ m2, m2 m) (only parsing) : C_scope.
Infix "##ₘ" := map_disjoint (at level 70) : C_scope.
Hint Extern 0 (_ ## _) => symmetry; eassumption.
Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
Notation "(.##ₘ m )" := (λ m2, m2 ## m) (only parsing) : C_scope.
Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
map_included (=).
......@@ -1313,19 +1313,19 @@ End Forall2.
(** ** Properties on the disjoint maps *)
Lemma map_disjoint_spec {A} (m1 m2 : M A) :
m1 m2 i x y, m1 !! i = Some x m2 !! i = Some y False.
m1 ## m2 i x y, m1 !! i = Some x m2 !! i = Some y False.
Proof.
split; intros Hm i; specialize (Hm i);
destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Lemma map_disjoint_alt {A} (m1 m2 : M A) :
m1 m2 i, m1 !! i = None m2 !! i = None.
m1 ## m2 i, m1 !! i = None m2 !! i = None.
Proof.
split; intros Hm1m2 i; specialize (Hm1m2 i);
destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Lemma map_not_disjoint {A} (m1 m2 : M A) :
¬m1 m2 i x1 x2, m1 !! i = Some x1 m2 !! i = Some x2.
¬m1 ## m2 i x1 x2, m1 !! i = Some x1 m2 !! i = Some x2.
Proof.
unfold disjoint, map_disjoint. rewrite map_not_Forall2 by solve_decision.
split; [|naive_solver].
......@@ -1333,26 +1333,26 @@ Proof.
Qed.
Global Instance map_disjoint_sym : Symmetric (map_disjoint : relation (M A)).
Proof. intros A m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed.
Lemma map_disjoint_empty_l {A} (m : M A) : m.
Lemma map_disjoint_empty_l {A} (m : M A) : ## m.
Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed.
Lemma map_disjoint_empty_r {A} (m : M A) : m .
Lemma map_disjoint_empty_r {A} (m : M A) : m ## .
Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed.
Lemma map_disjoint_weaken {A} (m1 m1' m2 m2' : M A) :
m1' m2' m1 m1' m2 m2' m1 m2.
m1' ## m2' m1 m1' m2 m2' m1 ## m2.
Proof. rewrite !map_subseteq_spec, !map_disjoint_spec. eauto. Qed.
Lemma map_disjoint_weaken_l {A} (m1 m1' m2 : M A) :
m1' m2 m1 m1' m1 m2.
m1' ## m2 m1 m1' m1 ## m2.
Proof. eauto using map_disjoint_weaken. Qed.
Lemma map_disjoint_weaken_r {A} (m1 m2 m2' : M A) :
m1 m2' m2 m2' m1 m2.
m1 ## m2' m2 m2' m1 ## m2.
Proof. eauto using map_disjoint_weaken. Qed.
Lemma map_disjoint_Some_l {A} (m1 m2 : M A) i x:
m1 m2 m1 !! i = Some x m2 !! i = None.
m1 ## m2 m1 !! i = Some x m2 !! i = None.
Proof. rewrite map_disjoint_spec, eq_None_not_Some. intros ?? [??]; eauto. Qed.
Lemma map_disjoint_Some_r {A} (m1 m2 : M A) i x:
m1 m2 m2 !! i = Some x m1 !! i = None.
m1 ## m2 m2 !! i = Some x m1 !! i = None.
Proof. rewrite (symmetry_iff map_disjoint). apply map_disjoint_Some_l. Qed.
Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i:=x]} m m !! i = None.
Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i:=x]} ## m m !! i = None.
Proof.
split; [|rewrite !map_disjoint_spec].
- intro. apply (map_disjoint_Some_l {[i := x]} _ _ x);
......@@ -1362,20 +1362,20 @@ Proof.
+ by rewrite lookup_singleton_ne.
Qed.
Lemma map_disjoint_singleton_r {A} (m : M A) i x :
m {[i := x]} m !! i = None.
m ## {[i := x]} m !! i = None.
Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_singleton_l. Qed.
Lemma map_disjoint_singleton_l_2 {A} (m : M A) i x :
m !! i = None {[i := x]} m.
m !! i = None {[i := x]} ## m.
Proof. by rewrite map_disjoint_singleton_l. Qed.
Lemma map_disjoint_singleton_r_2 {A} (m : M A) i x :
m !! i = None m {[i := x]}.
m !! i = None m ## {[i := x]}.
Proof. by rewrite map_disjoint_singleton_r. Qed.
Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1 m2 delete i m1 m2.
Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1 ## m2 delete i m1 ## m2.
Proof.
rewrite !map_disjoint_alt. intros Hdisjoint j. destruct (Hdisjoint j); auto.
rewrite lookup_delete_None. tauto.
Qed.
Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1 m2 m1 delete i m2.
Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1 ## m2 m1 ## delete i m2.
Proof. symmetry. by apply map_disjoint_delete_l. Qed.
(** ** Properties of the [union_with] operation *)
......@@ -1495,7 +1495,7 @@ Qed.
Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 m1 m2 .
Proof. eauto using map_positive_l. Qed.
Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
m1 m2 (m1 m2) !! i = Some x m1 !! i = Some x m2 !! i = Some x.
m1 ## m2 (m1 m2) !! i = Some x m1 !! i = Some x m2 !! i = Some x.
Proof.
intros Hdisjoint. rewrite lookup_union_Some_raw.
intuition eauto using map_disjoint_Some_r.
......@@ -1504,9 +1504,9 @@ Lemma lookup_union_Some_l {A} (m1 m2 : M A) i x :
m1 !! i = Some x (m1 m2) !! i = Some x.
Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
m1 m2 m2 !! i = Some x (m1 m2) !! i = Some x.
m1 ## m2 m2 !! i = Some x (m1 m2) !! i = Some x.
Proof. intro. rewrite lookup_union_Some; intuition. Qed.
Lemma map_union_comm {A} (m1 m2 : M A) : m1 m2 m1 m2 = m2 m1.
Lemma map_union_comm {A} (m1 m2 : M A) : m1 ## m2 m1 m2 = m2 m1.
Proof.
intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
intros i. specialize (Hdisjoint i).
......@@ -1524,14 +1524,14 @@ Lemma map_union_subseteq_l {A} (m1 m2 : M A) : m1 ⊆ m1 ∪ m2.
Proof.
rewrite map_subseteq_spec. intros ? i x. rewrite lookup_union_Some_raw. tauto.
Qed.
Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 m2 m2 m1 m2.
Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ## m2 m2 m1 m2.
Proof.
intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
Qed.
Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 m2 m1 m2 m3.
Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
m2 m3 m1 m3 m1 m2 m3.
m2 ## m3 m1 m3 m1 m2 m3.
Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 m2 m3 m1 m3 m2.
Proof.
......@@ -1539,52 +1539,52 @@ Proof.
rewrite !lookup_union_Some_raw. naive_solver.
Qed.
Lemma map_union_mono_r {A} (m1 m2 m3 : M A) :
m2 m3 m1 m2 m1 m3 m2 m3.
m2 ## m3 m1 m2 m1 m3 m2 m3.
Proof.
intros. rewrite !(map_union_comm _ m3)
by eauto using map_disjoint_weaken_l.
by apply map_union_mono_l.
Qed.
Lemma map_union_reflecting_l {A} (m1 m2 m3 : M A) :
m3 m1 m3 m2 m3 m1 m3 m2 m1 m2.
m3 ## m1 m3 ## m2 m3 m1 m3 m2 m1 m2.
Proof.
rewrite !map_subseteq_spec. intros Hm31 Hm32 Hm i x ?. specialize (Hm i x).
rewrite !lookup_union_Some in Hm by done. destruct Hm; auto.
by rewrite map_disjoint_spec in Hm31; destruct (Hm31 i x x).
Qed.
Lemma map_union_reflecting_r {A} (m1 m2 m3 : M A) :
m1 m3 m2 m3 m1 m3 m2 m3 m1 m2.
m1 ## m3 m2 ## m3 m1 m3 m2 m3 m1 m2.
Proof.
intros ??. rewrite !(map_union_comm _ m3) by done.
by apply map_union_reflecting_l.
Qed.
Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) :
m1 m3 m2 m3 m3 m1 = m3 m2 m1 = m2.
m1 ## m3 m2 ## m3 m3 m1 = m3 m2 m1 = m2.
Proof.
intros. apply (anti_symm ()); apply map_union_reflecting_l with m3;
auto using (reflexive_eq (R:=@subseteq (M A) _)).
Qed.
Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) :
m1 m3 m2 m3 m1 m3 = m2 m3 m1 = m2.
m1 ## m3 m2 ## m3 m1 m3 = m2 m3 m1 = m2.
Proof.
intros. apply (anti_symm ()); apply map_union_reflecting_r with m3;
auto using (reflexive_eq (R:=@subseteq (M A) _)).
Qed.
Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) :
m1 m2 m3 m1 m3 m2 m3.
m1 m2 ## m3 m1 ## m3 m2 ## m3.
Proof.
rewrite !map_disjoint_alt. setoid_rewrite lookup_union_None. naive_solver.
Qed.
Lemma map_disjoint_union_r {A} (m1 m2 m3 : M A) :
m1 m2 m3 m1 m2 m1 m3.
m1 ## m2 m3 m1 ## m2 m1 ## m3.
Proof.
rewrite !map_disjoint_alt. setoid_rewrite lookup_union_None. naive_solver.
Qed.
Lemma map_disjoint_union_l_2 {A} (m1 m2 m3 : M A) :
m1 m3 m2 m3 m1 m2 m3.
m1 ## m3 m2 ## m3 m1 m2 ## m3.
Proof. by rewrite map_disjoint_union_l. Qed.
Lemma map_disjoint_union_r_2 {A} (m1 m2 m3 : M A) :
m1 m2 m1 m3 m1 m2 m3.
m1 ## m2 m1 ## m3 m1 ## m2 m3.
Proof. by rewrite map_disjoint_union_r. Qed.
Lemma insert_union_singleton_l {A} (m : M A) i x : <[i:=x]>m = {[i := x]} m.
Proof.
......@@ -1601,22 +1601,22 @@ Proof.
by apply map_disjoint_singleton_l.
Qed.
Lemma map_disjoint_insert_l {A} (m1 m2 : M A) i x :
<[i:=x]>m1 m2 m2 !! i = None m1 m2.
<[i:=x]>m1 ## m2 m2 !! i = None m1 ## m2.
Proof.
rewrite insert_union_singleton_l.
by rewrite map_disjoint_union_l, map_disjoint_singleton_l.
Qed.
Lemma map_disjoint_insert_r {A} (m1 m2 : M A) i x :
m1 <[i:=x]>m2 m1 !! i = None m1 m2.
m1 ## <[i:=x]>m2 m1 !! i = None m1 ## m2.
Proof.
rewrite insert_union_singleton_l.
by rewrite map_disjoint_union_r, map_disjoint_singleton_r.
Qed.
Lemma map_disjoint_insert_l_2 {A} (m1 m2 : M A) i x :
m2 !! i = None m1 m2 <[i:=x]>m1 m2.
m2 !! i = None m1 ## m2 <[i:=x]>m1 ## m2.
Proof. by rewrite map_disjoint_insert_l. Qed.
Lemma map_disjoint_insert_r_2 {A} (m1 m2 : M A) i x :
m1 !! i = None m1 m2 m1 <[i:=x]>m2.
m1 !! i = None m1 ## m2 m1 ## <[i:=x]>m2.
Proof. by rewrite map_disjoint_insert_r. Qed.
Lemma insert_union_l {A} (m1 m2 : M A) i x :
<[i:=x]>(m1 m2) = <[i:=x]>m1 m2.
......@@ -1640,7 +1640,7 @@ Proof. apply delete_union_with. Qed.
(** ** Properties of the [union_list] operation *)
Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
ms m Forall (. m) ms.
ms ## m Forall (.## m) ms.
Proof.
split.
- induction ms; simpl; rewrite ?map_disjoint_union_l; intuition.
......@@ -1648,13 +1648,13 @@ Proof.
by rewrite map_disjoint_union_l.
Qed.
Lemma map_disjoint_union_list_r {A} (ms : list (M A)) (m : M A) :
m ms Forall (. m) ms.
m ## ms Forall (.## m) ms.
Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_union_list_l. Qed.
Lemma map_disjoint_union_list_l_2 {A} (ms : list (M A)) (m : M A) :
Forall (. m) ms ms m.
Forall (.## m) ms ms ## m.
Proof. by rewrite map_disjoint_union_list_l. Qed.
Lemma map_disjoint_union_list_r_2 {A} (ms : list (M A)) (m : M A) :
Forall (. m) ms m ms.
Forall (.## m) ms m ## ms.
Proof. by rewrite map_disjoint_union_list_r. Qed.
(** ** Properties of the folding the [delete] function *)
......@@ -1681,10 +1681,10 @@ Proof.
rewrite IHis, delete_insert_ne; intuition.
Qed.
Lemma map_disjoint_foldr_delete_l {A} (m1 m2 : M A) is :
m1 m2 foldr delete m1 is m2.
m1 ## m2 foldr delete m1 is ## m2.
Proof. induction is; simpl; auto using map_disjoint_delete_l. Qed.
Lemma map_disjoint_foldr_delete_r {A} (m1 m2 : M A) is :