option.v 15.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
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. *)
5
Require Export prelude.base prelude.tactics prelude.decidable.
6

7 8 9 10
Inductive option_reflect {A} (P : A  Prop) (Q : Prop) : option A  Type :=
  | ReflectSome x : P x  option_reflect P Q (Some x)
  | ReflectNone : Q  option_reflect P Q None.

11 12
(** * General definitions and theorems *)
(** Basic properties about equality. *)
13
Lemma None_ne_Some {A} (a : A) : None  Some a.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
Proof. congruence. Qed.
15
Lemma Some_ne_None {A} (a : A) : Some a  None.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
Proof. congruence. Qed.
17
Lemma eq_None_ne_Some {A} (x : option A) a : x = None  x  Some a.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Proof. congruence. Qed.
19
Instance Some_inj {A} : Injective (=) (=) (@Some A).
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21
Proof. congruence. Qed.

22
(** The non dependent elimination principle on the option type. *)
23 24
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's avatar
Robbert Krebbers committed
25

Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28
(** 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 :=
29
  match x with None => a | Some b => b end.
30

31 32
(** An alternative, but equivalent, definition of equality on the option
data type. This theorem is useful to prove that two options are the same. *)
33 34
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's avatar
Robbert Krebbers committed
35 36 37 38
Lemma option_eq_1 {A} (x y : option A) a : x = y  x = Some a  y = Some a.
Proof. congruence. Qed.
Lemma option_eq_1_alt {A} (x y : option A) a : x = y  y = Some a  x = Some a.
Proof. congruence. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
39

40 41 42 43 44 45 46
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's avatar
Robbert Krebbers committed
47

48 49
Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x).
Proof.
50 51 52 53 54 55 56
  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.
57
Qed.
58
Instance is_Some_dec {A} (x : option A) : Decision (is_Some x) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  match x with
60 61
  | Some x => left (ex_intro _ x eq_refl)
  | None => right is_Some_None
62
  end.
63 64 65 66

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's avatar
Robbert Krebbers committed
67 68 69 70
  match x return { a | x = Some a } + { x = None } with
  | Some a => inleft (a  eq_refl _)
  | None => inright eq_refl
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
71

72 73
Lemma eq_None_not_Some {A} (x : option A) : x = None  ¬is_Some x.
Proof. destruct x; unfold is_Some; naive_solver. Qed.
74
Lemma not_eq_None_Some `(x : option A) : x  None  is_Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
76

Robbert Krebbers's avatar
Robbert Krebbers committed
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
(** Lifting a relation point-wise to option *)
Inductive option_Forall2 {A B} (P: A  B  Prop) : option A  option B  Prop :=
  | Some_Forall2 x y : P x y  option_Forall2 P (Some x) (Some y)
  | None_Forall2 : option_Forall2 P None None.
Definition option_relation {A B} (R: A  B  Prop) (P: A  Prop) (Q: B  Prop)
    (mx : option A) (my : option B) : Prop :=
  match mx, my with
  | Some x, Some y => R x y
  | Some x, None => P x
  | None, Some y => Q y
  | None, None => True
  end.

(** Setoids *)
Section setoids.
92
  Context `{Equiv A} `{!Equivalence (() : relation A)}.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  Global Instance option_equiv : Equiv (option A) := option_Forall2 ().
94
  Global Instance option_equivalence : Equivalence (() : relation (option A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96 97 98 99 100 101 102 103 104 105 106 107
  Proof.
    split.
    * by intros []; constructor.
    * by destruct 1; constructor.
    * destruct 1; inversion 1; constructor; etransitivity; eauto.
  Qed.
  Global Instance Some_proper : Proper (() ==> ()) (@Some A).
  Proof. by constructor. Qed.
  Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
  Proof.
    intros x y; split; [destruct 1; fold_leibniz; congruence|].
    by intros <-; destruct x; constructor; fold_leibniz.
  Qed.
108 109 110 111 112
  Lemma equiv_None (mx : option A) : mx  None  mx = None.
  Proof. split; [by inversion_clear 1|by intros ->]. Qed.
  Lemma equiv_Some (mx my : option A) x :
    mx  my  mx = Some x   y, my = Some y  x  y.
  Proof. destruct 1; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114
End setoids.

115
(** Equality on [option] is decidable. *)
116 117 118 119
Instance option_eq_None_dec {A} (x : option A) : Decision (x = None) :=
  match x with Some _ => right (Some_ne_None _) | None => left eq_refl end.
Instance option_None_eq_dec {A} (x : option A) : Decision (None = x) :=
  match x with Some _ => right (None_ne_Some _) | None => left eq_refl end.
120
Instance option_eq_dec `{dec :  x y : A, Decision (x = y)}
121 122 123
  (x y : option A) : Decision (x = y).
