option.v 8.39 KB
Newer Older
1
From algebra Require Export cmra.
2
From algebra Require Import functor 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
13
14
    (c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
  {| chain_car n := from_option x (c n) |}.
Next Obligation.
15
16
17
  intros c x ? n [|i] ?; [omega|]; simpl.
  destruct (c 1) eqn:?; simplify_equality'.
  by feed inversion (chain_cauchy c n (S i)).
18
Qed.
19
Instance option_compl : Compl (option A) := λ c,
20
21
22
  match Some_dec (c 1) with
  | 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
32
    + by intros [x|]; constructor.
    + by destruct 1; constructor.
    + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
33
34
  - by inversion_clear 1; constructor; apply dist_S.
  - intros c n; unfold compl, option_compl.
35
    destruct (Some_dec (c 1)) as [[x Hx]|].
36
37
    { assert (is_Some (c (S n))) as [y Hy].
      { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. }
38
      rewrite Hy; constructor.
39
40
41
      by rewrite (conv_compl (option_chain c x Hx) n) /= Hy. }
    feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence.
    constructor.
42
Qed.
43
44
Canonical Structure optionC := CofeT option_cofe_mixin.
Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
45
Proof. by constructor. Qed.
46
Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
Robbert Krebbers's avatar
Robbert Krebbers committed
47
Proof. inversion_clear 1; split; eauto. Qed.
48
Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
Robbert Krebbers's avatar
Robbert Krebbers committed
49
Proof. by inversion_clear 1. Qed.
50
Global Instance None_timeless : Timeless (@None A).
51
Proof. inversion_clear 1; constructor. Qed.
52
Global Instance Some_timeless x : Timeless x  Timeless (Some x).
53
Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
54
55
Global Instance option_timeless `{! a : A, Timeless a} (mx : option A) : Timeless mx.
Proof. destruct mx; auto with typeclass_instances. Qed.
56
57
58
59
End cofe.

Arguments optionC : clear implicits.

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

Instance option_validN : ValidN (option A) := λ n mx,
65
  match mx with Some x => {n} x | None => True end.
66
Global Instance option_empty : Empty (option A) := None.
67
68
69
Instance option_unit : Unit (option A) := fmap unit.
Instance option_op : Op (option A) := union_with (λ x y, Some (x  y)).
Instance option_minus : Minus (option A) :=
70
  difference_with (λ x y, Some (x  y)).
71
Lemma option_includedN n (mx my : option A) :
72
  mx {n} my  mx = None   x y, mx = Some x  my = Some y  x {n} y.
73
74
Proof.
  split.
75
  - intros [mz Hmz].
76
77
78
    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_ands; auto;
79
      cofe_subst; eauto using cmra_includedN_l.
80
  - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
81
82
    by exists (Some z); constructor.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
84
85
86
Lemma None_includedN n (mx : option A) : None {n} mx.
Proof. rewrite option_includedN; auto. Qed.
Lemma Some_Some_includedN n (x y : A) : x {n} y  Some x {n} Some y.
Proof. rewrite option_includedN; eauto 10. Qed.
87
Definition Some_op a b : Some (a  b) = Some a  Some b := eq_refl.
Robbert Krebbers's avatar
Robbert Krebbers committed
88

89
Definition option_cmra_mixin  : CMRAMixin (option A).
90
91
Proof.
  split.
92
93
94
95
96
97
98
99
100
101
  - by intros n [x|]; destruct 1; constructor; cofe_subst.
  - by destruct 1; constructor; cofe_subst.
  - by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
  - by destruct 1; inversion_clear 1; constructor; cofe_subst.
  - 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.
  - by intros [x|]; constructor; rewrite cmra_unit_l.
  - by intros [x|]; constructor; rewrite cmra_unit_idemp.
  - intros n mx my; rewrite !option_includedN;intros [->|(x&y&->&->&?)]; auto.
102
    right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
103
  - intros n [x|] [y|]; rewrite /validN /option_validN /=;
104
      eauto using cmra_validN_op_l.
105
  - intros n mx my; rewrite option_includedN.
106
    intros [->|(x&y&->&->&?)]; [by destruct my|].
107
108
    by constructor; apply cmra_op_minus.
Qed.
109
Definition option_cmra_extend_mixin : CMRAExtendMixin (option A).
110
Proof.
111
  intros n mx my1 my2.
112
113
  destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
    try (by exfalso; inversion Hx'; auto).
114
  - destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
115
116
    { by inversion_clear Hx'. }
    by exists (Some z1, Some z2); repeat constructor.
117
118
119
  - by exists (Some x,None); inversion Hx'; repeat constructor.
  - by exists (None,Some x); inversion Hx'; repeat constructor.
  - exists (None,None); repeat constructor.
120
Qed.
121
122
Canonical Structure optionRA :=
  CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin.
123
124
Global Instance option_cmra_identity : CMRAIdentity optionRA.
Proof. split. done. by intros []. by inversion_clear 1. Qed.
125

126
(** Misc *)
127
128
129
130
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.
131
Lemma option_op_positive_dist_l n mx my : mx  my {n} None  mx {n} None.
132
Proof. by destruct mx, my; inversion_clear 1. Qed.
133
Lemma option_op_positive_dist_r n mx my : mx  my {n} None  my {n} None.
134
135
Proof. by destruct mx, my; inversion_clear 1. Qed.

136
137
138
139
140
141
142
143
144
145
146
(** Internalized properties *)
Lemma option_equivI {M} (x y : option A) :
  (x  y)%I  (match x, y with
               | Some a, Some b => a  b | None, None => True | _, _ => False
               end : uPred M)%I.
Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
Lemma option_validI {M} (x : option A) :
  ( x)%I  (match x with Some a =>  a | None => True end : uPred M)%I.
Proof. by destruct x. Qed.

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

170
171
172
173
(** 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.
174
175
Instance option_fmap_cmra_monotone {A B : cmraT} (f: A  B) `{!CMRAMonotone f} :
  CMRAMonotone (fmap f : option A  option B).
176
177
Proof.
  split.
178
  - intros n mx my; rewrite !option_includedN.
179
    intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @includedN_preserving.
180
  - by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
181
Qed.
182
183
184
185
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
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200

Program Definition optionF (Σ : iFunctor) : iFunctor := {|
  ifunctor_car := optionRA  Σ; ifunctor_map A B := optionC_map  ifunctor_map Σ
|}.
Next Obligation.
  by intros Σ A B n f g Hfg; apply optionC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
  intros Σ A x. rewrite /= -{2}(option_fmap_id x).
  apply option_fmap_setoid_ext=>y; apply ifunctor_map_id.
Qed.
Next Obligation.
  intros Σ A B C f g x. rewrite /= -option_fmap_compose.
  apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
Qed.