frac.v 9.71 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 6 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
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.

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)
41
    (H : maybe2 Frac (c 0) = Some (q,a)) : chain A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
  {| chain_car n := match c n return _ with Frac _ b => b | _ => a end |}.
Next Obligation.
44 45 46
  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
47 48
Qed.
Instance frac_compl : Compl (frac A) := λ c,
49
  match Some_dec (maybe2 Frac (c 0)) with
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  | inleft (exist (q,a) H) => Frac q (compl (frac_chain c q a H))
51
  | inright _ => c 0
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54 55 56 57 58 59 60 61 62 63 64 65
  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.
66 67 68 69
    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
70 71 72
          eauto with lia congruence f_equal. }
      rewrite Hy; constructor; auto.
      by rewrite (conv_compl n (frac_chain c q a Hx)) /= Hy. }
73 74
    feed inversion (chain_cauchy c 0 n); first lia;
       constructor; destruct (c 0); simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
75 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
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
124
Instance frac_core : Core (frac A) := λ _, .
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
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.

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.
  - 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 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.
161
Canonical Structure fracR : cmraT := CMRAT frac_cofe_mixin frac_cmra_mixin.
Ralf Jung's avatar
Ralf Jung committed
162
Global Instance frac_cmra_unit : CMRAUnit fracR.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Proof. split. done. by intros []. apply _. Qed.
164
Global Instance frac_cmra_discrete : CMRADiscrete A  CMRADiscrete fracR.
Robbert Krebbers's avatar
Robbert Krebbers committed
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
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) :
180
  (x  y)  (match x, y with
Robbert Krebbers's avatar
Robbert Krebbers committed
181 182 183
               | Frac q1 a, Frac q2 b => q1 = q2  a  b
               | FracUnit, FracUnit => True
               | _, _ => False
184
               end : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
185 186 187 188 189
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) :
190
  ( x)  (if x is Frac q a then  (q  1)%Qc   a else True : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
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
215
  apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
216 217 218
Qed.
End cmra.

219
Arguments fracR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
220 221 222 223 224 225 226 227

(* 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
228
      inversion Hx; setoid_subst; try apply: cmra_unit_least; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230 231 232 233
    destruct (included_preserving f a1 (a1  a3)) as [b ?].
    { by apply cmra_included_l. }
    by exists (Frac q3 b); constructor.
Qed.

234 235 236
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
237
|}.
238 239 240
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
241
Next Obligation.
242 243
  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
244 245
Qed.
Next Obligation.
246 247
  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
248
Qed.
249 250 251 252 253 254

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.