option.v 9.5 KB
 Robbert Krebbers committed Mar 10, 2016 1 2 ``````From iris.algebra Require Export cmra. From iris.algebra Require Import upred. `````` Robbert Krebbers committed Dec 15, 2015 3 4 `````` (* COFE *) `````` Robbert Krebbers committed Jan 14, 2016 5 6 7 ``````Section cofe. Context {A : cofeT}. Inductive option_dist : Dist (option A) := `````` Ralf Jung committed Feb 10, 2016 8 9 `````` | Some_dist n x y : x ≡{n}≡ y → Some x ≡{n}≡ Some y | None_dist n : None ≡{n}≡ None. `````` Robbert Krebbers committed Dec 15, 2015 10 ``````Existing Instance option_dist. `````` Robbert Krebbers committed Jan 14, 2016 11 ``````Program Definition option_chain `````` Ralf Jung committed Feb 29, 2016 12 `````` (c : chain (option A)) (x : A) (H : c 0 = Some x) : chain A := `````` Robbert Krebbers committed Dec 15, 2015 13 14 `````` {| chain_car n := from_option x (c n) |}. Next Obligation. `````` Ralf Jung committed Feb 29, 2016 15 16 17 `````` intros c x ? n i ?; simpl. destruct (c 0) eqn:?; simplify_eq/=. by feed inversion (chain_cauchy c n i). `````` Robbert Krebbers committed Dec 15, 2015 18 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 19 ``````Instance option_compl : Compl (option A) := λ c, `````` Ralf Jung committed Feb 29, 2016 20 `````` match Some_dec (c 0) with `````` Robbert Krebbers committed Dec 15, 2015 21 22 `````` | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None end. `````` Robbert Krebbers committed Jan 14, 2016 23 ``````Definition option_cofe_mixin : CofeMixin (option A). `````` Robbert Krebbers committed Dec 15, 2015 24 25 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 26 `````` - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|]. `````` Robbert Krebbers committed Dec 15, 2015 27 28 `````` intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist. by intros n; feed inversion (Hxy n). `````` Robbert Krebbers committed Feb 17, 2016 29 `````` - intros n; split. `````` Robbert Krebbers committed Dec 15, 2015 30 31 `````` + by intros [x|]; constructor. + by destruct 1; constructor. `````` Ralf Jung committed Feb 20, 2016 32 `````` + destruct 1; inversion_clear 1; constructor; etrans; eauto. `````` Robbert Krebbers committed Feb 17, 2016 33 `````` - by inversion_clear 1; constructor; apply dist_S. `````` Robbert Krebbers committed Feb 18, 2016 34 `````` - intros n c; unfold compl, option_compl. `````` Ralf Jung committed Feb 29, 2016 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. } `````` Robbert Krebbers committed Dec 15, 2015 38 `````` rewrite Hy; constructor. `````` Robbert Krebbers committed Feb 18, 2016 39 `````` by rewrite (conv_compl n (option_chain c x Hx)) /= Hy. } `````` Ralf Jung committed Feb 29, 2016 40 `````` feed inversion (chain_cauchy c 0 n); eauto with lia congruence. `````` Robbert Krebbers committed Feb 10, 2016 41 `````` constructor. `````` Robbert Krebbers committed Dec 15, 2015 42 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 43 ``````Canonical Structure optionC := CofeT option_cofe_mixin. `````` Robbert Krebbers committed Feb 24, 2016 44 45 46 ``````Global Instance option_discrete : Discrete A → Discrete optionC. Proof. inversion_clear 2; constructor; by apply (timeless _). Qed. `````` Robbert Krebbers committed Jan 14, 2016 47 ``````Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A). `````` Robbert Krebbers committed Dec 15, 2015 48 ``````Proof. by constructor. Qed. `````` Robbert Krebbers committed Feb 10, 2016 49 ``````Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A). `````` Robbert Krebbers committed Jan 16, 2016 50 ``````Proof. inversion_clear 1; split; eauto. Qed. `````` Robbert Krebbers committed Feb 11, 2016 51 ``````Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A). `````` Robbert Krebbers committed Jan 16, 2016 52 ``````Proof. by inversion_clear 1. Qed. `````` Robbert Krebbers committed Jan 14, 2016 53 ``````Global Instance None_timeless : Timeless (@None A). `````` Robbert Krebbers committed Dec 15, 2015 54 ``````Proof. inversion_clear 1; constructor. Qed. `````` Robbert Krebbers committed Jan 14, 2016 55 ``````Global Instance Some_timeless x : Timeless x → Timeless (Some x). `````` Robbert Krebbers committed Dec 15, 2015 56 ``````Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed. `````` Robbert Krebbers committed Jan 14, 2016 57 58 59 60 ``````End cofe. Arguments optionC : clear implicits. `````` Robbert Krebbers committed Dec 15, 2015 61 ``````(* CMRA *) `````` Robbert Krebbers committed Jan 14, 2016 62 63 64 ``````Section cmra. Context {A : cmraT}. `````` Robbert Krebbers committed Feb 24, 2016 65 66 ``````Instance option_valid : Valid (option A) := λ mx, match mx with Some x => ✓ x | None => True end. `````` Robbert Krebbers committed Jan 14, 2016 67 ``````Instance option_validN : ValidN (option A) := λ n mx, `````` Robbert Krebbers committed Dec 15, 2015 68 `````` match mx with Some x => ✓{n} x | None => True end. `````` Robbert Krebbers committed Feb 04, 2016 69 ``````Global Instance option_empty : Empty (option A) := None. `````` Ralf Jung committed Mar 08, 2016 70 ``````Instance option_core : Core (option A) := fmap core. `````` Robbert Krebbers committed Jan 14, 2016 71 ``````Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)). `````` Robbert Krebbers committed Feb 26, 2016 72 `````` `````` Robbert Krebbers committed Feb 26, 2016 73 ``````Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _. `````` Robbert Krebbers committed Feb 26, 2016 74 75 ``````Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl. `````` Robbert Krebbers committed Feb 26, 2016 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 committed Jan 16, 2016 88 `````` `````` Robbert Krebbers committed Jan 14, 2016 89 ``````Definition option_cmra_mixin : CMRAMixin (option A). `````` Robbert Krebbers committed Dec 15, 2015 90 91 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 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. `````` Robbert Krebbers committed Feb 24, 2016 95 `````` - intros [x|]; [apply cmra_valid_validN|done]. `````` Robbert Krebbers committed Feb 17, 2016 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 committed Mar 08, 2016 99 100 `````` - by intros [x|]; constructor; rewrite cmra_core_l. - by intros [x|]; constructor; rewrite cmra_core_idemp. `````` Robbert Krebbers committed Feb 26, 2016 101 `````` - intros mx my; rewrite !option_included ;intros [->|(x&y&->&->&?)]; auto. `````` Ralf Jung committed Mar 08, 2016 102 `````` right; exists (core x), (core y); eauto using cmra_core_preserving. `````` Robbert Krebbers committed Feb 17, 2016 103 `````` - intros n [x|] [y|]; rewrite /validN /option_validN /=; `````` Robbert Krebbers committed Feb 01, 2016 104 `````` eauto using cmra_validN_op_l. `````` Robbert Krebbers committed Feb 24, 2016 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. `````` Robbert Krebbers committed Dec 15, 2015 114 ``````Qed. `````` Robbert Krebbers committed Mar 01, 2016 115 ``````Canonical Structure optionR := CMRAT option_cofe_mixin option_cmra_mixin. `````` Ralf Jung committed Mar 08, 2016 116 ``````Global Instance option_cmra_unit : CMRAUnit optionR. `````` Robbert Krebbers committed Feb 04, 2016 117 ``````Proof. split. done. by intros []. by inversion_clear 1. Qed. `````` Robbert Krebbers committed Mar 01, 2016 118 ``````Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR. `````` Robbert Krebbers committed Feb 24, 2016 119 ``````Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed. `````` Robbert Krebbers committed Jan 14, 2016 120 `````` `````` Robbert Krebbers committed Feb 13, 2016 121 ``````(** Misc *) `````` Robbert Krebbers committed Feb 26, 2016 122 123 ``````Global Instance Some_cmra_monotone : CMRAMonotone Some. Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed. `````` Robbert Krebbers committed Feb 02, 2016 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. `````` Ralf Jung committed Feb 10, 2016 128 ``````Lemma option_op_positive_dist_l n mx my : mx ⋅ my ≡{n}≡ None → mx ≡{n}≡ None. `````` Robbert Krebbers committed Feb 02, 2016 129 ``````Proof. by destruct mx, my; inversion_clear 1. Qed. `````` Ralf Jung committed Feb 10, 2016 130 ``````Lemma option_op_positive_dist_r n mx my : mx ⋅ my ≡{n}≡ None → my ≡{n}≡ None. `````` Robbert Krebbers committed Feb 02, 2016 131 132 ``````Proof. by destruct mx, my; inversion_clear 1. Qed. `````` Robbert Krebbers committed Mar 15, 2016 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. `````` Robbert Krebbers committed Feb 13, 2016 139 140 ``````(** Internalized properties *) Lemma option_equivI {M} (x y : option A) : `````` Ralf Jung committed Mar 10, 2016 141 `````` (x ≡ y) ⊣⊢ (match x, y with `````` Robbert Krebbers committed Feb 13, 2016 142 `````` | Some a, Some b => a ≡ b | None, None => True | _, _ => False `````` Ralf Jung committed Mar 10, 2016 143 `````` end : uPred M). `````` Robbert Krebbers committed Feb 25, 2016 144 145 146 ``````Proof. uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor. Qed. `````` Robbert Krebbers committed Feb 13, 2016 147 ``````Lemma option_validI {M} (x : option A) : `````` Ralf Jung committed Mar 10, 2016 148 `````` (✓ x) ⊣⊢ (match x with Some a => ✓ a | None => True end : uPred M). `````` Robbert Krebbers committed Feb 25, 2016 149 ``````Proof. uPred.unseal. by destruct x. Qed. `````` Robbert Krebbers committed Feb 13, 2016 150 151 `````` (** Updates *) `````` Robbert Krebbers committed Feb 02, 2016 152 ``````Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x : `````` Ralf Jung committed Feb 03, 2016 153 `````` x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 154 ``````Proof. `````` Robbert Krebbers committed Feb 18, 2016 155 156 `````` intros Hx Hy n [y|] ?. { destruct (Hx n y) as (y'&?&?); auto. exists (Some y'); auto. } `````` Ralf Jung committed Mar 08, 2016 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)]. `````` Robbert Krebbers committed Feb 02, 2016 159 ``````Qed. `````` Robbert Krebbers committed Feb 02, 2016 160 ``````Lemma option_updateP' (P : A → Prop) x : `````` Ralf Jung committed Feb 03, 2016 161 `````` x ~~>: P → Some x ~~>: λ y, default False y P. `````` Robbert Krebbers committed Feb 02, 2016 162 ``````Proof. eauto using option_updateP. Qed. `````` Ralf Jung committed Feb 03, 2016 163 ``````Lemma option_update x y : x ~~> y → Some x ~~> Some y. `````` Robbert Krebbers committed Jan 16, 2016 164 ``````Proof. `````` Robbert Krebbers committed Feb 02, 2016 165 `````` rewrite !cmra_update_updateP; eauto using option_updateP with congruence. `````` Robbert Krebbers committed Jan 16, 2016 166 ``````Qed. `````` Ralf Jung committed Mar 08, 2016 167 ``````Lemma option_update_None `{Empty A, !CMRAUnit A} : ∅ ~~> Some ∅. `````` Robbert Krebbers committed Feb 08, 2016 168 ``````Proof. `````` Robbert Krebbers committed Feb 18, 2016 169 `````` intros n [x|] ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id; `````` Ralf Jung committed Mar 08, 2016 170 `````` auto using cmra_unit_validN. `````` Robbert Krebbers committed Feb 08, 2016 171 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 172 ``````End cmra. `````` Robbert Krebbers committed Mar 01, 2016 173 ``````Arguments optionR : clear implicits. `````` Robbert Krebbers committed Jan 14, 2016 174 `````` `````` Robbert Krebbers committed Feb 04, 2016 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. `````` Robbert Krebbers committed Jan 14, 2016 179 180 ``````Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A → option B). `````` Robbert Krebbers committed Dec 15, 2015 181 ``````Proof. `````` Robbert Krebbers committed Feb 26, 2016 182 `````` split; first apply _. `````` Robbert Krebbers committed Feb 26, 2016 183 `````` - intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f). `````` Robbert Krebbers committed Feb 26, 2016 184 185 `````` - intros mx my; rewrite !option_included. intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @included_preserving. `````` Robbert Krebbers committed Jan 14, 2016 186 ``````Qed. `````` Robbert Krebbers committed Feb 04, 2016 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 committed Feb 05, 2016 191 `````` `````` Robbert Krebbers committed Mar 02, 2016 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 committed Feb 05, 2016 195 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 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 committed Feb 05, 2016 199 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 200 201 `````` intros F A B x. rewrite /= -{2}(option_fmap_id x). apply option_fmap_setoid_ext=>y; apply cFunctor_id. `````` Ralf Jung committed Feb 05, 2016 202 203 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 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. `````` Ralf Jung committed Mar 07, 2016 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. `````` Robbert Krebbers committed Mar 02, 2016 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) |}. `````` Robbert Krebbers committed Mar 07, 2016 218 219 220 ``````Next Obligation. by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 02, 2016 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 committed Feb 05, 2016 228 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 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.``````