option.v 9.5 KB
Newer Older
1 2
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
3 4

(* COFE *)
5 6 7
Section cofe.
Context {A : cofeT}.
Inductive option_dist : Dist (option A) :=
8 9
  | Some_dist n x y : x {n} y  Some x {n} Some y
  | None_dist n : None {n} None.
10
Existing Instance option_dist.
11
Program Definition option_chain
12
    (c : chain (option A)) (x : A) (H : c 0 = Some x) : chain A :=
13 14
  {| chain_car n := from_option x (c n) |}.
Next Obligation.
15 16 17
  intros c x ? n i ?; simpl.
  destruct (c 0) eqn:?; simplify_eq/=.
  by feed inversion (chain_cauchy c n i).
18
Qed.
19
Instance option_compl : Compl (option A) := λ c,
20
  match Some_dec (c 0) with
21 22
  | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None
  end.
23
Definition option_cofe_mixin : CofeMixin (option A).
24 25
Proof.
  split.
26
  - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
27 28
    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
    by intros n; feed inversion (Hxy n).
29
  - intros n; split.
30 31
    + by intros [x|]; constructor.
    + by destruct 1; constructor.
32
    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
33
  - by inversion_clear 1; constructor; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
  - intros n c; unfold compl, option_compl.
35 36 37
    destruct (Some_dec (c 0)) as [[x Hx]|].
    { assert (is_Some (c n)) as [y Hy].
      { feed inversion (chain_cauchy c 0 n); eauto with lia congruence. }
38
      rewrite Hy; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
      by rewrite (conv_compl n (option_chain c x Hx)) /= Hy. }
40
    feed inversion (chain_cauchy c 0 n); eauto with lia congruence.
41
    constructor.
42
Qed.
43
Canonical Structure optionC := CofeT option_cofe_mixin.
44 45 46
Global Instance option_discrete : Discrete A  Discrete optionC.
Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.

47
Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
48
Proof. by constructor. Qed.
49
Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
Robbert Krebbers's avatar
Robbert Krebbers committed
50
Proof. inversion_clear 1; split; eauto. Qed.
51
Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Proof. by inversion_clear 1. Qed.
53
Global Instance None_timeless : Timeless (@None A).
54
Proof. inversion_clear 1; constructor. Qed.
55
Global Instance Some_timeless x : Timeless x  Timeless (Some x).
56
Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
57 58 59 60
End cofe.

Arguments optionC : clear implicits.

61
(* CMRA *)
62 63 64
Section cmra.
Context {A : cmraT}.

65 66
Instance option_valid : Valid (option A) := λ mx,
  match mx with Some x =>  x | None => True end.
67
Instance option_validN : ValidN (option A) := λ n mx,
68
  match mx with Some x => {n} x | None => True end.
69
Global Instance option_empty : Empty (option A) := None.
Ralf Jung's avatar
Ralf Jung committed
70
Instance option_core : Core (option A) := fmap core.
71
Instance option_op : Op (option A) := union_with (λ x y, Some (x  y)).
Robbert Krebbers's avatar
Robbert Krebbers committed
72

Robbert Krebbers's avatar
Robbert Krebbers committed
73
Definition Some_valid a :  Some a   a := reflexivity _.
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75
Definition Some_op a b : Some (a  b) = Some a  Some b := eq_refl.

Robbert Krebbers's avatar
Robbert Krebbers committed
76 77 78 79 80 81 82 83 84 85 86 87
Lemma option_included (mx my : option A) :
  mx  my  mx = None   x y, mx = Some x  my = Some y  x  y.
Proof.
  split.
  - intros [mz Hmz].
    destruct mx as [x|]; [right|by left].
    destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
    destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
      setoid_subst; eauto using cmra_included_l.
  - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
    by exists (Some z); constructor.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
88

89
Definition option_cmra_mixin  : CMRAMixin (option A).
90 91
Proof.
  split.
92 93 94
  - by intros n [x|]; destruct 1; constructor; cofe_subst.
  - by destruct 1; constructor; cofe_subst.
  - by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
95
  - intros [x|]; [apply cmra_valid_validN|done].
96 97 98
  - intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
  - intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
  - intros [x|] [y|]; constructor; rewrite 1?comm; auto.
Ralf Jung's avatar
Ralf Jung committed
99 100
  - by intros [x|]; constructor; rewrite cmra_core_l.
  - by intros [x|]; constructor; rewrite cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  - intros mx my; rewrite !option_included ;intros [->|(x&y&->&->&?)]; auto.
Ralf Jung's avatar
Ralf Jung committed
102
    right; exists (core x), (core y); eauto using cmra_core_preserving.
103
  - intros n [x|] [y|]; rewrite /validN /option_validN /=;
104
      eauto using cmra_validN_op_l.
