option.v 11.4 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 Jun 11, 2012 29 30 31 ``````Lemma option_eq {A} (x y : option A) : x = y ↔ ∀ a, x = Some a ↔ y = Some a. Proof. `````` Robbert Krebbers committed May 07, 2013 32 `````` split; [by intros; by subst |]. intros E. destruct x, y. `````` Robbert Krebbers committed Oct 19, 2012 33 34 35 36 `````` + by apply E. + symmetry. by apply E. + by apply E. + done. `````` Robbert Krebbers committed Jun 11, 2012 37 38 ``````Qed. `````` Robbert Krebbers committed Nov 12, 2012 39 ``````Inductive is_Some {A} : option A → Prop := `````` Robbert Krebbers committed May 07, 2013 40 `````` mk_is_Some x : is_Some (Some x). `````` Robbert Krebbers committed Jun 11, 2012 41 `````` `````` Robbert Krebbers committed Mar 25, 2013 42 43 44 45 ``````Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x). Proof. intros [?] p2. by refine match p2 in is_Some o return `````` Robbert Krebbers committed May 07, 2013 46 47 `````` match o with Some y => (mk_is_Some y =) | _ => λ _, False end p2 with mk_is_Some y => _ end. `````` Robbert Krebbers committed Mar 25, 2013 48 49 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 50 ``````Lemma mk_is_Some_alt `(x : option A) a : x = Some a → is_Some x. `````` Robbert Krebbers committed Nov 12, 2012 51 ``````Proof. intros. by subst. Qed. `````` Robbert Krebbers committed May 07, 2013 52 ``````Hint Resolve mk_is_Some_alt. `````` Robbert Krebbers committed Nov 12, 2012 53 54 55 56 57 58 59 60 ``````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 May 07, 2013 61 `````` match goal with H : is_Some _ |- _ => inversion H; clear H; subst end. `````` Robbert Krebbers committed Jun 11, 2012 62 `````` `````` Robbert Krebbers committed Jan 05, 2013 63 ``````Definition is_Some_proj `{x : option A} : is_Some x → A := `````` Robbert Krebbers committed Jun 11, 2012 64 `````` match x with `````` Robbert Krebbers committed Jan 05, 2013 65 `````` | Some a => λ _, a `````` Robbert Krebbers committed Nov 12, 2012 66 67 `````` | None => False_rect _ ∘ is_Some_None end. `````` Robbert Krebbers committed Jan 05, 2013 68 69 70 71 72 ``````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 73 74 ``````Instance is_Some_dec `(x : option A) : Decision (is_Some x) := match x with `````` Robbert Krebbers committed May 07, 2013 75 `````` | Some x => left (mk_is_Some x) `````` Robbert Krebbers committed Nov 12, 2012 76 `````` | None => right is_Some_None `````` Robbert Krebbers committed Jun 11, 2012 77 `````` end. `````` Robbert Krebbers committed Jan 05, 2013 78 79 80 81 82 ``````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 83 84 `````` Lemma eq_None_not_Some `(x : option A) : x = None ↔ ¬is_Some x. `````` Robbert Krebbers committed Nov 12, 2012 85 86 ``````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 87 ``````Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 88 `````` `````` Robbert Krebbers committed May 07, 2013 89 ``````Lemma mk_eq_Some {A} (x : option A) a : `````` Robbert Krebbers committed Jun 11, 2012 90 `````` is_Some x → (∀ b, x = Some b → b = a) → x = Some a. `````` Robbert Krebbers committed Nov 12, 2012 91 ``````Proof. destruct 1. intros. f_equal. auto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 92 `````` `````` Robbert Krebbers committed Aug 29, 2012 93 94 95 ``````(** 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 96 97 98 99 100 `````` 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 101 `````` end `````` Robbert Krebbers committed Feb 19, 2013 102 103 104 `````` | Some _, None => right (Some_ne_None _) | None, Some _ => right (None_ne_Some _) | None, None => left eq_refl `````` Robbert Krebbers committed Jun 11, 2012 105 106 `````` end. `````` Robbert Krebbers committed Aug 29, 2012 107 ``````(** * Monadic operations *) `````` Robbert Krebbers committed Nov 12, 2012 108 109 ``````Instance option_ret: MRet option := @Some. Instance option_bind: MBind option := λ A B f x, `````` Robbert Krebbers committed May 07, 2013 110 `````` match x with Some a => f a | None => None end. `````` Robbert Krebbers committed Nov 12, 2012 111 ``````Instance option_join: MJoin option := λ A x, `````` Robbert Krebbers committed May 07, 2013 112 `````` match x with Some x => x | None => None end. `````` Robbert Krebbers committed Nov 12, 2012 113 114 ``````Instance option_fmap: FMap option := @option_map. Instance option_guard: MGuard option := λ P dec A x, `````` Robbert Krebbers committed May 07, 2013 115 `````` match dec with left H => x H | _ => None end. `````` Robbert Krebbers committed Jun 11, 2012 116 `````` `````` Robbert Krebbers committed Feb 22, 2013 117 118 119 120 121 122 123 124 ``````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 Feb 19, 2013 125 126 127 128 129 130 131 132 ``````Lemma fmap_is_Some {A B} (f : A → B) (x : option A) : is_Some (f <\$> x) ↔ is_Some x. Proof. split; inversion 1. by destruct x. done. Qed. Lemma fmap_Some {A B} (f : A → B) (x : option A) y : f <\$> x = Some y ↔ ∃ x', x = Some x' ∧ y = f x'. Proof. unfold fmap, option_fmap. destruct x; naive_solver. Qed. Lemma fmap_None {A B} (f : A → B) (x : option A) : f <\$> x = None ↔ x = None. `````` Robbert Krebbers committed Nov 12, 2012 133 ``````Proof. unfold fmap, option_fmap. by destruct x. Qed. `````` Robbert Krebbers committed Jun 11, 2012 134 `````` `````` Robbert Krebbers committed May 07, 2013 135 ``````Lemma option_fmap_id {A} (x : option A) : id <\$> x = x. `````` Robbert Krebbers committed Feb 19, 2013 136 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Jan 05, 2013 137 138 139 ``````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 Feb 22, 2013 140 ``````Lemma option_bind_ext {A B} (f g : A → option B) x y : `````` Robbert Krebbers committed May 07, 2013 141 `````` (∀ a, f a = g a) → x = y → x ≫= f = y ≫= g. `````` Robbert Krebbers committed Feb 22, 2013 142 143 ``````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 144 `````` (∀ a, f a = g a) → x ≫= f = x ≫= g. `````` Robbert Krebbers committed Feb 22, 2013 145 146 147 148 149 ``````Proof. intros. by apply option_bind_ext. Qed. Section mapM. Context {A B : Type} (f : A → option B). `````` Robbert Krebbers committed May 07, 2013 150 `````` 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 151 152 153 `````` 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 154 `````` Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed. `````` Robbert Krebbers committed Feb 22, 2013 155 156 `````` 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 157 `````` Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed. `````` Robbert Krebbers committed Feb 22, 2013 158 `````` `````` Robbert Krebbers committed May 07, 2013 159 `````` 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 160 161 162 163 164 165 `````` 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 166 `````` 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 167 168 169 170 `````` Proof. induction 1 as [|???? Hf ? IH]; simpl; [done |]. rewrite Hf. simpl. by rewrite IH. Qed. `````` Robbert Krebbers committed May 07, 2013 171 `````` 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 172 173 `````` Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed. End mapM. `````` Robbert Krebbers committed Jan 05, 2013 174 `````` `````` Robbert Krebbers committed Nov 12, 2012 175 ``````Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat `````` Robbert Krebbers committed Aug 29, 2012 176 `````` match goal with `````` Robbert Krebbers committed May 07, 2013 177 `````` | _ => progress (unfold default in *) `````` Robbert Krebbers committed Oct 19, 2012 178 `````` | _ => first [progress simpl in * | progress simplify_equality] `````` Robbert Krebbers committed Jan 05, 2013 179 `````` | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ => `````` Robbert Krebbers committed Oct 19, 2012 180 `````` let Hx := fresh in `````` Robbert Krebbers committed Jan 05, 2013 181 182 183 184 185 `````` 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 186 `````` rewrite Hx in H; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 `````` | 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 206 `````` | H : mbind (M:=option) ?f ?o = ?x |- _ => `````` Robbert Krebbers committed Oct 19, 2012 207 208 `````` 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 209 `````` destruct o eqn:? `````` Robbert Krebbers committed Jan 05, 2013 210 211 212 213 214 215 216 217 218 219 220 221 222 `````` | 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 223 `````` let Hx := fresh in `````` Robbert Krebbers committed Jan 05, 2013 224 225 226 227 228 `````` 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 229 `````` rewrite Hx; clear Hx `````` Robbert Krebbers committed Jan 05, 2013 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 `````` | |- 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 249 `````` | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ => `````` Robbert Krebbers committed May 07, 2013 250 `````` let X := context C [ match dec with left H => x H | _ => None end ] in `````` Robbert Krebbers committed Feb 19, 2013 251 `````` change X in H; destruct_decide dec `````` Robbert Krebbers committed Nov 12, 2012 252 `````` | |- context C [@mguard option _ ?P ?dec _ ?x] => `````` Robbert Krebbers committed May 07, 2013 253 `````` let X := context C [ match dec with left H => x H | _ => None end ] in `````` Robbert Krebbers committed Feb 19, 2013 254 `````` change X; destruct_decide dec `````` Robbert Krebbers committed Jan 05, 2013 255 256 257 258 `````` | 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 259 `````` | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H `````` Robbert Krebbers committed Aug 29, 2012 260 `````` end. `````` Robbert Krebbers committed Jan 05, 2013 261 262 263 ``````Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto. `````` Robbert Krebbers committed Feb 22, 2013 264 265 ``````Hint Extern 800 => progress simplify_option_equality : simplify_option_equality. `````` Robbert Krebbers committed Aug 29, 2012 266 267 `````` (** * Union, intersection and difference *) `````` Robbert Krebbers committed Jan 05, 2013 268 ``````Instance option_union_with {A} : UnionWith A (option A) := λ f x y, `````` Robbert Krebbers committed Jun 11, 2012 269 `````` match x, y with `````` Robbert Krebbers committed Jan 05, 2013 270 `````` | Some a, Some b => f a b `````` Robbert Krebbers committed Jun 11, 2012 271 272 273 274 `````` | Some a, None => Some a | None, Some b => Some b | None, None => None end. `````` Robbert Krebbers committed May 07, 2013 275 276 277 ``````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 278 279 280 281 282 `````` 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 283 `````` `````` Robbert Krebbers committed Jan 05, 2013 284 285 ``````Section option_union_intersection_difference. Context {A} (f : A → A → option A). `````` Robbert Krebbers committed Jun 11, 2012 286 287 `````` Global Instance: LeftId (=) None (union_with f). `````` Robbert Krebbers committed Oct 19, 2012 288 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jun 11, 2012 289 `````` Global Instance: RightId (=) None (union_with f). `````` Robbert Krebbers committed Oct 19, 2012 290 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jun 11, 2012 291 `````` Global Instance: Commutative (=) f → Commutative (=) (union_with f). `````` Robbert Krebbers committed Jan 05, 2013 292 `````` Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. `````` Robbert Krebbers committed Feb 19, 2013 293 294 295 296 297 `````` 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 298 `````` Global Instance: Commutative (=) f → Commutative (=) (intersection_with f). `````` Robbert Krebbers committed Jan 05, 2013 299 `````` Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed. `````` Robbert Krebbers committed Feb 19, 2013 300 `````` `````` Robbert Krebbers committed Aug 21, 2012 301 `````` Global Instance: RightId (=) None (difference_with f). `````` Robbert Krebbers committed Oct 19, 2012 302 `````` Proof. by intros [?|]. Qed. `````` Robbert Krebbers committed Jan 05, 2013 303 ``End option_union_intersection_difference.``