Agreement.v 20.7 KB
Newer Older
1
Require Import Ssreflect.ssreflect Ssreflect.ssrfun Omega.
2
Require Import SPred PreoMet RA CMRA.
3

4 5
Set Bullet Behavior "Strict Subproofs".

6 7 8 9 10 11
Local Open Scope ra_scope.
Local Open Scope predom_scope.

Section Agreement.
  (* This is more complex than above, and it does not require a decidable equality. However, it needs
     a metric. It also comes with a CMRA. *)
Ralf Jung's avatar
Ralf Jung committed
12
  Context {T} `{T_ty : Setoid T} {mT: metric T}.
13
  Local Open Scope ra_scope.
14
  Local Open Scope nat.
15

16 17 18 19
  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.
20

21
  CoInductive ra_agree : Type :=
22
    ag_inj (v: SPred) (ts: chain T) (tsx: cvChain v ts).
23

24
  Global Instance ra_agree_unit : RA_unit ra_agree := fun x => x.
25
  Global Instance cmra_agree_valid : CMRA_valid _ :=
26
    fun x => match x with
Ralf Jung's avatar
Ralf Jung committed
27
             | ag_inj v _ _ => v
28
             end.
29
  Global Instance ra_agree_valid : RA_valid _ := compose valid_sp cmra_agree_valid.
30

31
(*  Local Ltac ra_ag_pi := match goal with
32 33
                           [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. *)
Ralf Jung's avatar
Ralf Jung committed
34 35
                           first [rewrite_pi pv12 pv11; rewrite_pi pv22 pv21; eexact H |
                                  rewrite_pi pv22 pv21; eexact H | rewrite_pi pv12 pv11; eexact H]
36
                         end. *)
37 38


39 40
  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) _ _.
41
  (* 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. *)
42
  Next Obligation.
43
    split; last split; exact:dist_bound||exact:bpred.
44
  Qed.
45
  Next Obligation.
46 47 48 49 50 51
    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.
52 53
  Qed.

54 55
  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.
56
  Proof.
57 58
    move=> n i HLe [pv1 [pv2 EQ]].
    eapply ts1x; assumption.
59 60 61 62 63
  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 =>
64
                 ag_inj (ra_ag_compinj_valid ts1 ts2 ts1x ts2x) ts1
65 66 67
                        (ra_ag_compinj_tsx ts1 ts2 ts1x ts2x)
               end.
  Program Definition ra_ag_inj (t: T): ra_agree :=
68
    ag_inj top_sp (fun _ => t) (fun _ _ _ _ => _).
69 70 71 72 73 74 75 76 77 78 79 80
  Next Obligation.
    eapply dist_refl. reflexivity.
  Qed.
  
  Lemma ra_ag_inj_valid t:
    ra_agree_valid (ra_ag_inj t).
  Proof.
    intros n. exact I.
  Qed.

  Definition ra_agree_eq (x y: ra_agree): Prop :=
    match x, y with
81
    | ag_inj v1 ts1 _, ag_inj v2 ts2 _ => v1 == v2 /\ (forall n, v1 n -> ts1 n = n = ts2 n)
82 83 84 85 86 87 88 89 90 91
    (* 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).

  Global Instance ra_agree_eq_equiv : Equivalence ra_agree_eq.
  Proof.
    split; repeat intro; ra_ag_destr; try (exact I || contradiction); [| |]. (* 3 goals left. *)
92 93 94
    - split; intros; reflexivity.
    - destruct H. split; intros; first by symmetry.
      symmetry. apply H0. rewrite H. assumption.
95 96
    - destruct H, H0.
      split; first (etransitivity; now eauto).
97 98
      intro; etransitivity; [now eapply H1 | ].
      eapply H2. rewrite -H. assumption.
99 100
  Qed.
  Global Instance ra_agree_type : Setoid ra_agree := mkType ra_agree_eq.
101

102
  Lemma ra_ag_dupl (x : ra_agree):
103 104 105
    x · x == x.
  Proof.
    ra_ag_destr. split.
106 107
    - split; simpl; first by firstorder. now firstorder.
    - move=>n ?. reflexivity.
108 109
  Qed.
  
110 111 112
  Global Instance ra_agree_res : RA ra_agree.
  Proof.
    split; repeat intro.
113
    - ra_ag_destr; [].
114 115 116
      destruct H as (HeqV1 & HeqT1), H0 as (HeqV2 & HeqT2).
      split.
      + split; intros (pv1 & pv2 & Heq).
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133
        * 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.
134
    - eapply ra_ag_dupl.
135
    - ra_ag_destr; unfold ra_valid, ra_agree_valid in *; firstorder.
136 137
    - exists t'. reflexivity.
    - ra_ag_destr; unfold ra_valid, ra_agree_valid in *. split; first reflexivity.
138
      intros. reflexivity.
Jan-Oliver Kaiser's avatar
Jan-Oliver Kaiser committed
139
    - ra_ag_destr; unfold ra_valid, ra_agree_valid in *; firstorder.
140
    - ra_ag_destr; [].
141
      destruct (H n) as [Hn _]. assumption.
142 143 144
  Qed.

  Lemma ra_ag_pord (x y: ra_agree):
145
    x  y <-> y · x == y.
146 147
  Proof.
    split.
148
    - move=>[z EQ]. ra_ag_destr; destruct EQ as [EQv EQts]; split.
149
      + split.
150 151
        * intros (pv1 & pv2 & EQt). assumption.
        * intros pv0. hnf. move:(pv0). rewrite -{1}EQv. move=>[pv1 [pv2 EQ']].
152 153 154
          do 2 (split; first assumption). erewrite <-EQts by (simpl; tauto). assumption.
      + intros. reflexivity.
    - intros EQ. exists y. assumption.
155 156 157 158 159 160
  Qed.

  (* We also have a metric *)
  Definition ra_agree_dist n :=
    match n with
    | O => fun _ _ => True
161
    | S _ => fun x y => match x, y with
162
                        | ag_inj v1 ts1 _, ag_inj v2 ts2 _ =>
163
                          v1 = n = v2 /\ (forall n', n' <= n -> v1 n' -> ts1 n' = n' = ts2 n')
164 165 166 167 168 169
                        end
    end.

  Global Program Instance ra_agree_metric : metric ra_agree := mkMetr ra_agree_dist.
  Next Obligation.
    repeat intro. destruct n as [|n]; first by auto.
170
    ra_ag_destr. destruct H as [EQv1 EQts1], H0 as [EQv2 EQts2]. split; move=>[EQv EQts]; split.
171
    - rewrite -EQv1 -EQv2. assumption.
172 173 174
    - 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.
175
    - rewrite EQv1 EQv2. assumption.
176 177 178
    - move=> n' HLe pv1. etransitivity; first (by eapply EQts1).
      etransitivity; last (symmetry; eapply EQts2; by eapply EQv2, EQv, EQv1).
      by eapply EQts, EQv1.
179 180 181
  Qed.
  Next Obligation.
    split.
182
    - intros Hall. ra_ag_destr.
183
      split.
184
      + eapply dist_refl. move=> [|n]; first by apply: dist_bound. destruct (Hall (S n)) as [EQ _].
185
        assumption.
186
      + intros n pv1. specialize (Hall (S n)). destruct n as [|n]; first by apply: dist_bound.
187 188 189 190 191
        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.
192
    ra_ag_destr; now firstorder.
193 194 195
  Qed.
  Next Obligation.
    repeat intro. destruct n as [|n]; first by auto.
196 197 198
    ra_ag_destr.
    destruct H as [EQv1 EQts1], H0 as [EQv2 EQts2].
    split; first now firstorder. intros.
199
    etransitivity; first by eapply EQts1. by eapply EQts2, EQv1.
200 201 202
  Qed.
  Next Obligation.
    repeat intro. destruct n as [|n]; first by auto.
203
    ra_ag_destr. destruct H as [EQv EQts]. split.
204
    - move=>n' HLe. eapply EQv. omega.
205
    - move=>n'' HLe pv1. eapply EQts, pv1. omega.
206 207 208 209 210 211 212
  Qed.

  Global Instance ra_ag_op_dist n:
    Proper (dist n ==> dist n ==> dist n) ra_ag_op.
  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.
213 214 215 216 217 218 219 220
    - 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.
221 222 223 224 225
  Qed.

  Global Instance ra_ag_inj_dist n:
    Proper (dist n ==> dist n) ra_ag_inj.
  Proof.
226 227 228
    move=>t1 t2 EQt. destruct n as [|n]; first by apply: dist_bound.
    simpl. rewrite -/dist. split.
    - move=>? _. reflexivity.
229
    - move=>m Hle _. eapply mono_dist, EQt. omega.
230
  Qed.
231

232 233 234 235 236 237 238 239 240 241 242
  Lemma ra_ag_prod_dist x y n:
    cmra_valid (x · y) n ->
    x · y = n = x.
  Proof.
    move=>Hval.  destruct n as [|n]; first exact: dist_bound.
    unfold cmra_valid in Hval. ra_ag_destr. simpl in Hval.
    destruct Hval as [pv1 [pv2 Heq]].
    split.
    - move=>m Hle /=. split.
      + move=>_. eapply dpred, pv1. omega.
      + move=>_.
243 244
        split; first by (eapply dpred, pv1; omega).
        split; first by (eapply dpred, pv2; omega).
245
        etransitivity; last (etransitivity; first (eapply mono_dist, Heq; omega)).
246 247 248
        * symmetry. etransitivity; first now eapply tsx0. reflexivity.
        * etransitivity; first now eapply tsx. reflexivity.
    - intros. reflexivity.
249 250
  Qed.

251
  Program Definition ra_ag_vchain (σ: chain ra_agree) {σc: cchain σ} : chain SPred :=
252 253 254 255
    fun i => match σ (S i) with
             | ag_inj v' _ _ => v'
             end.

256
  Instance ra_ag_vchain_c (σ: chain ra_agree) {σc: cchain σ} : cchain (ra_ag_vchain σ).
257 258
  Proof.
    intros n j m HLe1 HLe2. destruct n as [|n]; first by apply: dist_bound. unfold ra_ag_vchain.
259 260
    ddes (σ (S j)) at 1 3 as [v1 ts1 tsx1] deqn:EQ1.
    ddes (σ (S m)) at 1 3 as [v2 ts2 tsx2] deqn:EQ2.
261
    cchain_eleq σ at (S j) (S m) lvl:(S n); move=>[EQv _].
262
    assumption.
263 264
  Qed.

265 266 267
  Lemma ra_ag_vchain_compl_n (σ: chain ra_agree) {σc: cchain σ} n:
    compl (ra_ag_vchain σ) n ->
    forall m k, m <= n -> k >= n -> ra_ag_vchain σ k m.
268 269
  Proof.
    move=>pv m k HLe HLe'.
270
    assert (HTv := conv_cauchy (ra_ag_vchain σ) (S n) _ (le_refl _)).
271 272
    apply HTv in pv; last by omega.
    clear HTv. move:pv. unfold ra_ag_vchain.
273 274
    ddes (σ (S (S n))) at 1 3 as [v1 ts1 tsx1] deqn:EQ1.
    ddes (σ (S k)) at 1 3 as [v2 ts2 tsx2] deqn:EQ2=>pv.
275 276 277 278
    cchain_eleq σ at (S (S n)) (S k) lvl:(S m); move=>[EQv _].
    apply EQv; first omega. eapply dpred; eassumption.
  Qed.

279 280 281
  Lemma ra_ag_vchain_ucompl_n (σ: chain ra_agree) {σc: cchain σ} n:
    ra_ag_vchain σ (S n) n ->
    compl (ra_ag_vchain σ) n.
282 283
  Proof.
    move=>pv.
284
    assert (HTv := conv_cauchy (ra_ag_vchain σ) (S n) _ (le_refl _)).
285 286 287
    apply HTv in pv; last by omega. assumption.
  Qed.

288 289
  Lemma ra_ag_vchain_n (σ: chain ra_agree) {σc: cchain σ} n m:
    ra_ag_vchain σ n m -> forall v' ts' tsx', σ (S n) = ag_inj v' ts' tsx' -> v' m.
290 291 292
  Proof.
    move=>pv v' ts' tsx' EQ. move:pv EQ.
    unfold ra_ag_vchain.
293
    ddes (σ (S n)) at 1 3 as [vSn tsSn tsxSSn] deqn:EQSSn.
294 295 296 297
    move=>pv EQ. rewrite EQ in EQSSn. injection EQSSn=>{EQSSn EQ}EQ. destruct EQ.
    move=><-. assumption.
  Qed.

298
  Definition ra_ag_tsdiag_n (σ : chain ra_agree) n: T :=
299
    match σ (S n) with
300
    | ag_inj v' ts' tsx' => ts' n
301 302 303
    end.

  Program Definition ra_ag_compl (σ : chain ra_agree) {σc : cchain σ} :=
304
    ag_inj (compl (ra_ag_vchain σ))
305
           (fun n => ra_ag_tsdiag_n σ n) _.
306 307
  Next Obligation.
    move=>n i HLe pv. simpl. rewrite -/dist.    
308
    assert (pvc: compl (ra_ag_vchain σ) i) by assumption.
309 310
    destruct n as [|n]; first by apply: dist_bound.
    unfold ra_ag_tsdiag_n.
311 312
    ddes (σ (S i)) at 1 3 as [vSi tsSi tsxSi] deqn:EQSi.
    ddes (σ (S (S n))) at 1 3 as [vSSn tsSSn tsxSSn] deqn:EQSSn.
313 314 315 316 317
    cchain_eleq σ at (S i) (S (S n)) lvl:(S (S n)); move=>[EQv EQts].
    assert (pv': vSi i).
    { 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.
318
    { eapply EQts; first omega. eapply dpred, pv'. assumption. }
319
    move:(tsxSi (S n) i). move/(_ _ pv')=>EQ.
320
    etransitivity; last eassumption. reflexivity.
321 322 323 324 325
  Qed.

  Global Program Instance ra_ag_cmt : cmetric ra_agree := mkCMetr ra_ag_compl.
  Next Obligation.
    intros [| n]; [now intros; apply dist_bound | unfold ra_ag_compl].
326 327
    intros i HLe. destruct (σ i) as [vi] eqn: EQi; split.
    - assert (HT:=conv_cauchy (ra_ag_vchain σ)).
328 329 330
      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.
331
    - move=>j HLej pv1.
332 333
      destruct j as [|j]; first by apply: dist_bound.
      unfold ra_ag_tsdiag_n.
334 335 336 337
      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.
338 339 340 341 342 343
  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.
344 345
    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.
346 347 348 349
      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.
350 351
      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.
352 353 354 355
    }
    split.
    - move=>n. split; first by (intros (pv1 & pv2 & _); tauto).
      simpl. move=>pv. move:(pv). rewrite {1}/ra_ag_vchain. simpl.
356
      ddes (ρ (S n)) at 1 3 as [vρn tsρn tsxρn] deqn:EQρn.
357
      move=>pvρ.
358
      assert (pvσ: (ra_ag_vchain σ n) n).
359
      { unfold ra_ag_vchain.
360
        ddes (σ (S n)) at 1 3 as [vσn tsσn tsxσn] deqn:EQσn.
361
        specialize (H (S n)). rewrite ->ra_ag_pord, <-EQρn, <-EQσn, comm in H.
362
        destruct H as [EQv _]. rewrite <-EQv in pvρ. destruct pvρ as [pv1 _]. assumption. }
363 364
      do 2 (split; first assumption). symmetry. apply HT. assumption.
    - intros n (pv1 & pv2 & EQ). reflexivity.
365 366 367
  Qed.

  (* And finally, be ready for the CMRA *)
368 369 370 371
  Global Instance ra_ag_cmra : CMRA ra_agree.
  Proof.
    split.
    - now apply _.
Jan-Oliver Kaiser's avatar
Jan-Oliver Kaiser committed
372
    - by move=>[|n] t1 t2 EQt. 
373
    - move=>n t1 t2 EQt. destruct n as [|n]; first exact: dist_bound.
374
      ra_ag_destr; now firstorder.
375
    - move=>t. reflexivity.
376
    - move=> t1 t2. ra_ag_destr.
377
      move=>n [pv _]. exact pv.
378
  Qed.
379

380
  (* Provide a way to get an n-approximation of the element out of an n-valid agreement. *)
381
  Definition ra_ag_unInj x n: T :=
382
    match x with
383
    | ag_inj v ts _ => ts n
384 385
    end.

386 387
  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.
388 389 390 391 392
  Proof.
    move=>EQ. destruct n as [|n]; first exact: dist_bound.
    ra_ag_destr; now firstorder.
  Qed.

393 394
  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.
395 396 397
  Proof.
    ra_ag_destr.
    rewrite /ra_ag_unInj. symmetry.
398
    etransitivity; last (etransitivity; first eapply (tsx n1 n2)); assumption || reflexivity.
399 400
  Qed.

401 402
  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.
403
  Proof.
404 405 406
    rewrite comm.
    destruct x as [v ts tsx], d as [v' ts' tsx'] =>Heq.
    destruct n as [|n]; first exact: dist_bound. 
407 408
    unfold ra_ag_inj in Heq. destruct Heq as [EQv EQts]. unfold ra_ag_unInj.
    symmetry. eapply EQts; first reflexivity.
409
    eapply spredNE, HVal. symmetry. exact EQv.
410 411 412 413
  Qed.
  
  (* Provide a way to get the full T out of the agreement again. We don't need this, but I proved it before
     I realized. *)
414 415 416
  (* For this, we need a complete metric! *)
  Context {cmT: cmetric T}.

417
  Lemma ra_ag_tschain_c {v} (ts: chain T) (tsx: cvChain v ts) {HVal: (ag_inj v ts tsx)} : cchain ts.
418
  Proof.
419
    intros n j m HLe1 HLe2. destruct n as [|n]; first by apply: dist_bound. 
420 421
    etransitivity; first by eapply (tsx (S n)).
    symmetry. etransitivity; first by eapply (tsx (S n)).
422
    reflexivity.
423 424
  Qed.

425
  Program Definition ra_ag_unInjFull x {HVal: x}: T :=
426
    match x with
427
    | ag_inj v ts tsx => compl ts (σc:=ra_ag_tschain_c ts tsx (HVal:=_))
428 429
    end.

430 431
  Lemma ra_ag_unInjFull_dist x y {HVal1: x} {HVal2: y} n: (* The function is dependent, hence no "Proper" can be registered *)
    x = n = y -> ra_ag_unInjFull x (HVal:=HVal1) = n = ra_ag_unInjFull y (HVal:=HVal2).
432
  Proof.
433
    move=>EQ. destruct n as [|n]; first exact: dist_bound.
434 435
    destruct x as [xv xts xtsx].
    destruct y as [yv yts ytsx].
436
    destruct EQ as [_ EQts]. unfold ra_valid, ra_agree_valid in HVal1. unfold ra_valid, ra_agree_valid in HVal2.
437 438 439 440
    simpl. eapply umet_complete_extn. 
    eapply EQts.
    - reflexivity.
    - apply HVal1.
441
  Qed.
442

443 444 445
  (* 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.
446
  Proof.
447
    rewrite ra_ag_pord comm. destruct x as [v ts tsx]=>Heq.
448
    unfold ra_ag_inj in Heq. destruct Heq as [EQv EQts]. simpl. rewrite <-(umet_complete_const t).
449
    apply umet_complete_ext=>i. symmetry.
450 451
    eapply EQts. rewrite EQv. apply HVal.
  Qed.
452 453

End Agreement.
Ralf Jung's avatar
Ralf Jung committed
454
Arguments ra_agree T {_ _} : clear implicits.
455 456 457 458 459 460 461

Section AgreementMap.
  Context {T U: Type} `{cmT: cmetric T} `{cmU: cmetric U}.
  Local Open Scope pumet_scope.

  Program Definition ra_agree_map (f: T -n> U): ra_agree T -m> ra_agree U :=
    m[(fun x => match x with
462
                | ag_inj v ts tsx => ag_inj v (compose f ts) _
463 464 465 466
                end)].
  Next Obligation.
    move=>n i HLe pv. simpl. eapply met_morph_nonexp. specialize (tsx n i HLe pv).
    rewrite tsx.
467
    eapply dist_refl. reflexivity.
468 469 470 471 472 473
  Qed.
  Next Obligation.
    move=> x y EQxy.
    destruct n as [|n]; first by apply: dist_bound.
    repeat (match goal with [ x : ra_agree _ |- _ ] => destruct x end); try (contradiction EQxy || reflexivity); [].
    destruct EQxy as [Hv Hts]. split; first assumption.
474
    move=>n' HLe pv1. specialize (Hts n' HLe pv1). unfold compose. rewrite Hts. reflexivity.
475 476 477 478 479 480
  Qed.
  Next Obligation.
    move=>x y EQxy. apply ra_ag_pord. apply ra_ag_pord in EQxy.
    repeat (match goal with [ x : ra_agree _ |- _ ] => destruct x end); try (contradiction EQxy || reflexivity); [].
    destruct EQxy as [EQv EQts]. split; first split.
    - intros (pv1 & pv2 & _). assumption.
481 482 483
    - move=>pv. move/EQv:(pv)=>[pv1 [pv2 EQ]]. do 2 (split; first assumption).
      unfold compose. rewrite EQ. reflexivity.
    - unfold compose. intros n [pv1 [pv2 EQ]]. reflexivity.
484 485 486 487 488
  Qed.

  Global Instance ra_agree_map_resp: Proper (equiv ==> equiv) ra_agree_map.
  Proof.
    move=> x1 x2 EQx y.
489
    repeat (match goal with [ x : ra_agree _ |- _ ] => destruct x end).
490
    split; first reflexivity.
491
    move=>n pv1. rewrite EQx. unfold compose. reflexivity.
492 493 494 495
  Qed.
  Global Instance ra_agree_map_dist n: Proper (dist n ==> dist n) ra_agree_map.
  Proof.
    move=> x1 x2 EQx y.
496
    repeat (match goal with [ x : ra_agree _ |- _ ] => destruct x end).
497 498
    destruct n as [|n]; first by apply: dist_bound.
    split; first reflexivity.
499 500
    move=>n' HLe pv1. rewrite /compose. eapply mono_dist; last first.
    - rewrite EQx. reflexivity.
501 502 503 504 505 506 507 508 509 510 511 512
    - omega.
  Qed.
End AgreementMap.

Section AgreementMapComp.
  Local Open Scope pumet_scope.
  Context {T: Type} `{cmT: cmetric T}.

  Lemma ra_agree_map_id:
    ra_agree_map (umid T) == (pid (ra_agree T)).
  Proof.
    intros x.
513
    repeat (match goal with [ x : ra_agree _ |- _ ] => destruct x end).
514
    simpl. split; first reflexivity.
515
    reflexivity.
516 517 518 519 520 521 522 523
  Qed.
  
  Context {U V: Type} `{cmU: cmetric U} `{cmV: cmetric V}.

  Lemma ra_agree_map_comp (f: T -n> U) (g: U -n> V): 
    (ra_agree_map g)  (ra_agree_map f) == ra_agree_map (g <M< f).
  Proof.
    intros x.
524
    repeat (match goal with [ x : ra_agree _ |- _ ] => destruct x end).
525
    simpl. split; first reflexivity.
526
    intros. reflexivity.
527 528
  Qed.
End AgreementMapComp.