frac.v 10.2 KB
Newer Older
1
From Coq.QArith Require Import Qcanon.
2
3
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.
6
Local Arguments div _ _ !_ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

Inductive frac (A : Type) :=
  | Frac : Qp  A  frac A
  | FracUnit : frac A.
Arguments Frac {_} _ _.
Arguments FracUnit {_}.
Instance maybe_Frac {A} : Maybe2 (@Frac A) := λ x,
  match x with Frac q a => Some (q,a) | _ => None end.
Instance: Params (@Frac) 2.

Section cofe.
Context {A : cofeT}.
Implicit Types a b : A.
Implicit Types x y : frac A.

(* Cofe *)
Inductive frac_equiv : Equiv (frac A) :=
  | Frac_equiv q1 q2 a b : q1 = q2  a  b  Frac q1 a  Frac q2 b
  | FracUnit_equiv : FracUnit  FracUnit.
Existing Instance frac_equiv.
Inductive frac_dist : Dist (frac A) :=
  | Frac_dist q1 q2 a b n : q1 = q2  a {n} b  Frac q1 a {n} Frac q2 b
  | FracUnit_dist n : FracUnit {n} FracUnit.
Existing Instance frac_dist.

Global Instance Frac_ne q n : Proper (dist n ==> dist n) (@Frac A q).
Proof. by constructor. Qed.
Global Instance Frac_proper q : Proper (() ==> ()) (@Frac A q).
Proof. by constructor. Qed.
Global Instance Frac_inj : Inj2 (=) () () (@Frac A).
Proof. by inversion_clear 1. Qed.
Global Instance Frac_dist_inj n : Inj2 (=) (dist n) (dist n) (@Frac A).
Proof. by inversion_clear 1. Qed.

Program Definition frac_chain (c : chain (frac A)) (q : Qp) (a : A)
42
    (H : maybe2 Frac (c 0) = Some (q,a)) : chain A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
  {| chain_car n := match c n return _ with Frac _ b => b | _ => a end |}.
Next Obligation.
45
46
47
  intros c q a ? n i ?; simpl.
  destruct (c 0) eqn:?; simplify_eq/=.
  by feed inversion (chain_cauchy c n i).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
Qed.
Instance frac_compl : Compl (frac A) := λ c,
50
  match Some_dec (maybe2 Frac (c 0)) with
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  | inleft (exist (q,a) H) => Frac q (compl (frac_chain c q a H))
52
  | inright _ => c 0
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
56
57
58
59
60
61
62
63
64
65
66
  end.
Definition frac_cofe_mixin : CofeMixin (frac A).
Proof.
  split.
  - intros mx my; split.
    + by destruct 1; subst; constructor; try apply equiv_dist.
    + intros Hxy; feed inversion (Hxy 0); subst; constructor; try done.
      apply equiv_dist=> n; by feed inversion (Hxy n).
  - intros n; split.
    + by intros [q a|]; constructor.
    + by destruct 1; constructor.
    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
  - by inversion_clear 1; constructor; done || apply dist_S.
  - intros n c; unfold compl, frac_compl.
67
68
69
70
    destruct (Some_dec (maybe2 Frac (c 0))) as [[[q a] Hx]|].
    { assert (c 0 = Frac q a) by (by destruct (c 0); simplify_eq/=).
      assert ( b, c n = Frac q b) as [y Hy].
      { feed inversion (chain_cauchy c 0 n);
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
73
          eauto with lia congruence f_equal. }
      rewrite Hy; constructor; auto.
      by rewrite (conv_compl n (frac_chain c q a Hx)) /= Hy. }
74
75
    feed inversion (chain_cauchy c 0 n); first lia;
       constructor; destruct (c 0); simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
Qed.
Canonical Structure fracC : cofeT := CofeT frac_cofe_mixin.
Global Instance frac_discrete : Discrete A  Discrete fracC.
Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
Global Instance frac_leibniz : LeibnizEquiv A  LeibnizEquiv (frac A).
Proof. by destruct 2; f_equal; done || apply leibniz_equiv. Qed.

Global Instance Frac_timeless q (a : A) : Timeless a  Timeless (Frac q a).
Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
Global Instance FracUnit_timeless : Timeless (@FracUnit A).
Proof. by inversion_clear 1; constructor. Qed.
End cofe.

Arguments fracC : clear implicits.

(* Functor on COFEs *)
Definition frac_map {A B} (f : A  B) (x : frac A) : frac B :=
  match x with
  | Frac q a => Frac q (f a) | FracUnit => FracUnit
  end.
