agree.v 8.27 KB
Newer Older
1
From iris.algebra Require Export cmra.
2
From iris.base_logic Require Import base_logic.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
Local Hint Extern 10 (_  _) => omega.

5
Record agree (A : Type) : Type := Agree {
6
  agree_car : nat  A;
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  agree_is_valid : nat  Prop;
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  agree_valid_S n : agree_is_valid (S n)  agree_is_valid n
Robbert Krebbers's avatar
Robbert Krebbers committed
9
}.
10
Arguments Agree {_} _ _ _.
11
12
Arguments agree_car {_} _ _.
Arguments agree_is_valid {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14

Section agree.
15
Context {A : ofeT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
16

17
Instance agree_validN : ValidN (agree A) := λ n x,
18
  agree_is_valid x n   n', n'  n  agree_car x n {n'} agree_car x n'.
19
20
Instance agree_valid : Valid (agree A) := λ x,  n, {n} x.

Robbert Krebbers's avatar
Robbert Krebbers committed
21
Lemma agree_valid_le n n' (x : agree A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
  agree_is_valid x n  n'  n  agree_is_valid x n'.
Proof. induction 2; eauto using agree_valid_S. Qed.
24

25
Instance agree_equiv : Equiv (agree A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  ( n, agree_is_valid x n  agree_is_valid y n) 
27
  ( n, agree_is_valid x n  agree_car x n {n} agree_car y n).
28
Instance agree_dist : Dist (agree A) := λ n x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  ( n', n'  n  agree_is_valid x n'  agree_is_valid y n') 
30
  ( n', n'  n  agree_is_valid x n'  agree_car x n' {n'} agree_car y n').
31
Definition agree_ofe_mixin : OfeMixin (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
Proof.
  split.
34
  - intros x y; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
    + by intros Hxy n; split; intros; apply Hxy.
    + by intros Hxy; split; intros; apply Hxy with n.
37
  - split.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
39
40
    + by split.
    + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
    + intros x y z Hxy Hyz; split; intros n'; intros.
41
      * trans (agree_is_valid y n'). by apply Hxy. by apply Hyz.
42
      * trans (agree_car y n'). by apply Hxy. by apply Hyz, Hxy.
43
  - intros n x y Hxy; split; intros; apply Hxy; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Qed.
45
46
47
48
49
50
51
52
53
54
55
56
57
58
Canonical Structure agreeC := OfeT (agree A) agree_ofe_mixin.

Program Definition agree_compl : Compl agreeC := λ c,
  {| agree_car n := agree_car (c n) n;
     agree_is_valid n := agree_is_valid (c n) n |}.
Next Obligation.
  intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto.
Qed.
Global Program Instance agree_cofe : Cofe agreeC :=
  {| compl := agree_compl |}.
Next Obligation.
  intros n c; apply and_wlog_r; intros;
    symmetry; apply (chain_cauchy c); naive_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
59

60
Program Instance agree_op : Op (agree A) := λ x y,
61
  {| agree_car := agree_car x;
62
     agree_is_valid n := agree_is_valid x n  agree_is_valid y n  x {n} y |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Instance agree_pcore : PCore (agree A) := Some.
65

66
Instance: Comm () (@op (agree A) _).
67
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
Ralf Jung's avatar
...    
Ralf Jung committed
68
Lemma agree_idemp (x : agree A) : x  x  x.
69
Proof. split; naive_solver. Qed.
70
71
72
Instance:  n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n).
Proof.
  intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?].
73
74
  rewrite -(proj2 Hxy n') -1?(Hx n'); eauto using agree_valid_le.
  symmetry. by apply dist_le with n; try apply Hxy.
75
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78
79
80
Instance:  x : agree A, Proper (dist n ==> dist n) (op x).
Proof.
  intros n x y1 y2 [Hy' Hy]; split; [|done].
  split; intros (?&?&Hxy); repeat (intro || split);
    try apply Hy'; eauto using agree_valid_le.
81
82
  - etrans; [apply Hxy|apply Hy]; eauto using agree_valid_le.
  - etrans; [apply Hxy|symmetry; apply Hy, Hy'];
Robbert Krebbers's avatar
Robbert Krebbers committed
83
84
      eauto using agree_valid_le.
Qed.
85
Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
86
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
87
Instance: Proper (() ==> () ==> ()) op := ne_proper_2 _.
88
Instance: Assoc () (@op (agree A) _).
89
90
91
Proof.
  intros x y z; split; simpl; intuition;
    repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
92
    by cofe_subst; rewrite !agree_idemp.
93
Qed.
94

Robbert Krebbers's avatar
Robbert Krebbers committed
95
96
97
98
99
Lemma agree_included (x y : agree A) : x  y  y  x  y.
Proof.
  split; [|by intros ?; exists y].
  by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
100
101
102
103
104
105
106
107
Lemma agree_op_inv n (x1 x2 : agree A) : {n} (x1  x2)  x1 {n} x2.
Proof. intros Hxy; apply Hxy. Qed.
Lemma agree_valid_includedN n (x y : agree A) : {n} y  x {n} y  x {n} y.
Proof.
  move=> Hval [z Hy]; move: Hval; rewrite Hy.
  by move=> /agree_op_inv->; rewrite agree_idemp.
Qed.

108
Definition agree_cmra_mixin : CMRAMixin (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
  apply cmra_total_mixin; try apply _ || by eauto.
111
  - intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
112
    rewrite -(Hx n'); last auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
    symmetry; apply dist_le with n; try apply Hx; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  - intros x. apply agree_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
115
  - by intros n x y [(?&?&?) ?].
116
  - intros n x y1 y2 Hval Hx; exists x, x; simpl; split.
117
118
    + by rewrite agree_idemp.
    + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Qed.
120
Canonical Structure agreeR : cmraT :=
121
  CMRAT (agree A) agree_ofe_mixin agree_cmra_mixin.
122

Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
Global Instance agree_total : CMRATotal agreeR.
Proof. rewrite /CMRATotal; eauto. Qed.
125
Global Instance agree_persistent (x : agree A) : Persistent x.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Proof. by constructor. Qed.
127

Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
130
Program Definition to_agree (x : A) : agree A :=
  {| agree_car n := x; agree_is_valid n := True |}.
Solve Obligations with done.
131

Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
134
Global Instance to_agree_proper : Proper (() ==> ()) to_agree := ne_proper _.
135

136
Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree).
137
Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
138
139
140
141
142
143

Lemma to_agree_uninj n (x : agree A) : {n} x   y : A, to_agree y {n} x.
Proof.
  intros [??]. exists (agree_car x n).
  split; naive_solver eauto using agree_valid_le.
Qed.
144
145

(** Internalized properties *)
146
Lemma agree_equivI {M} a b : to_agree a  to_agree b  (a  b : uPred M).
147
148
149
Proof.
  uPred.unseal. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne.
Qed.
150
Lemma agree_validI {M} x y :  (x  y)  (x  y : uPred M).
151
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_inv. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
153
End agree.

154
Arguments agreeC : clear implicits.
155
Arguments agreeR : clear implicits.
156

157
Program Definition agree_map {A B} (f : A  B) (x : agree A) : agree B :=
158
  {| agree_car n := f (agree_car x n); agree_is_valid := agree_is_valid x;
159
     agree_valid_S := agree_valid_S _ x |}.
160
161
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
Proof. by destruct x. Qed.
162
163
Lemma agree_map_compose {A B C} (f : A  B) (g : B  C) (x : agree A) :
  agree_map (g  f) x = agree_map g (agree_map f x).
164
Proof. done. Qed.
165

Robbert Krebbers's avatar
Robbert Krebbers committed
166
Section agree_map.
167
  Context {A B : ofeT} (f : A  B) `{Hf:  n, Proper (dist n ==> dist n) f}.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
  Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
  Instance agree_map_proper : Proper (() ==> ()) (agree_map f) := ne_proper _.
171
172
173
174
  Lemma agree_map_ext (g : A  B) x :
    ( x, f x  g x)  agree_map f x  agree_map g x.
  Proof. by intros Hfg; split; simpl; intros; rewrite ?Hfg. Qed.
  Global Instance agree_map_monotone : CMRAMonotone (agree_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
177
178
179
180
181
    split; first apply _.
    - by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx].
    - intros x y; rewrite !agree_included=> ->.
      split; last done; split; simpl; last tauto.
      by intros (?&?&Hxy); repeat split; intros;
        try apply Hxy; try apply Hf; eauto using @agree_valid_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
  Qed.
End agree_map.
Robbert Krebbers's avatar
Robbert Krebbers committed
184

185
186
187
Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
  CofeMor (agree_map f : agreeC A  agreeC B).
Instance agreeC_map_ne A B n : Proper (dist n ==> dist n) (@agreeC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
188
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
  intros f g Hfg x; split; simpl; intros; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
191
  by apply dist_le with n; try apply Hfg.
Qed.
Ralf Jung's avatar
Ralf Jung committed
192

193
194
195
196
Program Definition agreeRF (F : cFunctor) : rFunctor := {|
  rFunctor_car A B := agreeR (cFunctor_car F A B);
  rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg)
|}.
197
198
199
Next Obligation.
  intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
Qed.
200
201
202
203
204
205
206
207
Next Obligation.
  intros F A B x; simpl. rewrite -{2}(agree_map_id x).
  apply agree_map_ext=>y. by rewrite cFunctor_id.
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose.
  apply agree_map_ext=>y; apply cFunctor_compose.
Qed.
208
209
210
211
212
213
214

Instance agreeRF_contractive F :
  cFunctorContractive F  rFunctorContractive (agreeRF F).
Proof.
  intros ? A1 A2 B1 B2 n ???; simpl.
  by apply agreeC_map_ne, cFunctor_contractive.
Qed.