Commit b7609d6a authored by Ralf Jung's avatar Ralf Jung

make the library work without any axioms

parent cff4a032
Require Import Ssreflect.ssreflect Ssreflect.ssrfun Omega.
Require Import world_prop core_lang lang iris_core iris_plog.
Require Import ModuRes.RA ModuRes.SPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap ModuRes.Agreement ModuRes.DecEnsemble ModuRes.Axioms ModuRes.CMRA.
Require Import ModuRes.RA ModuRes.SPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap ModuRes.Agreement ModuRes.DecEnsemble ModuRes.CMRA.
Set Bullet Behavior "Strict Subproofs".
......
Require Import Ssreflect.ssreflect Ssreflect.ssrfun Omega.
Require Import SPred PreoMet RA CMRA Axioms.
Require Import SPred PreoMet RA CMRA.
Set Bullet Behavior "Strict Subproofs".
......@@ -13,70 +13,59 @@ Section Agreement.
Local Open Scope ra_scope.
Local Open Scope nat.
Implicit Types (v: SPred).
Implicit Type (v: SPred).
Definition cvChain v (ts: chain T): Prop :=
forall n i (HLe: n <= i) (pv: v i), ts i = n = ts n.
Definition vChain v: Type := forall n, v n -> T.
Program Definition cvChain {v} (ts: vChain v): Prop :=
forall n i (HLe: n <= i) (v: v i), ts i _ = n = ts n _.
Next Obligation.
eapply dpred; eassumption.
Qed.
CoInductive ra_agree : Type :=
ag_inj (v: SPred) (ts: vChain v) (tsx: cvChain ts).
ag_inj (v: SPred) (ts: chain T) (tsx: cvChain v ts).
Global Instance ra_agree_unit : RA_unit ra_agree := fun x => x.
Global Program Instance cmra_agree_valid : CMRA_valid _ :=
Global Instance cmra_agree_valid : CMRA_valid _ :=
fun x => match x with
| ag_inj v _ _ => v
end.
Global Instance ra_agree_valid : RA_valid _ := compose valid_sp cmra_agree_valid.
Local Ltac ra_ag_pi := match goal with
(* Local Ltac ra_ag_pi := match goal with
[H: dist ?n (?ts1 ?pv11) (?ts2 ?pv21) |- dist ?n (?ts1 ?pv12) (?ts2 ?pv22) ] =>
(* Also try with less rewrites, as some of the pvs apeparing in the goal may be existentials. *)
first [rewrite_pi pv12 pv11; rewrite_pi pv22 pv21; eexact H |
rewrite_pi pv22 pv21; eexact H | rewrite_pi pv12 pv11; eexact H]
end.
end. *)
Program Definition ra_ag_compinj_valid {v1 v2} (ts1: vChain v1) (ts2: vChain v2) (ts1x: cvChain ts1) (ts2x: cvChain ts2): SPred :=
mkSPred (fun n => exists (pv1: v1 n) (pv2: v2 n), ts1 _ pv1 = n = ts2 _ pv2) _ _.
Program Definition ra_ag_compinj_valid {v1 v2} (ts1 ts2: chain T) (ts1x: cvChain v1 ts1) (ts2x: cvChain v2 ts2): SPred :=
mkSPred (fun n => v1 n /\ v2 n /\ ts1 n = n = ts2 n) _ _.
(* This has to be n-bounded equality for the operation to be non-expansive: A full equality at all step-indices here would become a proof obligation that we have to show based on just n-equality of our arguments. *)
Next Obligation.
do 2 eexists. exact:dist_bound.
Grab Existential Variables.
{ exact: bpred. }
{ exact: bpred. }
split; last split; exact:dist_bound||exact:bpred.
Qed.
Next Obligation.
intros n m ? (pv1 & pv2 & EQ). do 2 eexists.
transitivity (ts2 n pv2); last by eapply ts2x.
transitivity (ts1 n pv1); first by (symmetry; eapply ts1x).
eapply mono_dist; eassumption.
intros n m ? (pv1 & pv2 & EQ). split; last split.
- eapply dpred, pv1. assumption.
- eapply dpred, pv2. assumption.
- transitivity (ts2 n); last by eapply ts2x.
transitivity (ts1 n); first by (symmetry; eapply ts1x).
eapply mono_dist; eassumption.
Qed.
Program Definition ra_ag_compinj_ts {v1 v2} (ts1: vChain v1) (ts2: vChain v2) (ts1x: cvChain ts1) (ts2x: cvChain ts2):
vChain (ra_ag_compinj_valid ts1 ts2 ts1x ts2x) :=
fun n pv => ts1 n _.
Lemma ra_ag_compinj_tsx {v1 v2} (ts1: vChain v1) (ts2: vChain v2) (ts1x: cvChain ts1) (ts2x: cvChain ts2):
cvChain (ra_ag_compinj_ts ts1 ts2 ts1x ts2x).
Lemma ra_ag_compinj_tsx {v1 v2} (ts1: chain T) (ts2: chain T) (ts1x: cvChain v1 ts1) (ts2x: cvChain v2 ts2):
cvChain (ra_ag_compinj_valid ts1 ts2 ts1x ts2x) ts1.
Proof.
move=> n i HLe [pv1 [pv2 EQ]]. unfold ra_ag_compinj_ts.
transitivity (ts1 i pv1); first by f_equiv. (* RJ: I have no idea why this works... *)
move/(_ _ _ HLe pv1):(ts1x)=>ts1x'. ra_ag_pi.
move=> n i HLe [pv1 [pv2 EQ]].
eapply ts1x; assumption.
Qed.
Global Instance ra_ag_op : RA_op _ :=
fun x y => match x, y with
| ag_inj v1 ts1 ts1x, ag_inj v2 ts2 ts2x =>
ag_inj (ra_ag_compinj_valid ts1 ts2 ts1x ts2x) (ra_ag_compinj_ts ts1 ts2 ts1x ts2x)
ag_inj (ra_ag_compinj_valid ts1 ts2 ts1x ts2x) ts1
(ra_ag_compinj_tsx ts1 ts2 ts1x ts2x)
end.
Program Definition ra_ag_inj (t: T): ra_agree :=
ag_inj top_sp (fun _ _ => t) (fun _ _ _ _ => _).
ag_inj top_sp (fun _ => t) (fun _ _ _ _ => _).
Next Obligation.
eapply dist_refl. reflexivity.
Qed.
......@@ -89,28 +78,24 @@ Section Agreement.
Definition ra_agree_eq (x y: ra_agree): Prop :=
match x, y with
| ag_inj v1 ts1 _, ag_inj v2 ts2 _ => v1 == v2 /\ (forall n pv1 pv2, ts1 n pv1 = n = ts2 n pv2)
(* The equality on the ts looks way too strong. However,
thanks to PI, this is actally the same as
"if both are valid, then pv1 and pv2 agree somewhere". *)
| ag_inj v1 ts1 _, ag_inj v2 ts2 _ => v1 == v2 /\ (forall n, v1 n -> ts1 n = n = ts2 n)
(* Also, only the n-valid elements have to be only n-equal. Otherwise,
commutativity breaks: n-valid here means that the arguments were
n-equal. *)
end.
Local Ltac ra_ag_destr := repeat (match goal with [ x : ra_agree |- _ ] => destruct x end).
(*Local Ltac ra_ag_auto := first [by firstorder | split; [by firstorder|intros n pv1 pv2; pi pv1 pv2; by firstorder ]].*)
Global Instance ra_agree_eq_equiv : Equivalence ra_agree_eq.
Proof.
split; repeat intro; ra_ag_destr; try (exact I || contradiction); [| |]. (* 3 goals left. *)
- split; first reflexivity. intros. rewrite_pi pv1 pv2. reflexivity.
- destruct H. split; intros; by symmetry.
- split; intros; reflexivity.
- destruct H. split; intros; first by symmetry.
symmetry. apply H0. rewrite H. assumption.
- destruct H, H0.
split; first (etransitivity; now eauto).
intro; etransitivity; [now eapply H1 | now eapply H2].
Grab Existential Variables.
{ rewrite -H. assumption. }
intro; etransitivity; [now eapply H1 | ].
eapply H2. rewrite -H. assumption.
Qed.
Global Instance ra_agree_type : Setoid ra_agree := mkType ra_agree_eq.
......@@ -118,9 +103,8 @@ Section Agreement.
x · x == x.
Proof.
ra_ag_destr. split.
- split; simpl; first by firstorder.
move=>pv. exists pv pv. now firstorder.
- move=>n ? ?. unfold ra_ag_compinj_ts. pi.
- split; simpl; first by firstorder. now firstorder.
- move=>n ?. reflexivity.
Qed.
Global Instance ra_agree_res : RA ra_agree.
......@@ -130,48 +114,44 @@ Section Agreement.
destruct H as (HeqV1 & HeqT1), H0 as (HeqV2 & HeqT2).
split.
+ split; intros (pv1 & pv2 & Heq).
* move:(pv1)(pv2)=>pv1' pv2'. rewrite ->HeqV1 in pv1'. rewrite ->HeqV2 in pv2'. exists pv1' pv2'.
rewrite <-HeqT1, <-HeqT2. eapply Heq; eassumption.
* move:(pv1)(pv2)=>pv1' pv2'. rewrite <-HeqV1 in pv1'. rewrite <-HeqV2 in pv2'. exists pv1' pv2'.
rewrite ->HeqT1, ->HeqT2. eapply Heq; eassumption.
+ intros n pv1 pv2. by apply: HeqT1.
- ra_ag_destr; []. simpl. unfold ra_ag_compinj_ts in *. split.
+ intros n. split.
* intros [pv1 [[pv2 [pv3 EQ']] EQ]]. hnf.
assert (pv4: (ra_ag_compinj_valid ts1 ts0 tsx1 tsx0) n).
{ hnf. exists pv1 pv2. ra_ag_pi. }
exists pv4 pv3. rewrite <-EQ'. ra_ag_pi.
* intros [[pv1 [pv2 EQ']] [pv3 EQ]]. hnf. unfold ra_ag_compinj_ts in *.
assert (pv4: (ra_ag_compinj_valid ts0 ts tsx0 tsx) n).
{ hnf. exists pv2 pv3. rewrite <-EQ'. ra_ag_pi. }
exists pv1 pv4. ra_ag_pi.
+ intros n pv1 pv2. f_equiv. by eapply ProofIrrelevance.
- ra_ag_destr. unfold ra_op, ra_ag_op. unfold ra_ag_compinj_ts in *. split.
+ split; intros (pv1 & pv2 & Heq); do 2 eexists; symmetry; eassumption.
+ intros n [pv1 [pv2 EQ]] [pv3 [pv4 EQ']]. unfold ra_ag_compinj_ts in *. ra_ag_pi.
* move:(pv1)(pv2)=>pv1' pv2'. rewrite ->HeqV1 in pv1'. rewrite ->HeqV2 in pv2'.
split; first assumption. split; first assumption.
erewrite <-HeqT1, <-HeqT2 by assumption. eapply Heq; eassumption.
* move:(pv1)(pv2)=>pv1' pv2'. rewrite <-HeqV1 in pv1'. rewrite <-HeqV2 in pv2'.
split; first assumption. split; first assumption.
rewrite ->HeqT1, ->HeqT2 by assumption. eapply Heq; eassumption.
+ intros n [pv1 [pv1' _]]. by apply: HeqT1.
- ra_ag_destr; []. split.
+ intros n. rewrite /ra_ag_compinj_valid /=. split.
* intros [pv1 [[pv2 [pv3 EQ']] EQ]].
split_conjs; try assumption; []. by rewrite EQ.
* intros [[pv1 [pv2 EQ']] [pv3 EQ]]. split_conjs; try assumption; [].
by rewrite -EQ'.
+ intros n _. reflexivity.
- ra_ag_destr. unfold ra_op, ra_ag_op. split.
+ intros n. rewrite /ra_ag_compinj_valid /=. split; intros; split_conjs; try tauto; symmetry; tauto.
+ intros n [pv1 [pv2 EQ]]. assumption.
- eapply ra_ag_dupl.
- ra_ag_destr; unfold ra_valid, ra_agree_valid in *; firstorder.
- exists t'. reflexivity.
- ra_ag_destr; unfold ra_valid, ra_agree_valid in *. split; first reflexivity.
move=>n ? ?. apply equivR. f_equiv. by eapply ProofIrrelevance.
intros. reflexivity.
- ra_ag_destr; unfold ra_valid, ra_agree_valid in *; firstorder.
- ra_ag_destr; [].
destruct (H n) as [Hn _]. assumption.
Qed.
Lemma ra_ag_pord (x y: ra_agree):
x y <-> x · y == y.
x y <-> y · x == y.
Proof.
split.
- move=>[z EQ]. ra_ag_destr; destruct EQ as [EQv EQts]; split.
+ unfold ra_ag_compinj_ts in *; split.
+ split.
* intros (pv1 & pv2 & EQt). assumption.
* intros pv0. hnf. move:(pv0). rewrite -{1}EQv. move=>[pv1 [pv2 EQ']].
exists pv2 pv0. erewrite <-EQts. symmetry. ra_ag_pi.
+ unfold ra_ag_compinj_ts in *; move=>n [pv1 [pv2 EQ]] pv3. ra_ag_pi.
- intros EQ. exists y. rewrite comm. assumption.
Grab Existential Variables.
{ do 2 eexists. eassumption. }
do 2 (split; first assumption). erewrite <-EQts by (simpl; tauto). assumption.
+ intros. reflexivity.
- intros EQ. exists y. assumption.
Qed.
(* We also have a metric *)
......@@ -180,7 +160,7 @@ Section Agreement.
| O => fun _ _ => True
| S _ => fun x y => match x, y with
| ag_inj v1 ts1 _, ag_inj v2 ts2 _ =>
v1 = n = v2 /\ (forall n' pv1 pv2, n' <= n -> ts1 n' pv1 = n' = ts2 n' pv2)
v1 = n = v2 /\ (forall n', n' <= n -> v1 n' -> ts1 n' = n' = ts2 n')
end
end.
......@@ -189,16 +169,13 @@ Section Agreement.
repeat intro. destruct n as [|n]; first by auto.
ra_ag_destr. destruct H as [EQv1 EQts1], H0 as [EQv2 EQts2]. split; move=>[EQv EQts]; split.
- rewrite -EQv1 -EQv2. assumption.
- move=> n' pv1 pv2 HLe. etransitivity; first (symmetry; by eapply EQts1).
etransitivity; last (by eapply EQts2). by eapply EQts.
- move=> n' HLe pv1. etransitivity; first (symmetry; eapply EQts1; by apply EQv1).
etransitivity; last (eapply EQts2; by eapply EQv, EQv1). eapply EQts; first assumption.
by apply EQv1.
- rewrite EQv1 EQv2. assumption.
- move=> n' pv1 pv2 HLe. etransitivity; first (by eapply EQts1).
etransitivity; last (symmetry; by eapply EQts2). now eauto.
Grab Existential Variables.
{ by rewrite -EQv2. }
{ by rewrite -EQv1. }
{ by rewrite EQv2. }
{ by rewrite EQv1. }
- move=> n' HLe pv1. etransitivity; first (by eapply EQts1).
etransitivity; last (symmetry; eapply EQts2; by eapply EQv2, EQv, EQv1).
by eapply EQts, EQv1.
Qed.
Next Obligation.
split.
......@@ -206,29 +183,26 @@ Section Agreement.
split.
+ eapply dist_refl. move=> [|n]; first by apply: dist_bound. destruct (Hall (S n)) as [EQ _].
assumption.
+ intros n pv1 pv2. specialize (Hall (S n)). destruct n as [|n]; first by apply: dist_bound.
+ intros n pv1. specialize (Hall (S n)). destruct n as [|n]; first by apply: dist_bound.
now firstorder.
- repeat intro. destruct n as [|n]; first by auto. ra_ag_destr; now firstorder.
Qed.
Next Obligation.
repeat intro. destruct n as [|n]; first by auto.
ra_ag_destr; try firstorder; [].
- symmetry. now eauto.
ra_ag_destr; now firstorder.
Qed.
Next Obligation.
repeat intro. destruct n as [|n]; first by auto.
ra_ag_destr.
destruct H as [EQv1 EQts1], H0 as [EQv2 EQts2].
split; first now firstorder. intros.
etransitivity; first by eapply EQts1. by eapply EQts2.
Grab Existential Variables.
{ apply EQv1; first omega. assumption. }
etransitivity; first by eapply EQts1. by eapply EQts2, EQv1.
Qed.
Next Obligation.
repeat intro. destruct n as [|n]; first by auto.
ra_ag_destr. destruct H as [EQv EQts]. split.
- move=>n' HLe. eapply EQv. omega.
- move=>n'' pv1 pv2 HLe. eapply EQts. omega.
- move=>n'' HLe pv1. eapply EQts, pv1. omega.
Qed.
Global Instance ra_ag_op_dist n:
......@@ -236,18 +210,14 @@ Section Agreement.
Proof.
move=>a1 aa2 EQa b1 b2 EQb. destruct n as [|n]; first by apply: dist_bound.
ra_ag_destr; try firstorder; []. destruct EQa as [EQv1 EQts1], EQb as [EQv2 EQts2]. split.
- move=>n' HLe. split; move=>[pv1 [pv2 EQ]]; do 2 eexists.
+ etransitivity; first by (symmetry; eapply EQts1; omega).
etransitivity; last by (eapply EQts2; omega). eassumption.
+ etransitivity; first by (eapply EQts1; omega).
etransitivity; last by (symmetry; eapply EQts2; omega). eassumption.
- unfold ra_ag_compinj_ts in *. move=>n' [pv1 [pv2 EQ]] [pv3 [pv4 EQ']] HLe.
eapply EQts1. omega.
Grab Existential Variables.
{ apply EQv2; assumption. }
{ apply EQv1; assumption. }
{ apply EQv2; assumption. }
{ apply EQv1; assumption. }
- move=>n' HLe. simpl. split; move=>[pv1 [pv2 EQ]].
+ split; first by apply EQv1. split; first by apply EQv2.
etransitivity; first by (symmetry; eapply EQts1).
etransitivity; last by (eapply EQts2). eassumption.
+ split; first by apply EQv1. split; first by apply EQv2.
etransitivity; first by eapply EQts1, EQv1.
etransitivity; last by (symmetry; eapply EQts2, EQv2). eassumption.
- move=>n' HLe [pv1 [pv2 EQ]]. now eapply EQts1.
Qed.
Global Instance ra_ag_inj_dist n:
......@@ -256,7 +226,7 @@ Section Agreement.
move=>t1 t2 EQt. destruct n as [|n]; first by apply: dist_bound.
simpl. rewrite -/dist. split.
- move=>? _. reflexivity.
- move=>m _ _ Hle. eapply mono_dist, EQt. omega.
- move=>m Hle _. eapply mono_dist, EQt. omega.
Qed.
Lemma ra_ag_prod_dist x y n:
......@@ -270,13 +240,12 @@ Section Agreement.
- move=>m Hle /=. split.
+ move=>_. eapply dpred, pv1. omega.
+ move=>_.
assert (pv0: v0 m) by (eapply dpred, pv1; omega).
assert (pv: v m) by (eapply dpred, pv2; omega).
exists pv0 pv. assert (m <= S n) by omega.
split; first by (eapply dpred, pv1; omega).
split; first by (eapply dpred, pv2; omega).
etransitivity; last (etransitivity; first (eapply mono_dist, Heq; omega)).
* symmetry. etransitivity; first now eapply tsx0. pi.
* etransitivity; first now eapply tsx. pi.
- move=>m pvcomp pv3 Hle. unfold ra_ag_compinj_ts. pi.
* symmetry. etransitivity; first now eapply tsx0. reflexivity.
* etransitivity; first now eapply tsx. reflexivity.
- intros. reflexivity.
Qed.
Program Definition ra_ag_vchain (σ: chain ra_agree) {σc: cchain σ} : chain SPred :=
......@@ -326,19 +295,14 @@ Section Agreement.
move=><-. assumption.
Qed.
Program Definition ra_ag_tsdiag_n (σ : chain ra_agree) {σc : cchain σ} n {pv: compl (ra_ag_vchain σ) n}: T :=
Definition ra_ag_tsdiag_n (σ : chain ra_agree) n: T :=
match σ (S n) with
| ag_inj v' ts' tsx' => ts' n _
| ag_inj v' ts' tsx' => ts' n
end.
Next Obligation.
unfold ra_ag_vchain in pv. move: pv.
ddes (σ (S n)) at 1 3 as [vSSn tsSSn tsxSSn] deqn:EQ; move=>pv.
injection Heq_anonymous=>_ ->. assumption.
Qed.
Program Definition ra_ag_compl (σ : chain ra_agree) {σc : cchain σ} :=
ag_inj (compl (ra_ag_vchain σ))
(fun n pv => ra_ag_tsdiag_n σ n (pv:=pv)) _.
(fun n => ra_ag_tsdiag_n σ n) _.
Next Obligation.
move=>n i HLe pv. simpl. rewrite -/dist.
assert (pvc: compl (ra_ag_vchain σ) i) by assumption.
......@@ -351,9 +315,9 @@ Section Agreement.
{ move:pvc. move/ra_ag_vchain_compl_n. case/(_ i i _ _)/Wrap; [omega|].
move/ra_ag_vchain_n=>H. eapply H. symmetry. eassumption. }
etransitivity; last first.
{ eapply EQts. omega. }
{ eapply EQts; first omega. eapply dpred, pv'. assumption. }
move:(tsxSi (S n) i). move/(_ _ pv')=>EQ.
etransitivity; last eassumption. pi.
etransitivity; last eassumption. reflexivity.
Qed.
Global Program Instance ra_ag_cmt : cmetric ra_agree := mkCMetr ra_ag_compl.
......@@ -364,26 +328,27 @@ Section Agreement.
rewrite (HT (S n)). unfold ra_ag_vchain.
ddes (σ (S i)) at 1 3 as [vSi tsSi tsxSi] deqn:EQSi.
cchain_eleq σ at (S i) i lvl: (S n); move=>[EQv _]. assumption.
- move=>j pv1 pv2 HLej.
- move=>j HLej pv1.
destruct j as [|j]; first by apply: dist_bound.
unfold ra_ag_tsdiag_n.
ddes (σ (S (S j))) at 1 3 as [vSSj tsSSj tsxSSj] deqn:EQSSj.
cchain_eleq σ at (S (S j)) i lvl: (S j); move=>[EQv EQts].
eapply EQts. omega.
rewrite /ra_ag_vchain /= in pv1. move:pv1.
ddes (σ (S (S j))) at 1 3 6 as [vSSj tsSSj tsxSSj] deqn:EQSSj.
intros pv1. cchain_eleq σ at (S (S j)) i lvl: (S j); move=>[EQv EQts].
eapply EQts; first reflexivity. assumption.
Qed.
(* And we have a pcmType, too! *)
Global Instance ra_ag_pcm: pcmType ra_agree.
Proof.
split. repeat intro. eapply ra_ag_pord. unfold compl, ra_ag_cmt, ra_ag_compl.
assert (HT: forall n pv1 pv2, ra_ag_tsdiag_n σ (pv:=pv1) n = n = ra_ag_tsdiag_n ρ (pv:=pv2) n).
{ move=>n pv1 pv2. destruct n as [|n]; first by apply: dist_bound.
assert (HT: forall n, ra_ag_vchain ρ n n -> ra_ag_tsdiag_n σ n = n = ra_ag_tsdiag_n ρ n).
{ move=>n pv. destruct n as [|n]; first by apply: dist_bound.
unfold ra_ag_tsdiag_n.
ddes (σ (S (S n))) at 1 3 as [vσn tsσn tsxσn] deqn:EQσn.
ddes (ρ (S (S n))) at 1 3 as [vρn tsρn tsxρn] deqn:EQρn.
specialize (H (S (S n))). rewrite ->ra_ag_pord in H.
rewrite <-EQσn, <-EQρn in H. destruct H as [EQv EQts].
erewrite <-EQts. unfold ra_ag_compinj_ts. pi.
rewrite <-EQσn, <-EQρn, comm in H. destruct H as [EQv EQts].
apply EQts. rewrite EQv. rewrite /ra_ag_vchain -EQρn in pv. assumption.
}
split.
- move=>n. split; first by (intros (pv1 & pv2 & _); tauto).
......@@ -393,20 +358,10 @@ Section Agreement.
assert (pvσ: (ra_ag_vchain σ n) n).
{ unfold ra_ag_vchain.
ddes (σ (S n)) at 1 3 as [vσn tsσn tsxσn] deqn:EQσn.
specialize (H (S n)). rewrite ->ra_ag_pord, <-EQρn, <-EQσn in H.
specialize (H (S n)). rewrite ->ra_ag_pord, <-EQρn, <-EQσn, comm in H.
destruct H as [EQv _]. rewrite <-EQv in pvρ. destruct pvρ as [pv1 _]. assumption. }
do 2 eexists. etransitivity; last (etransitivity; first by eapply HT).
+ eapply dist_refl. reflexivity.
+ eapply dist_refl. reflexivity.
- intros n (pv1 & pv2 & EQ) pv3.
now eapply HT.
Grab Existential Variables.
{ eapply ra_ag_vchain_ucompl_n. eapply spredNE, pvσ.
eapply (chain_cauchy (ra_ag_vchain σ)); first apply _; omega. }
{ assumption. }
{ apply EQv. eapply ra_ag_vchain_n.
- eapply ra_ag_vchain_compl_n with (m:=S n) (k:=S n); first (by eexact pv2); omega.
- symmetry. eassumption. }
do 2 (split; first assumption). symmetry. apply HT. assumption.
- intros n (pv1 & pv2 & EQ). reflexivity.
Qed.
(* And finally, be ready for the CMRA *)
......@@ -423,42 +378,34 @@ Section Agreement.
Qed.
(* Provide a way to get an n-approximation of the element out of an n-valid agreement. *)
Program Definition ra_ag_unInj x n {HVal: cmra_valid x n}: T :=
Definition ra_ag_unInj x n: T :=
match x with
| ag_inj v ts _ => (ts n _)
| ag_inj v ts _ => ts n
end.
Lemma ra_ag_unInj_dist x y n {HVal1: cmra_valid x n} {HVal2: cmra_valid y n}: (* The function is dependent, hence no "Proper" can be registered *)
x = n = y -> ra_ag_unInj x n (HVal:=HVal1) = n = ra_ag_unInj y n (HVal:=HVal2).
Lemma ra_ag_unInj_dist x y n (HVal1: cmra_valid x n): (* we need validity, hence no "Proper" can be registered *)
x = n = y -> ra_ag_unInj x n = n = ra_ag_unInj y n.
Proof.
move=>EQ. destruct n as [|n]; first exact: dist_bound.
ra_ag_destr; now firstorder.
Qed.
Lemma ra_ag_unInj_move x n1 n2 (Hle: n1 <= n2) {HVal1: cmra_valid x n1} {HVal2: cmra_valid x n2}:
ra_ag_unInj x n1 (HVal:=HVal1) = n1 = ra_ag_unInj x n2 (HVal:=HVal2).
Lemma ra_ag_unInj_move x n1 n2 (Hle: n1 <= n2) {HVal2: cmra_valid x n2}:
ra_ag_unInj x n1 = n1 = ra_ag_unInj x n2.
Proof.
ra_ag_destr.
rewrite /ra_ag_unInj. symmetry.
etransitivity; last (etransitivity; first eapply (tsx n1 n2)); pi.
Grab Existential Variables.
{ exact HVal2. }
etransitivity; last (etransitivity; first eapply (tsx n1 n2)); assumption || reflexivity.
Qed.
Lemma ra_ag_unInj_pi x n {HVal1: cmra_valid x n} {HVal2: cmra_valid x n}:
ra_ag_unInj x n (HVal:=HVal1) = ra_ag_unInj x n (HVal:=HVal2).
Proof.
ra_ag_destr. rewrite /ra_ag_unInj. pi.
Qed.
Lemma ra_ag_inj_unInj_ext x n {HVal: cmra_valid x n} t d:
d · ra_ag_inj t = n = x -> ra_ag_unInj x n (HVal:=HVal) = n = t.
Lemma ra_ag_inj_unInj_ext x n (HVal: cmra_valid x n) t d:
d · ra_ag_inj t = n = x -> ra_ag_unInj x n = n = t.
Proof.
rewrite comm.
destruct x as [v ts tsx], d as [v' ts' tsx'] =>Heq.
destruct n as [|n]; first exact: dist_bound.
unfold ra_ag_inj in Heq. destruct Heq as [EQv EQts]. unfold ra_ag_compinj_ts in EQts. unfold ra_ag_unInj.
symmetry. eapply EQts; last reflexivity.
unfold ra_ag_inj in Heq. destruct Heq as [EQv EQts]. unfold ra_ag_unInj.
symmetry. eapply EQts; first reflexivity.
eapply spredNE, HVal. symmetry. exact EQv.
Qed.
......@@ -467,20 +414,17 @@ Section Agreement.
(* For this, we need a complete metric! *)
Context {cmT: cmetric T}.
Program Definition ra_ag_tschain v (ts: vChain v) (tsx: cvChain ts) {HVal: (ag_inj v ts tsx)}: chain T :=
fun i => ts i _.
Instance ra_ag_tschain_c v (ts: vChain v) (tsx: cvChain ts) {HVal: (ag_inj v ts tsx)} : cchain (ra_ag_tschain v ts tsx (HVal:=HVal)).
Lemma ra_ag_tschain_c {v} (ts: chain T) (tsx: cvChain v ts) {HVal: (ag_inj v ts tsx)} : cchain ts.
Proof.
intros n j m HLe1 HLe2. destruct n as [|n]; first by apply: dist_bound. unfold ra_ag_tschain.
intros n j m HLe1 HLe2. destruct n as [|n]; first by apply: dist_bound.
etransitivity; first by eapply (tsx (S n)).
symmetry. etransitivity; first by eapply (tsx (S n)).
apply equivR. f_equiv. eapply ProofIrrelevance.
reflexivity.
Qed.
Program Definition ra_ag_unInjFull x {HVal: x}: T :=
match x with
| ag_inj v ts tsx => compl (ra_ag_tschain v ts tsx (HVal:=_))
| ag_inj v ts tsx => compl ts (σc:=ra_ag_tschain_c ts tsx (HVal:=_))
end.
Lemma ra_ag_unInjFull_dist x y {HVal1: x} {HVal2: y} n: (* The function is dependent, hence no "Proper" can be registered *)
......@@ -490,17 +434,19 @@ Section Agreement.
destruct x as [xv xts xtsx].
destruct y as [yv yts ytsx].
destruct EQ as [_ EQts]. unfold ra_valid, ra_agree_valid in HVal1. unfold ra_valid, ra_agree_valid in HVal2.
simpl. eapply umet_complete_extn. unfold ra_ag_tschain.
eapply EQts. reflexivity.
simpl. eapply umet_complete_extn.
eapply EQts.
- reflexivity.
- apply HVal1.
Qed.
(* Correctness of the embedding (and of the entire construction, really - together with the duplicability shown above) *)
Lemma ra_ag_inj_unInjFull x {HVal: x} t:
ra_ag_inj t x -> ra_ag_unInjFull x (HVal:=HVal) == t.
Proof.
rewrite ra_ag_pord. destruct x as [v ts tsx]=>Heq.
rewrite ra_ag_pord comm. destruct x as [v ts tsx]=>Heq.
unfold ra_ag_inj in Heq. destruct Heq as [EQv EQts]. simpl. rewrite <-(umet_complete_const t).
apply umet_complete_ext=>i. unfold ra_ag_tschain. unfold ra_ag_compinj_ts in EQts. symmetry.
apply umet_complete_ext=>i. symmetry.
eapply EQts. rewrite EQv. apply HVal.
Qed.
......@@ -513,29 +459,28 @@ Section AgreementMap.