diff --git a/coq/ra/infrastructure.v b/coq/ra/infrastructure.v
index 9c55f8ce2c8836389feadefd318f54a3ecc5bd0b..80b137f3416ad1c4a6083018abf64e77e40c2f9a 100644
--- a/coq/ra/infrastructure.v
+++ b/coq/ra/infrastructure.v
@@ -1,14 +1,14 @@
From mathcomp Require Import ssreflect ssrbool seq.
-From iris.prelude Require Export strings list numbers.
+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.
Global Set Asymmetric Patterns.
Global Set Bullet Behavior "Strict Subproofs".
From Coq Require Export Utf8.
-Instance injective_dec_eq
+Definition 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.
+ f (g : A -> option B) (Inj : ∀ x, g (f x) = Some x) : ∀ x y : B, Decision (x = y).
Proof.
move => x y. case: (decide (f x = f y)).
- move/(f_equal g). rewrite !Inj => [[]]. by left.
@@ -357,4 +357,58 @@ Proof.
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
+Proof. tauto. Qed.
+
+
+
+
+(* Lifting relations via projections *)
+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_PreOrder : (@PreOrder T r) → (@PreOrder X (@rel_of X T f r)) | 10.
+Proof.
+ econstructor; repeat intro; unfold rel_of in *;
+ eauto using PreOrder_Reflexive, PreOrder_Transitive.
+Qed.
+Instance rel_of_Transitive : (@Transitive T r) → (@Transitive X (@rel_of X T f r)) | 10.
+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)) | 10.
+Proof.
+ repeat intro; unfold rel_of in *.
+ by eapply irreflexive_eq.
+Qed.
+Instance rel_of_Total : (@Total T r) → (@Total X (@rel_of X T f r)) | 10.
+Proof.
+ repeat intro; unfold rel_of in *.
+ eauto with typeclass_instances.
+Qed.
+Instance flip_Total : (@Total T r) → (@Total T (flip r)) | 10.
+Proof.
+ repeat intro; eauto with typeclass_instances.
+Qed.
+
+
+
+(* Miscellaneous *)
+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.
\ No newline at end of file
diff --git a/coq/ra/lang.v b/coq/ra/lang.v
index 527fccfd9762fefec2add0183bb04eca14628d48..b79d075465988469d3171cf36a7fef9660fc12c2 100644
--- a/coq/ra/lang.v
+++ b/coq/ra/lang.v
@@ -27,7 +27,11 @@ Definition cons_binder (mx : binder) (X : list string) : list string :=
Infix ":b:" := cons_binder (at level 60, right associativity).
Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
Proof.
- solve_decision. Defined.
+ (* infinite loop yeah yeah yeah *)
+ (* solve_decision. *)
+ destruct x1,x2; try (by left); try by right.
+ case: (decide (s = s0)) => [->|]; [by left|by right => [[]]].
+Defined.
Instance set_unfold_cons_binder x mx X P :
SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
diff --git a/coq/ra/lifting.v b/coq/ra/lifting.v
index 47cd47f853b3b1cd6837a4eac959bfed368373d9..54ffae9f6058129f6dfbdef0a45a0b26c0e30396 100644
--- a/coq/ra/lifting.v
+++ b/coq/ra/lifting.v
@@ -106,8 +106,10 @@ Qed.
(* rewrite later_sep -(wp_value_pvs _ _ (Lit _)) //. *)
(* Qed. *)
+Instance constant_dec {T : Prop} {X : Type} `{Decision T} : ∀ x, (Decision ((λ x : X, T) x)) := _.
+
Inductive drf_pre_na (σ : state) π l :=
-| _singleton_na (V : View) (tl : Time) (ViewOf : threads σ !! π = Some V) (Local : V !! l = Some tl) (Max : MaxTime (λ _, True) (mem σ) l (Some tl)).
+| _singleton_na (V : View) (tl : Time) (ViewOf : threads σ !! π = Some V) (Local : V !! l = Some tl) (Max : MaxTime (filter (λ m : message, True) (msgs $ mem σ)) l (Some tl)).
Inductive drf_pre_at (σ : state) π l :=
| _singleton_at (V : View) (tl tn : Time) (ViewOf : threads σ !! π = Some V) (Local : V !! l = Some tl) (NATS : nats σ !! l = Some tn) (LE : (tn ≤ tl)%positive).
@@ -127,13 +129,15 @@ Proof.
case H: (machine.val m).
- exfalso. apply/Pos.lt_nle : Local => F. apply: F.
rewrite -EqTime.
- by apply: MaxTime_Some_Lt => //.
+ apply: MaxTime_Some_Lt => //.
+ apply/elem_of_MS_filter; tauto.
- exfalso.
destruct (t_d).
- + apply/Pos.lt_nle : (Pos.le_lt_trans _ _ _ Alloc Local) => F. apply: F.
+ + apply/Pos.lt_nle : (Pos.lt_trans _ _ _ Alloc Local) => F. apply: F.
rewrite -EqTime.
apply: MaxTime_Some_Lt => //.
- + inversion TD. by eauto.
+ apply/elem_of_MS_filter; tauto.
+ + inversion TD. apply: NoEl; first apply/elem_of_MS_filter; by eauto.
- constructor.
Qed.
@@ -157,8 +161,8 @@ Inductive read_at_post (σ : state) (π : thread) x (v : Z) : Prop :=
(In : m ∈ msgs $ mem σ)
(ViewOf : (threads σ) !! π = Some V)
(Local : V !! x = Some t')
- (TimeLt : t' ≤ machine.time m)
- (VUpd : V' = V ∪ {[x:=machine.time m]} ∪ machine.view m)
+ (TimeLt : t' ⊑ machine.time m)
+ (VUpd : V' = V ⊔ {[x:=machine.time m]} ⊔ machine.view m)
.
Inductive read_na_post (σ : state) (π : thread) x (v : Z) : Prop :=
@@ -170,9 +174,9 @@ Inductive read_na_post (σ : state) (π : thread) x (v : Z) : Prop :=
(In : m ∈ msgs $ mem σ)
(ViewOf : (threads σ) !! π = Some V)
(Local : V !! x = Some t')
- (TimeLt : t' ≤ machine.time m)
- (VUpd : V' = V ∪ {[x:=machine.time m]} ∪ machine.view m)
- (Max : MaxTime (λ _, True) (mem σ) x (Some $ machine.time m))
+ (TimeLt : t' ⊑ machine.time m)
+ (VUpd : V' = V ⊔ {[x:=machine.time m]} ⊔ machine.view m)
+ (Max : MaxTime (filter (λ _, True) (msgs $ mem σ)) x (Some $ machine.time m))
.
Lemma wp_load_at_pst E π σ l Φ :
@@ -189,14 +193,14 @@ Proof.
subst.
move: (ITOk _ Inv _ _ ViewOf _ _ Local) => [m [In [EqLoc [EqTime SubView]]]].
assert (IsVal := initialized_reads_value _ _ _ Init m In EqLoc EqTime).
- case H: (machine.val m) => [| |v]; try (by rewrite H in IsVal; inversion IsVal).
+ case HVal: (machine.val m) => [| |v]; try (by rewrite HVal in IsVal; inversion IsVal).
eexists.
- exists (mkState (<[π:=V ∪ view m]> (threads σ)) (mem σ) (nats σ) : state).
+ exists (mkState (<[π:=V ⊔ view m]> (threads σ)) (mem σ) (nats σ) : state).
econstructor; first (eright; first by constructor).
econstructor; try eauto.
+ move => ? [<-]. by econstructor.
- + move => ? ? [<-] [<-]. by econstructor.
- + simpl. assert (proof := Th_Read V (mem σ) m). rewrite -> H, EqTime, EqLoc in proof.
+ + move => ? ? [<-] [<-]. econstructor => //. by rewrite NATS.
+ + simpl. assert (proof := Th_Read V (mem σ) m). rewrite -> HVal, EqTime, EqLoc in proof.
eapply proof => //.
intros. rewrite Local in H0. by move : H0 => [->].
- iSplitL "HP"; first by [].
@@ -211,7 +215,7 @@ Proof.
inversion H11. simplify_eq.
iApply "HΦ". iSplit; last by [].
destruct B. destruct Init. rewrite ViewOf0 in ViewOf. simplify_option_eq.
- iPureIntro. econstructor; subst; eauto.
+ iPureIntro. econstructor; subst; eauto. exact: Lt.
Qed.
Lemma wp_load_na_pst E π σ l Φ :
diff --git a/coq/ra/machine.v b/coq/ra/machine.v
index 641b2e65ff797b445e7466ba66f4e4a07e737d4e..96709299de9a2b9e46466a7914d5af0dd3561a73 100644
--- a/coq/ra/machine.v
+++ b/coq/ra/machine.v
@@ -214,7 +214,7 @@ Section RAMachine.
- exfalso. by apply: (MT_nomsg Max1); first exact: MT_msg_In.
Qed.
- Instance MessageSet_Filter : Filter message MessageSet :=
+ Global Instance MessageSet_Filter : Filter message MessageSet :=
λ P EqDec M, of_list (filter P (elements M)).
Lemma elem_of_MS_filter {M : MessageSet} `{DecP : ∀ m, Decision (P m)} {m} : m ∈ filter P M ↔ P m ∧ m ∈ M.
@@ -577,7 +577,7 @@ Section RAMachine.
| is_deallocated t_d t_a
(TD : MaxTime (filter (λ m, (m.(val) = D)) M) x t_d)
(TA : MaxTime (filter (λ m, (m.(val) = A)) M) x t_a)
- (DeAlloc : t_a ⊠t_d)
+ (DeAlloc : t_a ⊑ t_d)
(Local: t_d ⊑ ot).
Inductive initialized (M : MessageSet) x t : Prop :=
@@ -667,23 +667,10 @@ Section RAMachine.
(* Qed. *)
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).
+ merge_sort (flip $ rel_of time ((⊑)%positive)) (of_loc M x).
Definition hist_upto (M : MessageSet) (x : Loc) t : list message :=
(fix f l :=
@@ -704,25 +691,10 @@ Section RAMachine.
by eexists (_::nil).
Qed.
- Lemma elem_of_contains (T : Type) (l1 l2 : list T) (t : T) : l2 `contains` l1 → t ∈ l2 → t ∈ l1.
+ Lemma hist_upto_sorted M x t : StronglySorted (flip $ rel_of time (⊑)%positive) (hist_upto M x t).
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.
+ Admitted.
- 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.
@@ -743,22 +715,23 @@ Section RAMachine.
{ 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 (StronglySorted (flip $ rel_of time ((⊑))) (hist M x)); last first.
+ { apply StronglySorted_merge_sort; eauto using PreOrder_Transitive with typeclass_instances. }
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. }
+ cut (m ∈ hist M x); last by exact: hist_complete.
revert NotNil.
generalize (hist M x).
- induction l => // NotNil Elem Prefix.
- case: (decide _) => [?|?].
+ induction l => // NotNil Elem Correct Prefix Sorted.
+ case: (decide _) => [EqTime|NEQTime].
case_match; simplify_eq.
- rewrite (_ : m = a) //.
destruct (disj m a) as [Eq|Disj]; eauto.
- + apply: proj2. apply/Elem. apply/elem_of_cons. tauto.
+ + apply: proj2. apply/Correct. apply/elem_of_cons. tauto.
+ destruct Disj as [NEqLoc|NEqTime]; exfalso.
- * apply: NEqLoc. symmetry. apply: proj1. apply/Elem. apply/elem_of_cons. tauto.
+ * apply: NEqLoc. symmetry. apply: proj1. apply/Correct. apply/elem_of_cons. tauto.
* by eauto.
- cbn.
destruct l.
@@ -766,14 +739,19 @@ Section RAMachine.
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/elem_of_cons: Elem => [|].
+ { move => Eq. by rewrite Eq in NEQTime. }
+ inversion Sorted.
+ etransitivity. apply: IHl => //.
+ * move => ? ?. apply/Correct. apply/elem_of_cons. tauto.
* move => m' ? ? ?.
- case: (decide (m' = a)) => [?|?]; first subst.
- apply: Prefix => //. apply/not_elem_of_cons; split => //.
- *
-
-
+ case: (decide (m' = a)) => [?|?]; first subst; last first.
+ { apply: Prefix => //. apply/not_elem_of_cons; split => //. }
+ assert (LE : (flip $ rel_of time (⊑)) a m).
+ { inversion Sorted. eapply Forall_forall; by eauto. }
+ exact: Pos.Private_Tac.le_neq_lt.
+ * exact: suffix_of_cons_r.
+ Qed.
Definition AllocCond (hist : list message) (m : message) :=
match val m with
@@ -782,22 +760,23 @@ Section RAMachine.
| D => ∀ m' hist', hist = m' :: hist' → val m' ≠D
end.
- Definition alloc_inv (M : MessageSet) :=
+ 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 →
+ 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)
+ | VInj _ => allocated (filter (λ m', time m' ⊠time m) M) (loc m) (time m)
+ | A => deallocated (filter (λ m', time m' ⊠time m) M) (loc m) (Some (time m))
+ | D => allocated (filter (λ m', time m' ⊠time m) M) (loc m) (time m)
end.
Proof.
move/(_ _ In). rewrite /AllocCond.
case_match.
- - case HHist : hist_upto => //.
-
-
+ - case HHist: (hist_upto M (loc m) (time m)).
+ + econstructor; [eleft|eleft| |] => //.
+ *
+ Admitted.
Inductive adjacent m1 m2 :=
adj (EqLoc : m2.(loc) = m1.(loc)) (GtTime : m2.(time) = m1.(time)+1).
@@ -865,27 +844,14 @@ Section RAMachine.
{ 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_join; left; exact: In); intuition; *)
- (* transitivity tl => //; exact: Pos.lt_le_incl). *)
-
- (* Qed. *)
+ 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. *)
+ admit.
+ }
+ { admit. }
+ * admit.
Admitted.
Lemma dealloc_inv_helper1 m (M1 M2 : MessageSet) :
@@ -925,23 +891,17 @@ Section RAMachine.
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.
+ admit.
- 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.
+ admit.
- 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.
+ admit.
+ move => ?. left. constructor. econstructor.
* apply/elem_of_join. right. apply/elem_of_singleton.
reflexivity.
@@ -953,45 +913,19 @@ Section RAMachine.
+ 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.
+ * admit.
+ * rewrite [_ ⊔ R]comm. admit.
+ 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 ->] /=.
+ admit.
- 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)) *)
- (* 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_join; left; assumption.
+ admit.
+ + admit.
Admitted.