diff --git a/coq/ra/_CoqProject b/coq/ra/_CoqProject
index e65919141ca07c463a1db6177a5347bcef7befac..83a5e928c81acd3753ef30af22c4168a957219d7 100644
--- a/coq/ra/_CoqProject
+++ b/coq/ra/_CoqProject
@@ -1,4 +1,5 @@
-Q . ra
+infrastructure.v
machine.v
lang.v
tactics.v
diff --git a/coq/ra/infrastructure.v b/coq/ra/infrastructure.v
new file mode 100644
index 0000000000000000000000000000000000000000..9c55f8ce2c8836389feadefd318f54a3ecc5bd0b
--- /dev/null
+++ b/coq/ra/infrastructure.v
@@ -0,0 +1,360 @@
+From mathcomp Require Import ssreflect ssrbool seq.
+From iris.prelude Require Export strings list numbers.
+From iris.prelude Require Export gmap finite mapset.
+Global Generalizable All Variables.
+Global Set Automatic Coercions Import.
+Global Set Asymmetric Patterns.
+Global Set Bullet Behavior "Strict Subproofs".
+From Coq Require Export Utf8.
+Instance injective_dec_eq
+ `{H : ∀ x y : A, Decision (x = y)} {B : Type}
+ f (g : A -> option B) (Inj : ∀ x, g (f x) = Some x) : ∀ x y : B, Decision (x = y) | 1000.
+Proof.
+ move => x y. case: (decide (f x = f y)).
+ - move/(f_equal g). rewrite !Inj => [[]]. by left.
+ - move => NEq. right => Eq. apply: NEq. by rewrite Eq.
+Qed.
+
+Class Extension A := extension : relation A.
+Instance: Params (@extension) 2.
+Infix "⊑" := extension (at level 70) : C_scope.
+Notation "(⊑)" := extension (only parsing) : C_scope.
+Notation "( X ⊑ )" := (extension 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.
+
+Class StrictExtension A := strict_extension : relation A.
+Instance: Params (@strict_extension) 2.
+Infix "âŠ" := strict_extension (at level 70) : C_scope.
+Notation "(âŠ)" := strict_extension (only parsing) : C_scope.
+Notation "( X ⊠)" := (strict_extension 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.
+
+Class Join A := join : A → A → A.
+Instance: Params (@join) 2.
+Infix "⊔" := join (at level 50, left associativity) : C_scope.
+Notation "(⊔)" := join (only parsing) : C_scope.
+Notation "( x ⊔)" := (join x) (only parsing) : C_scope.
+Notation "(⊔ x )" := (λ y, join y x) (only parsing) : C_scope.
+Infix "⊔*" := (zip_with (⊔)) (at level 50, left associativity) : C_scope.
+Notation "(⊔*)" := (zip_with (⊔)) (only parsing) : C_scope.
+Infix "⊔**" := (zip_with (zip_with (⊔)))
+ (at level 50, left associativity) : C_scope.
+Infix "⊔*⊔**" := (zip_with (prod_zip (⊔) (⊔*)))
+ (at level 50, left associativity) : C_scope.
+
+
+Class JoinSemiLattice A `{Extension A, Join A} : Prop := {
+ join_semi_lattice_pre :>> PreOrder (⊑);
+ join_ext_l X Y : X ⊑ X ⊔ Y;
+ join_ext_r X Y : Y ⊑ X ⊔ Y;
+ join_least X Y Z : X ⊑ Z → Y ⊑ Z → X ⊔ Y ⊑ Z
+}.
+
+Instance JSL_Comm `{E : Extension A} `{J : Join A} `{@PartialOrder A (⊑)} `{@JoinSemiLattice A E J} : @Comm A _ (=) (⊔).
+Proof.
+ move => ? ?.
+ apply: anti_symm; apply: join_least; by eauto using join_ext_l, join_ext_r.
+Qed.
+
+Instance JSL_Assoc `{E : Extension A} `{J : Join A} `{@PartialOrder A (⊑)} `{@JoinSemiLattice A E J} : @Assoc A (=) (⊔).
+Proof.
+ move => ? ? ?.
+ apply: anti_symm; repeat apply: join_least;
+ by eauto using PreOrder_Transitive, join_ext_l, join_ext_r.
+Qed.
+
+(* Generic Instances for Extension, Join and JoinSemiLattice *)
+Instance prod_Extension `{Extension A} `{Extension B} : Extension (A * B) :=
+ λ p1 p2, p1.1 ⊑ p2.1 ∧ p1.2 ⊑ p2.2.
+Instance prod_PreOrder `{Extension A} `{Extension B} `{PreOrder A (⊑)} `{PreOrder B (⊑)} : @PreOrder (A * B) (⊑).
+Proof.
+ econstructor.
+ - move => ?; cbv; split; by apply PreOrder_Reflexive.
+ - move => ? ? ? [H11 H12] [H21 H22]; split.
+ + by apply (PreOrder_Transitive _ _ _ H11 H21).
+ + by apply (PreOrder_Transitive _ _ _ H12 H22).
+Qed.
+
+Instance prod_PartialOrder `{Extension A} `{Extension B} `{PartialOrder A (⊑)} `{PartialOrder B (⊑)} : @PartialOrder (A * B) (⊑).
+Proof.
+ econstructor.
+ - by apply prod_PreOrder.
+ - move => [? ?] [? ?] [? ?] [? ?]. f_equal; by apply: anti_symm.
+Qed.
+
+Instance prod_Join `{Join A} `{Join B} : Join (A * B) :=
+ λ p1 p2, (p1.1 ⊔ p2.1, p1.2 ⊔ p2.2).
+Instance prod_JSL `{JoinSemiLattice A} `{JoinSemiLattice B} : JoinSemiLattice (A * B).
+Proof.
+ econstructor.
+ - exact: prod_PreOrder.
+ - move => ? ?; split; by apply join_ext_l.
+ - move => ? ?; split; by apply join_ext_r.
+ - move => ? ? ? [? ?] [? ?]. split; by apply join_least.
+Qed.
+
+Instance option_Extension `{Extension T} : Extension (option T) :=
+ λ o1 o2, match o1 with
+ | None => True
+ | Some t1 => match o2 with
+ | None => False
+ | Some t2 => t1 ⊑ t2
+ end
+ end.
+
+Instance option_StrictExtension `{StrictExtension T} : StrictExtension (option T) :=
+ λ o1 o2, match o1 with
+ | None => match o2 with
+ | None => False
+ | Some t2 => True
+ end
+ | Some t1 => match o2 with
+ | None => False
+ | Some t2 => t1 ⊠t2
+ end
+ end.
+
+Instance option_StrictOrder `{StrictExtension T} `{StrictOrder T (âŠ)} : @StrictOrder (option T) (âŠ).
+Proof.
+ econstructor.
+ - move => ?. cbv; repeat case_match => //. by apply: StrictOrder_Irreflexive.
+ - move => ? ? ?. cbv; repeat case_match => //. by apply: StrictOrder_Transitive.
+Qed.
+
+Instance option_Join `{Join T} : Join (option T) :=
+ λ o1 o2, match o1 with
+ | None => o2
+ | Some t1 => match o2 with
+ | None => o1
+ | Some t2 => Some $ t1 ⊔ t2
+ end
+ end.
+Instance option_PreOrder `{Extension T} `{PreOrder T (⊑)} : @PreOrder (option T) (⊑).
+Proof.
+ econstructor.
+ - move => ?; cbv; repeat case_match => //.
+ exact: PreOrder_Reflexive.
+ - move => ? ? ?; cbv; repeat case_match => //.
+ exact: PreOrder_Transitive.
+Qed.
+
+Instance option_PartialOrder `{Extension T} `{PartialOrder T (⊑)} : @PartialOrder (option T) (⊑).
+Proof.
+ econstructor.
+ - by eauto with typeclass_instances.
+ - move => [?|] [?|] //; cbv => ? ?. f_equal. exact: anti_symm.
+Qed.
+
+Instance option_Reflexive `{Extension T} `{Reflexive T (⊑)} : @Reflexive (option T) (⊑).
+Proof. move => ?. cbv. by case_match. Qed.
+
+Instance option_AntiSymm `{Extension T} `{AntiSymm T (=) (⊑)} : AntiSymm (=) ((⊑) : relation (option T)).
+Proof.
+ move => ? ?; cbv; repeat case_match => //; move => H1 H2. apply/f_equal.
+ by apply (@anti_symm _ _ _ H0).
+Qed.
+
+Instance option_Comm `{Join T} `{@Comm T _ (=) join} : @Comm (option T) _ (=) (join).
+Proof.
+ move => ? ?; cbv; repeat case_match => //. f_equal. by apply comm.
+Qed.
+
+(* Instance option_Assoc `{Join T} `{@Assoc T (=) join} : @Assoc (option T) (=) (join). *)
+(* Proof. *)
+(* move => ? ? ?. cbv; repeat case_match => //; f_equal; simplify_option_eq. *)
+(* - by apply assoc. *)
+(* - reflexivity. *)
+(* - reflexivity. *)
+(* Qed. *)
+
+Instance option_JSL `{JoinSemiLattice T} : JoinSemiLattice (option T).
+Proof.
+ econstructor.
+ - exact: option_PreOrder.
+ - move => ? ?. cbv; repeat case_match => //; simplify_option_eq.
+ + by apply join_ext_l.
+ + by apply PreOrder_Reflexive.
+ - move => ? ?. cbv; repeat case_match => //; simplify_option_eq.
+ + by apply join_ext_r.
+ + by apply PreOrder_Reflexive.
+ - move => ? ? ?; cbv; repeat case_match => //; simplify_option_eq.
+ by apply join_least.
+Qed.
+
+(* Some auxilliary lemmas about option instances *)
+Lemma option_ext_is_Some `{Extension T} (o1 o2 : option T) : o1 ⊑ o2 -> is_Some o1 -> is_Some o2.
+Proof.
+ cbv; (repeat case_match).
+ - by eauto.
+ - by eauto.
+ - by move => _ [] //.
+Qed.
+
+Lemma join_None `{Join T} (o1 : option T) : o1 ⊔ None = o1.
+Proof. by cbv; repeat case_match. Qed.
+Lemma option_subseteq_None_l `{Extension T} (o1 o2 : option T) : o1 ⊑ None ↔ o1 = None.
+Proof. by cbv; repeat case_match. Qed.
+
+
+(* Positive instances *)
+Instance positive_Extension : Extension positive := (≤)%positive.
+Instance positive_StrictExtension : StrictExtension positive := (<)%positive.
+Instance positive_Join : Join positive := Pos.max.
+Instance positive_PreOrder : PreOrder (⊑)%positive.
+Proof.
+ econstructor; unfold extension, positive_Extension;
+ by eauto using Pos.le_refl, Pos.le_trans.
+Qed.
+Instance positive_PartialOrder : PartialOrder (⊑)%positive.
+Proof.
+ econstructor.
+ - by eauto with typeclass_instances.
+ - exact: Pos.le_antisym.
+Qed.
+Instance positive_StrictOrder : StrictOrder (âŠ)%positive.
+Proof.
+ econstructor; unfold strict_extension, positive_StrictExtension.
+ - move => ? ?. exact: Pos.lt_irrefl.
+ - exact: Pos.lt_trans.
+Qed.
+Instance positive_Total : Total (⊑)%positive.
+Proof.
+ move => x y. case: (decide (x ≤ y)%positive); try tauto.
+ move/Pos.lt_nle/Pos.lt_le_incl. tauto.
+Qed.
+
+Instance positive_Reflexive : Reflexive (⊑)%positive.
+Proof. exact: Pos.le_refl. Qed.
+Instance positive_AntiSymm : AntiSymm (=) (⊑)%positive.
+Proof. exact: Pos.le_antisym. Qed.
+(* Instance positive_Comm : Comm (=) (join)%positive. *)
+(* Proof. exact: Pos.max_comm. Qed. *)
+(* Instance positive_Assoc : Assoc (=) (join)%positive. *)
+(* Proof. exact: Pos.max_assoc. Qed. *)
+
+Instance poisitive_JSL : JoinSemiLattice positive.
+Proof.
+ econstructor.
+ - by eauto with typeclass_instances.
+ - move => ? ?. exact: Pos.le_max_l.
+ - move => ? ?. exact: Pos.le_max_r.
+ - move => ? ? ?. exact: Pos.max_lub.
+Qed.
+
+
+(* gmap instances *)
+Instance gmap_countable `{Countable K} `{Countable A} : Countable (gmap K A) :=
+ injective_countable (map_to_list : _ -> list (K * A))
+ ((λ l : list (_ * _), Some (map_of_list l)) : list _ -> option _) _.
+Proof.
+ intros. f_equal. exact: map_of_to_list.
+Qed.
+
+Instance gmap_Join `{Countable K} `{Join A} : Join (gmap K A) :=
+ union_with (λ a1 a2, Some $ a1 ⊔ a2).
+
+Lemma lookup_join `{Countable K} `{Join A} (f1 f2 : gmap K A) k : (f1 ⊔ f2) !! k = f1 !! k ⊔ f2 !! k.
+Proof.
+ rewrite lookup_union_with.
+ by do 2!case: (_ !! k).
+Qed.
+
+Instance gmap_Assoc `{Countable K} `{Join A} `{@Assoc A (=) join} : @Assoc (gmap K A) (=) join.
+Proof.
+ move => ? ? ?. apply: map_eq => k.
+ rewrite !lookup_union_with.
+ repeat case: (_ !! k) => //=.
+ move => ? ? ?. f_equal. by apply assoc.
+Qed.
+
+Instance gmap_Extension `{Countable K} `{Extension A} : Extension (gmap K A) :=
+ λ f1 f2, ∀ k, f1 !! k ⊑ f2 !! k.
+
+Instance gmap_PreOrder `{Countable K} `{Extension A} `{PreOrder A (⊑)} : @PreOrder (gmap K A) (⊑).
+Proof.
+ econstructor.
+ - move => ? ?; reflexivity.
+ - move => ? ? ? ? ? ?. by etransitivity.
+Qed.
+Instance gmap_PartialOrder `{Countable K} `{Extension A} `{PartialOrder A (⊑)} : @PartialOrder (gmap K A) (⊑).
+Proof.
+ econstructor.
+ - by eauto with typeclass_instances.
+ - move => ? ? ? ?. apply: map_eq => k. by apply: anti_symm.
+Qed.
+
+Instance gmap_JSL `{Countable K} `{JoinSemiLattice A} : JoinSemiLattice (gmap K A).
+Proof.
+ econstructor.
+ - exact: gmap_PreOrder.
+ - move => ? ? ?. rewrite lookup_join. by apply join_ext_l.
+ - move => ? ? ?. rewrite lookup_join. by apply join_ext_r.
+ - move => ? ? ? ? ? ?. rewrite lookup_join. by apply join_least.
+Qed.
+
+(* unit instances *)
+Instance unit_Extension : Extension () :=
+ λ u1 u2, True.
+Instance unit_Join : Join () :=
+ λ u1 u2, tt.
+Instance unit_PreOrder : @PreOrder () (⊑).
+Proof. econstructor; by auto. Qed.
+Instance unit_JSL : JoinSemiLattice ().
+Proof. econstructor; first exact: unit_PreOrder; by auto. Qed.
+
+(* gset instances *)
+Instance gset_Extension `{Countable K} : Extension (gset K) :=
+ λ s1 s2, ∀ k, k ∈ s1 → k ∈ s2.
+Instance gset_Join `{Countable K} : Join (gset K) :=
+ λ s1 s2, Mapset (join (A:=gmap K ()) (mapset_car s1) (mapset_car s2)).
+Instance gset_PreOrder `{Countable K} : @PreOrder (gset K) (extension).
+Proof.
+ econstructor.
+ - by move => ? ? //.
+ - move => ? ? ? ? ? ?. by eauto.
+Qed.
+Instance gset_PartialOrder `{Countable K} : @PartialOrder (gset K) (extension).
+Proof.
+ econstructor.
+ - by eauto with typeclass_instances.
+ - move => ? ? H1 H2. apply/mapset_eq => ?. split; by [move/H1|move/H2].
+Qed.
+Instance gset_JSL `{Countable K} : JoinSemiLattice (gset K).
+Proof.
+ econstructor.
+ - exact: gset_PreOrder.
+ - move => ? ? ? In. do 2!red. rewrite lookup_join. rewrite In. by case: (_ !! _) => //.
+ - move => ? ? ? In. do 2!red. rewrite lookup_join. rewrite In. by case: (_ !! _) => //.
+ - move => ? ? ? H1 H2 k.
+ move: (H1 k) (H2 k).
+ unfold elem_of, mapset_elem_of.
+ rewrite lookup_join. by repeat case : (_ !! _) => [[]|] //.
+Qed.
+
+Lemma gset_Assoc `{Countable K} : @Assoc (gset K) (=) join.
+Proof. move => ? ? ?. by rewrite /join /gset_Join gmap_Assoc. Qed.
+
+Lemma elem_of_join `{Countable K} (s1 s2 : gset K) (k : K) : k ∈ (join s1 s2) ↔ k ∈ s1 ∨ k ∈ s2.
+Proof.
+ unfold elem_of, mapset_elem_of. cbn.
+ unfold join, gmap_Join.
+ rewrite lookup_union_with.
+ repeat case: (_ !! k) => [[]|]; tauto.
+Qed.
+
+Lemma elem_of_extension `{Countable K} (X Y : gset K) : X ⊑ Y ↔ (∀ x : K, x ∈ X → x ∈ Y).
+Proof. tauto. Qed.
\ No newline at end of file
diff --git a/coq/ra/machine.v b/coq/ra/machine.v
index f2acc194e0113bd76deea56e6b22bb64d945bb79..641b2e65ff797b445e7466ba66f4e4a07e737d4e 100644
--- a/coq/ra/machine.v
+++ b/coq/ra/machine.v
@@ -1,6 +1,6 @@
From mathcomp Require Import ssreflect ssrbool seq.
-From iris.prelude Require Export strings list numbers.
-From iris.prelude Require Export gmap finite co_pset mapset.
+From iris.prelude Require Export strings list numbers sorting.
+From iris.prelude Require Export gmap finite mapset.
Global Generalizable All Variables.
Global Set Automatic Coercions Import.
@@ -10,6 +10,8 @@ From Coq Require Export Utf8.
Open Scope positive.
+From ra Require Export infrastructure.
+
Reserved Notation "'<' x → v @ t , R >" (at level 20, format "< x → v @ t , R >",
x at level 21, v at level 21, t at level 21, R at level 21).
@@ -17,17 +19,6 @@ Reserved Notation "'<' x → v @ t , R >" (at level 20, format "< x → v @ t ,
Section RAMachine.
Context `{Countable Loc} `{Countable Val0}.
- Section Infrastructure.
- Instance injective_dec_eq
- `{H : ∀ x y : A, Decision (x = y)} {B : Type}
- f (g : A -> option B) (Inj : ∀ x, g (f x) = Some x) : ∀ x y : B, Decision (x = y) | 1000.
- Proof.
- move => x y. case: (decide (f x = f y)).
- - move/(f_equal g). rewrite !Inj => [[]]. by left.
- - move => NEq. right => Eq. apply: NEq. by rewrite Eq.
- Qed.
- End Infrastructure.
-
Inductive Val :=
| A | D | VInj (v : Val0).
(* Definition isval : _ -> Prop := λ v, match v with V _ => True | _ => False end. *)
@@ -48,53 +39,6 @@ Section RAMachine.
}.
Global Arguments mkMessage _ _ _%positive _.
-
- Global Instance Time_SubsetEq : SubsetEq Time := Pos.le.
- Global Instance Time_Union : Union Time := Pos.max.
- Global Instance Time_SubsteqAntiSymm : AntiSymm (=) (Time_SubsetEq) := Pos.le_antisym.
- Global Instance Time_JoinSemiLattice : JoinSemiLattice Time.
- Proof.
- split.
- - by auto with typeclass_instances.
- - by firstorder using Pos.le_max_l.
- - by firstorder using Pos.le_max_r.
- - move => t1 t2 t3 H13 H23. by apply/Pos.max_lub_iff.
- Qed.
-
- Global Existing Instance option_union | 1000.
- Global Instance opt_le_union `{Union T} : Union (option T) | 0 :=
- λ o1 o2, match o1 with | Some x => Some match o2 with Some y => (x ∪ y) | None => x end | None => o2 end.
- Global Instance opt_le_SubsetEq `{SubsetEq T} : SubsetEq (option T) :=
- λ o1 o2, match o1, o2 with | Some x, Some y => x ⊆ y | None, _ => True | Some _, _ => False end.
- Global Instance opt_le_PreOrder `{S : SubsetEq T} `{PreOrder _ S} : PreOrder (opt_le_SubsetEq).
- Proof.
- split.
- - move => [x|]; cbn; reflexivity.
- - move => [x|] [y|] [z|]; cbn; first (by transitivity y); tauto.
- Qed.
- Global Instance opt_le_AntiSymm `{S : SubsetEq T} `{AntiSymm T (=) S} : AntiSymm (=) opt_le_SubsetEq.
- Proof.
- move => [?|] [?|] //= S1 S2. f_equal. by apply H3.
- Qed.
-
- Lemma option_subseteq_is_Some `{SubsetEq T} (o1 o2 : option T) : o1 ⊆ o2 -> is_Some o1 -> is_Some o2.
- Proof.
- unfold subseteq, opt_le_SubsetEq. (repeat case_match).
- - by eauto.
- - by eauto.
- - by move => _ [] //.
- Qed.
-
- Global Instance opt_le_JoinSemiLattice `{JoinSemiLattice T} : JoinSemiLattice (option T).
- Proof.
- split.
- - exact: opt_le_PreOrder.
- - move => [x|] [y|]; cbn; first (apply: union_subseteq_l); by auto.
- - move => [x|] [y|]; cbn; first (apply: union_subseteq_r); by auto.
- - move => [x|] [y|] [z|]; cbn; first (apply: union_least); by auto.
- Qed.
-
-
Definition message_tuple : Type := Loc * (Val * (Time * View)).
Definition msg_to_tuple (m : message) : message_tuple := (m.(loc), (m.(val), (m.(time), m.(view)))).
Definition tuple_to_msg (m : message_tuple) : message :=
@@ -102,26 +46,6 @@ Section RAMachine.
| (l, (v, (t, R))) => mkMessage l v t R
end.
- Global Instance View_countable : Countable View :=
- injective_countable (map_to_list : View -> list (Loc * Time))
- ((λ l : list (Loc * Time), Some (map_of_list l)) : list _ -> option View) _.
- Proof.
- intros. f_equal. exact: map_of_to_list.
- Qed.
-
- Global Instance View_SubsetEq : SubsetEq View := λ X Y, ∀ x, @subseteq _ opt_le_SubsetEq (X !! x) (Y !! x).
- Global Instance View_PreOrder : PreOrder View_SubsetEq.
- Proof.
- split.
- - move => X x. reflexivity.
- - move => X Y Z HXY HYZ x. by transitivity (Y !! x).
- Qed.
- Global Instance View_SubsetEq_AntiSym `{AntiSymm (option Time) (=) (subseteq)} : AntiSymm (=) View_SubsetEq.
- Proof.
- move => ? ? S1 S2. apply: map_eq => x.
- by apply: anti_symm.
- Qed.
-
Definition val_to_sum : Val -> _ := λ v, match v with | A => inl () | D => inr (inl ()) | VInj v => inr (inr v) end.
Definition sum_to_val : _ -> Val := λ s, match s with | inl () => A | inr (inl ()) => D | inr (inr v) => VInj v end.
Global Instance Val_dec_eq : ∀ v1 v2 : Val, Decision (v1 = v2) :=
@@ -143,33 +67,6 @@ Section RAMachine.
Global Instance message_dec_eq : ∀ (m1 m2 : message), Decision (m1 = m2) := _.
Global Instance message_countable : Countable message := _.
-
- Global Instance View_Union : Union View := union_with (λ t1 t2, Some (t1 ∪ t2)).
-
- Global Instance View_JoinSemiLattice : JoinSemiLattice View | 0.
- Proof.
- split.
- - by auto with typeclass_instances.
- - move => X Y x.
- rewrite lookup_union_with.
- case : (X !! x) => [tX|]; case : (Y !! x) => [tY|]; cbn.
- + apply union_subseteq_l.
- + reflexivity.
- + reflexivity.
- + tauto.
- - move => X Y x.
- rewrite lookup_union_with.
- case : (X !! x) => [tX|]; case : (Y !! x) => [tY|]; cbn.
- + apply union_subseteq_r.
- + reflexivity.
- + reflexivity.
- + tauto.
- - move => X Y Z HXY HYZ x. move: (HXY x) (HYZ x).
- rewrite lookup_union_with.
- case : (X !! x) => [tX|]; case : (Y !! x) => [tY|]; case : (Z !! x) => [tZ|]; cbn; try tauto.
- apply union_least.
- Qed.
-
End Definitions.
@@ -222,22 +119,11 @@ Section RAMachine.
x at level 21, v at level 21, t at level 21, R at level 21).
Section Machine.
-
-
Definition msg_disj m m' := m.(loc) ≠m'.(loc) ∨ m.(time) ≠m.(time).
Lemma msg_disj_symm m1 m2 : msg_disj m1 m2 -> msg_disj m2 m1.
Proof. now firstorder. Qed.
- Existing Instance message_dec_eq.
- Existing Instance message_countable.
Notation MessageSet := (gset message).
- Existing Instance mapset_elem_of.
- Existing Instance mapset_empty.
- Existing Instance mapset_union.
- Existing Instance mapset_intersection.
- Existing Instance mapset_singleton.
-
- Global Instance MessageSet_JoinSemiLattice : JoinSemiLattice MessageSet := _.
Definition MS_disj (M M' : MessageSet) := ∀ m m', m ∈ M -> m' ∈ M' -> msg_disj m m'.
@@ -246,25 +132,88 @@ Section RAMachine.
Definition pairwise_disj (M : MessageSet) := ∀ m m', m ∈ M -> m' ∈ M -> m = m' ∨ msg_disj m m'.
Definition view_ok (M : MessageSet) V :=
- ∀ x t, V !! x = Some t → ∃ m, m ∈ M ∧ m.(loc) = x ∧ m.(time) = t ∧ m.(view) ⊆ V.
+ ∀ x t, V !! x = Some t → ∃ m, m ∈ M ∧ m.(loc) = x ∧ m.(time) = t ∧ m.(view) ⊑ V.
Definition timemap_ok (M : MessageSet) (T : timemap) :=
∀ x t, T !! x = Some t → ∃ m, m ∈ M ∧ m.(loc) = x ∧ m.(time) = t.
Definition timemap_complete (M : MessageSet) (T : timemap) :=
∀ m, m ∈ M → is_Some (T !! m.(loc)).
- Inductive MaxTime (M : MessageSet) (x : Loc) : option Time -> Prop :=
+ Inductive MaxTime (M : MessageSet) (x : Loc) : option Time -> Type :=
| MT_None (NoEl : ∀ m, m ∈ M -> m.(loc) = x -> False) : MaxTime M x None
| MT_Some t v R (El : <x → v@t, R> ∈ M)
(Le : ∀ m, m ∈ M -> m.(loc) = x -> m.(time) ≤ t) :
MaxTime M x (Some t)
.
+ Definition MT_nomsg `(Max : MaxTime M x None) : ∀ m, m ∈ M -> m.(loc) = x -> False :=
+ match Max with
+ | MT_None NoEl => NoEl
+ end.
+
+ Definition MT_msg `(Max : MaxTime M x (Some t)) : message :=
+ <x →
+ match Max with MT_Some _ v _ _ _ => v end
+ @ t, match Max with MT_Some t v R _ _ => R end >.
+
+ Definition MT_msg_loc `(Max : MaxTime M x (Some t)) : loc (MT_msg Max) = x := eq_refl.
+
+ Definition MT_msg_time `(Max : MaxTime M x (Some t)) : time (MT_msg Max) = t := eq_refl.
+
+ Definition MT_msg_In `(Max : MaxTime M x (Some t)) : MT_msg Max ∈ M :=
+ match Max as Max' in MaxTime _ _ ot return
+ match ot as ot' return MaxTime _ _ ot' -> Prop with
+ | None => λ _, True
+ | Some t => λ MT, MT_msg MT ∈ M
+ end Max'
+ with
+ | MT_None _ => I
+ | MT_Some t v R EL _ => EL
+ end.
+
+ Hint Extern 0 (loc (MT_msg _)) => apply MT_msg_loc.
+ Hint Extern 0 (time (MT_msg _)) => apply MT_msg_time.
+ Hint Extern 0 ((@MT_msg ?M _ _ _) ∈ ?M) => apply MT_msg_In.
+ Definition MT_msg_In_unf `(Max : MaxTime M x (Some t)) :
+ <loc (MT_msg Max) → val (MT_msg Max) @ time (MT_msg Max) , view (MT_msg Max)> ∈ M :=
+ match Max as Max' in MaxTime _ _ ot return
+ match ot as ot' return MaxTime _ _ ot' -> Prop with
+ | None => λ _, True
+ | Some t => λ Max,
+ <loc (MT_msg Max) → val (MT_msg Max) @ time (MT_msg Max) , view (MT_msg Max)> ∈ M
+ end Max'
+ with
+ | MT_None _ => I
+ | MT_Some t v R EL _ => EL
+ end.
+
+ Definition MT_msg_max `(Max : MaxTime M x (Some t)) :
+ ∀ m, m ∈ M -> loc m = x -> time m ≤ time (MT_msg Max) :=
+ match Max as Max' in MaxTime _ _ ot return
+ match ot as ot' return MaxTime _ _ ot' -> Prop with
+ | None => λ _, True
+ | Some t => λ MT,
+ ∀ m, m ∈ M -> loc m = x -> time m ≤ time (MT_msg MT)
+ end Max'
+ with
+ | MT_None _ => I
+ | MT_Some t v R _ LE => LE
+ end.
+
Lemma MaxTime_Some_Lt {M x t} :
MaxTime M x (Some t) ->
∀ m, m ∈ M -> m.(loc) = x -> m.(time) ≤ t.
Proof. by inversion 1. Qed.
+ Definition MT_fun `(Max1 : MaxTime M x ot1) `(Max2 : MaxTime M x ot2) : ot1 = ot2.
+ Proof.
+ destruct ot1 as [t1|], ot2 as [t2|] => //;
+ rewrite -?(MT_msg_time Max1) -?(MT_msg_time Max2).
+ - f_equal. apply: anti_symm; by apply: MT_msg_max.
+ - exfalso. by apply: (MT_nomsg Max2); first exact: MT_msg_In.
+ - exfalso. by apply: (MT_nomsg Max1); first exact: MT_msg_In.
+ Qed.
+
Instance MessageSet_Filter : Filter message MessageSet :=
λ P EqDec M, of_list (filter P (elements M)).
@@ -273,47 +222,47 @@ Section RAMachine.
by rewrite !elem_of_of_list !elem_of_list_filter elem_of_elements.
Qed.
- Lemma MS_filter_union {M1 M2 : MessageSet} `{DecP : ∀ m, Decision (P m)} :
- filter P (M1 ∪ M2) = filter P M1 ∪ filter P M2.
+ Lemma MS_filter_join {M1 M2 : MessageSet} `{DecP : ∀ m, Decision (P m)} :
+ filter P (M1 ⊔ M2) = filter P M1 ⊔ filter P M2.
Proof.
apply mapset_eq => m.
- rewrite elem_of_union !elem_of_MS_filter elem_of_union.
+ rewrite elem_of_join !elem_of_MS_filter elem_of_join.
tauto.
Qed.
- Lemma MaxTime_pred_mono `{∀ m, Decision (P1 m)} `{∀ m, Decision (P2 m)} {M x ot1 ot2} : MaxTime (filter P1 M) x ot1 -> MaxTime (filter P2 M) x ot2 -> (∀ m, P1 m -> P2 m) -> ot1 ⊆ ot2.
+ Lemma MaxTime_pred_mono `{∀ m, Decision (P1 m)} `{∀ m, Decision (P2 m)} {M x ot1 ot2} : MaxTime (filter P1 M) x ot1 -> MaxTime (filter P2 M) x ot2 -> (∀ m, P1 m -> P2 m) -> ot1 ⊑ ot2.
Proof.
- (* inversion 1; inversion 1 => HP; subst. *)
- (* - reflexivity. *)
- (* - reflexivity. *)
- (* - exfalso. *)
- (* apply: NoEl. first apply HP. first eassumption; first by []. exact: HP. *)
- (* - cbn. destruct El as (? & ? & In & ?). *)
- (* apply: (Le0 _ In eq_refl). exact: HP. *)
- (* Qed. *)
- Admitted.
+ case ot1, ot2 => MT1 MT2 HP //.
+ - rewrite -(MT_msg_time MT1) -(MT_msg_time MT2).
+ apply: MT_msg_max; last exact: MT_msg_loc.
+ apply/elem_of_MS_filter. move/elem_of_MS_filter : (MT_msg_In MT1) => []; split; by eauto.
+ - exfalso. apply: (MT_nomsg MT2); last exact: MT_msg_loc.
+ + apply/elem_of_MS_filter. case/elem_of_MS_filter : (MT_msg_In MT1). by auto.
+ Qed.
Lemma MaxTime_set_mono {M1 M2 x ot1 ot2} :
- MaxTime M1 x ot1 -> MaxTime M2 x ot2 -> MaxTime (M1 ∪ M2) x (ot1 ∪ ot2).
+ MaxTime M1 x ot1 -> MaxTime M2 x ot2 -> MaxTime (M1 ⊔ M2) x (ot1 ⊔ ot2).
Proof.
- inversion 1; inversion 1; subst.
- - constructor => m /elem_of_union []; by firstorder.
- - econstructor.
- + apply/elem_of_union; right; eassumption.
- + move => m /elem_of_union [/NoEl|/Le]; by intuition.
- - econstructor.
- + apply/elem_of_union; left; eassumption.
- + move => m /elem_of_union [/Le|/NoEl]; by intuition.
- - assert (Dec : {t ∪ t0 = t} + {t ∪ t0 = t0}).
- { exact: Pos.max_dec. }
- assert (LT' : ∀ m : message, m ∈ M1 ∪ M2 → loc m = x → time m ≤ t ∪ t0).
- { move => ? /elem_of_union [/Le|/Le0] EqLoc.
- - transitivity t; last exact: Pos.le_max_l; exact: EqLoc.
- - transitivity t0; last exact: Pos.le_max_r; exact: EqLoc.
+ move: ot1 ot2 => [t1|] [t2|] MT1 MT2; cbn.
+ rewrite -?(MT_msg_time MT1) -?(MT_msg_time MT2); cbn.
+ - assert (Dec : {join t1 t2 = t1} + {join t1 t2 = t2}) by exact: Pos.max_dec.
+ pose (m := if Dec then MT_msg MT1 else MT_msg MT2).
+ assert (if Dec then t2 ⊑ t1 else t1 ⊑ t2).
+ { destruct Dec as [Eq|Eq]; rewrite /= -Eq. by apply join_ext_r. by apply join_ext_l. }
+ assert (∀ m', m' ∈ M1 ⊔ M2 -> loc m' = x -> time m' ≤ time m).
+ { destruct Dec; simpl in *; unfold m;
+ (move => ? /elem_of_join [|] In EqLoc;
+ [move : (MT_msg_max MT1 _ In EqLoc)|move : (MT_msg_max MT2 _ In EqLoc)]);
+ by eauto using Pos.le_trans.
}
- + case: Dec => [Dec|Dec]; (econstructor => //; rewrite Dec; apply/elem_of_union).
- * left. eassumption.
- * right. eassumption.
+ destruct Dec as [Eq|Eq]; cbn in *; rewrite Eq;
+ econstructor => //;
+ apply/elem_of_join; [left|right]; exact: MT_msg_In.
+ - econstructor; first (apply/elem_of_join; left; exact: MT_msg_In).
+ move => ? /elem_of_join [|/(MT_nomsg MT2) //] ? ?. exact: MT_msg_max.
+ - econstructor; first (apply/elem_of_join; right; exact: MT_msg_In).
+ move => ? /elem_of_join [/(MT_nomsg MT1) //|] ? ?. exact: MT_msg_max.
+ - econstructor. move => ? /elem_of_join [|] /MT_nomsg; by eauto.
Qed.
Record memory :=
@@ -321,15 +270,15 @@ Section RAMachine.
msgs :> MessageSet;
_ : pairwise_disj msgs
}.
- Implicit Type (M : memory).
+
Definition memory_ok : ∀ M, pairwise_disj M.(msgs) := ltac:(by destruct 0).
Program Definition add_ins (M : memory) m : MS_msg_disj M m -> memory :=
- fun H => mkMemory (union (msgs M) (singleton m)) _.
+ fun H => mkMemory (join (msgs M) (singleton m)) _.
Next Obligation.
intros M m ? m1 m2.
- move => /elem_of_union [El1|/elem_of_singleton Eq1];
- move => /elem_of_union [El2|/elem_of_singleton Eq2].
+ move => /elem_of_join [El1|/elem_of_singleton Eq1];
+ move => /elem_of_join [El2|/elem_of_singleton Eq2].
- case: (memory_ok _ _ _ El1 El2); by [left | right].
- rewrite -> Eq2. right. apply: msg_disj_symm. exact: H3.
- rewrite -> Eq1. right; exact: H3.
@@ -337,12 +286,12 @@ Section RAMachine.
Qed.
Lemma MaxTime_add_ins_old (M M2 : MessageSet) x ot (NEq : ∀ m, m ∈ M2 → x ≠m.(loc)) :
- MaxTime M x ot -> MaxTime (M ∪ M2) x ot.
+ MaxTime M x ot -> MaxTime (M ⊔ M2) x ot.
Proof.
- inversion 1; econstructor.
- - move => ? /elem_of_union [/NoEl //|In ?]. exact: NEq.
- - apply/elem_of_union; left; eauto.
- - move => ? /elem_of_union [/Le //|In ?]. exfalso; exact: NEq.
+ case: ot => [t|] => MT1; econstructor.
+ - apply/elem_of_join. left; by apply: (MT_msg_In MT1).
+ - move => ? /elem_of_join [/(MT_msg_max MT1)|/NEq NEq' ?]; first auto. by destruct NEq'.
+ - move => ? /elem_of_join [/(MT_nomsg MT1)|/NEq NEq' ?]; first tauto. by destruct NEq'.
Qed.
(* Instance View_Singleton : Singleton (Loc * Time) View := λ xt, <[xt.1 := xt.2]> empty. *)
@@ -352,17 +301,17 @@ Section RAMachine.
| Th_Read m acc
(InM : m ∈ msgs M)
(Lt : ∀ t', V !! m.(loc) = Some t' -> (t' ≤ m.(time))) (* TODO: must not be None! *)
- : thread_red V M (ERead acc m.(loc) m.(val)) (V ∪ m.(view)) M
+ : thread_red V M (ERead acc m.(loc) m.(val)) (V ⊔ m.(view)) M
| Th_Write x v t V' m acc
(Lt : ∀ t', V !! x = Some t' -> (t' < t)) (* TODO: must not be None! *)
- (EV' : V' = V ∪ {[x := t]})
+ (EV' : V' = V ⊔ {[x := t]})
(Em : m = < x → v @ t, V' >)
(Disj : MS_msg_disj M m)
: thread_red V M (EWrite acc x v) V' (add_ins M m Disj)
| Th_Update x v_r t R V' m v_w
(InM : <x→v_r@t, R> ∈ msgs M)
(Lt : ∀ t', V !! x = Some t' -> (t' ≤ t)) (* TODO: must not be None! *)
- (EV' : V' = V ∪ {[x := t+1]} ∪ R)
+ (EV' : V' = V ⊔ {[x := t+1]} ⊔ R)
(Em : m = < x → v_w @ t + 1, V' >)
(Disj : MS_msg_disj M m)
: thread_red V M (EUpdate x v_r v_w) V' (add_ins M m Disj)
@@ -379,21 +328,21 @@ Section RAMachine.
Definition msgs_ok M := ∀ m, m ∈ msgs M → msg_ok m ∧ view_ok (msgs M) m.(view).
Definition threads_ok σ := ∀ π V, threads σ !! π = Some V → view_ok (mem σ) V.
- Definition view_mono V V' := ∀ x, V !! x ⊆ V' !! x.
+ Definition view_mono V V' := V ⊑ V'.
Definition thread_inv (V : View) (M : memory) := msgs_ok M ∧ view_ok M V.
- Definition msgs_mono M M' := msgs M ⊆ msgs M'.
+ Definition msgs_mono M M' := msgs M ⊑ msgs M'.
Section ThreadReduction.
- Lemma view_ok_mono : Proper ((⊆) ==> (=) ==> impl) view_ok.
+ Lemma view_ok_mono : Proper ((⊑) ==> (=) ==> impl) view_ok.
Proof.
- move => M1 M2 /elem_of_subseteq HM V1 V2 <- {V2} VOk x t HVt2.
+ move => M1 M2 /elem_of_extension HM V1 V2 <- {V2} VOk x t HVt2.
edestruct (VOk) as (m & A & B & C & D); first eassumption.
exists m; repeat split; by auto.
Qed.
- Lemma lookup_union (X Y : View) x ot : (X ∪ Y) !! x = ot → X !! x = ot ∨ Y !! x = ot.
+ Lemma lookup_join (X Y : View) x ot : (X ⊔ Y) !! x = ot → X !! x = ot ∨ Y !! x = ot.
Proof.
rewrite lookup_union_with.
case : (X !! x) => [tX|];
@@ -402,56 +351,55 @@ Section RAMachine.
- left. f_equal. by symmetry.
- right. f_equal. by symmetry.
Qed.
-
- Lemma lookup_union_max (X Y : View) x : (X ∪ Y) !! x = X !! x ∪ Y !! x.
+ Lemma lookup_join_max (X Y : View) x : (X ⊔ Y) !! x = X !! x ⊔ Y !! x.
Proof. rewrite lookup_union_with.
case : (X !! x) => [tX|];
case : (Y !! x) => [tY|]; cbn; by auto.
Qed.
- Lemma view_union_assoc V R S : V ∪ (R ∪ S) = (V ∪ R) ∪ S.
+ Lemma view_join_assoc V R S : V ⊔ (R ⊔ S) = (V ⊔ R) ⊔ S.
Proof.
apply: map_eq => x.
rewrite !lookup_union_with.
repeat case : (_ !! x) => [?|]; cbn; try auto.
- unfold union, Time_Union. by rewrite Pos.max_assoc.
+ f_equal. exact: Pos.max_assoc.
Qed.
Lemma msg_ok_write V (x : Loc) v t
(Lt : ∀ t' : Time, V !! x = Some t' → t' < t)
- : msg_ok (<x→v@t,(V ∪ {[x := t]})>).
+ : msg_ok (<x→v@t,(V ⊔ {[x := t]})>).
Proof.
- cbv [msg_ok] => /=. rewrite lookup_union_max lookup_singleton.
+ cbv [msg_ok] => /=. rewrite lookup_join_max lookup_singleton.
case HVx : (V !! _) => [?|] //=.
move/Lt : HVx => HVx; cbn. f_equal.
- apply: (anti_symm (⊆)).
- - apply union_least; last reflexivity.
+ apply: (anti_symm).
+ - apply join_least; last reflexivity.
exact: Pos.lt_le_incl.
- - by apply union_subseteq_r.
+ - by apply join_ext_r.
Qed.
- Lemma view_ok_write M V x v t
+ Lemma view_ok_write (M : memory) V x v t
(VOk : view_ok M V)
- (Disj : MS_msg_disj M (<x→v@t,(V ∪ {[x := t]})>)) :
- view_ok (add_ins M (<x→v@t,(V ∪ {[x := t]})>) Disj)
- (view (<x→v@t,(V ∪ {[x := t]})>)).
+ (Disj : MS_msg_disj M (<x→v@t,(V ⊔ {[x := t]})>)) :
+ view_ok (add_ins M (<x→v@t,(V ⊔ {[x := t]})>) Disj)
+ (view (<x→v@t,(V ⊔ {[x := t]})>)).
Proof.
- move => z tz /lookup_union [/VOk|/lookup_singleton_Some [<- <-]].
+ move => z tz /lookup_join [/VOk|/lookup_singleton_Some [<- <-]].
- move => [[y vy ty Ry] /= [Hm1 [Hm2 [Hm3 Hm4]]]]; subst.
exists (<z → vy @ tz, Ry>) => /=. repeat (split; first try (reflexivity || eassumption)).
- + apply elem_of_union; by left.
- + transitivity V; first assumption. by apply union_subseteq_l.
+ + apply elem_of_join; by left.
+ + transitivity V; first assumption. by apply join_ext_l.
- eexists; repeat split;
- first (apply/elem_of_union; right; by apply elem_of_singleton); by auto.
+ first (apply/elem_of_join; right; by apply elem_of_singleton); by auto.
Qed.
Lemma msg_ok_update M V R x v_r v_w t
(MOk : msg_ok (<x→v_r@t,R>))
(InM : <x→v_r@t,R> ∈ msgs M)
(Lt : ∀ t' : Time, V !! x = Some t' → t' ≤ t)
- : msg_ok (<x→v_w@(t + 1),(V ∪ {[x := t + 1]} ∪ R)>).
+ : msg_ok (<x→v_w@(t + 1),(V ⊔ {[x := t + 1]} ⊔ R)>).
Proof with eauto using Pos.lt_add_diag_r, Pos.lt_le_incl.
- cbv [msg_ok] => /=. rewrite !lookup_union_max lookup_singleton MOk.
+ cbv [msg_ok] => /=. rewrite !lookup_join_max lookup_singleton MOk.
case HVx : (V !! _) => [?|] //=.
- move/Lt : HVx => HVx; cbn. f_equal.
apply: Pos.le_antisym.
@@ -459,7 +407,7 @@ Section RAMachine.
* transitivity t...
* reflexivity.
* trivial ...
- + rewrite (_ : _ ∪ (t + 1) = t + 1); first rewrite (_ : t + 1 ∪ t = t + 1).
+ + rewrite (_ : _ ⊔ (t + 1) = t + 1); first rewrite (_ : t + 1 ⊔ t = t + 1).
* reflexivity.
* apply/Pos.max_l_iff...
* apply/Pos.max_r_iff. transitivity t...
@@ -470,32 +418,32 @@ Section RAMachine.
(InM : <x→v_r@t,R> ∈ msgs M)
(VOk : view_ok M V)
(ROk : view_ok M R)
- (Disj : MS_msg_disj M (<x→v_w@(t + 1),(V ∪ {[x := t + 1]} ∪ R)>)) :
- view_ok (add_ins M (<x→v_w@(t + 1),(V ∪ {[x := t + 1]} ∪ R)>) Disj)
- (view (<x→v_w@(t + 1),(V ∪ {[x := t + 1]} ∪ R)>)).
+ (Disj : MS_msg_disj M (<x→v_w@(t + 1),(V ⊔ {[x := t + 1]} ⊔ R)>)) :
+ view_ok (add_ins M (<x→v_w@(t + 1),(V ⊔ {[x := t + 1]} ⊔ R)>) Disj)
+ (view (<x→v_w@(t + 1),(V ⊔ {[x := t + 1]} ⊔ R)>)).
Proof.
- move => z tz /lookup_union [/lookup_union [/VOk|/lookup_singleton_Some [<- <-]]|/ROk].
+ move => z tz /lookup_join [/lookup_join [/VOk|/lookup_singleton_Some [<- <-]]|/ROk].
- move => [[y vy ty Ry] /= [Hm1 [Hm2 [Hm3 Hm4]]]]; subst.
exists (<z → vy @ tz, Ry>) => /=. repeat (split; first try (reflexivity || eassumption)).
- + apply elem_of_union; by left.
- + transitivity V; first assumption. rewrite -assoc. by apply union_subseteq_l.
+ + apply elem_of_join; by left.
+ + transitivity V; first assumption. rewrite -assoc. by apply join_ext_l.
- eexists; repeat split;
- first (apply/elem_of_union; right; by apply elem_of_singleton); by auto.
+ first (apply/elem_of_join; right; by apply elem_of_singleton); by auto.
- move => [[y vy ty Ry] /= [Hm1 [Hm2 [Hm3 Hm4]]]]; subst.
exists (<z → vy @ tz, Ry>) => /=. repeat (split; first try (reflexivity || eassumption)).
- + apply elem_of_union; by left.
- + transitivity R; first assumption. by apply union_subseteq_r.
+ + apply elem_of_join; by left.
+ + transitivity R; first assumption. by apply join_ext_r.
Qed.
Lemma msgs_ok_add_ins x v t M V m' R
(MOk : msgs_ok M)
(VOk : view_ok M V)
- (Disj : MS_msg_disj M (<x→v@t,(V ∪ R)>)):
+ (Disj : MS_msg_disj M (<x→v@t,(V ⊔ R)>)):
m' ∈ msgs M → msg_ok m' ∧ view_ok (add_ins M _ Disj) (view m').
Proof.
move/MOk => []; split; first by auto.
apply: view_ok_mono; last by eassumption.
- { by eapply union_subseteq_l. }
+ { by eapply join_ext_l. }
{ reflexivity. }
Qed.
@@ -506,31 +454,31 @@ Section RAMachine.
induction 1; subst.
- split; first assumption.
move => y ty Hyty.
- case/lookup_union: Hyty.
+ case/lookup_join: Hyty.
+ move/VOk => [[? vy ? Ry] /= [Hm1 [Hm2 [Hm3 Hm4]]]]; subst.
exists (<y → vy @ ty, Ry>) => /=. repeat (split; first (reflexivity || eassumption)).
transitivity V; first assumption.
- now apply union_subseteq_l.
+ now apply join_ext_l.
+ move/MOk : InM => [_] ROk /ROk [[? vy ? Ry] /= [Hm1 [Hm2 [Hm3 Hm4]]]]; subst.
exists (<y → vy @ ty, Ry>) => /=. repeat (split; first (reflexivity || eassumption)).
transitivity (view m); first assumption.
- now apply union_subseteq_r.
+ now apply join_ext_r.
- split.
- + move => m' /elem_of_union [|/elem_of_singleton ->].
+ + move => m' /elem_of_join [|/elem_of_singleton ->].
* exact: msgs_ok_add_ins.
* split; [exact: msg_ok_write|exact: view_ok_write].
+ exact: view_ok_write.
- case: (MOk _ InM) => [? ?].
split.
- + move => m' /elem_of_union [|/elem_of_singleton ->].
- * rewrite -view_union_assoc. exact: msgs_ok_add_ins.
+ + move => m' /elem_of_join [|/elem_of_singleton ->].
+ * rewrite -view_join_assoc. exact: msgs_ok_add_ins.
* split; [exact: msg_ok_update|exact: view_ok_update].
+ exact: view_ok_update.
Qed.
- Lemma add_ins_mono M m Disj : msgs M ⊆ msgs (add_ins M m Disj).
+ Lemma add_ins_mono M m Disj : msgs M ⊑ msgs (add_ins M m Disj).
Proof.
- move => ? ?. apply/elem_of_union. by left.
+ move => ? ?. apply/elem_of_join. by left.
Qed.
Lemma thread_red_msgs_mono V M evt V' M' : thread_red V M evt V' M' -> msgs_mono M M'.
@@ -543,39 +491,19 @@ Section RAMachine.
Lemma thread_red_view_mono V M evt V' M' : thread_inv V M -> thread_red V M evt V' M' -> view_mono V V'.
Proof.
- move => ThrdInv. inversion 1; subst.
- - unfold view_mono.
- move => y.
- rewrite lookup_union_with.
- case: (V !! y) => [t1|] //.
- case: (view m !! y) => [t2|] //.
- cbn. by apply union_subseteq_l.
- - move => y.
- rewrite lookup_union_with.
- case: (V !! y) => [t1|] //.
- case: (decide (x = y)) => [<-|?].
- + rewrite lookup_singleton.
- cbn. by apply union_subseteq_l.
- + by rewrite lookup_singleton_ne.
- - move => y.
- rewrite !lookup_union_with.
- case: (V !! y) => [t1|] //.
- case: (R !! y) => [t2|];
- (case: (decide (x = y)) => [<-|?];
- first (rewrite lookup_singleton); last rewrite lookup_singleton_ne //).
- * cbn. rewrite -assoc. by apply union_subseteq_l.
- * cbn. by apply union_subseteq_l.
- * cbn. by apply union_subseteq_l.
+ move => ThrdInv. inversion 1; subst; try by apply join_ext_l.
+ - red. rewrite -assoc.
+ by apply join_ext_l.
Qed.
End ThreadReduction.
- Instance Lookup_opt_gmap `{Countable K} : Lookup K M (option (gmap K M)).
- Proof.
- move => M k [f|].
- - exact: (f !! k).
- - exact: None.
- Defined.
+ (* Instance Lookup_opt_gmap `{Countable K} : Lookup K M (option (gmap K M)). *)
+ (* Proof. *)
+ (* move => M k [f|]. *)
+ (* - exact: (f !! k). *)
+ (* - exact: None. *)
+ (* Defined. *)
Section DataRaces.
Inductive drf_red (σ σ' : state) (V : View) (x: Loc) : access -> Prop :=
@@ -583,7 +511,7 @@ Section RAMachine.
(LV : V !! x = Some tl)
(LNA : (nats σ) !! x = otna)
(Hσ' : nats σ' = nats σ)
- (GE : otna ⊆ Some tl)
+ (GE : otna ⊑ Some tl)
:
drf_red σ σ' V x at_hack
| drf_na tl t'
@@ -599,25 +527,25 @@ Section RAMachine.
Definition nats_ok (M : MessageSet) nats := timemap_ok (M) (nats).
Definition nats_complete (M : MessageSet) nats := timemap_complete M nats.
- Lemma nats_ok_mono : Proper ((⊆) ==> (=) ==> impl) nats_ok.
+ Lemma nats_ok_mono : Proper ((⊑) ==> (=) ==> impl) nats_ok.
Proof.
move => M1 M2 /elem_of_subseteq HM V1 V2 <- {V2} NOk x t HVt2.
edestruct NOk as (m & ? & ? & ?); first eassumption.
exists m; repeat split; by auto.
Qed.
- Lemma nats_complete_mono : Proper ((=) ==> (⊆) ==> impl) nats_complete.
+ Lemma nats_complete_mono : Proper ((=) ==> (⊑) ==> impl) nats_complete.
Proof.
move => M1 M2 <- V1 V2 Subs NCom m /NCom [] t Hmt.
- eapply option_subseteq_is_Some; by eauto.
+ eapply option_ext_is_Some; by eauto.
Qed.
- Lemma nats_complete_add_ins M m (D : MS_msg_disj M m) T :
+ Lemma nats_complete_add_ins (M : memory) m (D : MS_msg_disj M m) T :
(∃ m', m' ∈ msgs M ∧ m'.(loc) = m.(loc)) ->
nats_complete M T -> nats_complete (add_ins M _ D) T.
Proof.
move => [m' [In EqLoc]] NCom m'' /=.
- move/elem_of_union => [/NCom //|/elem_of_singleton ->].
+ move/elem_of_join => [/NCom //|/elem_of_singleton ->].
rewrite -EqLoc.
exact: NCom.
Qed.
@@ -626,7 +554,7 @@ Section RAMachine.
Lemma drf_red_safe σ σ' π x acc : msgs_mono (mem σ) (mem σ') -> drf_red σ σ' π x acc -> nats_ok (mem σ) (nats σ) -> nats_ok (mem σ') (nats σ').
Proof.
move => Mono. inversion 1; subst; move => Inv y t.
- - rewrite Hσ' => /Inv [? [? [? ?]]].
+ - rewrite Hσ' => /Inv [? [? [? ?]]];
eexists; repeat split; first exact: Mono; by assumption.
- rewrite Hσ'.
rewrite lookup_insert_Some. move => [[Eq Eq']|[_ /Inv]].
@@ -641,23 +569,23 @@ Section RAMachine.
Inductive allocated (M : MessageSet) x t : Prop :=
| is_allocated t_d t_a
(TD : MaxTime (filter (λ m, (m.(val) = D)) M) x t_d)
- (TA : MaxTime (filter (λ m, (m.(val) = D)) M) x (Some t_a))
- (Alloc : t_d ⊆ Some t_a)
- (Local: t_a ≤ t).
+ (TA : MaxTime (filter (λ m, (m.(val) = A)) M) x (Some t_a))
+ (Alloc : t_d ⊠Some t_a)
+ (Local: t_a ⊑ t).
Inductive deallocated (M : MessageSet) x ot : Prop :=
| is_deallocated t_d t_a
(TD : MaxTime (filter (λ m, (m.(val) = D)) M) x t_d)
- (TA : MaxTime (filter (λ m, (m.(val) = D)) M) x t_a)
- (DeAlloc : t_a ⊆ t_d)
- (Local: t_d ⊆ ot).
+ (TA : MaxTime (filter (λ m, (m.(val) = A)) M) x t_a)
+ (DeAlloc : t_a ⊠t_d)
+ (Local: t_d ⊑ ot).
Inductive initialized (M : MessageSet) x t : Prop :=
| is_initialized t_d t_a
(TD : MaxTime (filter (λ m, (m.(val) = D)) M) x t_d)
- (TA : MaxTime (filter (λ m, (m.(val) = D)) M) x (Some t_a))
- (Alloc : t_d ⊆ Some t_a)
- (Local: t_a < t).
+ (TA : MaxTime (filter (λ m, (m.(val) = A)) M) x (Some t_a))
+ (Alloc : t_d ⊠Some t_a)
+ (Local: t_a ⊠t).
Inductive alloc_red (M : MessageSet) (V : View) (x : Loc) : event -> Prop :=
@@ -690,30 +618,33 @@ Section RAMachine.
Lemma init_is_alloc M x t : initialized M x t -> allocated M x t.
Proof.
- inversion 1. econstructor; eauto. exact: Pos.lt_le_incl.
+ inversion 1. econstructor; [exact: TD|exact: TA| |] => //.
+ exact: Pos.lt_le_incl.
Qed.
- Lemma alloc_time_mono M m t : allocated M (m.(loc)) t -> t ≤ m.(time) -> allocated M (m.(loc)) (m.(time)).
+ Lemma alloc_time_mono M m t : allocated M (m.(loc)) t -> t ⊑ m.(time) -> allocated M (m.(loc)) (m.(time)).
Proof.
- inversion 1; intro; econstructor; eauto. etransitivity; eauto.
+ inversion 1. econstructor; [exact: TD|exact: TA| |] => //.
+ etransitivity; by eauto.
Qed.
Lemma alloc_add_ins_old (M : MessageSet) m x t (NEq : x ≠m.(loc)) :
allocated M x t ->
- allocated (M ∪ {[m]}) x t.
+ allocated (M ⊔ {[m]}) x t.
Proof.
inversion 1; econstructor; eauto.
- - rewrite MS_filter_union. apply: MaxTime_add_ins_old => //.
+ - rewrite MS_filter_join. apply: MaxTime_add_ins_old => //.
by move => ? /elem_of_MS_filter [? /elem_of_singleton ->].
- - rewrite MS_filter_union. apply: MaxTime_add_ins_old => //.
+ - rewrite MS_filter_join. apply: MaxTime_add_ins_old => //.
by move => ? /elem_of_MS_filter [? /elem_of_singleton ->].
Qed.
Lemma alloc_add_ins_new (M : MessageSet) m t (IsVal : m.(val) ≠D) (LE : t ≤ time m):
allocated M (m.(loc)) t ->
- allocated (M ∪ {[m]}) (m.(loc)) (m.(time)).
+ allocated (M ⊔ {[m]}) (m.(loc)) (m.(time)).
Proof.
- (* assert (HE : ∃ ot_a', ot_a' ⊆ Some (time m) ∧ MaxTime (λ m, val m = A) {[m]} (loc m) (ot_a')). *)
+ destruct m.
+ (* assert (HE : ∃ ot_a', ot_a' ⊑ Some (time m) ∧ MaxTime (λ m, val m = A) {[m]} (loc m) (ot_a')). *)
(* { case: (decide (val m = A)) => ?. *)
(* - exists (Some (time m)); split => //. *)
(* econstructor. destruct m. *)
@@ -734,16 +665,159 @@ Section RAMachine.
(* apply Pos.max_lub_iff; split; last eassumption. *)
(* by etransitivity; eauto. *)
(* Qed. *)
- Admitted.
+ Admitted.
+
+ Definition rel_of {T X : Type} (f : T -> X) (r : relation X) : relation T :=
+ λ (t1 t2 : T), r (f t1) (f t2).
+ Instance rel_of_Transitive : (@Transitive T r) → (@Transitive X (@rel_of X T f r)).
+ Proof.
+ repeat intro; unfold rel_of in *.
+ by eauto with typeclass_instances.
+ Qed.
+ Instance rel_of_Irreflexive : (@Irreflexive T r) → (@Irreflexive X (@rel_of X T f r)).
+ Proof.
+ repeat intro; unfold rel_of in *.
+ by eapply irreflexive_eq.
+ Qed.
+
+ Definition of_loc (M : MessageSet) (x : Loc) : list message :=
+ filter (λ m, loc m = x) (elements M).
+ Definition hist (M : MessageSet) (x : Loc) : list message :=
+ merge_sort (rel_of time (⊑)) (of_loc M x).
+
+ Definition hist_upto (M : MessageSet) (x : Loc) t : list message :=
+ (fix f l :=
+ match l with
+ | nil => nil
+ | m :: l => if decide(time m = t) then l else f l
+ end
+ ) (hist M x).
+
+ Lemma hist_upto_suffix M x t : suffix_of (hist_upto M x t) (hist M x).
+ Proof.
+ unfold hist_upto.
+ generalize (hist M x).
+ induction l => //.
+ case_match.
+ - by eexists (_::nil).
+ - etransitivity; first eassumption.
+ by eexists (_::nil).
+ Qed.
+
+ Lemma elem_of_contains (T : Type) (l1 l2 : list T) (t : T) : l2 `contains` l1 → t ∈ l2 → t ∈ l1.
+ Proof.
+ induction 1 => //.
+ - move/elem_of_cons => [->|?]; apply/elem_of_cons; tauto.
+ - move/elem_of_cons => [->|/elem_of_cons [->|?]]; apply/elem_of_cons.
+ + right; apply/elem_of_cons; tauto.
+ + by left.
+ + right; apply/elem_of_cons; tauto.
+ - move/IHcontains => ?. apply/elem_of_cons. tauto.
+ - by move/IHcontains1/IHcontains2.
+ Qed.
+
+ Lemma elem_of_merge_sort {T : Type} {r} `{∀ x y : T, Decision (r x y)} (t : T) (l : list T) : t ∈ merge_sort r l ↔ t ∈ l.
+ Proof.
+ split;
+ apply: elem_of_contains; apply Permutation_contains.
+ - exact: merge_sort_Permutation.
+ - symmetry. exact: merge_sort_Permutation.
+ Qed.
+
+ Lemma elem_of_hist (M : MessageSet) x m : m ∈ hist M x ↔ (loc m = x ∧ m ∈ M).
+ Proof.
+ rewrite elem_of_merge_sort /of_loc elem_of_list_filter.
+ intuition; by apply/elem_of_elements.
+ Qed.
+
+ Lemma hist_complete {M : MessageSet} {x} {m} (In : m ∈ M) (EqLoc : loc m = x) :
+ m ∈ hist M x.
+ Proof.
+ by apply/elem_of_hist.
+ Qed.
+
+ Lemma hist_exact (M : MessageSet) (disj : pairwise_disj M) x m (In : m ∈ M) (EqLoc : loc m = x) : suffix_of (m :: hist_upto M x (time m)) (hist M x).
+ Proof.
+ unfold hist_upto.
+ assert (NotNil : hist M x ≠nil).
+ { case HHist : (hist) => //.
+ exfalso. apply/elem_of_nil. rewrite -HHist. exact: hist_complete.
+ }
+ cut (StronglySorted (rel_of time (⊑)) (hist M x)); last first.
+ { apply StronglySorted_merge_sort.
+ cut (∀ m', m' ∈ M → loc m' = x → m' ∉ hist M x → time m < time m'); last first.
+ { by move => ? In' EqLoc' /(_ (hist_complete In' EqLoc')). }
+ cut (∀ m, m ∈ hist M x → loc m = x ∧ m ∈ M); last first.
+ { move => ? ?. exact/elem_of_hist. }
+ revert NotNil.
+ generalize (hist M x).
+ induction l => // NotNil Elem Prefix.
+ case: (decide _) => [?|?].
+ case_match; simplify_eq.
+ - rewrite (_ : m = a) //.
+ destruct (disj m a) as [Eq|Disj]; eauto.
+ + apply: proj2. apply/Elem. apply/elem_of_cons. tauto.
+ + destruct Disj as [NEqLoc|NEqTime]; exfalso.
+ * apply: NEqLoc. symmetry. apply: proj1. apply/Elem. apply/elem_of_cons. tauto.
+ * by eauto.
+ - cbn.
+ destruct l.
+ + rewrite (_ : m = a) //.
+ case: (decide (m = a)) => // ?.
+ exfalso. apply: Pos.lt_irrefl. apply: Prefix => //.
+ apply/not_elem_of_cons; by eauto using not_elem_of_nil.
+ + etransitivity. apply: IHl => //.
+ * move => ? ?. apply/Elem. apply/elem_of_cons. tauto.
+ * move => m' ? ? ?.
+ case: (decide (m' = a)) => [?|?]; first subst.
+ apply: Prefix => //. apply/not_elem_of_cons; split => //.
+ *
+
+
+
+ Definition AllocCond (hist : list message) (m : message) :=
+ match val m with
+ | VInj v => ∃ m' hist', hist = m' :: hist' ∧ val m' ≠D
+ | A => ∀ m_d hist', hist = m_d :: hist' → val m_d = D
+ | D => ∀ m' hist', hist = m' :: hist' → val m' ≠D
+ end.
+
+ Definition alloc_inv (M : MessageSet) :=
+ ∀ m (In : m ∈ M), AllocCond (hist_upto M (loc m) (time m)) m.
+
+ Lemma alloc_inv_val (M : MessageSet) m (In : m ∈ M) :
+ alloc_inv M →
+ match val m with
+ | VInj _ => allocated M (loc m) (time m)
+ | A => deallocated M (loc m) (Some (time m))
+ | D => allocated M (loc m) (time m)
+ end.
+ Proof.
+ move/(_ _ In). rewrite /AllocCond.
+ case_match.
+ - case HHist : hist_upto => //.
+
+
Inductive adjacent m1 m2 :=
adj (EqLoc : m2.(loc) = m1.(loc)) (GtTime : m2.(time) = m1.(time)+1).
Definition dealloc_inv (M : MessageSet) :=
- ∀ m (In : m ∈ M) (IsD : m.(val) = D), MaxTime M m.(loc) (Some m.(time)) ∨ ∃ m', m ∈ M ∧ adjacent m m' ∧ m'.(val) = A.
+ ∀ m (In : m ∈ M) (IsD : m.(val) = D), inhabited (MaxTime M m.(loc) (Some m.(time))) ∨ ∃ m', m ∈ M ∧ adjacent m m' ∧ m'.(val) = A.
Definition alloc_inv (M : MessageSet) :=
∀ m (In : m ∈ M), allocated M (m.(loc)) (m.(time)).
+
+ Lemma MT_singl_None `{Dec : ∀ m : message, Decision (P m)} {x v t V l} : (P (<x→v@t,V>) → False) → `(MaxTime (filter P {[<x→v@t,V>]}) l None).
+ Proof.
+ move => F; constructor => ? /elem_of_MS_filter [? /elem_of_singleton ?]; by subst.
+ Qed.
+ Lemma MT_singl_Some `{Dec : ∀ m : message, Decision (P m)} {x v t V} : (P (<x→v@t,V>)) → `(MaxTime (filter P {[<x→v@t,V>]}) x (Some t)).
+ Proof.
+ move => T; econstructor.
+ - apply/elem_of_MS_filter; split; first eassumption. exact/elem_of_singleton.
+ - move => ? /elem_of_MS_filter [? /elem_of_singleton ?]. by subst.
+ Qed.
Lemma alloc_thread_red_alloc σ π x evt V V' σ' acc
(HAcc : acc_of evt = Some acc)
@@ -756,30 +830,82 @@ Section RAMachine.
Proof.
inversion ThRed; clear ThRed;
inversion DRFRed; clear DRFRed;
- inversion AllocRed; clear AllocRed;
- subst;
+ inversion AllocRed; clear AllocRed;
+ simplify_eq;
simpl in HAcc; try by (simplify_option_eq; tauto);
try (rewrite LT in LV;
inversion LV;
subst t0;
clear LV);
(apply Lt in LT || apply Lt in LV); try by [].
- - move => m /elem_of_union [/AllocInv|/elem_of_singleton ->].
- case: (decide (loc m = x0)) => [EqLoc|].
-
- (* (move => m /elem_of_union [/AllocInv [? [In [? ?]]]|/elem_of_singleton ->] /= *)
- (* ; first (eexists; split; first (apply/elem_of_union; by left); by [])); *)
+ - move => m /elem_of_join [/AllocInv [t_d t_a TD TA ? ?]|/elem_of_singleton ->].
+ + econstructor; eauto; rewrite MS_filter_join;
+ [rewrite -(join_None t_d)| rewrite -(join_None (Some t_a))];
+ apply MaxTime_set_mono => //; exact: MT_singl_None.
+ + destruct Alloc. econstructor; eauto.
+ * rewrite MS_filter_join -(join_None t_d).
+ apply MaxTime_set_mono => //; exact: MT_singl_None.
+ * rewrite MS_filter_join -(join_None (Some t_a)).
+ apply MaxTime_set_mono => //; exact: MT_singl_None.
+ * move/Lt : LV => ?. transitivity tl => //. exact: Pos.lt_le_incl.
+ - move => m /elem_of_join [/AllocInv [t_d t_a TD TA ? ?]|/elem_of_singleton ->].
+ + econstructor; eauto; rewrite MS_filter_join;
+ [rewrite -(join_None t_d)| rewrite -(join_None (Some t_a))];
+ apply MaxTime_set_mono => //; exact: MT_singl_None.
+ + destruct Alloc. econstructor; eauto.
+ * rewrite MS_filter_join -(join_None t_d).
+ apply MaxTime_set_mono => //; exact: MT_singl_None.
+ * rewrite MS_filter_join -(join_None (Some t_a)).
+ apply MaxTime_set_mono => //; exact: MT_singl_None.
+ * move/Lt : LV => ?. transitivity tl => //. exact: Pos.lt_le_incl.
+ - move => m /elem_of_join [/AllocInv [t_d t_a TD TA ? ?]|/elem_of_singleton ->].
+ + case: (decide (loc m = x0)) => [EqLoc|NEqLoc].
+ * econstructor; try rewrite MS_filter_join.
+ { apply: MaxTime_set_mono => //. rewrite EqLoc. exact: MT_singl_Some. }
+ { rewrite -(join_None (Some _)). apply: MaxTime_set_mono => //.
+ exact: MT_singl_None. }
+ {
+ destruct Alloc. exfalso. apply: Pos.lt_irrefl.
+ econstructor; eauto; rewrite MS_filter_join;
+ [rewrite -(join_None t_d)| rewrite -(join_None (Some t_a))];
+ apply MaxTime_set_mono => //; exact: alloc_aux1.
+ + destruct Alloc. econstructor; eauto.
+ * rewrite MS_filter_join -(join_None t_d).
+ apply MaxTime_set_mono => //; exact: alloc_aux1.
+ * rewrite MS_filter_join -(join_None (Some t_a)).
+ apply MaxTime_set_mono => //; exact: alloc_aux1.
+ * move/Lt : LV => ?. transitivity tl => //. exact: Pos.lt_le_incl.
+
+ (move => ? /elem_of_join [/AllocInv [? [In [? ?]]]|/elem_of_singleton ->] /=
+ ; first (eexists; split; first (apply/elem_of_join; by left); by [])).
(* try by (destruct Alloc; *)
(* inversion TA; *)
(* subst; *)
(* destruct El as (? & ? & In & ?); *)
- (* eexists; split; first (apply/elem_of_union; left; exact: In); intuition; *)
+ (* eexists; split; first (apply/elem_of_join; left; exact: In); intuition; *)
(* transitivity tl => //; exact: Pos.lt_le_incl). *)
(* Qed. *)
Admitted.
-
-
+
+ Lemma dealloc_inv_helper1 m (M1 M2 : MessageSet) :
+ (∃ (m' : message), m ∈ M1 ∧ adjacent m m' ∧ val m' = A) ->
+ ∃ m' : message, m ∈ M1 ⊔ M2 ∧ adjacent m m' ∧ val m' = A.
+ Proof.
+ destruct 1 as (? & In' & ?). eexists. split; last eassumption.
+ apply/elem_of_join; left; assumption.
+ Qed.
+
+ Lemma dealloc_inv_helper2 M1
+ `(HMax : MaxTime M1 (loc m) (Some (time m)))
+ `(NEqx : x ≠loc m) v t V :
+ inhabited (MaxTime (M1 ⊔ {[<x→v@t,(V ⊔ {[x := t]})>]}) (loc m) (Some (time m))).
+ Proof.
+ rewrite (_ : Some (time m) = Some (time m) ⊔ None) //.
+ constructor. apply: MaxTime_set_mono => //.
+ by constructor => ? /elem_of_singleton -> /NEqx //.
+ Qed.
+
Lemma alloc_thread_red_dealloc σ π x evt V V' σ' acc :
acc_of evt = Some acc ->
threads σ !! π = Some V -> thread_red V (mem σ) evt V' (mem σ') -> drf_red σ σ' V x acc -> alloc_red (mem σ) V x evt -> dealloc_inv (mem σ) -> dealloc_inv (mem σ').
@@ -792,71 +918,61 @@ Section RAMachine.
inversion LV;
subst t0;
clear LV);
- (apply Lt in LT || apply Lt in LV); try by [].
- - move => m /elem_of_union [|/elem_of_singleton ->] /=.
- + move => In Eq; move : (DeAllocInv _ In Eq) => [HMax|].
- * destruct Alloc. left.
- case: (decide (x0 = loc m)) => [Eqx0|NEqx0].
- (* { intros. rewrite <- Eqx0 in *. *)
- (* assert (EqTm : time m = t_d). *)
- (* { *)
- (* assert (Some t_d ⊆ Some (time m)) *)
- (* by (apply: MaxTime_pred_mono; [exact: TD|exact: HMax|by []]). *)
- (* assert (time m ≤ t_d). *)
- (* { inversion TD. exact: Le. } *)
- (* cbn in H4. *)
- (* exact: (anti_symm _ _ _ _ H4). *)
- (* } *)
- (* exfalso. *)
- (* rewrite -> EqTm in *. *)
- (* assert (t_a ≤ t_d). *)
- (* { exact: (MaxTime_pred_mono TA HMax). } *)
- (* exact: (proj1 (Pos.le_nlt _ _) _ Alloc). *)
- (* } *)
- admit.
- rewrite (_ : Some (time m) = Some (time m) ∪ None) //.
- apply: MaxTime_set_mono => //.
- constructor => ? /elem_of_singleton -> /NEqx0.
- tauto.
- * destruct 1 as (? & In' & ?). right. eexists; split; last eassumption.
- apply/elem_of_union; left; assumption.
- + by inversion 0.
- - move => m /elem_of_union [|/elem_of_singleton ->] /=.
- + move => In Eq; move : (DeAllocInv _ In Eq) => [HMax|].
- * destruct Alloc. left.
- case: (decide (x0 = loc m)) => [Eqx0|NEqx0].
- (* { intros. rewrite <- Eqx0 in *. *)
- (* assert (EqTm : time m = t_d). *)
- (* { *)
- (* assert (Some t_d ⊆ Some (time m)) *)
- (* by (apply: MaxTime_pred_mono; [exact: TD|exact: HMax|by []]). *)
- (* assert (time m ≤ t_d). *)
- (* { inversion TD. exact: Le. } *)
- (* cbn in H4. *)
- (* exact: (anti_symm _ _ _ _ H4). *)
- (* } *)
- (* exfalso. *)
- (* rewrite -> EqTm in *. *)
- (* assert (t_a ≤ t_d). *)
- (* { exact: (MaxTime_pred_mono TA HMax). } *)
- (* exact: (proj1 (Pos.le_nlt _ _) _ Alloc). *)
- (* } *)
- admit.
- rewrite (_ : Some (time m) = Some (time m) ∪ None) //.
- apply: MaxTime_set_mono => //.
- constructor => ? /elem_of_singleton -> /NEqx0.
- tauto.
- * destruct 1 as (? & In' & ?). right. eexists; split; last eassumption.
- apply/elem_of_union; left; assumption.
- + by inversion 0.
- - move => m /elem_of_union [|/elem_of_singleton ->] /=.
+ (apply Lt in LT || apply Lt in LV); try by [];
+ try destruct Alloc;
+ try destruct Init.
+ - move => m /elem_of_join [|/elem_of_singleton ->] /=; last (by inversion 0);
+ move => In Eq; move : (DeAllocInv _ In Eq); intros [[HMax]|];
+ [left|right; exact: dealloc_inv_helper1].
+ case: (decide (x0 = loc m)) => [Eqx0|NEqx0]; last exact: dealloc_inv_helper2.
+ exfalso.
+ move: (MT_fun TD TA) => [] ?; subst.
+ by apply: StrictOrder_Irreflexive Alloc.
+ - move => m /elem_of_join [|/elem_of_singleton ->] /=; last (by inversion 0);
+ move => In Eq; move : (DeAllocInv _ In Eq); intros [[HMax]|];
+ [left|right; exact: dealloc_inv_helper1].
+ case: (decide (x0 = loc m)) => [Eqx0|NEqx0]; last exact: dealloc_inv_helper2.
+ exfalso.
+ move: (MT_fun TD TA) => [] ?; subst.
+ by apply: StrictOrder_Irreflexive Alloc.
+ - move => m /elem_of_join [|/elem_of_singleton ->] /=.
+ + move => In Eq; move : (DeAllocInv _ In Eq); intros [[HMax]|];
+ [left|right; exact: dealloc_inv_helper1].
+ case: (decide (x0 = loc m)) => [Eqx0|NEqx0]; last exact: dealloc_inv_helper2.
+ exfalso.
+ move: (MT_fun TD TA) => [] ?; subst.
+ by apply: StrictOrder_Irreflexive Alloc.
+ + move => ?. left. constructor. econstructor.
+ * apply/elem_of_join. right. apply/elem_of_singleton.
+ reflexivity.
+ * move => ? /elem_of_join [In|/elem_of_singleton ->] Eqx0; last reflexivity.
+ etransitivity.
+ exact:(MaxTime_Some_Lt Max).
+ exact: Pos.lt_le_incl.
+ - move => m /elem_of_join [|/elem_of_singleton ->] /=.
+ + move => In Eq; move : (DeAllocInv _ In Eq); intros [[HMax]|];
+ [left|right; exact: dealloc_inv_helper1].
+ case: (decide (x0 = loc m)) => [Eqx0|NEqx0].
+ * exfalso.
+ move: (MT_fun TD TA) => [] ?; subst.
+ by apply: StrictOrder_Irreflexive Alloc.
+ * rewrite [_ ⊔ R]comm.
+ + move => ?. left. constructor. econstructor.
+ * apply/elem_of_join. right. apply/elem_of_singleton.
+ reflexivity.
+ * move => ? /elem_of_join [In|/elem_of_singleton ->] Eqx0; last reflexivity.
+ etransitivity.
+ exact:(MaxTime_Some_Lt Max).
+ exact: Pos.lt_le_incl.
+ - move => m /elem_of_join [|/elem_of_singleton ->] /=.
+ - move => m /elem_of_join [|/elem_of_singleton ->] /=.
+ move => In Eq; move : (DeAllocInv _ In Eq) => [HMax|].
* destruct Alloc. left.
case: (decide (x0 = loc m)) => [Eqx0|NEqx0].
(* { intros. rewrite <- Eqx0 in *. *)
(* assert (EqTm : time m = t_d). *)
(* { *)
- (* assert (Some t_d ⊆ Some (time m)) *)
+ (* assert (Some t_d ⊑ Some (time m)) *)
(* by (apply: MaxTime_pred_mono; [exact: TD|exact: HMax|by []]). *)
(* assert (time m ≤ t_d). *)
(* { inversion TD. exact: Le. } *)
@@ -870,20 +986,12 @@ Section RAMachine.
(* exact: (proj1 (Pos.le_nlt _ _) _ Alloc). *)
(* } *)
admit.
- rewrite (_ : Some (time m) = Some (time m) ∪ None) //.
+ rewrite (_ : Some (time m) = Some (time m) ⊔ None) //.
apply: MaxTime_set_mono => //.
constructor => ? /elem_of_singleton -> /NEqx0.
tauto.
* destruct 1 as (? & In' & ?). right. eexists; split; last eassumption.
- apply/elem_of_union; left; assumption.
- + destruct Alloc.
- move => ?. left. econstructor.
- * apply/elem_of_union. right. apply/elem_of_singleton.
- reflexivity.
- * move => ? /elem_of_union [In|/elem_of_singleton ->] Eqx0; last reflexivity.
- etransitivity.
- exact:(MaxTime_Some_Lt Max).
- exact: Pos.lt_le_incl.
+ apply/elem_of_join; left; assumption.
Admitted.