more updates; added infrastructure file for typeclasses

coq/ra/_CoqProject

 -Q . ra
+infrastructure.v
 machine.v
 lang.v
 tactics.v

coq/ra/infrastructure.v

+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

coq/ra/machine.v

 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.