option.v 7.49 KB
Newer Older
1
Require Export algebra.cmra.
2 3

(* COFE *)
4 5 6
Section cofe.
Context {A : cofeT}.
Inductive option_dist : Dist (option A) :=
7 8 9 10
  | option_0_dist (x y : option A) : x ={0}= y
  | Some_dist n x y : x ={n}= y  Some x ={n}= Some y
  | None_dist n : None ={n}= None.
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
  intros c x ? n i ?; simpl; destruct (decide (i = 0)) as [->|].
16 17 18 19
  { by replace n with 0 by lia. }
  feed inversion (chain_cauchy c 1 i); auto with lia congruence.
  feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
Qed.
20
Instance option_compl : Compl (option A) := λ c,
21 22 23
  match Some_dec (c 1) with
  | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None
  end.
24
Definition option_cofe_mixin : CofeMixin (option A).
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
Proof.
  split.
  * intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
    by intros n; feed inversion (Hxy n).
  * intros n; split.
    + by intros [x|]; constructor.
    + by destruct 1; constructor.
    + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
  * by inversion_clear 1; constructor; apply dist_S.
  * constructor.
  * intros c n; unfold compl, option_compl.
    destruct (decide (n = 0)) as [->|]; [constructor|].
    destruct (Some_dec (c 1)) as [[x Hx]|].
    { assert (is_Some (c n)) as [y Hy].
      { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
      rewrite Hy; constructor.
      by rewrite (conv_compl (option_chain c x Hx) n); simpl; rewrite Hy. }
    feed inversion (chain_cauchy c 1 n); auto with lia congruence; constructor.
Qed.
45 46
Canonical Structure optionC := CofeT option_cofe_mixin.
Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
47
Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49 50 51
Global Instance is_Some_ne n : Proper (dist (S n) ==> iff) (@is_Some A).
Proof. inversion_clear 1; split; eauto. Qed.
Global Instance Some_dist_inj : Injective (dist n) (dist n) (@Some A).
Proof. by inversion_clear 1. Qed.
52
Global Instance None_timeless : Timeless (@None A).
53
Proof. inversion_clear 1; constructor. Qed.
54
Global Instance Some_timeless x : Timeless x  Timeless (Some x).
55
Proof. by intros ?; inversion_clear 1; constructor; apply timeless. 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 67 68
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) :=
69
  difference_with (λ x y, Some (x  y)).
70
Lemma option_includedN n (mx my : option A) :
71 72 73 74 75 76 77
  mx {n} my  n = 0  mx = None   x y, mx = Some x  my = Some y  x {n} y.
Proof.
  split.
  * intros [mz Hmz]; destruct n as [|n]; [by left|right].
    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;
78
      cofe_subst; eauto using cmra_includedN_l.
79 80 81 82
  * 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
83 84 85 86 87
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.

88
Definition option_cmra_mixin  : CMRAMixin (option A).
89 90 91 92 93 94
Proof.
  split.
  * by intros n [x|]; destruct 1; constructor;
      repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
  * by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _).
  * destruct 1 as [[?|] [?|]| |]; unfold validN, option_validN; simpl;
95
     intros ?; auto using cmra_validN_0;
96 97 98
     eapply (_ : Proper (dist _ ==> impl) ({_})); eauto.
  * by destruct 1; inversion_clear 1; constructor;
      repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
99 100 101 102 103 104
  * intros [x|]; unfold validN, option_validN; auto using cmra_validN_0.
  * intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
  * intros [x|] [y|] [z|]; constructor; rewrite ?associative; auto.
  * intros [x|] [y|]; constructor; rewrite 1?commutative; auto.
  * by intros [x|]; constructor; rewrite cmra_unit_l.
  * by intros [x|]; constructor; rewrite cmra_unit_idempotent.
105
  * intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto.
106 107 108
    do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
  * intros n [x|] [y|]; rewrite /validN /option_validN /=;
      eauto using cmra_validN_op_l.
109 110 111 112
  * intros n mx my; rewrite option_includedN.
    intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|].
    by constructor; apply cmra_op_minus.
Qed.
113
Definition option_cmra_extend_mixin : CMRAExtendMixin (option A).
114 115 116 117 118 119 120 121 122 123 124 125
Proof.
  intros n mx my1 my2; destruct (decide (n = 0)) as [->|].
  { by exists (mx, None); repeat constructor; destruct mx; constructor. }
  destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
    try (by exfalso; inversion Hx'; auto).
  * destruct (cmra_extend_op 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.
Qed.
126 127 128
Canonical Structure optionRA :=
  CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin.

129 130 131 132 133 134 135 136 137 138
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.
Lemma option_op_positive_dist_l n mx my : mx  my ={n}= None  mx ={n}= None.
Proof. by destruct mx, my; inversion_clear 1. Qed.
Lemma option_op_positive_dist_r n mx my : mx  my ={n}= None  my ={n}= None.
Proof. by destruct mx, my; inversion_clear 1. Qed.

Lemma option_updateP (P : A  Prop) (Q : option A  Prop) x :
139
  x ~~>: P  ( y, P y  Q (Some y))  Some x ~~>: Q.
140 141 142 143 144 145
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.
146
Lemma option_updateP' (P : A  Prop) x :
147
  x ~~>: P  Some x ~~>: λ y, default False y P.
148
Proof. eauto using option_updateP. Qed.
149
Lemma option_update x y : x ~~> y  Some x ~~> Some y.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Proof.
151
  rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Qed.
153 154 155 156
End cmra.

Arguments optionRA : clear implicits.

157 158 159 160
(** 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.
161 162
Instance option_fmap_cmra_monotone {A B : cmraT} (f: A  B) `{!CMRAMonotone f} :
  CMRAMonotone (fmap f : option A  option B).
163 164 165 166
Proof.
  split.
  * intros n mx my; rewrite !option_includedN.
    intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving.
167 168
  * by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
Qed.
169 170 171 172
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.