Proof.
 refine
124
  match x, y with
125 126
  | Some a, Some b => cast_if (decide (a = b))
  | None, None => left _ | _, _ => right _
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  end; clear dec; abstract congruence.
128
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
129

130
(** * Monadic operations *)
131 132
Instance option_ret: MRet option := @Some.
Instance option_bind: MBind option := λ A B f x,
133
  match x with Some a => f a | None => None end.
134
Instance option_join: MJoin option := λ A x,
135
  match x with Some x => x | None => None end.
136 137
Instance option_fmap: FMap option := @option_map.
Instance option_guard: MGuard option := λ P dec A x,
138
  match dec with left H => x H | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
139

140 141 142
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 :
143
  f <$> x = Some y   x', x = Some x'  y = f x'.
144 145 146
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.
147
Lemma option_fmap_id {A} (x : option A) : id <$> x = x.
148
Proof. by destruct x. Qed.
149 150 151
Lemma option_fmap_compose {A B} (f : A  B) {C} (g : B  C) x :
  g  f <$> x = g <$> f <$> x.
Proof. by destruct x. Qed.
152 153 154
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's avatar
Robbert Krebbers committed
155
Lemma option_bind_assoc {A B C} (f : A  option B)
156
  (g : B  option C) (x : option A) : (x = f) = g = x = (mbind g  f).
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Proof. by destruct x; simpl. Qed.
158
Lemma option_bind_ext {A B} (f g : A  option B) x y :
159
  ( a, f a = g a)  x = y  x = f = y = g.
160
Proof. intros. destruct x, y; simplify_equality; csimpl; auto. Qed.
161
Lemma option_bind_ext_fun {A B} (f g : A  option B) x :
162
  ( a, f a = g a)  x = f = x = g.
163
Proof. intros. by apply option_bind_ext. Qed.
164 165 166 167 168 169
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.
170 171
  split; [|by intros [->|(?&->&?)]].
  destruct x; intros; simplify_equality'; eauto.
172
Qed.
173 174
Lemma bind_with_Some {A} (x : option A) : x = Some = x.
Proof. by destruct x. Qed.
175

176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
(** ** Inverses of constructors *)
(** We can do this in a fancy way using dependent types, but rewrite does
not particularly like type level reductions. *)
Class Maybe {A B : Type} (c : A  B) :=
  maybe : B  option A.
Arguments maybe {_ _} _ {_} !_ /.
Class Maybe2 {A1 A2 B : Type} (c : A1  A2  B) :=
  maybe2 : B  option (A1 * A2).
Arguments maybe2 {_ _ _} _ {_} !_ /.
Class Maybe3 {A1 A2 A3 B : Type} (c : A1  A2  A3  B) :=
  maybe3 : B  option (A1 * A2 * A3).
Arguments maybe3 {_ _ _ _} _ {_} !_ /.
Class Maybe4 {A1 A2 A3 A4 B : Type} (c : A1  A2  A3  A4  B) :=
  maybe4 : B  option (A1 * A2 * A3 * A4).
Arguments maybe4 {_ _ _ _ _} _ {_} !_ /.

Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1  c2) := λ x,
  maybe c1 x = maybe c2.
Arguments maybe_comp _ _ _ _ _ _ _ !_ /.

Instance maybe_inl {A B} : Maybe (@inl A B) := λ xy,
  match xy with inl x => Some x | _ => None end.
Instance maybe_inr {A B} : Maybe (@inr A B) := λ xy,
  match xy with inr y => Some y | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
200 201
Instance maybe_Some {A} : Maybe (@Some A) := id.
Arguments maybe_Some _ !_ /.
202

203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
(** * Union, intersection and difference *)
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
  match x, y with
  | Some a, Some b => f a b
  | Some a, None => Some a
  | None, Some b => Some b
  | None, None => None
  end.
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,
  match x, y with
  | Some a, Some b => f a b
  | Some a, None => Some a
  | None, _ => None
  end.
Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
Lemma option_union_Some {A} (x y : option A) z :
  x  y = Some z  x = Some z  y = Some z.
Proof. destruct x, y; intros; simplify_equality; auto. Qed.

