option.v 7.23 KB
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export algebra.cmra. `````` Robbert Krebbers committed Dec 15, 2015 2 3 `````` (* COFE *) `````` Robbert Krebbers committed Jan 14, 2016 4 5 6 ``````Section cofe. Context {A : cofeT}. Inductive option_dist : Dist (option A) := `````` Robbert Krebbers committed Dec 15, 2015 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. `````` Robbert Krebbers committed Jan 14, 2016 11 ``````Program Definition option_chain `````` Robbert Krebbers committed Dec 15, 2015 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. `````` Robbert Krebbers committed Jan 14, 2016 15 `````` intros c x ? n i ?; simpl; destruct (decide (i = 0)) as [->|]. `````` Robbert Krebbers committed Dec 15, 2015 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. `````` Robbert Krebbers committed Jan 14, 2016 20 ``````Instance option_compl : Compl (option A) := λ c, `````` Robbert Krebbers committed Dec 15, 2015 21 22 23 `````` match Some_dec (c 1) with | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None end. `````` Robbert Krebbers committed Jan 14, 2016 24 ``````Definition option_cofe_mixin : CofeMixin (option A). `````` Robbert Krebbers committed Dec 15, 2015 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. `````` Robbert Krebbers committed Jan 14, 2016 45 46 ``````Canonical Structure optionC := CofeT option_cofe_mixin. Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A). `````` Robbert Krebbers committed Dec 15, 2015 47 ``````Proof. by constructor. Qed. `````` Robbert Krebbers committed Jan 16, 2016 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. `````` Robbert Krebbers committed Jan 14, 2016 52 ``````Global Instance None_timeless : Timeless (@None A). `````` Robbert Krebbers committed Dec 15, 2015 53 ``````Proof. inversion_clear 1; constructor. Qed. `````` Robbert Krebbers committed Jan 14, 2016 54 ``````Global Instance Some_timeless x : Timeless x → Timeless (Some x). `````` Robbert Krebbers committed Dec 15, 2015 55 ``````Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed. `````` Robbert Krebbers committed Jan 14, 2016 56 57 58 59 60 ``````End cofe. Arguments optionC : clear implicits. Instance option_fmap_ne {A B : cofeT} (f : A → B) n: `````` Robbert Krebbers committed Dec 15, 2015 61 62 `````` 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 16, 2016 63 `````` `````` Robbert Krebbers committed Dec 15, 2015 64 ``````(* CMRA *) `````` Robbert Krebbers committed Jan 14, 2016 65 66 67 68 ``````Section cmra. Context {A : cmraT}. Instance option_validN : ValidN (option A) := λ n mx, `````` Robbert Krebbers committed Dec 15, 2015 69 `````` match mx with Some x => ✓{n} x | None => True end. `````` Robbert Krebbers committed Jan 14, 2016 70 71 72 ``````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) := `````` Robbert Krebbers committed Dec 15, 2015 73 `````` difference_with (λ x y, Some (x ⩪ y)). `````` Robbert Krebbers committed Jan 14, 2016 74 ``````Lemma option_includedN n (mx my : option A) : `````` Robbert Krebbers committed Dec 15, 2015 75 76 77 78 79 80 81 `````` 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; `````` Robbert Krebbers committed Feb 01, 2016 82 `````` cofe_subst; eauto using cmra_includedN_l. `````` Robbert Krebbers committed Dec 15, 2015 83 84 85 86 `````` * intros [->|[->|(x&y&->&->&z&Hz)]]; try (by exists my; destruct my; constructor). by exists (Some z); constructor. Qed. `````` Robbert Krebbers committed Jan 16, 2016 87 88 89 90 91 ``````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. `````` Robbert Krebbers committed Jan 14, 2016 92 ``````Definition option_cmra_mixin : CMRAMixin (option A). `````` Robbert Krebbers committed Dec 15, 2015 93 94 95 96 97 98 ``````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; `````` Robbert Krebbers committed Feb 01, 2016 99 `````` intros ?; auto using cmra_validN_0; `````` Robbert Krebbers committed Dec 15, 2015 100 101 102 `````` eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto. * by destruct 1; inversion_clear 1; constructor; repeat apply (_ : Proper (dist _ ==> _ ==> _) _). `````` Robbert Krebbers committed Feb 01, 2016 103 104 105 106 107 108 `````` * 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. `````` Robbert Krebbers committed Dec 15, 2015 109 `````` * intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto. `````` Robbert Krebbers committed Feb 01, 2016 110 111 112 `````` 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. `````` Robbert Krebbers committed Dec 15, 2015 113 114 115 116 `````` * intros n mx my; rewrite option_includedN. intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|]. by constructor; apply cmra_op_minus. Qed. `````` Robbert Krebbers committed Jan 14, 2016 117 ``````Definition option_cmra_extend_mixin : CMRAExtendMixin (option A). `````` Robbert Krebbers committed Dec 15, 2015 118 119 120 121 122 123 124 125 126 127 128 129 ``````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. `````` Robbert Krebbers committed Jan 14, 2016 130 131 132 ``````Canonical Structure optionRA := CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin. `````` Robbert Krebbers committed Feb 02, 2016 133 134 135 136 137 138 139 140 141 142 ``````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 : `````` Ralf Jung committed Feb 03, 2016 143 `````` x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 144 145 146 147 148 149 ``````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. `````` Robbert Krebbers committed Feb 02, 2016 150 ``````Lemma option_updateP' (P : A → Prop) x : `````` Ralf Jung committed Feb 03, 2016 151 `````` x ~~>: P → Some x ~~>: λ y, default False y P. `````` Robbert Krebbers committed Feb 02, 2016 152 ``````Proof. eauto using option_updateP. Qed. `````` Ralf Jung committed Feb 03, 2016 153 ``````Lemma option_update x y : x ~~> y → Some x ~~> Some y. `````` Robbert Krebbers committed Jan 16, 2016 154 ``````Proof. `````` Robbert Krebbers committed Feb 02, 2016 155 `````` rewrite !cmra_update_updateP; eauto using option_updateP with congruence. `````` Robbert Krebbers committed Jan 16, 2016 156 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 157 158 159 160 161 162 ``````End cmra. Arguments optionRA : clear implicits. 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 163 164 165 166 ``````Proof. split. * intros n mx my; rewrite !option_includedN. intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving. `````` Robbert Krebbers committed Jan 14, 2016 167 168 `````` * by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving. Qed.``````