105 106 107 108 109 110 111 112 113
  - intros n mx my1 my2.
    destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
      try (by exfalso; inversion Hx'; auto).
    + destruct (cmra_extend n x y1 y2) as ([z1 z2]&?&?&?); auto.
      { by inversion_clear Hx'. }
      by exists (Some z1, Some z2); repeat constructor.
    + by exists (Some x,None); inversion Hx'; repeat constructor.
    + by exists (None,Some x); inversion Hx'; repeat constructor.
    + exists (None,None); repeat constructor.
114
Qed.
115
Canonical Structure optionR := CMRAT option_cofe_mixin option_cmra_mixin.
Ralf Jung's avatar
Ralf Jung committed
116
Global Instance option_cmra_unit : CMRAUnit optionR.
117
Proof. split. done. by intros []. by inversion_clear 1. Qed.
118
Global Instance option_cmra_discrete : CMRADiscrete A  CMRADiscrete optionR.
119
Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
120

121
(** Misc *)
Robbert Krebbers's avatar
Robbert Krebbers committed
122 123
Global Instance Some_cmra_monotone : CMRAMonotone Some.
Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
124 125 126 127
Lemma op_is_Some mx my : is_Some (mx  my)  is_Some mx  is_Some my.
Proof.
  destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
Qed.
128
Lemma option_op_positive_dist_l n mx my : mx  my {n} None  mx {n} None.
129
Proof. by destruct mx, my; inversion_clear 1. Qed.
130
Lemma option_op_positive_dist_r n mx my : mx  my {n} None  my {n} None.
131 132
Proof. by destruct mx, my; inversion_clear 1. Qed.

133 134 135 136 137 138
Global Instance Some_persistent (x : A) : Persistent x  Persistent (Some x).
Proof. by constructor. Qed.
Global Instance option_persistent (mx : option A) :
  ( x : A, Persistent x)  Persistent mx.
Proof. intros. destruct mx. apply _. apply cmra_unit_persistent. Qed.

139 140
(** Internalized properties *)
Lemma option_equivI {M} (x y : option A) :
141
  (x  y)  (match x, y with
142
               | Some a, Some b => a  b | None, None => True | _, _ => False
143
               end : uPred M).
144 145 146
Proof.
  uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
147
Lemma option_validI {M} (x : option A) :
148
  ( x)  (match x with Some a =>  a | None => True end : uPred M).
149
Proof. uPred.unseal. by destruct x. Qed.
150 151

(** Updates *)
152
Lemma option_updateP (P : A  Prop) (Q : option A  Prop) x :
153
  x ~~>: P  ( y, P y  Q (Some y))  Some x ~~>: Q.
154
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156
  intros Hx Hy n [y|] ?.
  { destruct (Hx n y) as (y'&?&?); auto. exists (Some y'); auto. }
Ralf Jung's avatar
Ralf Jung committed
157 158
  destruct (Hx n (core x)) as (y'&?&?); rewrite ?cmra_core_r; auto.
  by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
159
Qed.
160
Lemma option_updateP' (P : A  Prop) x :
161
  x ~~>: P  Some x ~~>: λ y, default False y P.
162
Proof. eauto using option_updateP. Qed.
163
Lemma option_update x y : x ~~> y  Some x ~~> Some y.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof.
165
  rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Qed.
Ralf Jung's avatar
Ralf Jung committed
167
Lemma option_update_None `{Empty A, !CMRAUnit A} :  ~~> Some .
168
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  intros n [x|] ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id;
Ralf Jung's avatar
Ralf Jung committed
170
    auto using cmra_unit_validN.
171
Qed.
172
End cmra.
173
Arguments optionR : clear implicits.
174

175 176 177 178
(** Functor *)
Instance option_fmap_ne {A B : cofeT} (f : A  B) n:
  Proper (dist n ==> dist n) f  Proper (dist n==>dist n) (fmap (M:=option) f).
Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
179 180
Instance option_fmap_cmra_monotone {A B : cmraT} (f: A  B) `{!CMRAMonotone f} :
  CMRAMonotone (fmap f : option A  option B).
181
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
  split; first apply _.
183
  - intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f).
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
  - intros mx my; rewrite !option_included.
    intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @included_preserving.
186
Qed.
187 188 189 190
Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
  CofeMor (fmap f : optionC A  optionC B).
Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
191

192 193 194
Program Definition optionCF (F : cFunctor) : cFunctor := {|
  cFunctor_car A B := optionC (cFunctor_car F A B);
  cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg)
Ralf Jung's avatar
Ralf Jung committed
195
|}.
196 197 198
Next Obligation.
  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
Qed.
Ralf Jung's avatar
Ralf Jung committed
199
Next Obligation.
200 201
  intros F A B x. rewrite /= -{2}(option_fmap_id x).
  apply option_fmap_setoid_ext=>y; apply cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
202 203
Qed.
Next Obligation.
204 205 206 207
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
  apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
Qed.

208 209 210 211 212 213
Instance optionCF_contractive F :
  cFunctorContractive F  cFunctorContractive (optionCF F).
Proof.
  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
Qed.

214 215 216 217
Program Definition optionRF (F : rFunctor) : rFunctor := {|
  rFunctor_car A B := optionR (rFunctor_car F A B);
  rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
|}.
218 219 220
Next Obligation.
  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
Qed.
221 222 223 224 225 226 227
Next Obligation.
  intros F A B x. rewrite /= -{2}(option_fmap_id x).
  apply option_fmap_setoid_ext=>y; apply rFunctor_id.
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
  apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
228
Qed.
229 230 231 232 233 234

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