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