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