option.v 7 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 Aug 29, 2012 25 26 27 ``````(** The [maybe] function allows us to get the value out of the option type by specifying a default value. *) Definition maybe {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 Aug 29, 2012 65 ``````Definition is_Some_sigT `(x : option A) : is_Some x → { a | x = Some a } := `````` Robbert Krebbers committed Jun 11, 2012 66 `````` match x with `````` Robbert Krebbers committed Nov 12, 2012 67 68 69 70 71 72 73 74 `````` | None => False_rect _ ∘ is_Some_None | Some a => λ _, a ↾ eq_refl end. 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 75 76 77 `````` end. Lemma eq_None_not_Some `(x : option A) : x = None ↔ ¬is_Some x. `````` Robbert Krebbers committed Nov 12, 2012 78 79 80 ``````Proof. split. by destruct 2. destruct x. by intros []. done. Qed. Lemma not_eq_None_Some `(x : option A) : x ≠ None ↔ is_Some x. Proof. rewrite eq_None_not_Some. intuition auto using dec_stable. Qed. `````` Robbert Krebbers committed Jun 11, 2012 81 `````` `````` Robbert Krebbers committed Aug 29, 2012 82 ``````Lemma make_eq_Some {A} (x : option A) a : `````` Robbert Krebbers committed Jun 11, 2012 83 `````` is_Some x → (∀ b, x = Some b → b = a) → x = Some a. `````` Robbert Krebbers committed Nov 12, 2012 84 ``````Proof. destruct 1. intros. f_equal. auto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 85 `````` `````` Robbert Krebbers committed Aug 29, 2012 86 87 88 ``````(** 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 89 90 91 92 93 94 `````` match x with | Some a => match y with | Some b => match dec a b with | left H => left (f_equal _ H) `````` Robbert Krebbers committed Aug 21, 2012 95 `````` | right H => right (H ∘ injective Some _ _) `````` Robbert Krebbers committed Jun 11, 2012 96 97 98 99 100 101 102 103 104 105 `````` end | None => right (Some_ne_None _) end | None => match y with | Some _ => right (None_ne_Some _) | None => left eq_refl end end. `````` Robbert Krebbers committed Aug 29, 2012 106 ``````(** * Monadic operations *) `````` Robbert Krebbers committed Nov 12, 2012 107 108 ``````Instance option_ret: MRet option := @Some. Instance option_bind: MBind option := λ A B f x, `````` Robbert Krebbers committed Jun 11, 2012 109 110 111 112 `````` match x with | Some a => f a | None => None end. `````` Robbert Krebbers committed Nov 12, 2012 113 ``````Instance option_join: MJoin option := λ A x, `````` Robbert Krebbers committed Jun 11, 2012 114 115 116 117 `````` match x with | Some x => x | None => None end. `````` Robbert Krebbers committed Nov 12, 2012 118 119 120 ``````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 121 `````` `````` Robbert Krebbers committed Aug 21, 2012 122 123 ``````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 124 ``````Proof. split; inversion 1. done. by destruct x. Qed. `````` Robbert Krebbers committed Aug 21, 2012 125 126 ``````Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) : x = None ↔ f <\$> x = None. `````` Robbert Krebbers committed Nov 12, 2012 127 ``````Proof. unfold fmap, option_fmap. by destruct x. Qed. `````` Robbert Krebbers committed Jun 11, 2012 128 `````` `````` Robbert Krebbers committed Nov 12, 2012 129 ``````Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat `````` Robbert Krebbers committed Aug 29, 2012 130 `````` match goal with `````` Robbert Krebbers committed Oct 19, 2012 131 132 133 134 135 136 137 `````` | _ => first [progress simpl in * | progress simplify_equality] | H : mbind (M:=option) (A:=?A) ?f ?o = ?x |- _ => let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; let Hx := fresh in assert (o = Some x') as Hx by tac; rewrite Hx in H; clear Hx `````` Robbert Krebbers committed Aug 29, 2012 138 `````` | H : mbind (M:=option) ?f ?o = ?x |- _ => `````` Robbert Krebbers committed Oct 19, 2012 139 140 `````` 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 141 `````` destruct o eqn:? `````` Robbert Krebbers committed Oct 19, 2012 142 143 144 145 146 147 `````` | |- mbind (M:=option) (A:=?A) ?f ?o = ?x => let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x; let Hx := fresh in assert (o = Some x') as Hx by tac; rewrite Hx; clear Hx `````` Robbert Krebbers committed Nov 12, 2012 148 149 150 151 152 153 `````` | 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 Aug 29, 2012 154 `````` end. `````` Robbert Krebbers committed Nov 12, 2012 155 ``````Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto. `````` Robbert Krebbers committed Aug 29, 2012 156 157 `````` (** * Union, intersection and difference *) `````` Robbert Krebbers committed Jun 11, 2012 158 159 160 161 162 163 164 ``````Instance option_union: UnionWith option := λ A f x y, match x, y with | Some a, Some b => Some (f a b) | Some a, None => Some a | None, Some b => Some b | None, None => None end. `````` Robbert Krebbers committed Aug 21, 2012 165 ``````Instance option_intersection: IntersectionWith option := λ A f x y, `````` Robbert Krebbers committed Jun 11, 2012 166 167 168 169 `````` match x, y with | Some a, Some b => Some (f a b) | _, _ => None end. `````` Robbert Krebbers committed Aug 21, 2012 170 171 172 173 174 175 ``````Instance option_difference: DifferenceWith option := λ A f x y, 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 176 `````` `````` Robbert Krebbers committed Aug 21, 2012 177 ``````Section option_union_intersection. `````` Robbert Krebbers committed Jun 11, 2012 178 179 180 `````` Context {A} (f : A → A → A). Global Instance: LeftId (=) None (union_with f). `````` Robbert Krebbers committed Oct 19, 2012 181 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jun 11, 2012 182 `````` Global Instance: RightId (=) None (union_with f). `````` Robbert Krebbers committed Oct 19, 2012 183 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jun 11, 2012 184 `````` Global Instance: Commutative (=) f → Commutative (=) (union_with f). `````` Robbert Krebbers committed Aug 29, 2012 185 186 `````` Proof. intros ? [?|] [?|]; compute; try reflexivity. `````` Robbert Krebbers committed Oct 19, 2012 187 `````` by rewrite (commutative f). `````` Robbert Krebbers committed Aug 29, 2012 188 `````` Qed. `````` Robbert Krebbers committed Jun 11, 2012 189 `````` Global Instance: Associative (=) f → Associative (=) (union_with f). `````` Robbert Krebbers committed Aug 29, 2012 190 191 `````` Proof. intros ? [?|] [?|] [?|]; compute; try reflexivity. `````` Robbert Krebbers committed Oct 19, 2012 192 `````` by rewrite (associative f). `````` Robbert Krebbers committed Aug 29, 2012 193 `````` Qed. `````` Robbert Krebbers committed Jun 11, 2012 194 `````` Global Instance: Idempotent (=) f → Idempotent (=) (union_with f). `````` Robbert Krebbers committed Aug 29, 2012 195 196 `````` Proof. intros ? [?|]; compute; try reflexivity. `````` Robbert Krebbers committed Oct 19, 2012 197 `````` by rewrite (idempotent f). `````` Robbert Krebbers committed Aug 29, 2012 198 199 200 201 202 `````` Qed. Global Instance: Commutative (=) f → Commutative (=) (intersection_with f). Proof. intros ? [?|] [?|]; compute; try reflexivity. `````` Robbert Krebbers committed Oct 19, 2012 203 `````` by rewrite (commutative f). `````` Robbert Krebbers committed Aug 29, 2012 204 205 206 207 `````` Qed. Global Instance: Associative (=) f → Associative (=) (intersection_with f). Proof. intros ? [?|] [?|] [?|]; compute; try reflexivity. `````` Robbert Krebbers committed Oct 19, 2012 208 `````` by rewrite (associative f). `````` Robbert Krebbers committed Aug 29, 2012 209 210 211 212 `````` Qed. Global Instance: Idempotent (=) f → Idempotent (=) (intersection_with f). Proof. intros ? [?|]; compute; try reflexivity. `````` Robbert Krebbers committed Oct 19, 2012 213 `````` by rewrite (idempotent f). `````` Robbert Krebbers committed Aug 29, 2012 214 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 215 216 217 218 219 220 ``````End option_union_intersection. Section option_difference. Context {A} (f : A → A → option A). Global Instance: RightId (=) None (difference_with f). `````` Robbert Krebbers committed Oct 19, 2012 221 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Aug 21, 2012 222 ``End option_difference.``