Instance: Params (@frac_map) 2.

Lemma frac_map_id {A} (x : frac A) : frac_map id x = x.
Proof. by destruct x. Qed.
Lemma frac_map_compose {A B C} (f : A  B) (g : B  C) (x : frac A) :
  frac_map (g  f) x = frac_map g (frac_map f x).
Proof. by destruct x. Qed.
Lemma frac_map_ext {A B : cofeT} (f g : A  B) x :
  ( x, f x  g x)  frac_map f x  frac_map g x.
Proof. by destruct x; constructor. Qed.
Instance frac_map_cmra_ne {A B : cofeT} n :
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@frac_map A B).
Proof. intros f f' Hf; destruct 1; constructor; by try apply Hf. Qed.
Definition fracC_map {A B} (f : A -n> B) : fracC A -n> fracC B :=
  CofeMor (frac_map f).
Instance fracC_map_ne A B n : Proper (dist n ==> dist n) (@fracC_map A B).
Proof. intros f f' Hf []; constructor; by try apply Hf. Qed.

Section cmra.
Context {A : cmraT}.
Implicit Types a b : A.
Implicit Types x y : frac A.

(* CMRA *)
Instance frac_valid : Valid (frac A) := λ x,
  match x with Frac q a => (q  1)%Qc   a | FracUnit => True end.
Instance frac_validN : ValidN (frac A) := λ n x,
  match x with Frac q a => (q  1)%Qc  {n} a | FracUnit => True end.
Global Instance frac_empty : Empty (frac A) := FracUnit.
Ralf Jung's avatar
Ralf Jung committed
125
Instance frac_core : Core (frac A) := λ _, .
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
128
129
130
131
Instance frac_op : Op (frac A) := λ x y,
  match x, y with
  | Frac q1 a, Frac q2 b => Frac (q1 + q2) (a  b)
  | Frac q a, FracUnit | FracUnit, Frac q a => Frac q a
  | FracUnit, FracUnit => FracUnit
  end.
