option.v 8.93 KB
 Robbert Krebbers committed Aug 29, 2012 1 2 3 4 ``````(* Copyright (c) 2012, 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 Oct 19, 2012 5 ``````Require Export base tactics decidable. `````` Robbert Krebbers committed Aug 29, 2012 6 7 8 `````` (** * General definitions and theorems *) (** Basic properties about equality. *) `````` Robbert Krebbers committed Jun 11, 2012 9 10 11 12 13 14 ``````Lemma None_ne_Some `(a : A) : None ≠ Some a. Proof. congruence. Qed. Lemma Some_ne_None `(a : A) : Some a ≠ None. Proof. congruence. Qed. Lemma eq_None_ne_Some `(x : option A) a : x = None → x ≠ Some a. Proof. congruence. Qed. `````` Robbert Krebbers committed Aug 21, 2012 15 ``````Instance Some_inj {A} : Injective (=) (=) (@Some A). `````` Robbert Krebbers committed Jun 11, 2012 16 17 ``````Proof. congruence. Qed. `````` Robbert Krebbers committed Aug 29, 2012 18 19 ``````(** The non dependent elimination principle on the option type. *) Definition option_case {A B} (f : A → B) (b : B) (x : option A) : B := `````` Robbert Krebbers committed Jun 11, 2012 20 21 22 23 24 `````` match x with | None => b | Some a => f a end. `````` Robbert Krebbers committed Jan 05, 2013 25 26 27 ``````(** 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 Aug 21, 2012 28 29 `````` match x with | None => a `````` Robbert Krebbers committed Aug 29, 2012 30 `````` | Some b => b `````` Robbert Krebbers committed Aug 21, 2012 31 32 `````` end. `````` Robbert Krebbers committed Aug 29, 2012 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 Jun 11, 2012 35 36 37 38 ``````Lemma option_eq {A} (x y : option A) : x = y ↔ ∀ a, x = Some a ↔ y = Some a. Proof. split. `````` Robbert Krebbers committed Oct 19, 2012 39 `````` { intros. by subst. } `````` Robbert Krebbers committed Aug 29, 2012 40 `````` intros E. destruct x, y. `````` Robbert Krebbers committed Oct 19, 2012 41 42 43 44 `````` + by apply E. + symmetry. by apply E. + by apply E. + done. `````` Robbert Krebbers committed Jun 11, 2012 45 46 ``````Qed. `````` Robbert Krebbers committed Nov 12, 2012 47 48 ``````Inductive is_Some {A} : option A → Prop := make_is_Some x : is_Some (Some x). `````` Robbert Krebbers committed Jun 11, 2012 49 `````` `````` Robbert Krebbers committed Nov 12, 2012 50 51 52 53 54 55 56 57 58 59 60 ``````Lemma make_is_Some_alt `(x : option A) a : x = Some a → is_Some x. Proof. intros. by subst. Qed. Hint Resolve make_is_Some_alt. Lemma is_Some_None {A} : ¬is_Some (@None A). Proof. by inversion 1. Qed. Hint Resolve is_Some_None. Lemma is_Some_alt `(x : option A) : is_Some x ↔ ∃ y, x = Some y. Proof. split. inversion 1; eauto. intros [??]. by subst. Qed. Ltac inv_is_Some := repeat `````` Robbert Krebbers committed Jun 11, 2012 61 `````` match goal with `````` Robbert Krebbers committed Nov 12, 2012 62 `````` | H : is_Some _ |- _ => inversion H; clear H; subst `````` Robbert Krebbers committed Aug 21, 2012 63 `````` end. `````` Robbert Krebbers committed Jun 11, 2012 64 `````` `````` Robbert Krebbers committed Jan 05, 2013 65 ``````Definition is_Some_proj `{x : option A} : is_Some x → A := `````` Robbert Krebbers committed Jun 11, 2012 66 `````` match x with `````` Robbert Krebbers committed Jan 05, 2013 67 `````` | Some a => λ _, a `````` Robbert Krebbers committed Nov 12, 2012 68 69 `````` | None => False_rect _ ∘ is_Some_None end. `````` Robbert Krebbers committed Jan 05, 2013 70 71 72 73 74 ``````Definition Some_dec `(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. `````` Robbert Krebbers committed Nov 12, 2012 75 76 77 78 ``````Instance is_Some_dec `(x : option A) : Decision (is_Some x) := match x with | Some x => left (make_is_Some x) | None => right is_Some_None `````` Robbert Krebbers committed Jun 11, 2012 79 `````` end. `````` Robbert Krebbers committed Jan 05, 2013 80 81 82 83 84 ``````Instance None_dec `(x : option A) : Decision (x = None) := match x with | Some x => right (Some_ne_None x) | None => left eq_refl end. `````` Robbert Krebbers committed Jun 11, 2012 85 86 `````` Lemma eq_None_not_Some `(x : option A) : x = None ↔ ¬is_Some x. `````` Robbert Krebbers committed Nov 12, 2012 87 88 ``````Proof. split. by destruct 2. destruct x. by intros []. done. Qed. Lemma not_eq_None_Some `(x : option A) : x ≠ None ↔ is_Some x. `````` Robbert Krebbers committed Jan 05, 2013 89 ``````Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 90 `````` `````` Robbert Krebbers committed Aug 29, 2012 91 ``````Lemma make_eq_Some {A} (x : option A) a : `````` Robbert Krebbers committed Jun 11, 2012 92 `````` is_Some x → (∀ b, x = Some b → b = a) → x = Some a. `````` Robbert Krebbers committed Nov 12, 2012 93 ``````Proof. destruct 1. intros. f_equal. auto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 94 `````` `````` Robbert Krebbers committed Aug 29, 2012 95 96 97 ``````(** Equality on [option] is decidable. *) Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)} (x y : option A) : Decision (x = y) := `````` Robbert Krebbers committed Jun 11, 2012 98 99 100 101 `````` match x with | Some a => match y with | Some b => `````` Robbert Krebbers committed Jan 05, 2013 102 103 104 105 `````` match dec a b with | left H => left (f_equal _ H) | right H => right (H ∘ injective Some _ _) end `````` Robbert Krebbers committed Jun 11, 2012 106 107 108 `````` | None => right (Some_ne_None _) end | None => `````` Robbert Krebbers committed Jan 05, 2013 109 110 111 112 `````` match y with | Some _ => right (None_ne_Some _) | None => left eq_refl end `````` Robbert Krebbers committed Jun 11, 2012 113 114 `````` end. `````` Robbert Krebbers committed Aug 29, 2012 115 ``````(** * Monadic operations *) `````` Robbert Krebbers committed Nov 12, 2012 116 117 ``````Instance option_ret: MRet option := @Some. Instance option_bind: MBind option := λ A B f x, `````` Robbert Krebbers committed Jun 11, 2012 118 119 120 121 `````` match x with | Some a => f a | None => None end. `````` Robbert Krebbers committed Nov 12, 2012 122 ``````Instance option_join: MJoin option := λ A x, `````` Robbert Krebbers committed Jun 11, 2012 123 124 125 126 `````` match x with | Some x => x | None => None end. `````` Robbert Krebbers committed Nov 12, 2012 127 128 129 ``````Instance option_fmap: FMap option := @option_map. Instance option_guard: MGuard option := λ P dec A x, if dec then x else None. `````` Robbert Krebbers committed Jun 11, 2012 130 `````` `````` Robbert Krebbers committed Aug 21, 2012 131 132 ``````Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) : is_Some x ↔ is_Some (f <\$> x). `````` Robbert Krebbers committed Nov 12, 2012 133 ``````Proof. split; inversion 1. done. by destruct x. Qed. `````` Robbert Krebbers committed Aug 21, 2012 134 135 ``````Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) : x = None ↔ f <\$> x = None. `````` Robbert Krebbers committed Nov 12, 2012 136 ``````Proof. unfold fmap, option_fmap. by destruct x. Qed. `````` Robbert Krebbers committed Jun 11, 2012 137 `````` `````` Robbert Krebbers committed Jan 05, 2013 138 139 140 141 ``````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. `````` Robbert Krebbers committed Nov 12, 2012 142 ``````Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat `````` Robbert Krebbers committed Aug 29, 2012 143 `````` match goal with `````` Robbert Krebbers committed Oct 19, 2012 144 `````` | _ => first [progress simpl in * | progress simplify_equality] `````` Robbert Krebbers committed Jan 05, 2013 145 `````` | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ => `````` Robbert Krebbers committed Oct 19, 2012 146 `````` let Hx := fresh in `````` Robbert Krebbers committed Jan 05, 2013 147 148 149 150 151 `````` first [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; assert (o = Some x') as Hx by tac | assert (o = None) as Hx by tac ]; `````` Robbert Krebbers committed Oct 19, 2012 152 `````` rewrite Hx in H; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 `````` | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ => let Hx := fresh in first [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; assert (o = Some x') as Hx by tac | assert (o = None) as Hx by tac ]; rewrite Hx in H; clear Hx | H : context [ match ?o with _ => _ end ] |- _ => match type of o with | option ?A => let Hx := fresh in first [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; assert (o = Some x') as Hx by tac | assert (o = None) as Hx by tac ]; rewrite Hx in H; clear Hx end `````` Robbert Krebbers committed Aug 29, 2012 172 `````` | H : mbind (M:=option) ?f ?o = ?x |- _ => `````` Robbert Krebbers committed Oct 19, 2012 173 174 `````` match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match x with Some _ => idtac | None => idtac | _ => fail 1 end; `````` Robbert Krebbers committed Aug 29, 2012 175 `````` destruct o eqn:? `````` Robbert Krebbers committed Jan 05, 2013 176 177 178 179 180 181 182 183 184 185 186 187 188 `````` | 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; destruct o eqn:? | 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; destruct o eqn:? | 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; destruct o eqn:? | |- context [mbind (M:=option) (A:=?A) ?f ?o] => `````` Robbert Krebbers committed Oct 19, 2012 189 `````` let Hx := fresh in `````` Robbert Krebbers committed Jan 05, 2013 190 191 192 193 194 `````` first [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; assert (o = Some x') as Hx by tac | assert (o = None) as Hx by tac ]; `````` Robbert Krebbers committed Oct 19, 2012 195 `````` rewrite Hx; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 `````` | |- context [fmap (M:=option) (A:=?A) ?f ?o] => let Hx := fresh in first [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; assert (o = Some x') as Hx by tac | assert (o = None) as Hx by tac ]; rewrite Hx; clear Hx | |- context [ match ?o with _ => _ end ] => match type of o with | option ?A => let Hx := fresh in first [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; assert (o = Some x') as Hx by tac | assert (o = None) as Hx by tac ]; rewrite Hx; clear Hx end `````` Robbert Krebbers committed Nov 12, 2012 215 216 217 218 219 220 `````` | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ => let X := context C [ if dec then x else None ] in change X in H; destruct dec | |- context C [@mguard option _ ?P ?dec _ ?x] => let X := context C [ if dec then x else None ] in change X; destruct dec `````` Robbert Krebbers committed Jan 05, 2013 221 222 223 224 `````` | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ => assert (y = x) by congruence; clear H2 | H1 : ?o = Some ?x, H2 : ?o = None |- _ => congruence `````` Robbert Krebbers committed Aug 29, 2012 225 `````` end. `````` Robbert Krebbers committed Jan 05, 2013 226 227 228 229 ``````Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto. Hint Extern 100 => simplify_option_equality : simplify_option_equality. `````` Robbert Krebbers committed Aug 29, 2012 230 231 `````` (** * Union, intersection and difference *) `````` Robbert Krebbers committed Jan 05, 2013 232 ``````Instance option_union_with {A} : UnionWith A (option A) := λ f x y, `````` Robbert Krebbers committed Jun 11, 2012 233 `````` match x, y with `````` Robbert Krebbers committed Jan 05, 2013 234 `````` | Some a, Some b => f a b `````` Robbert Krebbers committed Jun 11, 2012 235 236 237 238 `````` | Some a, None => Some a | None, Some b => Some b | None, None => None end. `````` Robbert Krebbers committed Jan 05, 2013 239 240 ``````Instance option_intersection_with {A} : IntersectionWith A (option A) := λ f x y, `````` Robbert Krebbers committed Jun 11, 2012 241 `````` match x, y with `````` Robbert Krebbers committed Jan 05, 2013 242 `````` | Some a, Some b => f a b `````` Robbert Krebbers committed Jun 11, 2012 243 244 `````` | _, _ => None end. `````` Robbert Krebbers committed Jan 05, 2013 245 246 ``````Instance option_difference_with {A} : DifferenceWith A (option A) := λ f x y, `````` Robbert Krebbers committed Aug 21, 2012 247 248 249 250 251 `````` match x, y with | Some a, Some b => f a b | Some a, None => Some a | None, _ => None end. `````` Robbert Krebbers committed Jun 11, 2012 252 `````` `````` Robbert Krebbers committed Jan 05, 2013 253 254 ``````Section option_union_intersection_difference. Context {A} (f : A → A → option A). `````` Robbert Krebbers committed Jun 11, 2012 255 256 `````` Global Instance: LeftId (=) None (union_with f). `````` Robbert Krebbers committed Oct 19, 2012 257 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jun 11, 2012 258 `````` Global Instance: RightId (=) None (union_with f). `````` Robbert Krebbers committed Oct 19, 2012 259 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jun 11, 2012 260 `````` Global Instance: Commutative (=) f → Commutative (=) (union_with f). `````` Robbert Krebbers committed Jan 05, 2013 261 `````` Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. `````` Robbert Krebbers committed Aug 29, 2012 262 `````` Global Instance: Commutative (=) f → Commutative (=) (intersection_with f). `````` Robbert Krebbers committed Jan 05, 2013 263 `````` Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. `````` Robbert Krebbers committed Aug 21, 2012 264 `````` Global Instance: RightId (=) None (difference_with f). `````` Robbert Krebbers committed Oct 19, 2012 265 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jan 05, 2013 266 ``End option_union_intersection_difference.``