Section option_union_intersection_difference.
  Context {A} (f : A  A  option A).
  Global Instance: LeftId (=) None (union_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightId (=) None (union_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: Commutative (=) f  Commutative (=) (union_with f).
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
  Global Instance: LeftAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: Commutative (=) f  Commutative (=) (intersection_with f).
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
  Global Instance: RightId (=) None (difference_with f).
  Proof. by intros [?|]. Qed.
End option_union_intersection_difference.

(** * Tactics *)
243 244
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
245 246 247 248 249 250 251 252
  | H : appcontext C [@mguard option _ ?P ?dec] |- _ =>
    change (@mguard option _ P dec) with (λ A (x : P  option A),
      match @decide P dec with left H' => x H' | _ => None end) in *;
    destruct_decide (@decide P dec) as Hx
  | |- appcontext C [@mguard option _ ?P ?dec] =>
    change (@mguard option _ P dec) with (λ A (x : P  option A),
      match @decide P dec with left H' => x H' | _ => None end) in *;
    destruct_decide (@decide P dec) as Hx
253 254 255
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
256

Robbert Krebbers's avatar
Robbert Krebbers committed
257
Lemma option_guard_True {A} P `{Decision P} (x : option A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
258 259
  P  guard P; x = x.
Proof. intros. by case_option_guard. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
260
Lemma option_guard_False {A} P `{Decision P} (x : option A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
261 262
  ¬P  guard P; x = None.
Proof. intros. by case_option_guard. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
263 264 265
Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (x : option A) :
  (P  Q)  guard P; x = guard Q; x.
Proof. intros [??]. repeat case_option_guard; intuition. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
266

Robbert Krebbers's avatar
Robbert Krebbers committed
267
Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
268 269 270 271 272
  let assert_Some_None A o H := first
    [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
      assert (o = Some x') as H by tac
    | assert (o = None) as H by tac ]
  in repeat match goal with
273 274 275
  | H : appcontext [@mret _ _ ?A] |- _ =>
     change (@mret _ _ A) with (@Some A) in H
  | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
Robbert Krebbers's avatar
Robbert Krebbers committed
276
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
277
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
278
  | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
279 280 281
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
  | H : context [default (A:=?A) _ ?o _] |- _ =>
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
282 283
  | H : context [from_option (A:=?A) _ ?o] |- _ =>
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
284 285 286
  | H : context [ match ?o with _ => _ end ] |- _ =>
    match type of o with
    | option ?A =>
287
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
288 289
    end
  | |- context [mbind (M:=option) (A:=?A) ?f ?o] =>
290
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  | |- context [fmap (M:=option) (A:=?A) ?f ?o] =>
292 293 294 295 296
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
  | |- context [default (A:=?A) _ ?o _] =>
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
  | |- context [from_option (A:=?A) _ ?o] =>
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
297 298 299
  | |- context [ match ?o with _ => _ end ] =>
    match type of o with
    | option ?A =>
300
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
301
    end
302 303 304 305
  | H : context [decide _] |- _ => rewrite decide_True in H by tac
  | H : context [decide _] |- _ => rewrite decide_False in H by tac
  | H : context [mguard _ _] |- _ => rewrite option_guard_False in H by tac
  | H : context [mguard _ _] |- _ => rewrite option_guard_True in H by tac
306 307 308 309
  | _ => rewrite decide_True by tac
  | _ => rewrite decide_False by tac
  | _ => rewrite option_guard_True by tac
  | _ => rewrite option_guard_False by tac
Robbert Krebbers's avatar
Robbert Krebbers committed
310 311
  end.
Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
312
  repeat match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
313 314
  | _ => progress simplify_equality'
  | _ => progress simpl_option_monad by tac
315 316 317 318
  | _ : maybe _ ?x = Some _ |- _ => is_var x; destruct x
  | _ : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
  | _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
  | _ : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
319
  | H : _  _ = Some _ |- _ => apply option_union_Some in H; destruct H
320
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
321 322
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
323 324 325
    let y := fresh in destruct o as [y|] eqn:?;
      [change (f y = x) in H|change (None = x) in H]
  | H : ?x = mbind (M:=option) ?f ?o |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
326 327
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
328 329
    let y := fresh in destruct o as [y|] eqn:?;
      [change (x = f y) in H|change (x = None) in H]
330
  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
331 332
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
333 334 335
    let y := fresh in destruct o as [y|] eqn:?;
      [change (Some (f y) = x) in H|change (None = x) in H]
  | H : ?x = fmap (M:=option) ?f ?o |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
336 337
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
338 339
    let y := fresh in destruct o as [y|] eqn:?;
      [change (x = Some (f y)) in H|change (x = None) in H]
340
  | _ => progress case_decide
341
  | _ => progress case_option_guard
342
  end.
343
Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.