option.v 18.4 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 Mar 10, 2016 5 ``````From iris.prelude Require Export tactics. `````` Ralf Jung committed Jan 03, 2017 6 ``````Set Default Proof Using "Type*". `````` Robbert Krebbers committed Nov 11, 2015 7 8 9 10 11 12 13 `````` 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. *) `````` Robbert Krebbers committed Mar 21, 2016 14 ``````Lemma None_ne_Some {A} (x : A) : None ≠ Some x. `````` Robbert Krebbers committed Nov 11, 2015 15 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed Mar 21, 2016 16 ``````Lemma Some_ne_None {A} (x : A) : Some x ≠ None. `````` Robbert Krebbers committed Nov 11, 2015 17 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed Mar 21, 2016 18 ``````Lemma eq_None_ne_Some {A} (mx : option A) x : mx = None → mx ≠ Some x. `````` Robbert Krebbers committed Nov 11, 2015 19 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed Feb 11, 2016 20 ``````Instance Some_inj {A} : Inj (=) (=) (@Some A). `````` Robbert Krebbers committed Nov 11, 2015 21 22 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed May 27, 2016 23 24 ``````(** The [from_option] is the eliminator for option. *) Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B := `````` Robbert Krebbers committed Mar 21, 2016 25 `````` match mx with None => y | Some x => f x end. `````` Robbert Krebbers committed May 27, 2016 26 27 ``````Instance: Params (@from_option) 3. Arguments from_option {_ _} _ _ !_ /. `````` Robbert Krebbers committed Nov 11, 2015 28 `````` `````` Robbert Krebbers committed May 27, 2016 29 30 31 ``````(* The eliminator again, but with the arguments in different order, which is sometimes more convenient. *) Notation default y mx f := (from_option f y mx) (only parsing). `````` Robbert Krebbers committed Nov 11, 2015 32 33 34 `````` (** 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 Mar 21, 2016 35 36 37 ``````Lemma option_eq {A} (mx my: option A): mx = my ↔ ∀ x, mx = Some x ↔ my = Some x. Proof. split; [by intros; by subst |]. destruct mx, my; naive_solver. Qed. Lemma option_eq_1 {A} (mx my: option A) x : mx = my → mx = Some x → my = Some x. `````` Robbert Krebbers committed Nov 11, 2015 38 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed Mar 21, 2016 39 40 ``````Lemma option_eq_1_alt {A} (mx my : option A) x : mx = my → my = Some x → mx = Some x. `````` Robbert Krebbers committed Nov 11, 2015 41 42 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed Mar 21, 2016 43 44 45 ``````Definition is_Some {A} (mx : option A) := ∃ x, mx = Some x. Instance: Params (@is_Some) 1. `````` Robbert Krebbers committed Oct 03, 2016 46 47 48 49 ``````Lemma is_Some_alt {A} (mx : option A) : is_Some mx ↔ match mx with Some _ => True | None => False end. Proof. unfold is_Some. destruct mx; naive_solver. Qed. `````` Robbert Krebbers committed Mar 21, 2016 50 ``````Lemma mk_is_Some {A} (mx : option A) x : mx = Some x → is_Some mx. `````` Robbert Krebbers committed Nov 11, 2015 51 52 53 54 55 56 ``````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 Oct 03, 2016 57 58 59 60 61 ``````Lemma eq_None_not_Some {A} (mx : option A) : mx = None ↔ ¬is_Some mx. Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed. Lemma not_eq_None_Some {A} (mx : option A) : mx ≠ None ↔ is_Some mx. Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed. `````` Robbert Krebbers committed Mar 21, 2016 62 ``````Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx). `````` Robbert Krebbers committed Nov 11, 2015 63 ``````Proof. `````` Robbert Krebbers committed Mar 21, 2016 64 65 `````` set (P (mx : option A) := match mx with Some _ => True | _ => False end). set (f mx := match mx return P mx → is_Some mx with `````` Robbert Krebbers committed Nov 11, 2015 66 `````` Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end). `````` Robbert Krebbers committed Mar 21, 2016 67 68 69 70 `````` set (g mx (H : is_Some mx) := match H return P mx with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end). assert (∀ mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst). intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1. `````` Robbert Krebbers committed Nov 11, 2015 71 ``````Qed. `````` Robbert Krebbers committed Oct 03, 2016 72 `````` `````` Robbert Krebbers committed Mar 21, 2016 73 74 ``````Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) := match mx with `````` Robbert Krebbers committed Nov 11, 2015 75 76 77 78 `````` | Some x => left (ex_intro _ x eq_refl) | None => right is_Some_None end. `````` Robbert Krebbers committed Mar 21, 2016 79 80 ``````Definition is_Some_proj {A} {mx : option A} : is_Some mx → A := match mx with Some x => λ _, x | None => False_rect _ ∘ is_Some_None end. `````` Robbert Krebbers committed Oct 03, 2016 81 `````` `````` Robbert Krebbers committed Mar 21, 2016 82 83 84 ``````Definition Some_dec {A} (mx : option A) : { x | mx = Some x } + { mx = None } := match mx return { x | mx = Some x } + { mx = None } with | Some x => inleft (x ↾ eq_refl _) `````` Robbert Krebbers committed Nov 11, 2015 85 86 87 88 `````` | None => inright eq_refl end. (** Lifting a relation point-wise to option *) `````` Robbert Krebbers committed May 27, 2016 89 90 91 ``````Inductive option_Forall2 {A B} (R: A → B → Prop) : option A → option B → Prop := | Some_Forall2 x y : R x y → option_Forall2 R (Some x) (Some y) | None_Forall2 : option_Forall2 R None None. `````` Robbert Krebbers committed Nov 11, 2015 92 93 94 95 96 97 98 99 100 ``````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. `````` Robbert Krebbers committed May 27, 2016 101 102 103 104 105 106 107 108 109 110 111 112 113 ``````Section Forall2. Context {A} (R : relation A). Global Instance option_Forall2_refl : Reflexive R → Reflexive (option_Forall2 R). Proof. intros ? [?|]; by constructor. Qed. Global Instance option_Forall2_sym : Symmetric R → Symmetric (option_Forall2 R). Proof. destruct 2; by constructor. Qed. Global Instance option_Forall2_trans : Transitive R → Transitive (option_Forall2 R). Proof. destruct 2; inversion_clear 1; constructor; etrans; eauto. Qed. Global Instance option_Forall2_equiv : Equivalence R → Equivalence (option_Forall2 R). Proof. destruct 1; split; apply _. Qed. End Forall2. `````` Robbert Krebbers committed Nov 11, 2015 114 ``````(** Setoids *) `````` Robbert Krebbers committed May 27, 2016 115 116 ``````Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 (≡). `````` Robbert Krebbers committed Nov 11, 2015 117 ``````Section setoids. `````` Robbert Krebbers committed Jan 05, 2017 118 `````` Context `{Equiv A}. `````` Robbert Krebbers committed May 27, 2016 119 `````` Implicit Types mx my : option A. `````` Robbert Krebbers committed Mar 21, 2016 120 121 `````` Lemma equiv_option_Forall2 mx my : mx ≡ my ↔ option_Forall2 (≡) mx my. `````` Robbert Krebbers committed Jan 05, 2017 122 `````` Proof. done. Qed. `````` Robbert Krebbers committed Mar 21, 2016 123 `````` `````` Robbert Krebbers committed Jan 05, 2017 124 125 `````` Global Instance option_equivalence : Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (option A)). `````` Robbert Krebbers committed May 27, 2016 126 `````` Proof. apply _. Qed. `````` Robbert Krebbers committed Nov 11, 2015 127 `````` Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A). `````` Robbert Krebbers committed Jan 05, 2017 128 `````` Proof. by constructor. Qed. `````` Robbert Krebbers committed Sep 21, 2016 129 `````` Global Instance Some_equiv_inj : Inj (≡) (≡) (@Some A). `````` Robbert Krebbers committed Jan 05, 2017 130 `````` Proof. by inversion_clear 1. Qed. `````` Robbert Krebbers committed Nov 11, 2015 131 `````` Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A). `````` Robbert Krebbers committed Jan 05, 2017 132 `````` Proof. intros x y; destruct 1; f_equal; by apply leibniz_equiv. Qed. `````` Robbert Krebbers committed Mar 21, 2016 133 `````` `````` Robbert Krebbers committed May 27, 2016 134 `````` Lemma equiv_None mx : mx ≡ None ↔ mx = None. `````` Robbert Krebbers committed Jan 05, 2017 135 `````` Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed. `````` Robbert Krebbers committed May 27, 2016 136 `````` Lemma equiv_Some_inv_l mx my x : `````` Robbert Krebbers committed Nov 18, 2015 137 `````` mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y. `````` Robbert Krebbers committed Jan 05, 2017 138 `````` Proof. destruct 1; naive_solver. Qed. `````` Robbert Krebbers committed May 27, 2016 139 140 `````` Lemma equiv_Some_inv_r mx my y : mx ≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡ y. `````` Robbert Krebbers committed Jan 05, 2017 141 `````` Proof. destruct 1; naive_solver. Qed. `````` Robbert Krebbers committed May 27, 2016 142 `````` Lemma equiv_Some_inv_l' my x : Some x ≡ my → ∃ x', Some x' = my ∧ x ≡ x'. `````` Robbert Krebbers committed Jan 05, 2017 143 144 145 `````` Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed. Lemma equiv_Some_inv_r' `{!Equivalence ((≡) : relation A)} mx y : mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'. `````` Robbert Krebbers committed May 27, 2016 146 `````` Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed. `````` Robbert Krebbers committed Mar 21, 2016 147 `````` `````` Robbert Krebbers committed Jan 16, 2016 148 `````` Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A). `````` Robbert Krebbers committed Jan 05, 2017 149 `````` Proof. inversion_clear 1; split; eauto. Qed. `````` Robbert Krebbers committed May 27, 2016 150 151 152 `````` Global Instance from_option_proper {B} (R : relation B) (f : A → B) : Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f). Proof. destruct 3; simpl; auto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 153 154 ``````End setoids. `````` Robbert Krebbers committed May 27, 2016 155 156 ``````Typeclasses Opaque option_equiv. `````` Robbert Krebbers committed Nov 11, 2015 157 ``````(** Equality on [option] is decidable. *) `````` Robbert Krebbers committed Mar 21, 2016 158 159 160 161 ``````Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None) := match mx with Some _ => right (Some_ne_None _) | None => left eq_refl end. Instance option_None_eq_dec {A} (mx : option A) : Decision (None = mx) := match mx with Some _ => right (None_ne_Some _) | None => left eq_refl end. `````` Robbert Krebbers committed Sep 20, 2016 162 ``````Instance option_eq_dec `{dec : EqDecision A} : EqDecision (option A). `````` Robbert Krebbers committed Nov 11, 2015 163 ``````Proof. `````` Robbert Krebbers committed Sep 20, 2016 164 `````` refine (λ mx my, `````` Robbert Krebbers committed Mar 21, 2016 165 166 `````` match mx, my with | Some x, Some y => cast_if (decide (x = y)) `````` Robbert Krebbers committed Nov 11, 2015 167 `````` | None, None => left _ | _, _ => right _ `````` Robbert Krebbers committed Sep 20, 2016 168 `````` end); clear dec; abstract congruence. `````` Robbert Krebbers committed Nov 11, 2015 169 170 171 172 ``````Defined. (** * Monadic operations *) Instance option_ret: MRet option := @Some. `````` Robbert Krebbers committed Mar 21, 2016 173 174 175 176 ``````Instance option_bind: MBind option := λ A B f mx, match mx with Some x => f x | None => None end. Instance option_join: MJoin option := λ A mmx, match mmx with Some mx => mx | None => None end. `````` Robbert Krebbers committed Nov 11, 2015 177 ``````Instance option_fmap: FMap option := @option_map. `````` Robbert Krebbers committed Mar 21, 2016 178 179 ``````Instance option_guard: MGuard option := λ P dec A f, match dec with left H => f H | _ => None end. `````` Robbert Krebbers committed Nov 11, 2015 180 `````` `````` Robbert Krebbers committed Mar 21, 2016 181 182 183 184 185 ``````Lemma fmap_is_Some {A B} (f : A → B) mx : is_Some (f <\$> mx) ↔ is_Some mx. Proof. unfold is_Some; destruct mx; naive_solver. Qed. Lemma fmap_Some {A B} (f : A → B) mx y : f <\$> mx = Some y ↔ ∃ x, mx = Some x ∧ y = f x. Proof. destruct mx; naive_solver. Qed. `````` 186 ``````Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)} `````` Ralf Jung committed Nov 22, 2016 187 188 189 190 191 192 193 194 195 `````` (f : A → B) mx y : f <\$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x. Proof. destruct mx; simpl; split. - intros ?%Some_equiv_inj. eauto. - intros (? & ->%Some_inj & ?). constructor. done. - intros ?%symmetry%equiv_None. done. - intros (? & ? & ?). done. Qed. `````` Robbert Krebbers committed Dec 09, 2016 196 ``````Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)} `````` 197 198 `````` (f : A → B) mx y : f <\$> mx ≡ Some y → ∃ x, mx = Some x ∧ y ≡ f x. `````` Robbert Krebbers committed Dec 09, 2016 199 ``````Proof. by rewrite fmap_Some_equiv. Qed. `````` Robbert Krebbers committed Mar 21, 2016 200 201 202 203 204 205 206 207 208 209 ``````Lemma fmap_None {A B} (f : A → B) mx : f <\$> mx = None ↔ mx = None. Proof. by destruct mx. Qed. Lemma option_fmap_id {A} (mx : option A) : id <\$> mx = mx. Proof. by destruct mx. Qed. Lemma option_fmap_compose {A B} (f : A → B) {C} (g : B → C) mx : g ∘ f <\$> mx = g <\$> f <\$> mx. Proof. by destruct mx. Qed. Lemma option_fmap_ext {A B} (f g : A → B) mx : (∀ x, f x = g x) → f <\$> mx = g <\$> mx. Proof. intros; destruct mx; f_equal/=; auto. Qed. `````` 210 ``````Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A → B) mx : `````` Robbert Krebbers committed Mar 21, 2016 211 212 213 214 215 `````` (∀ x, f x ≡ g x) → f <\$> mx ≡ g <\$> mx. Proof. destruct mx; constructor; auto. Qed. Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx : (f <\$> mx) ≫= g = mx ≫= g ∘ f. Proof. by destruct mx. Qed. `````` Robbert Krebbers committed Nov 11, 2015 216 ``````Lemma option_bind_assoc {A B C} (f : A → option B) `````` Robbert Krebbers committed Mar 21, 2016 217 218 219 220 221 222 223 `````` (g : B → option C) (mx : option A) : (mx ≫= f) ≫= g = mx ≫= (mbind g ∘ f). Proof. by destruct mx; simpl. Qed. Lemma option_bind_ext {A B} (f g : A → option B) mx my : (∀ x, f x = g x) → mx = my → mx ≫= f = my ≫= g. Proof. destruct mx, my; naive_solver. Qed. Lemma option_bind_ext_fun {A B} (f g : A → option B) mx : (∀ x, f x = g x) → mx ≫= f = mx ≫= g. `````` Robbert Krebbers committed Nov 11, 2015 224 ``````Proof. intros. by apply option_bind_ext. Qed. `````` Robbert Krebbers committed Mar 21, 2016 225 226 227 228 229 230 231 232 ``````Lemma bind_Some {A B} (f : A → option B) (mx : option A) y : mx ≫= f = Some y ↔ ∃ x, mx = Some x ∧ f x = Some y. Proof. destruct mx; naive_solver. Qed. Lemma bind_None {A B} (f : A → option B) (mx : option A) : mx ≫= f = None ↔ mx = None ∨ ∃ x, mx = Some x ∧ f x = None. Proof. destruct mx; naive_solver. Qed. Lemma bind_with_Some {A} (mx : option A) : mx ≫= Some = mx. Proof. by destruct mx. Qed. `````` Robbert Krebbers committed Nov 11, 2015 233 `````` `````` Robbert Krebbers committed Jun 14, 2016 234 235 236 237 ``````Instance option_fmap_proper `{Equiv A, Equiv B} (f : A → B) : Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=option) f). Proof. destruct 2; constructor; auto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 ``````(** ** 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 *) `````` Robbert Krebbers committed Mar 21, 2016 266 267 268 269 270 ``````Instance option_union_with {A} : UnionWith A (option A) := λ f mx my, match mx, my with | Some x, Some y => f x y | Some x, None => Some x | None, Some y => Some y `````` Robbert Krebbers committed Nov 11, 2015 271 272 273 `````` | None, None => None end. Instance option_intersection_with {A} : IntersectionWith A (option A) := `````` Robbert Krebbers committed Mar 21, 2016 274 275 276 277 278 `````` λ f mx my, match mx, my with Some x, Some y => f x y | _, _ => None end. Instance option_difference_with {A} : DifferenceWith A (option A) := λ f mx my, match mx, my with | Some x, Some y => f x y | Some x, None => Some x `````` Robbert Krebbers committed Nov 11, 2015 279 280 281 `````` | None, _ => None end. Instance option_union {A} : Union (option A) := union_with (λ x _, Some x). `````` Robbert Krebbers committed Mar 21, 2016 282 283 284 285 `````` Lemma option_union_Some {A} (mx my : option A) z : mx ∪ my = Some z → mx = Some z ∨ my = Some z. Proof. destruct mx, my; naive_solver. Qed. `````` Robbert Krebbers committed Nov 11, 2015 286 `````` `````` Robbert Krebbers committed May 27, 2016 287 288 289 290 ``````Class DiagNone {A B C} (f : option A → option B → option C) := diag_none : f None None = None. Section union_intersection_difference. `````` Robbert Krebbers committed Nov 11, 2015 291 `````` Context {A} (f : A → A → option A). `````` Robbert Krebbers committed May 27, 2016 292 293 294 295 296 297 298 299 `````` Global Instance union_with_diag_none : DiagNone (union_with f). Proof. reflexivity. Qed. Global Instance intersection_with_diag_none : DiagNone (intersection_with f). Proof. reflexivity. Qed. Global Instance difference_with_diag_none : DiagNone (difference_with f). Proof. reflexivity. Qed. Global Instance union_with_left_id : LeftId (=) None (union_with f). `````` Robbert Krebbers committed Nov 11, 2015 300 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed May 27, 2016 301 `````` Global Instance union_with_right_id : RightId (=) None (union_with f). `````` Robbert Krebbers committed Nov 11, 2015 302 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed May 27, 2016 303 `````` Global Instance union_with_comm : Comm (=) f → Comm (=) (union_with f). `````` Robbert Krebbers committed Feb 11, 2016 304 `````` Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed. `````` Robbert Krebbers committed May 27, 2016 305 `````` Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f). `````` Robbert Krebbers committed Nov 11, 2015 306 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed May 27, 2016 307 `````` Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f). `````` Robbert Krebbers committed Nov 11, 2015 308 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed May 27, 2016 309 `````` Global Instance difference_with_comm : Comm (=) f → Comm (=) (intersection_with f). `````` Robbert Krebbers committed Feb 11, 2016 310 `````` Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed. `````` Robbert Krebbers committed May 27, 2016 311 `````` Global Instance difference_with_right_id : RightId (=) None (difference_with f). `````` Robbert Krebbers committed Nov 11, 2015 312 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed May 27, 2016 313 ``````End union_intersection_difference. `````` Robbert Krebbers committed Nov 11, 2015 314 315 316 317 `````` (** * Tactics *) Tactic Notation "case_option_guard" "as" ident(Hx) := match goal with `````` Robbert Krebbers committed Nov 16, 2016 318 `````` | H : context C [@mguard option _ ?P ?dec] |- _ => `````` Robbert Krebbers committed Mar 21, 2016 319 320 `````` change (@mguard option _ P dec) with (λ A (f : P → option A), match @decide P dec with left H' => f H' | _ => None end) in *; `````` Robbert Krebbers committed Nov 11, 2015 321 `````` destruct_decide (@decide P dec) as Hx `````` Robbert Krebbers committed Nov 16, 2016 322 `````` | |- context C [@mguard option _ ?P ?dec] => `````` Robbert Krebbers committed Mar 21, 2016 323 324 `````` change (@mguard option _ P dec) with (λ A (f : P → option A), match @decide P dec with left H' => f H' | _ => None end) in *; `````` Robbert Krebbers committed Nov 11, 2015 325 326 327 328 329 `````` destruct_decide (@decide P dec) as Hx end. Tactic Notation "case_option_guard" := let H := fresh in case_option_guard as H. `````` Robbert Krebbers committed Mar 21, 2016 330 331 ``````Lemma option_guard_True {A} P `{Decision P} (mx : option A) : P → guard P; mx = mx. `````` Robbert Krebbers committed Nov 11, 2015 332 ``````Proof. intros. by case_option_guard. Qed. `````` Robbert Krebbers committed Mar 21, 2016 333 334 ``````Lemma option_guard_False {A} P `{Decision P} (mx : option A) : ¬P → guard P; mx = None. `````` Robbert Krebbers committed Nov 11, 2015 335 ``````Proof. intros. by case_option_guard. Qed. `````` Robbert Krebbers committed Mar 21, 2016 336 337 ``````Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) : (P ↔ Q) → guard P; mx = guard Q; mx. `````` Robbert Krebbers committed Nov 11, 2015 338 339 ``````Proof. intros [??]. repeat case_option_guard; intuition. Qed. `````` Robbert Krebbers committed Jan 12, 2016 340 ``````Tactic Notation "simpl_option" "by" tactic3(tac) := `````` Robbert Krebbers committed Mar 21, 2016 341 `````` let assert_Some_None A mx H := first `````` Robbert Krebbers committed Nov 11, 2015 342 `````` [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; `````` Robbert Krebbers committed Mar 21, 2016 343 344 `````` assert (mx = Some x') as H by tac | assert (mx = None) as H by tac ] `````` Robbert Krebbers committed Nov 11, 2015 345 `````` in repeat match goal with `````` Robbert Krebbers committed Nov 16, 2016 346 `````` | H : context [@mret _ _ ?A] |- _ => `````` Robbert Krebbers committed Nov 11, 2015 347 `````` change (@mret _ _ A) with (@Some A) in H `````` Robbert Krebbers committed Nov 16, 2016 348 `````` | |- context [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A) `````` Robbert Krebbers committed Mar 21, 2016 349 350 351 352 `````` | H : context [mbind (M:=option) (A:=?A) ?f ?mx] |- _ => let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx | H : context [fmap (M:=option) (A:=?A) ?f ?mx] |- _ => let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx `````` Robbert Krebbers committed May 27, 2016 353 `````` | H : context [from_option (A:=?A) _ _ ?mx] |- _ => `````` Robbert Krebbers committed Mar 21, 2016 354 355 356 `````` let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx | H : context [ match ?mx with _ => _ end ] |- _ => match type of mx with `````` Robbert Krebbers committed Nov 11, 2015 357 `````` | option ?A => `````` Robbert Krebbers committed Mar 21, 2016 358 `````` let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx `````` Robbert Krebbers committed Nov 11, 2015 359 `````` end `````` Robbert Krebbers committed Mar 21, 2016 360 361 362 363 `````` | |- context [mbind (M:=option) (A:=?A) ?f ?mx] => let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx | |- context [fmap (M:=option) (A:=?A) ?f ?mx] => let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx `````` Robbert Krebbers committed May 27, 2016 364 `````` | |- context [from_option (A:=?A) _ _ ?mx] => `````` Robbert Krebbers committed Mar 21, 2016 365 366 367 `````` let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx | |- context [ match ?mx with _ => _ end ] => match type of mx with `````` Robbert Krebbers committed Nov 11, 2015 368 `````` | option ?A => `````` Robbert Krebbers committed Mar 21, 2016 369 `````` let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx `````` Robbert Krebbers committed Nov 11, 2015 370 371 372 373 374 375 376 377 378 `````` 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 379 380 381 382 `````` | 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 383 `````` end. `````` Robbert Krebbers committed Feb 17, 2016 384 ``````Tactic Notation "simplify_option_eq" "by" tactic3(tac) := `````` Robbert Krebbers committed Nov 11, 2015 385 `````` repeat match goal with `````` Robbert Krebbers committed Feb 17, 2016 386 `````` | _ => progress simplify_eq/= `````` Robbert Krebbers committed Jan 12, 2016 387 `````` | _ => progress simpl_option by tac `````` Robbert Krebbers committed Nov 11, 2015 388 389 390 391 392 `````` | _ : 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 `````` Robbert Krebbers committed Mar 21, 2016 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 `````` | H : mbind (M:=option) ?f ?mx = ?my |- _ => match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end; match my with Some _ => idtac | None => idtac | _ => fail 1 end; let x := fresh in destruct mx as [x|] eqn:?; [change (f x = my) in H|change (None = my) in H] | H : ?my = mbind (M:=option) ?f ?mx |- _ => match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end; match my with Some _ => idtac | None => idtac | _ => fail 1 end; let x := fresh in destruct mx as [x|] eqn:?; [change (my = f x) in H|change (my = None) in H] | H : fmap (M:=option) ?f ?mx = ?my |- _ => match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end; match my with Some _ => idtac | None => idtac | _ => fail 1 end; let x := fresh in destruct mx as [x|] eqn:?; [change (Some (f x) = my) in H|change (None = my) in H] | H : ?my = fmap (M:=option) ?f ?mx |- _ => match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end; match my with Some _ => idtac | None => idtac | _ => fail 1 end; let x := fresh in destruct mx as [x|] eqn:?; [change (my = Some (f x)) in H|change (my = None) in H] `````` Robbert Krebbers committed Nov 11, 2015 413 414 415 `````` | _ => progress case_decide | _ => progress case_option_guard end. `````` Robbert Krebbers committed Feb 17, 2016 416 ``Tactic Notation "simplify_option_eq" := simplify_option_eq by eauto.``