option.v 15.2 KB
Newer Older
 Robbert Krebbers committed Feb 08, 2015 1 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) `````` Robbert Krebbers committed Aug 29, 2012 2 3 4 ``````(* 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 Nov 16, 2015 5 ``````Require Export prelude.base prelude.tactics prelude.decidable. `````` Robbert Krebbers committed Aug 29, 2012 6 `````` `````` Robbert Krebbers committed May 02, 2014 7 8 9 10 ``````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. `````` Robbert Krebbers committed Aug 29, 2012 11 12 ``````(** * General definitions and theorems *) (** Basic properties about equality. *) `````` Robbert Krebbers committed May 02, 2014 13 ``````Lemma None_ne_Some {A} (a : A) : None ≠ Some a. `````` Robbert Krebbers committed Jun 11, 2012 14 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed May 02, 2014 15 ``````Lemma Some_ne_None {A} (a : A) : Some a ≠ None. `````` Robbert Krebbers committed Jun 11, 2012 16 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed May 02, 2014 17 ``````Lemma eq_None_ne_Some {A} (x : option A) a : x = None → x ≠ Some a. `````` Robbert Krebbers committed Jun 11, 2012 18 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed Aug 21, 2012 19 ``````Instance Some_inj {A} : Injective (=) (=) (@Some A). `````` Robbert Krebbers committed Jun 11, 2012 20 21 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed Aug 29, 2012 22 ``````(** The non dependent elimination principle on the option type. *) `````` Robbert Krebbers committed May 07, 2013 23 24 ``````Definition default {A B} (b : B) (x : option A) (f : A → B) : B := match x with None => b | Some a => f a end. `````` Robbert Krebbers committed Jun 11, 2012 25 `````` `````` Robbert Krebbers committed Jan 05, 2013 26 27 28 ``````(** 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 := `````` Robbert Krebbers committed May 07, 2013 29 `````` match x with None => a | Some b => b end. `````` Robbert Krebbers committed Aug 21, 2012 30 `````` `````` Robbert Krebbers committed Aug 29, 2012 31 32 ``````(** An alternative, but equivalent, definition of equality on the option data type. This theorem is useful to prove that two options are the same. *) `````` Robbert Krebbers committed May 15, 2013 33 34 ``````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. `````` Robbert Krebbers committed Sep 03, 2014 35 36 37 38 ``````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. `````` Robbert Krebbers committed Jun 11, 2012 39 `````` `````` Robbert Krebbers committed May 15, 2013 40 41 42 43 44 45 46 ``````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. `````` Robbert Krebbers committed Jun 11, 2012 47 `````` `````` Robbert Krebbers committed Mar 25, 2013 48 49 ``````Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x). Proof. `````` Robbert Krebbers committed May 15, 2013 50 51 52 53 54 55 56 `````` 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. `````` Robbert Krebbers committed Mar 25, 2013 57 ``````Qed. `````` Robbert Krebbers committed May 15, 2013 58 ``````Instance is_Some_dec {A} (x : option A) : Decision (is_Some x) := `````` Robbert Krebbers committed Jun 11, 2012 59 `````` match x with `````` Robbert Krebbers committed May 15, 2013 60 61 `````` | Some x => left (ex_intro _ x eq_refl) | None => right is_Some_None `````` Robbert Krebbers committed Nov 12, 2012 62 `````` end. `````` Robbert Krebbers committed May 15, 2013 63 64 65 66 `````` 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 } := `````` Robbert Krebbers committed Jan 05, 2013 67 68 69 70 `````` match x return { a | x = Some a } + { x = None } with | Some a => inleft (a ↾ eq_refl _) | None => inright eq_refl end. `````` Robbert Krebbers committed Jun 11, 2012 71 `````` `````` Robbert Krebbers committed May 15, 2013 72 73 ``````Lemma eq_None_not_Some {A} (x : option A) : x = None ↔ ¬is_Some x. Proof. destruct x; unfold is_Some; naive_solver. Qed. `````` Robbert Krebbers committed Nov 12, 2012 74 ``````Lemma not_eq_None_Some `(x : option A) : x ≠ None ↔ is_Some x. `````` Robbert Krebbers committed Jan 05, 2013 75 ``````Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 76 `````` `````` Robbert Krebbers committed Feb 03, 2017 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 ``````(** 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 Feb 03, 2017 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 Feb 03, 2017 95 96 97 98 99 100 101 102 103 `````` Proof. split. * by intros []; constructor. * by destruct 1; constructor. * destruct 1; inversion 1; constructor; etransitivity; eauto. 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 Feb 03, 2017 112 113 ``````End setoids. `````` Robbert Krebbers committed Aug 29, 2012 114 ``````(** Equality on [option] is decidable. *) `````` Robbert Krebbers committed May 02, 2014 115 116 117 118 ``````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. `````` Robbert Krebbers committed Aug 29, 2012 119 ``````Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)} `````` Robbert Krebbers committed May 02, 2014 120 121 122 `````` (x y : option A) : Decision (x = y). Proof. refine `````` Robbert Krebbers committed Feb 19, 2013 123 `````` match x, y with `````` Robbert Krebbers committed May 02, 2014 124 125 `````` | Some a, Some b => cast_if (decide (a = b)) | None, None => left _ | _, _ => right _ `````` Robbert Krebbers committed Dec 18, 2014 126 `````` end; clear dec; abstract congruence. `````` Robbert Krebbers committed May 02, 2014 127 ``````Defined. `````` Robbert Krebbers committed Jun 11, 2012 128 `````` `````` Robbert Krebbers committed Aug 29, 2012 129 ``````(** * Monadic operations *) `````` Robbert Krebbers committed Nov 12, 2012 130 131 ``````Instance option_ret: MRet option := @Some. Instance option_bind: MBind option := λ A B f x, `````` Robbert Krebbers committed May 07, 2013 132 `````` match x with Some a => f a | None => None end. `````` Robbert Krebbers committed Nov 12, 2012 133 ``````Instance option_join: MJoin option := λ A x, `````` Robbert Krebbers committed May 07, 2013 134 `````` match x with Some x => x | None => None end. `````` Robbert Krebbers committed Nov 12, 2012 135 136 ``````Instance option_fmap: FMap option := @option_map. Instance option_guard: MGuard option := λ P dec A x, `````` Robbert Krebbers committed May 07, 2013 137 `````` match dec with left H => x H | _ => None end. `````` Robbert Krebbers committed Jun 11, 2012 138 `````` `````` Robbert Krebbers committed May 15, 2013 139 140 141 ``````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 : `````` Robbert Krebbers committed Feb 19, 2013 142 `````` f <\$> x = Some y ↔ ∃ x', x = Some x' ∧ y = f x'. `````` Robbert Krebbers committed May 15, 2013 143 144 145 ``````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. `````` Robbert Krebbers committed May 07, 2013 146 ``````Lemma option_fmap_id {A} (x : option A) : id <\$> x = x. `````` Robbert Krebbers committed Feb 19, 2013 147 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed May 02, 2014 148 149 150 ``````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 Jun 17, 2013 151 152 153 ``````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. `````` Robbert Krebbers committed Jan 05, 2013 154 ``````Lemma option_bind_assoc {A B C} (f : A → option B) `````` Robbert Krebbers committed May 15, 2013 155 `````` (g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f). `````` Robbert Krebbers committed Jan 05, 2013 156 ``````Proof. by destruct x; simpl. Qed. `````` Robbert Krebbers committed Feb 22, 2013 157 ``````Lemma option_bind_ext {A B} (f g : A → option B) x y : `````` Robbert Krebbers committed May 07, 2013 158 `````` (∀ a, f a = g a) → x = y → x ≫= f = y ≫= g. `````` Robbert Krebbers committed Jun 16, 2014 159 ``````Proof. intros. destruct x, y; simplify_equality; csimpl; auto. Qed. `````` Robbert Krebbers committed Feb 22, 2013 160 ``````Lemma option_bind_ext_fun {A B} (f g : A → option B) x : `````` Robbert Krebbers committed May 07, 2013 161 `````` (∀ a, f a = g a) → x ≫= f = x ≫= g. `````` Robbert Krebbers committed Feb 22, 2013 162 ``````Proof. intros. by apply option_bind_ext. Qed. `````` Robbert Krebbers committed Jun 17, 2013 163 164 165 166 167 168 ``````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. `````` Robbert Krebbers committed May 02, 2014 169 170 `````` split; [|by intros [->|(?&->&?)]]. destruct x; intros; simplify_equality'; eauto. `````` Robbert Krebbers committed Jun 17, 2013 171 ``````Qed. `````` Robbert Krebbers committed May 02, 2014 172 173 ``````Lemma bind_with_Some {A} (x : option A) : x ≫= Some = x. Proof. by destruct x. Qed. `````` Robbert Krebbers committed Feb 22, 2013 174 `````` `````` Robbert Krebbers committed Nov 06, 2014 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 ``````(** ** 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. `````` Robbert Krebbers committed Dec 18, 2014 199 200 ``````Instance maybe_Some {A} : Maybe (@Some A) := id. Arguments maybe_Some _ !_ /. `````` Robbert Krebbers committed Nov 06, 2014 201 `````` `````` Robbert Krebbers committed Aug 04, 2014 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 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 ``````(** * 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. Proof. destruct x, y; intros; simplify_equality; auto. Qed. 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. Global Instance: Commutative (=) f → Commutative (=) (union_with f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. Global Instance: LeftAbsorb (=) None (intersection_with f). Proof. by intros [?|]. Qed. Global Instance: RightAbsorb (=) None (intersection_with f). Proof. by intros [?|]. Qed. Global Instance: Commutative (=) f → Commutative (=) (intersection_with f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. Global Instance: RightId (=) None (difference_with f). Proof. by intros [?|]. Qed. End option_union_intersection_difference. (** * Tactics *) `````` Robbert Krebbers committed Jun 17, 2013 242 243 ``````Tactic Notation "case_option_guard" "as" ident(Hx) := match goal with `````` Robbert Krebbers committed Feb 08, 2015 244 245 246 247 248 249 250 251 `````` | 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 `````` Robbert Krebbers committed Jun 17, 2013 252 253 254 `````` end. Tactic Notation "case_option_guard" := let H := fresh in case_option_guard as H. `````` Robbert Krebbers committed Jan 05, 2013 255 `````` `````` Robbert Krebbers committed May 22, 2014 256 ``````Lemma option_guard_True {A} P `{Decision P} (x : option A) : `````` Robbert Krebbers committed Jun 24, 2013 257 258 `````` P → guard P; x = x. Proof. intros. by case_option_guard. Qed. `````` Robbert Krebbers committed May 22, 2014 259 ``````Lemma option_guard_False {A} P `{Decision P} (x : option A) : `````` Robbert Krebbers committed Jun 24, 2013 260 261 `````` ¬P → guard P; x = None. Proof. intros. by case_option_guard. Qed. `````` Robbert Krebbers committed May 22, 2014 262 263 264 ``````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 Jun 24, 2013 265 `````` `````` Robbert Krebbers committed Jan 12, 2016 266 ``````Tactic Notation "simpl_option" "by" tactic3(tac) := `````` Robbert Krebbers committed May 02, 2014 267 268 269 270 271 `````` 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 `````` Robbert Krebbers committed Sep 30, 2014 272 273 274 `````` | H : appcontext [@mret _ _ ?A] |- _ => change (@mret _ _ A) with (@Some A) in H | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A) `````` Robbert Krebbers committed Jan 05, 2013 275 `````` | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ => `````` Robbert Krebbers committed May 02, 2014 276 `````` let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 277 `````` | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ => `````` Robbert Krebbers committed May 02, 2014 278 279 280 `````` 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 `````` Robbert Krebbers committed Jan 27, 2015 281 282 `````` | H : context [from_option (A:=?A) _ ?o] |- _ => let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 283 284 285 `````` | H : context [ match ?o with _ => _ end ] |- _ => match type of o with | option ?A => `````` Robbert Krebbers committed May 02, 2014 286 `````` let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 287 288 `````` end | |- context [mbind (M:=option) (A:=?A) ?f ?o] => `````` Robbert Krebbers committed May 02, 2014 289 `````` let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 290 `````` | |- context [fmap (M:=option) (A:=?A) ?f ?o] => `````` Robbert Krebbers committed May 02, 2014 291 292 293 294 295 `````` 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 `````` Robbert Krebbers committed Jan 05, 2013 296 297 298 `````` | |- context [ match ?o with _ => _ end ] => match type of o with | option ?A => `````` Robbert Krebbers committed May 02, 2014 299 `````` let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 300 `````` end `````` Robbert Krebbers committed Apr 22, 2015 301 302 303 304 `````` | 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 `````` Robbert Krebbers committed May 02, 2014 305 306 307 308 `````` | _ => 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 May 22, 2014 309 310 `````` end. Tactic Notation "simplify_option_equality" "by" tactic3(tac) := `````` Robbert Krebbers committed Jun 16, 2014 311 `````` repeat match goal with `````` Robbert Krebbers committed May 22, 2014 312 `````` | _ => progress simplify_equality' `````` Robbert Krebbers committed Jan 12, 2016 313 `````` | _ => progress simpl_option by tac `````` Robbert Krebbers committed Nov 06, 2014 314 315 316 317 `````` | _ : 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 `````` Robbert Krebbers committed Aug 04, 2014 318 `````` | H : _ ∪ _ = Some _ |- _ => apply option_union_Some in H; destruct H `````` Robbert Krebbers committed Jun 23, 2014 319 `````` | H : mbind (M:=option) ?f ?o = ?x |- _ => `````` Robbert Krebbers committed May 22, 2014 320 321 `````` match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match x with Some _ => idtac | None => idtac | _ => fail 1 end; `````` Robbert Krebbers committed Jun 23, 2014 322 323 324 `````` 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 |- _ => `````` Robbert Krebbers committed May 22, 2014 325 326 `````` match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match x with Some _ => idtac | None => idtac | _ => fail 1 end; `````` Robbert Krebbers committed Jun 23, 2014 327 328 `````` let y := fresh in destruct o as [y|] eqn:?; [change (x = f y) in H|change (x = None) in H] `````` Robbert Krebbers committed Jun 25, 2014 329 `````` | H : fmap (M:=option) ?f ?o = ?x |- _ => `````` Robbert Krebbers committed May 22, 2014 330 331 `````` match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match x with Some _ => idtac | None => idtac | _ => fail 1 end; `````` Robbert Krebbers committed Jun 25, 2014 332 333 334 `````` 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 |- _ => `````` Robbert Krebbers committed May 22, 2014 335 336 `````` match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match x with Some _ => idtac | None => idtac | _ => fail 1 end; `````` Robbert Krebbers committed Jun 25, 2014 337 338 `````` let y := fresh in destruct o as [y|] eqn:?; [change (x = Some (f y)) in H|change (x = None) in H] `````` Robbert Krebbers committed May 02, 2014 339 `````` | _ => progress case_decide `````` Robbert Krebbers committed Jun 17, 2013 340 `````` | _ => progress case_option_guard `````` Robbert Krebbers committed Aug 29, 2012 341 `````` end. `````` Robbert Krebbers committed May 02, 2014 342 ``Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.``