option.v 15.7 KB
 Robbert Krebbers committed Nov 11, 2015 1 2 3 4 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects general purpose definitions and theorems on the option data type that are not in the Coq standard library. *) `````` Robbert Krebbers committed Feb 13, 2016 5 ``````From prelude Require Export base tactics decidable. `````` Robbert Krebbers committed Nov 11, 2015 6 7 8 9 10 11 12 13 14 15 16 17 18 `````` Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type := | ReflectSome x : P x → option_reflect P Q (Some x) | ReflectNone : Q → option_reflect P Q None. (** * General definitions and theorems *) (** Basic properties about equality. *) Lemma None_ne_Some {A} (a : A) : None ≠ Some a. Proof. congruence. Qed. Lemma Some_ne_None {A} (a : A) : Some a ≠ None. Proof. congruence. Qed. Lemma eq_None_ne_Some {A} (x : option A) a : x = None → x ≠ Some a. Proof. congruence. Qed. `````` Robbert Krebbers committed Feb 11, 2016 19 ``````Instance Some_inj {A} : Inj (=) (=) (@Some A). `````` Robbert Krebbers committed Nov 11, 2015 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 ``````Proof. congruence. Qed. (** The non dependent elimination principle on the option type. *) Definition default {A B} (b : B) (x : option A) (f : A → B) : B := match x with None => b | Some a => f a end. (** The [from_option] function allows us to get the value out of the option type by specifying a default value. *) Definition from_option {A} (a : A) (x : option A) : A := match x with None => a | Some b => b end. (** An alternative, but equivalent, definition of equality on the option data type. This theorem is useful to prove that two options are the same. *) Lemma option_eq {A} (x y : option A) : x = y ↔ ∀ a, x = Some a ↔ y = Some a. Proof. split; [by intros; by subst |]. destruct x, y; naive_solver. Qed. Lemma option_eq_1 {A} (x y : option A) a : x = y → x = Some a → y = Some a. Proof. congruence. Qed. Lemma option_eq_1_alt {A} (x y : option A) a : x = y → y = Some a → x = Some a. Proof. congruence. Qed. Definition is_Some {A} (x : option A) := ∃ y, x = Some y. Lemma mk_is_Some {A} (x : option A) y : x = Some y → is_Some x. Proof. intros; red; subst; eauto. Qed. Hint Resolve mk_is_Some. Lemma is_Some_None {A} : ¬is_Some (@None A). Proof. by destruct 1. Qed. Hint Resolve is_Some_None. Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x). Proof. set (P (y : option A) := match y with Some _ => True | _ => False end). set (f x := match x return P x → is_Some x with Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end). set (g x (H : is_Some x) := match H return P x with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end). assert (∀ x H, f x (g x H) = H) as f_g by (by intros ? [??]; subst). intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct x, p1. Qed. Instance is_Some_dec {A} (x : option A) : Decision (is_Some x) := match x with | Some x => left (ex_intro _ x eq_refl) | None => right is_Some_None end. Definition is_Some_proj {A} {x : option A} : is_Some x → A := match x with Some a => λ _, a | None => False_rect _ ∘ is_Some_None end. Definition Some_dec {A} (x : option A) : { a | x = Some a } + { x = None } := match x return { a | x = Some a } + { x = None } with | Some a => inleft (a ↾ eq_refl _) | None => inright eq_refl end. Lemma eq_None_not_Some {A} (x : option A) : x = None ↔ ¬is_Some x. Proof. destruct x; unfold is_Some; naive_solver. Qed. Lemma not_eq_None_Some `(x : option A) : x ≠ None ↔ is_Some x. Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed. (** Lifting a relation point-wise to option *) Inductive option_Forall2 {A B} (P: A → B → Prop) : option A → option B → Prop := | Some_Forall2 x y : P x y → option_Forall2 P (Some x) (Some y) | None_Forall2 : option_Forall2 P None None. Definition option_relation {A B} (R: A → B → Prop) (P: A → Prop) (Q: B → Prop) (mx : option A) (my : option B) : Prop := match mx, my with | Some x, Some y => R x y | Some x, None => P x | None, Some y => Q y | None, None => True end. (** Setoids *) Section setoids. `````` Robbert Krebbers committed Nov 18, 2015 92 `````` Context `{Equiv A} `{!Equivalence ((≡) : relation A)}. `````` Robbert Krebbers committed Nov 11, 2015 93 `````` Global Instance option_equiv : Equiv (option A) := option_Forall2 (≡). `````` Robbert Krebbers committed Nov 18, 2015 94 `````` Global Instance option_equivalence : Equivalence ((≡) : relation (option A)). `````` Robbert Krebbers committed Nov 11, 2015 95 96 `````` Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 97 98 `````` - by intros []; constructor. - by destruct 1; constructor. `````` Ralf Jung committed Feb 20, 2016 99 `````` - destruct 1; inversion 1; constructor; etrans; eauto. `````` Robbert Krebbers committed Nov 11, 2015 100 101 102 103 `````` Qed. Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A). Proof. by constructor. Qed. Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A). `````` Robbert Krebbers committed Dec 15, 2015 104 `````` Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed. `````` Robbert Krebbers committed Nov 18, 2015 105 106 107 108 109 `````` Lemma equiv_None (mx : option A) : mx ≡ None ↔ mx = None. Proof. split; [by inversion_clear 1|by intros ->]. Qed. Lemma equiv_Some (mx my : option A) x : mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y. Proof. destruct 1; naive_solver. Qed. `````` Robbert Krebbers committed Jan 16, 2016 110 111 `````` Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A). Proof. inversion_clear 1; split; eauto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 ``````End setoids. (** Equality on [option] is decidable. *) Instance option_eq_None_dec {A} (x : option A) : Decision (x = None) := match x with Some _ => right (Some_ne_None _) | None => left eq_refl end. Instance option_None_eq_dec {A} (x : option A) : Decision (None = x) := match x with Some _ => right (None_ne_Some _) | None => left eq_refl end. Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)} (x y : option A) : Decision (x = y). Proof. refine match x, y with | Some a, Some b => cast_if (decide (a = b)) | None, None => left _ | _, _ => right _ end; clear dec; abstract congruence. Defined. (** * Monadic operations *) Instance option_ret: MRet option := @Some. Instance option_bind: MBind option := λ A B f x, match x with Some a => f a | None => None end. Instance option_join: MJoin option := λ A x, match x with Some x => x | None => None end. Instance option_fmap: FMap option := @option_map. Instance option_guard: MGuard option := λ P dec A x, match dec with left H => x H | _ => None end. Lemma fmap_is_Some {A B} (f : A → B) x : is_Some (f <\$> x) ↔ is_Some x. Proof. unfold is_Some; destruct x; naive_solver. Qed. Lemma fmap_Some {A B} (f : A → B) x y : f <\$> x = Some y ↔ ∃ x', x = Some x' ∧ y = f x'. Proof. destruct x; naive_solver. Qed. Lemma fmap_None {A B} (f : A → B) x : f <\$> x = None ↔ x = None. Proof. by destruct x. Qed. Lemma option_fmap_id {A} (x : option A) : id <\$> x = x. Proof. by destruct x. Qed. Lemma option_fmap_compose {A B} (f : A → B) {C} (g : B → C) x : g ∘ f <\$> x = g <\$> f <\$> x. Proof. by destruct x. Qed. `````` Robbert Krebbers committed Feb 04, 2016 151 152 153 154 155 156 ``````Lemma option_fmap_ext {A B} (f g : A → B) x : (∀ y, f y = g y) → f <\$> x = g <\$> x. Proof. destruct x; simpl; auto with f_equal. Qed. Lemma option_fmap_setoid_ext `{Equiv A, Equiv B} (f g : A → B) x : (∀ y, f y ≡ g y) → f <\$> x ≡ g <\$> x. Proof. destruct x; constructor; auto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 157 158 159 160 161 162 163 164 ``````Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) x : (f <\$> x) ≫= g = x ≫= g ∘ f. Proof. by destruct x. Qed. Lemma option_bind_assoc {A B C} (f : A → option B) (g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f). Proof. by destruct x; simpl. Qed. Lemma option_bind_ext {A B} (f g : A → option B) x y : (∀ a, f a = g a) → x = y → x ≫= f = y ≫= g. `````` Robbert Krebbers committed Feb 17, 2016 165 ``````Proof. intros. destruct x, y; simplify_eq; csimpl; auto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 166 167 168 169 170 171 172 173 174 175 ``````Lemma option_bind_ext_fun {A B} (f g : A → option B) x : (∀ a, f a = g a) → x ≫= f = x ≫= g. Proof. intros. by apply option_bind_ext. Qed. Lemma bind_Some {A B} (f : A → option B) (x : option A) b : x ≫= f = Some b ↔ ∃ a, x = Some a ∧ f a = Some b. Proof. split. by destruct x as [a|]; [exists a|]. by intros (?&->&?). Qed. Lemma bind_None {A B} (f : A → option B) (x : option A) : x ≫= f = None ↔ x = None ∨ ∃ a, x = Some a ∧ f a = None. Proof. split; [|by intros [->|(?&->&?)]]. `````` Robbert Krebbers committed Feb 17, 2016 176 `````` destruct x; intros; simplify_eq/=; eauto. `````` Robbert Krebbers committed Nov 11, 2015 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 ``````Qed. Lemma bind_with_Some {A} (x : option A) : x ≫= Some = x. Proof. by destruct x. Qed. (** ** Inverses of constructors *) (** We can do this in a fancy way using dependent types, but rewrite does not particularly like type level reductions. *) Class Maybe {A B : Type} (c : A → B) := maybe : B → option A. Arguments maybe {_ _} _ {_} !_ /. Class Maybe2 {A1 A2 B : Type} (c : A1 → A2 → B) := maybe2 : B → option (A1 * A2). Arguments maybe2 {_ _ _} _ {_} !_ /. Class Maybe3 {A1 A2 A3 B : Type} (c : A1 → A2 → A3 → B) := maybe3 : B → option (A1 * A2 * A3). Arguments maybe3 {_ _ _ _} _ {_} !_ /. Class Maybe4 {A1 A2 A3 A4 B : Type} (c : A1 → A2 → A3 → A4 → B) := maybe4 : B → option (A1 * A2 * A3 * A4). Arguments maybe4 {_ _ _ _ _} _ {_} !_ /. Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1 ∘ c2) := λ x, maybe c1 x ≫= maybe c2. Arguments maybe_comp _ _ _ _ _ _ _ !_ /. Instance maybe_inl {A B} : Maybe (@inl A B) := λ xy, match xy with inl x => Some x | _ => None end. Instance maybe_inr {A B} : Maybe (@inr A B) := λ xy, match xy with inr y => Some y | _ => None end. Instance maybe_Some {A} : Maybe (@Some A) := id. Arguments maybe_Some _ !_ /. (** * Union, intersection and difference *) Instance option_union_with {A} : UnionWith A (option A) := λ f x y, match x, y with | Some a, Some b => f a b | Some a, None => Some a | None, Some b => Some b | None, None => None end. Instance option_intersection_with {A} : IntersectionWith A (option A) := λ f x y, match x, y with Some a, Some b => f a b | _, _ => None end. Instance option_difference_with {A} : DifferenceWith A (option A) := λ f x y, match x, y with | Some a, Some b => f a b | Some a, None => Some a | None, _ => None end. Instance option_union {A} : Union (option A) := union_with (λ x _, Some x). Lemma option_union_Some {A} (x y : option A) z : x ∪ y = Some z → x = Some z ∨ y = Some z. `````` Robbert Krebbers committed Feb 17, 2016 227 ``````Proof. destruct x, y; intros; simplify_eq; auto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 228 229 230 231 232 233 234 `````` Section option_union_intersection_difference. Context {A} (f : A → A → option A). Global Instance: LeftId (=) None (union_with f). Proof. by intros [?|]. Qed. Global Instance: RightId (=) None (union_with f). Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Feb 11, 2016 235 236 `````` Global Instance: Comm (=) f → Comm (=) (union_with f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed. `````` Robbert Krebbers committed Nov 11, 2015 237 238 239 240 `````` Global Instance: LeftAbsorb (=) None (intersection_with f). Proof. by intros [?|]. Qed. Global Instance: RightAbsorb (=) None (intersection_with f). Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Feb 11, 2016 241 242 `````` Global Instance: Comm (=) f → Comm (=) (intersection_with f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed. `````` Robbert Krebbers committed Nov 11, 2015 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 `````` Global Instance: RightId (=) None (difference_with f). Proof. by intros [?|]. Qed. End option_union_intersection_difference. (** * Tactics *) Tactic Notation "case_option_guard" "as" ident(Hx) := match goal with | H : appcontext C [@mguard option _ ?P ?dec] |- _ => change (@mguard option _ P dec) with (λ A (x : P → option A), match @decide P dec with left H' => x H' | _ => None end) in *; destruct_decide (@decide P dec) as Hx | |- appcontext C [@mguard option _ ?P ?dec] => change (@mguard option _ P dec) with (λ A (x : P → option A), match @decide P dec with left H' => x H' | _ => None end) in *; destruct_decide (@decide P dec) as Hx end. Tactic Notation "case_option_guard" := let H := fresh in case_option_guard as H. Lemma option_guard_True {A} P `{Decision P} (x : option A) : P → guard P; x = x. Proof. intros. by case_option_guard. Qed. Lemma option_guard_False {A} P `{Decision P} (x : option A) : ¬P → guard P; x = None. Proof. intros. by case_option_guard. Qed. Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (x : option A) : (P ↔ Q) → guard P; x = guard Q; x. Proof. intros [??]. repeat case_option_guard; intuition. Qed. `````` Robbert Krebbers committed Jan 12, 2016 272 ``````Tactic Notation "simpl_option" "by" tactic3(tac) := `````` Robbert Krebbers committed Nov 11, 2015 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 `````` let assert_Some_None A o H := first [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; assert (o = Some x') as H by tac | assert (o = None) as H by tac ] in repeat match goal with | H : appcontext [@mret _ _ ?A] |- _ => change (@mret _ _ A) with (@Some A) in H | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A) | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx | H : context [default (A:=?A) _ ?o _] |- _ => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx | H : context [from_option (A:=?A) _ ?o] |- _ => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx | H : context [ match ?o with _ => _ end ] |- _ => match type of o with | option ?A => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx end | |- context [mbind (M:=option) (A:=?A) ?f ?o] => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx | |- context [fmap (M:=option) (A:=?A) ?f ?o] => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx | |- context [default (A:=?A) _ ?o _] => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx | |- context [from_option (A:=?A) _ ?o] => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx | |- context [ match ?o with _ => _ end ] => match type of o with | option ?A => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx end | H : context [decide _] |- _ => rewrite decide_True in H by tac | H : context [decide _] |- _ => rewrite decide_False in H by tac | H : context [mguard _ _] |- _ => rewrite option_guard_False in H by tac | H : context [mguard _ _] |- _ => rewrite option_guard_True in H by tac | _ => rewrite decide_True by tac | _ => rewrite decide_False by tac | _ => rewrite option_guard_True by tac | _ => rewrite option_guard_False by tac `````` Robbert Krebbers committed Jan 22, 2016 315 316 317 318 `````` | H : context [None ∪ _] |- _ => rewrite (left_id_L None (∪)) in H | H : context [_ ∪ None] |- _ => rewrite (right_id_L None (∪)) in H | |- context [None ∪ _] => rewrite (left_id_L None (∪)) | |- context [_ ∪ None] => rewrite (right_id_L None (∪)) `````` Robbert Krebbers committed Nov 11, 2015 319 `````` end. `````` Robbert Krebbers committed Feb 17, 2016 320 ``````Tactic Notation "simplify_option_eq" "by" tactic3(tac) := `````` Robbert Krebbers committed Nov 11, 2015 321 `````` repeat match goal with `````` Robbert Krebbers committed Feb 17, 2016 322 `````` | _ => progress simplify_eq/= `````` Robbert Krebbers committed Jan 12, 2016 323 `````` | _ => progress simpl_option by tac `````` Robbert Krebbers committed Nov 11, 2015 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 `````` | _ : maybe _ ?x = Some _ |- _ => is_var x; destruct x | _ : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x | _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x | _ : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x | H : _ ∪ _ = Some _ |- _ => apply option_union_Some in H; destruct H | H : mbind (M:=option) ?f ?o = ?x |- _ => match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match x with Some _ => idtac | None => idtac | _ => fail 1 end; let y := fresh in destruct o as [y|] eqn:?; [change (f y = x) in H|change (None = x) in H] | H : ?x = mbind (M:=option) ?f ?o |- _ => match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match x with Some _ => idtac | None => idtac | _ => fail 1 end; let y := fresh in destruct o as [y|] eqn:?; [change (x = f y) in H|change (x = None) in H] | H : fmap (M:=option) ?f ?o = ?x |- _ => match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match x with Some _ => idtac | None => idtac | _ => fail 1 end; let y := fresh in destruct o as [y|] eqn:?; [change (Some (f y) = x) in H|change (None = x) in H] | H : ?x = fmap (M:=option) ?f ?o |- _ => match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match x with Some _ => idtac | None => idtac | _ => fail 1 end; let y := fresh in destruct o as [y|] eqn:?; [change (x = Some (f y)) in H|change (x = None) in H] | _ => progress case_decide | _ => progress case_option_guard end. `````` Robbert Krebbers committed Feb 17, 2016 352 ``Tactic Notation "simplify_option_eq" := simplify_option_eq by eauto.``