Commit ebcb867c authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Ralf Jung

Initial Iris commit

parent 02f213ce
...@@ -23,6 +23,7 @@ Arguments compose _ _ _ _ _ _ /. ...@@ -23,6 +23,7 @@ Arguments compose _ _ _ _ _ _ /.
Arguments flip _ _ _ _ _ _ /. Arguments flip _ _ _ _ _ _ /.
Arguments const _ _ _ _ /. Arguments const _ _ _ _ /.
Typeclasses Transparent id compose flip const. Typeclasses Transparent id compose flip const.
Instance: Params (@pair) 2.
(** Change [True] and [False] into notations in order to enable overloading. (** Change [True] and [False] into notations in order to enable overloading.
We will use this in the file [assertions] to give [True] and [False] a We will use this in the file [assertions] to give [True] and [False] a
...@@ -792,6 +793,11 @@ Instance pointwise_transitive {A} `{R : relation B} : ...@@ -792,6 +793,11 @@ Instance pointwise_transitive {A} `{R : relation B} :
Transitive R Transitive (pointwise_relation A R) | 9. Transitive R Transitive (pointwise_relation A R) | 9.
Proof. firstorder. Qed. Proof. firstorder. Qed.
(** ** Unit *)
Instance unit_equiv : Equiv unit := λ _ _, True.
Instance unit_equivalence : Equivalence (@equiv unit _).
Proof. repeat split. Qed.
(** ** Products *) (** ** Products *)
Instance prod_map_injective {A A' B B'} (f : A A') (g : B B') : Instance prod_map_injective {A A' B B'} (f : A A') (g : B B') :
Injective (=) (=) f Injective (=) (=) g Injective (=) (=) f Injective (=) (=) g
...@@ -825,6 +831,15 @@ Section prod_relation. ...@@ -825,6 +831,15 @@ Section prod_relation.
Proof. firstorder eauto. Qed. Proof. firstorder eauto. Qed.
End prod_relation. End prod_relation.
Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation () ().
Instance pair_proper `{Equiv A, Equiv B} :
Proper (() ==> () ==> ()) (@pair A B) | 0 := _.
Instance fst_proper `{Equiv A, Equiv B} :
Proper (() ==> ()) (@fst A B) | 0 := _.
Instance snd_proper `{Equiv A, Equiv B} :
Proper (() ==> ()) (@snd A B) | 0 := _.
Typeclasses Opaque prod_equiv.
(** ** Other *) (** ** Other *)
Lemma or_l P Q : ¬Q P Q P. Lemma or_l P Q : ¬Q P Q P.
Proof. tauto. Qed. Proof. tauto. Qed.
......
...@@ -249,7 +249,7 @@ Ltac unfold_elem_of := ...@@ -249,7 +249,7 @@ Ltac unfold_elem_of :=
For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is
generally powerful enough. This tactic either fails or proves the goal. *) generally powerful enough. This tactic either fails or proves the goal. *)
Tactic Notation "solve_elem_of" tactic3(tac) := Tactic Notation "solve_elem_of" tactic3(tac) :=
simpl in *; setoid_subst;
decompose_empty; decompose_empty;
unfold_elem_of; unfold_elem_of;
solve [intuition (simplify_equality; tac)]. solve [intuition (simplify_equality; tac)].
...@@ -261,7 +261,7 @@ fails or loops on very small goals generated by [solve_elem_of] already. We ...@@ -261,7 +261,7 @@ fails or loops on very small goals generated by [solve_elem_of] already. We
use the [naive_solver] tactic as a substitute. This tactic either fails or use the [naive_solver] tactic as a substitute. This tactic either fails or
proves the goal. *) proves the goal. *)
Tactic Notation "esolve_elem_of" tactic3(tac) := Tactic Notation "esolve_elem_of" tactic3(tac) :=
simpl in *; setoid_subst;
decompose_empty; decompose_empty;
unfold_elem_of; unfold_elem_of;
naive_solver tac. naive_solver tac.
...@@ -273,6 +273,11 @@ Section collection. ...@@ -273,6 +273,11 @@ Section collection.
Global Instance: Lattice C. Global Instance: Lattice C.
Proof. split. apply _. firstorder auto. solve_elem_of. Qed. Proof. split. apply _. firstorder auto. solve_elem_of. Qed.
Global Instance difference_proper : Proper (() ==> () ==> ()) ().
Proof.
intros X1 X2 HX Y1 Y2 HY; apply elem_of_equiv; intros x.
by rewrite !elem_of_difference, HX, HY.
Qed.
Lemma intersection_singletons x : {[x]} {[x]} {[x]}. Lemma intersection_singletons x : {[x]} {[x]} {[x]}.
Proof. esolve_elem_of. Qed. Proof. esolve_elem_of. Qed.
Lemma difference_twice X Y : (X Y) Y X Y. Lemma difference_twice X Y : (X Y) Y X Y.
...@@ -283,6 +288,8 @@ Section collection. ...@@ -283,6 +288,8 @@ Section collection.
Proof. esolve_elem_of. Qed. Proof. esolve_elem_of. Qed.
Lemma difference_union_distr_l X Y Z : (X Y) Z X Z Y Z. Lemma difference_union_distr_l X Y Z : (X Y) Z X Z Y Z.
Proof. esolve_elem_of. Qed. Proof. esolve_elem_of. Qed.
Lemma difference_union_distr_r X Y Z : Z (X Y) (Z X) (Z Y).
Proof. esolve_elem_of. Qed.
Lemma difference_intersection_distr_l X Y Z : (X Y) Z X Z Y Z. Lemma difference_intersection_distr_l X Y Z : (X Y) Z X Z Y Z.
Proof. esolve_elem_of. Qed. Proof. esolve_elem_of. Qed.
...@@ -298,6 +305,8 @@ Section collection. ...@@ -298,6 +305,8 @@ Section collection.
Proof. unfold_leibniz. apply difference_diag. Qed. Proof. unfold_leibniz. apply difference_diag. Qed.
Lemma difference_union_distr_l_L X Y Z : (X Y) Z = X Z Y Z. 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. 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).
Proof. unfold_leibniz. apply difference_union_distr_r. Qed.
Lemma difference_intersection_distr_l_L X Y Z : Lemma difference_intersection_distr_l_L X Y Z :
(X Y) Z = X Z Y Z. (X Y) Z = X Z Y Z.
Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed. Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
...@@ -518,16 +527,13 @@ Section collection_monad. ...@@ -518,16 +527,13 @@ Section collection_monad.
Global Instance collection_fmap_proper {A B} (f : A B) : Global Instance collection_fmap_proper {A B} (f : A B) :
Proper (() ==> ()) (fmap f). Proper (() ==> ()) (fmap f).
Proof. intros X Y E. esolve_elem_of. Qed. Proof. intros X Y [??]; split; esolve_elem_of. Qed.
Global Instance collection_ret_proper {A} :
Proper ((=) ==> ()) (@mret M _ A).
Proof. intros X Y E. esolve_elem_of. Qed.
Global Instance collection_bind_proper {A B} (f : A M B) : Global Instance collection_bind_proper {A B} (f : A M B) :
Proper (() ==> ()) (mbind f). Proper (() ==> ()) (mbind f).
Proof. intros X Y E. esolve_elem_of. Qed. Proof. intros X Y [??]; split; esolve_elem_of. Qed.
Global Instance collection_join_proper {A} : Global Instance collection_join_proper {A} :
Proper (() ==> ()) (@mjoin M _ A). Proper (() ==> ()) (@mjoin M _ A).
Proof. intros X Y E. esolve_elem_of. Qed. Proof. intros X Y [??]; split; esolve_elem_of. Qed.
Lemma collection_bind_singleton {A B} (f : A M B) x : {[ x ]} = f f x. Lemma collection_bind_singleton {A B} (f : A M B) x : {[ x ]} = f f x.
Proof. esolve_elem_of. Qed. Proof. esolve_elem_of. Qed.
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This file collects definitions and theorems on finite collections. Most (** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction importantly, it implements a fold and size function and some useful induction
principles on finite collections . *) principles on finite collections . *)
Require Import Permutation ars listset. Require Import Permutation relations listset.
Require Export numbers collections. Require Export numbers collections.
Instance collection_size `{Elements A C} : Size C := length elements. Instance collection_size `{Elements A C} : Size C := length elements.
......
...@@ -77,15 +77,15 @@ Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed. ...@@ -77,15 +77,15 @@ Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
Lemma delete_insert_dom {A} (m : M A) i x : Lemma delete_insert_dom {A} (m : M A) i x :
i dom D m delete i (<[i:=x]>m) = m. i dom D m delete i (<[i:=x]>m) = m.
Proof. rewrite not_elem_of_dom. apply delete_insert. Qed. 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. Proof.
rewrite map_disjoint_spec, elem_of_equiv_empty. rewrite map_disjoint_spec, elem_of_equiv_empty.
setoid_rewrite elem_of_intersection. setoid_rewrite elem_of_intersection.
setoid_rewrite elem_of_dom. unfold is_Some. naive_solver. setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
Qed. 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. 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. Proof. apply map_disjoint_dom. Qed.
Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 m2) dom D m1 dom D m2. Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 m2) dom D m1 dom D m2.
Proof. Proof.
......
...@@ -5,7 +5,7 @@ finite maps and collects some theory on it. Most importantly, it proves useful ...@@ -5,7 +5,7 @@ finite maps and collects some theory on it. Most importantly, it proves useful
induction principles for finite maps and implements the tactic induction principles for finite maps and implements the tactic
[simplify_map_equality] to simplify goals involving finite maps. *) [simplify_map_equality] to simplify goals involving finite maps. *)
Require Import Permutation. Require Import Permutation.
Require Export ars vector orders. Require Export relations vector orders.
(** * Axiomatization of finite maps *) (** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of (** We require Leibniz equality to be extensional on finite maps. This of
...@@ -71,25 +71,26 @@ Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) := ...@@ -71,25 +71,26 @@ Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) := Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
λ f, merge (difference_with f). λ f, merge (difference_with f).
Instance map_equiv `{ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 1 := λ m1 m2,
i, m1 !! i m2 !! i.
(** The relation [intersection_forall R] on finite maps describes that the (** The relation [intersection_forall R] on finite maps describes that the
relation [R] holds for each pair in the intersection. *) relation [R] holds for each pair in the intersection. *)
Definition map_Forall `{Lookup K A M} (P : K A Prop) : M Prop := Definition map_Forall `{Lookup K A M} (P : K A Prop) : M Prop :=
λ m, i x, m !! i = Some x P i x. λ m, i x, m !! i = Some x P i x.
Definition map_Forall2 `{ A, Lookup K A (M A)} {A B} Definition map_relation `{ A, Lookup K A (M A)} {A B} (R : A B Prop)
(R : A B Prop) (P : A Prop) (Q : B Prop) (P : A Prop) (Q : B Prop) (m1 : M A) (m2 : M B) : Prop := i,
(m1 : M A) (m2 : M B) : Prop := i, option_relation R P Q (m1 !! i) (m2 !! i).
match m1 !! i, m2 !! i with
| Some x, Some y => R x y
| Some x, None => P x
| None, Some y => Q y
| None, None => True
end.
Definition map_included `{ A, Lookup K A (M A)} {A} Definition map_included `{ A, Lookup K A (M A)} {A}
(R : relation A) : relation (M A) := map_Forall2 R (λ _, False) (λ _, True). (R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
Instance map_disjoint `{ A, Lookup K A (M A)} {A} : Disjoint (M A) := Definition map_disjoint `{ A, Lookup K A (M A)} {A} : relation (M A) :=
map_Forall2 (λ _ _, False) (λ _, True) (λ _, True). 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.
Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) := Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
map_Forall2 (=) (λ _, False) (λ _, True). map_included (=).
(** The union of two finite maps only has a meaningful definition for maps (** The union of two finite maps only has a meaningful definition for maps
that are disjoint. However, as working with partial functions is inconvenient that are disjoint. However, as working with partial functions is inconvenient
...@@ -114,12 +115,67 @@ Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A), ...@@ -114,12 +115,67 @@ Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
Section theorems. Section theorems.
Context `{FinMap K M}. Context `{FinMap K M}.
(** ** Setoids *)
Section setoid.
Context `{Equiv A}.
Global Instance map_equivalence `{!Equivalence (() : relation A)} :
Equivalence (() : relation (M A)).
Proof.
split.
* by intros m i.
* by intros m1 m2 ? i.
* by intros m1 m2 m3 ?? i; transitivity (m2 !! i).
Qed.
Global Instance lookup_proper (i : K) :
Proper (() ==> ()) (lookup (M:=M A) i).
Proof. by intros m1 m2 Hm. Qed.
Global Instance partial_alter_proper :
Proper ((() ==> ()) ==> (=) ==> () ==> ()) partial_alter.
Proof.
by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
try apply Hf; apply lookup_proper.
Qed.
Global Instance insert_proper (i : K) :
Proper (() ==> () ==> ()) (insert (M:=M A) i).
Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
Global Instance delete_proper (i : K) :
Proper (() ==> ()) (delete (M:=M A) i).
Proof. by apply partial_alter_proper; [constructor|]. Qed.
Global Instance alter_proper :
Proper ((() ==> ()) ==> (=) ==> () ==> ()) (alter (A:=A) (M:=M A)).
Proof.
intros ?? Hf; apply partial_alter_proper.
by destruct 1; constructor; apply Hf.
Qed.
Lemma merge_ext f g
`{!PropHolds (f None None = None), !PropHolds (g None None = None)} :
(() ==> () ==> ())%signature f g
(() ==> () ==> ())%signature (merge f) (merge g).
Proof.
by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
Qed.
Global Instance union_with_proper :
Proper ((() ==> () ==> ()) ==> () ==> () ==> ()) union_with.
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
by do 2 destruct 1; first [apply Hf | constructor].
Qed.
Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
Proof.
intros m1 m2; split.
* by intros Hm; apply map_eq; intros i; unfold_leibniz; apply lookup_proper.
* by intros <-; intros i; fold_leibniz.
Qed.
End setoid.
(** ** General properties *)
Lemma map_eq_iff {A} (m1 m2 : M A) : m1 = m2 i, m1 !! i = m2 !! i. Lemma map_eq_iff {A} (m1 m2 : M A) : m1 = m2 i, m1 !! i = m2 !! i.
Proof. split. by intros ->. apply map_eq. Qed. Proof. split. by intros ->. apply map_eq. Qed.
Lemma map_subseteq_spec {A} (m1 m2 : M A) : Lemma map_subseteq_spec {A} (m1 m2 : M A) :
m1 m2 i x, m1 !! i = Some x m2 !! i = Some x. m1 m2 i x, m1 !! i = Some x m2 !! i = Some x.
Proof. Proof.
unfold subseteq, map_subseteq, map_Forall2. split; intros Hm i; unfold subseteq, map_subseteq, map_relation. split; intros Hm i;
specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver. specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver.
Qed. Qed.
Global Instance: EmptySpec (M A). Global Instance: EmptySpec (M A).
...@@ -129,9 +185,10 @@ Proof. ...@@ -129,9 +185,10 @@ Proof.
Qed. Qed.
Global Instance: {A} (R : relation A), PreOrder R PreOrder (map_included R). Global Instance: {A} (R : relation A), PreOrder R PreOrder (map_included R).
Proof. Proof.
split; [intros m i; by destruct (m !! i)|]. split; [intros m i; by destruct (m !! i); simpl|].
intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i). intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
destruct (m1 !! i), (m2 !! i), (m3 !! i); try done; etransitivity; eauto. destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_equality';
done || etransitivity; eauto.
Qed. Qed.
Global Instance: PartialOrder (() : relation (M A)). Global Instance: PartialOrder (() : relation (M A)).
Proof. Proof.
...@@ -357,8 +414,8 @@ Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x : ...@@ -357,8 +414,8 @@ Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
( y, m !! i = Some y R y x) map_included R m (<[i:=x]>m). ( y, m !! i = Some y R y x) map_included R m (<[i:=x]>m).
Proof. Proof.
intros ? j; destruct (decide (i = j)) as [->|]. intros ? j; destruct (decide (i = j)) as [->|].
* rewrite lookup_insert. destruct (m !! j); eauto. * rewrite lookup_insert. destruct (m !! j); simpl; eauto.
* rewrite lookup_insert_ne by done. by destruct (m !! j). * rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
Qed. Qed.
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None m <[i:=x]>m. Lemma insert_subseteq {A} (m : M A) i x : m !! i = None m <[i:=x]>m.
Proof. apply partial_alter_subseteq. Qed. Proof. apply partial_alter_subseteq. Qed.
...@@ -465,6 +522,17 @@ Proof. ...@@ -465,6 +522,17 @@ Proof.
* by rewrite lookup_omap, !lookup_singleton. * by rewrite lookup_omap, !lookup_singleton.
* by rewrite lookup_omap, !lookup_singleton_ne. * by rewrite lookup_omap, !lookup_singleton_ne.
Qed. Qed.
Lemma map_fmap_id {A} (m : M A) : id <$> m = m.
Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
Lemma map_fmap_compose {A B C} (f : A B) (g : B C) (m : M A) :
g f <$> m = g <$> f <$> m.
Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
Lemma map_fmap_ext {A B} (f1 f2 : A B) m :
( i x, m !! i = Some x f1 x = f2 x) f1 <$> m = f2 <$> m.
Proof.
intros Hi; apply map_eq; intros i; rewrite !lookup_fmap.
by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
Qed.
(** ** Properties of conversion to lists *) (** ** Properties of conversion to lists *)
Lemma map_to_list_unique {A} (m : M A) i x y : Lemma map_to_list_unique {A} (m : M A) i x y :
...@@ -807,7 +875,7 @@ Lemma insert_merge_r m1 m2 i x z : ...@@ -807,7 +875,7 @@ Lemma insert_merge_r m1 m2 i x z :
Proof. by intros; apply partial_alter_merge_r. Qed. Proof. by intros; apply partial_alter_merge_r. Qed.
End more_merge. End more_merge.
(** ** Properties on the [map_Forall2] relation *) (** ** Properties on the [map_relation] relation *)
Section Forall2. Section Forall2.
Context {A B} (R : A B Prop) (P : A Prop) (Q : B Prop). Context {A B} (R : A B Prop) (P : A Prop) (Q : B Prop).
Context `{ x y, Decision (R x y), x, Decision (P x), y, Decision (Q y)}. Context `{ x y, Decision (R x y), x, Decision (P x), y, Decision (Q y)}.
...@@ -819,8 +887,8 @@ Let f (mx : option A) (my : option B) : option bool := ...@@ -819,8 +887,8 @@ Let f (mx : option A) (my : option B) : option bool :=
| None, Some y => Some (bool_decide (Q y)) | None, Some y => Some (bool_decide (Q y))
| None, None => None | None, None => None
end. end.
Lemma map_Forall2_alt (m1 : M A) (m2 : M B) : Lemma map_relation_alt (m1 : M A) (m2 : M B) :
map_Forall2 R P Q m1 m2 map_Forall (λ _, Is_true) (merge f m1 m2). map_relation R P Q m1 m2 map_Forall (λ _, Is_true) (merge f m1 m2).
Proof. Proof.
split. split.
* intros Hm i P'; rewrite lookup_merge by done; intros. * intros Hm i P'; rewrite lookup_merge by done; intros.
...@@ -830,71 +898,72 @@ Proof. ...@@ -830,71 +898,72 @@ Proof.
destruct (m1 !! i), (m2 !! i); simplify_equality'; auto; destruct (m1 !! i), (m2 !! i); simplify_equality'; auto;
by eapply bool_decide_unpack, Hm. by eapply bool_decide_unpack, Hm.
Qed. Qed.
Global Instance map_Forall2_dec `{ x y, Decision (R x y), x, Decision (P x), Global Instance map_relation_dec `{ x y, Decision (R x y), x, Decision (P x),
y, Decision (Q y)} m1 m2 : Decision (map_Forall2 R P Q m1 m2). y, Decision (Q y)} m1 m2 : Decision (map_relation R P Q m1 m2).
Proof. Proof.
refine (cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2)))); refine (cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2))));
abstract by rewrite map_Forall2_alt. abstract by rewrite map_relation_alt.
Defined. Defined.
(** Due to the finiteness of finite maps, we can extract a witness if the (** Due to the finiteness of finite maps, we can extract a witness if the
relation does not hold. *) relation does not hold. *)
Lemma map_not_Forall2 (m1 : M A) (m2 : M B) : Lemma map_not_Forall2 (m1 : M A) (m2 : M B) :
¬map_Forall2 R P Q m1 m2 i, ¬map_relation R P Q m1 m2 i,
( x y, m1 !! i = Some x m2 !! i = Some y ¬R x y) ( x y, m1 !! i = Some x m2 !! i = Some y ¬R x y)
( x, m1 !! i = Some x m2 !! i = None ¬P x) ( x, m1 !! i = Some x m2 !! i = None ¬P x)
( y, m1 !! i = None m2 !! i = Some y ¬Q y). ( y, m1 !! i = None m2 !! i = Some y ¬Q y).
Proof. Proof.
split. split.
* rewrite map_Forall2_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i. * rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
rewrite lookup_merge in Hm by done. rewrite lookup_merge in Hm by done.
destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack. destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
* by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm; * unfold map_relation, option_relation.
by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
specialize (Hm i); simplify_option_equality. specialize (Hm i); simplify_option_equality.
Qed. Qed.
End Forall2. End Forall2.
(** ** Properties on the disjoint maps *) (** ** Properties on the disjoint maps *)
Lemma map_disjoint_spec {A} (m1 m2 : M A) : 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. Proof.
split; intros Hm i; specialize (Hm i); split; intros Hm i; specialize (Hm i);
destruct (m1 !! i), (m2 !! i); naive_solver. destruct (m1 !! i), (m2 !! i); naive_solver.
Qed. Qed.
Lemma map_disjoint_alt {A} (m1 m2 : M A) : 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. Proof.
split; intros Hm1m2 i; specialize (Hm1m2 i); split; intros Hm1m2 i; specialize (Hm1m2 i);
destruct (m1 !! i), (m2 !! i); naive_solver. destruct (m1 !! i), (m2 !! i); naive_solver.
Qed. Qed.
Lemma map_not_disjoint {A} (m1 m2 : M A) : 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. Proof.
unfold disjoint, map_disjoint. rewrite map_not_Forall2 by solve_decision. unfold disjoint, map_disjoint. rewrite map_not_Forall2 by solve_decision.
split; [|naive_solver]. split; [|naive_solver].
intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver. intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver.
Qed. Qed.
Global Instance: Symmetric (@disjoint (M A) _). Global Instance: Symmetric (map_disjoint : relation (M A)).
Proof. intros A m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed. 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. 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. 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) : 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. Proof. rewrite !map_subseteq_spec, !map_disjoint_spec. eauto. Qed.
Lemma map_disjoint_weaken_l {A} (m1 m1' m2 : M A) : 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. Proof. eauto using map_disjoint_weaken. Qed.
Lemma map_disjoint_weaken_r {A} (m1 m2 m2' : M A) : 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. Proof. eauto using map_disjoint_weaken. Qed.
Lemma map_disjoint_Some_l {A} (m1 m2 : M A) i x: 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. Proof. rewrite map_disjoint_spec, eq_None_not_Some. intros ?? [??]; eauto. Qed.
Lemma map_disjoint_Some_r {A} (m1 m2 : M A) i x: 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