132
Instance frac_div : Div (frac A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
135
  match x, y with
  | _, FracUnit => x
  | Frac q1 a, Frac q2 b =>
136
     match q1 - q2 with Some q => Frac q (a ÷ b) | None => FracUnit end%Qp
Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
  | FracUnit, _ => FracUnit
  end.

Lemma Frac_op q1 q2 a b : Frac q1 a  Frac q2 b = Frac (q1 + q2) (a  b).
Proof. done. Qed.

Definition frac_cmra_mixin : CMRAMixin (frac A).
Proof.
  split.
  - intros n []; destruct 1; constructor; by cofe_subst. 
  - constructor.
  - do 2 destruct 1; split; by cofe_subst.
  - do 2 destruct 1; simplify_eq/=; try case_match; constructor; by cofe_subst.
  - intros [q a|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
  - intros n [q a|]; destruct 1; split; auto using cmra_validN_S.
  - intros [q1 a1|] [q2 a2|] [q3 a3|]; constructor; by rewrite ?assoc.
  - intros [q1 a1|] [q2 a2|]; constructor; by rewrite 1?comm ?[(q1+_)%Qp]comm.
  - intros []; by constructor.
  - done.
  - by exists FracUnit.
  - intros n [q1 a1|] [q2 a2|]; destruct 1; split; eauto using cmra_validN_op_l.
    trans (q1 + q2)%Qp; simpl; last done.
    rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak.
  - intros [q1 a1|] [q2 a2|] [[q3 a3|] Hx];
      inversion_clear Hx; simplify_eq/=; auto.
162
    + rewrite Qp_op_minus. by constructor; [|apply cmra_op_div; exists a3].
Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
165
166
167
168
169
170
171
172
173
    + rewrite Qp_minus_diag. by constructor.
  - intros n [q a|] y1 y2 Hx Hx'; last first.
    { by exists (, ); destruct y1, y2; inversion_clear Hx'. }
    destruct Hx, y1 as [q1 b1|], y2 as [q2 b2|].
    + apply (inj2 Frac) in Hx'; destruct Hx' as [-> ?].
      destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto.
      exists (Frac q1 z1,Frac q2 z2); by repeat constructor.
    + exists (Frac q a, ); inversion_clear Hx'; by repeat constructor.
    + exists (, Frac q a); inversion_clear Hx'; by repeat constructor.
    + exfalso; inversion_clear Hx'.
Qed.
174
Canonical Structure fracR : cmraT := CMRAT frac_cofe_mixin frac_cmra_mixin.
Ralf Jung's avatar
Ralf Jung committed
175
Global Instance frac_cmra_unit : CMRAUnit fracR.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Proof. split. done. by intros []. apply _. Qed.
177
Global Instance frac_cmra_discrete : CMRADiscrete A  CMRADiscrete fracR.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
Proof.
  split; first apply _.
  intros [q a|]; destruct 1; split; auto using cmra_discrete_valid.
Qed.

Lemma frac_validN_inv_l n y a : {n} (Frac 1 a  y)  y = .
Proof.
  destruct y as [q b|]; [|done]=> -[Hq ?]; destruct (Qcle_not_lt _ _ Hq).
  by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
Qed.
Lemma frac_valid_inv_l y a :  (Frac 1 a  y)  y = .
Proof. intros. by apply frac_validN_inv_l with 0 a, cmra_valid_validN. Qed.

(** Internalized properties *)
Lemma frac_equivI {M} (x y : frac A) :
193
  (x  y)  (match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
196
               | Frac q1 a, Frac q2 b => q1 = q2  a  b
               | FracUnit, FracUnit => True
               | _, _ => False
197
               end : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
200
201
202
Proof.
  uPred.unseal; do 2 split; first by destruct 1.
  by destruct x, y; destruct 1; try constructor.
Qed.
Lemma frac_validI {M} (x : frac A) :
203
  ( x)  (if x is Frac q a then  (q  1)%Qc   a else True : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
Proof. uPred.unseal. by destruct x. Qed.

(** ** Local updates *)
Global Instance frac_local_update_full p a :
  LocalUpdate (λ x, if x is Frac q _ then q = 1%Qp else False) (λ _, Frac p a).
Proof.
  split; first by intros ???.
  by intros n [q b|] y; [|done]=> -> /frac_validN_inv_l ->.
Qed.
Global Instance frac_local_update `{!LocalUpdate Lv L} :
  LocalUpdate (λ x, if x is Frac _ a then Lv a else False) (frac_map L).
Proof.
  split; first apply _. intros n [p a|] [q b|]; simpl; try done.
  intros ? [??]; constructor; [done|by apply (local_updateN L)].
Qed.

(** Updates *)
Lemma frac_update_full (a1 a2 : A) :  a2  Frac 1 a1 ~~> Frac 1 a2.
Proof.
  move=> ? n y /frac_validN_inv_l ->. split. done. by apply cmra_valid_validN.
Qed.
Lemma frac_update (a1 a2 : A) p : a1 ~~> a2  Frac p a1 ~~> Frac p a2.
Proof.
  intros Ha n [q b|] [??]; split; auto.
Ralf Jung's avatar
Ralf Jung committed
228
  apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
231
Qed.
End cmra.

232
Arguments fracR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
235
236
237
238
239
240

(* Functor *)
Instance frac_map_cmra_monotone {A B : cmraT} (f : A  B) :
  CMRAMonotone f  CMRAMonotone (frac_map f).
Proof.
  split; try apply _.
  - intros n [p a|]; destruct 1; split; auto using validN_preserving.
  - intros [q1 a1|] [q2 a2|] [[q3 a3|] Hx];
Ralf Jung's avatar
Ralf Jung committed
241
      inversion Hx; setoid_subst; try apply: cmra_unit_least; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
243
244
245
246
    destruct (included_preserving f a1 (a1  a3)) as [b ?].
    { by apply cmra_included_l. }
    by exists (Frac q3 b); constructor.
Qed.

247
248
249
Program Definition fracRF (F : rFunctor) : rFunctor := {|
  rFunctor_car A B := fracR (rFunctor_car F A B);
  rFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg)
Robbert Krebbers's avatar
Robbert Krebbers committed
250
|}.
251
252
253
Next Obligation.
  by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_ne.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
Next Obligation.
255
256
  intros F A B x. rewrite /= -{2}(frac_map_id x).
  apply frac_map_ext=>y; apply rFunctor_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
258
Qed.
Next Obligation.
259
260
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -frac_map_compose.
  apply frac_map_ext=>y; apply rFunctor_compose.
Robbert Krebbers's avatar
Robbert Krebbers committed
261
Qed.
262
263
264
265
266
267

Instance fracRF_contractive F :
  rFunctorContractive F  rFunctorContractive (fracRF F).
Proof.
  by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive.
Qed.