frac.v 7.89 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
Local Arguments op _ _ !_ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6 7
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.

Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10 11 12
Inductive frac A := Frac { frac_perm : Qp ; frac_car : A  }.
Add Printing Constructor frac.
Arguments Frac {_} _ _.
Arguments frac_perm {_} _.
Arguments frac_car {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14 15 16 17 18 19 20
Instance: Params (@Frac) 2.

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

(* Cofe *)
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22 23 24
Instance frac_equiv : Equiv (frac A) := λ x y,
  frac_perm x = frac_perm y  frac_car x  frac_car y.
Instance frac_dist : Dist (frac A) := λ n x y,
  frac_perm x = frac_perm y  frac_car x {n} frac_car y.
Robbert Krebbers's avatar
Robbert Krebbers committed
25 26 27 28 29 30

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).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Proof. by destruct 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Global Instance Frac_dist_inj n : Inj2 (=) (dist n) (dist n) (@Frac A).
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34 35 36 37 38 39 40 41 42 43 44 45
Proof. by destruct 1. Qed.

Global Instance frac_perm_ne n : Proper (dist n ==> (=)) (@frac_perm A).
Proof. by destruct 1. Qed.
Global Instance frac_car_ne n : Proper (dist n ==> dist n) (@frac_car A).
Proof. by destruct 1. Qed.
Global Instance frac_perm_proper : Proper (() ==> (=)) (@frac_perm A).
Proof. by destruct 1. Qed.
Global Instance frac_car_proper : Proper (() ==> ()) (@frac_car A).
Proof. by destruct 1. Qed.

Program Definition frac_chain (c : chain (frac A)) : chain A :=
  {| chain_car n := match c n return _ with Frac _ b => b end |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
  intros c n i ?; simpl. destruct (c 0) eqn:?; simplify_eq/=.
48
  by feed inversion (chain_cauchy c n i).
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50
Qed.
Instance frac_compl : Compl (frac A) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  Frac (frac_perm (c 0)) (compl (frac_chain c)).
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54 55 56 57 58 59
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
    + by intros [q a]; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62 63
    + by destruct 1; constructor.
    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
  - by inversion_clear 1; constructor; done || apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66
  - intros n c; constructor; simpl.
    + destruct (chain_cauchy c 0 n); auto with lia.
    + apply (conv_compl n (frac_chain c)).
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Qed.
68
Canonical Structure fracC : cofeT := CofeT (frac A) frac_cofe_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof. intros ? [??] [??] [??]; f_equal; done || by apply leibniz_equiv. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
73 74 75 76 77 78 79 80 81

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

Arguments fracC : clear implicits.

(* Functor on COFEs *)
Definition frac_map {A B} (f : A  B) (x : frac A) : frac B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  match x with Frac q a => Frac q (f a) end.
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85 86 87 88 89 90 91
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof. destruct x; constructor; simpl; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94
Instance frac_map_cmra_ne {A B : cofeT} n :
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@frac_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
95
Proof. intros f f' Hf [??] [??] [??]; constructor; by try apply Hf. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
96 97 98 99 100 101 102 103 104 105 106
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.

Instance frac_valid : Valid (frac A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
107 108
  (frac_perm x  1)%Qc   frac_car x.
Global Arguments frac_valid !_/.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Instance frac_validN : ValidN (frac A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111 112
  (frac_perm x  1)%Qc  {n} frac_car x.
Global Arguments frac_validN _ !_/.
Instance frac_pcore : PCore (frac A) := λ _, None.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Instance frac_op : Op (frac A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115
  Frac (frac_perm x + frac_perm y) (frac_car x  frac_car y).
Global Arguments frac_op !_ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
116 117 118 119 120 121

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.
Robbert Krebbers's avatar
Robbert Krebbers committed
122 123 124 125 126 127 128 129
  split; try discriminate.
  - intros n [??] [??] [??] [??]; constructor; by cofe_subst. 
  - intros ? [??] [??] [??] [??]; split; by cofe_subst.
  - intros [??]; 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 n [q1 a1] [q2 a2]; destruct 1; split; eauto using cmra_validN_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
130 131
    trans (q1 + q2)%Qp; simpl; last done.
    rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak.
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133 134 135 136
  - intros n [q a] y1 y2 Hx 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Canonical Structure fracR := CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin.
139

140
Global Instance frac_cmra_discrete : CMRADiscrete A  CMRADiscrete fracR.
Robbert Krebbers's avatar
Robbert Krebbers committed
141 142
Proof.
  split; first apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
  intros [q a]; destruct 1; split; auto using cmra_discrete_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
144 145 146 147
Qed.

(** Internalized properties *)
Lemma frac_equivI {M} (x y : frac A) :
148
  x  y  (frac_perm x = frac_perm y  frac_car x  frac_car y : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
149
Proof. by uPred.unseal. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Lemma frac_validI {M} (x : frac A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152
   x  ( (frac_perm x  1)%Qc   frac_car x : uPred M).
Proof. by uPred.unseal. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
153

154 155 156
(** Exclusive *)
Global Instance frac_full_exclusive a : Exclusive (Frac 1 a).
Proof.
157
  move => [[??]?][/Qcle_not_lt[]]; simpl in *.
158 159 160
  by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
161 162
(** ** Local updates *)
Global Instance frac_local_update `{!LocalUpdate Lv L} :
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  LocalUpdate (λ x, Lv (frac_car x)) (frac_map L).
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  split; first apply _. intros n [p a] [q b]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
166 167 168 169 170 171
  intros ? [??]; constructor; [done|by apply (local_updateN L)].
Qed.

(** Updates *)
Lemma frac_update (a1 a2 : A) p : a1 ~~> a2  Frac p a1 ~~> Frac p a2.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173
  intros Ha n mz [??]; split; first by destruct mz.
  pose proof (Ha n (frac_car <$> mz)); destruct mz; naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
174 175 176
Qed.
End cmra.

177
Arguments fracR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
178 179 180 181 182 183

(* Functor *)
Instance frac_map_cmra_monotone {A B : cmraT} (f : A  B) :
  CMRAMonotone f  CMRAMonotone (frac_map f).
Proof.
  split; try apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
  - intros n [p a]; destruct 1; split; simpl in *; auto using validN_preserving.
  - intros [q1 a1] [q2 a2] [[q3 a3] [??]]; setoid_subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
186 187 188 189 190
    destruct (included_preserving f a1 (a1  a3)) as [b ?].
    { by apply cmra_included_l. }
    by exists (Frac q3 b); constructor.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
191 192 193
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
194
|}.
195 196 197
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
198
Next Obligation.
199 200
  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
201 202
Qed.
Next Obligation.
203 204
  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
205
Qed.
206

Robbert Krebbers's avatar
Robbert Krebbers committed
207 208
Instance fracRF_contractive F :
  rFunctorContractive F  rFunctorContractive (fracRF F).
209 210 211
Proof.
  by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive.
Qed.