option.v 11.1 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 Feb 22, 2013 95 96 97 98 99 100 101 102 ``````Definition mapM `{!MBind M} `{!MRet M} {A B} (f : A → M B) : list A → M (list B) := fix go l := match l with | [] => mret [] | x :: l => y ← f x; k ← go l; mret (y :: k) end. `````` Robbert Krebbers committed May 15, 2013 103 104 105 ``````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 106 `````` f <\$> x = Some y ↔ ∃ x', x = Some x' ∧ y = f x'. `````` Robbert Krebbers committed May 15, 2013 107 108 109 ``````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 110 `````` `````` Robbert Krebbers committed May 07, 2013 111 ``````Lemma option_fmap_id {A} (x : option A) : id <\$> x = x. `````` Robbert Krebbers committed Feb 19, 2013 112 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Jan 05, 2013 113 ``````Lemma option_bind_assoc {A B C} (f : A → option B) `````` Robbert Krebbers committed May 15, 2013 114 `````` (g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f). `````` Robbert Krebbers committed Jan 05, 2013 115 ``````Proof. by destruct x; simpl. Qed. `````` Robbert Krebbers committed Feb 22, 2013 116 ``````Lemma option_bind_ext {A B} (f g : A → option B) x y : `````` Robbert Krebbers committed May 07, 2013 117 `````` (∀ a, f a = g a) → x = y → x ≫= f = y ≫= g. `````` Robbert Krebbers committed Feb 22, 2013 118 119 ``````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 120 `````` (∀ a, f a = g a) → x ≫= f = x ≫= g. `````` Robbert Krebbers committed Feb 22, 2013 121 122 123 124 125 ``````Proof. intros. by apply option_bind_ext. Qed. Section mapM. Context {A B : Type} (f : A → option B). `````` Robbert Krebbers committed May 07, 2013 126 `````` Lemma mapM_ext (g : A → option B) l : (∀ x, f x = g x) → mapM f l = mapM g l. `````` Robbert Krebbers committed Feb 22, 2013 127 128 129 `````` Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed. Lemma Forall2_mapM_ext (g : A → option B) l k : Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k. `````` Robbert Krebbers committed May 07, 2013 130 `````` Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed. `````` Robbert Krebbers committed Feb 22, 2013 131 132 `````` Lemma Forall_mapM_ext (g : A → option B) l : Forall (λ x, f x = g x) l → mapM f l = mapM g l. `````` Robbert Krebbers committed May 07, 2013 133 `````` Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed. `````` Robbert Krebbers committed Feb 22, 2013 134 `````` `````` Robbert Krebbers committed May 07, 2013 135 `````` Lemma mapM_Some_1 l k : mapM f l = Some k → Forall2 (λ x y, f x = Some y) l k. `````` Robbert Krebbers committed Feb 22, 2013 136 137 138 139 140 141 `````` Proof. revert k. induction l as [|x l]; intros [|y k]; simpl; try done. * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l). * destruct (f x) eqn:?; simpl; [|discriminate]. destruct (mapM f l); intros; simplify_equality. constructor; auto. Qed. `````` Robbert Krebbers committed May 07, 2013 142 `````` Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k. `````` Robbert Krebbers committed Feb 22, 2013 143 144 145 146 `````` Proof. induction 1 as [|???? Hf ? IH]; simpl; [done |]. rewrite Hf. simpl. by rewrite IH. Qed. `````` Robbert Krebbers committed May 07, 2013 147 `````` Lemma mapM_Some l k : mapM f l = Some k ↔ Forall2 (λ x y, f x = Some y) l k. `````` Robbert Krebbers committed Feb 22, 2013 148 149 `````` Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed. End mapM. `````` Robbert Krebbers committed Jan 05, 2013 150 `````` `````` Robbert Krebbers committed Nov 12, 2012 151 ``````Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat `````` Robbert Krebbers committed Aug 29, 2012 152 `````` match goal with `````` Robbert Krebbers committed May 07, 2013 153 `````` | _ => progress (unfold default in *) `````` Robbert Krebbers committed Oct 19, 2012 154 `````` | _ => first [progress simpl in * | progress simplify_equality] `````` Robbert Krebbers committed Jan 05, 2013 155 `````` | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ => `````` Robbert Krebbers committed Oct 19, 2012 156 `````` let Hx := fresh in `````` Robbert Krebbers committed Jan 05, 2013 157 158 159 160 161 `````` 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 162 `````` rewrite Hx in H; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 `````` | 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 182 `````` | H : mbind (M:=option) ?f ?o = ?x |- _ => `````` Robbert Krebbers committed Oct 19, 2012 183 184 `````` 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 185 `````` destruct o eqn:? `````` Robbert Krebbers committed Jan 05, 2013 186 187 188 189 190 191 192 193 194 195 196 197 198 `````` | 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 199 `````` let Hx := fresh in `````` Robbert Krebbers committed Jan 05, 2013 200 201 202 203 204 `````` 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 205 `````` rewrite Hx; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 `````` | |- 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 225 `````` | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ => `````` Robbert Krebbers committed May 07, 2013 226 `````` let X := context C [ match dec with left H => x H | _ => None end ] in `````` Robbert Krebbers committed Feb 19, 2013 227 `````` change X in H; destruct_decide dec `````` Robbert Krebbers committed Nov 12, 2012 228 `````` | |- context C [@mguard option _ ?P ?dec _ ?x] => `````` Robbert Krebbers committed May 07, 2013 229 `````` let X := context C [ match dec with left H => x H | _ => None end ] in `````` Robbert Krebbers committed Feb 19, 2013 230 `````` change X; destruct_decide dec `````` Robbert Krebbers committed Jan 05, 2013 231 232 233 234 `````` | 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 Feb 22, 2013 235 `````` | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H `````` Robbert Krebbers committed Aug 29, 2012 236 `````` end. `````` Robbert Krebbers committed Jan 05, 2013 237 238 239 ``````Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto. `````` Robbert Krebbers committed Feb 22, 2013 240 241 ``````Hint Extern 800 => progress simplify_option_equality : simplify_option_equality. `````` Robbert Krebbers committed Aug 29, 2012 242 243 `````` (** * Union, intersection and difference *) `````` Robbert Krebbers committed Jan 05, 2013 244 ``````Instance option_union_with {A} : UnionWith A (option A) := λ f x y, `````` Robbert Krebbers committed Jun 11, 2012 245 `````` match x, y with `````` Robbert Krebbers committed Jan 05, 2013 246 `````` | Some a, Some b => f a b `````` Robbert Krebbers committed Jun 11, 2012 247 248 249 250 `````` | Some a, None => Some a | None, Some b => Some b | None, None => None end. `````` Robbert Krebbers committed May 07, 2013 251 252 253 ``````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 254 255 256 257 258 `````` 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 259 `````` `````` Robbert Krebbers committed Jan 05, 2013 260 261 ``````Section option_union_intersection_difference. Context {A} (f : A → A → option A). `````` Robbert Krebbers committed Jun 11, 2012 262 263 `````` Global Instance: LeftId (=) None (union_with f). `````` Robbert Krebbers committed Oct 19, 2012 264 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jun 11, 2012 265 `````` Global Instance: RightId (=) None (union_with f). `````` Robbert Krebbers committed Oct 19, 2012 266 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jun 11, 2012 267 `````` Global Instance: Commutative (=) f → Commutative (=) (union_with f). `````` Robbert Krebbers committed Jan 05, 2013 268 `````` Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. `````` Robbert Krebbers committed Feb 19, 2013 269 270 271 272 273 `````` 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 274 `````` Global Instance: Commutative (=) f → Commutative (=) (intersection_with f). `````` Robbert Krebbers committed Jan 05, 2013 275 `````` Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. `````` Robbert Krebbers committed Feb 19, 2013 276 `````` `````` Robbert Krebbers committed Aug 21, 2012 277 `````` Global Instance: RightId (=) None (difference_with f). `````` Robbert Krebbers committed Oct 19, 2012 278 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jan 05, 2013 279 ``End option_union_intersection_difference.``