option.v 15.8 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
  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).
104
  Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
105 106 107 108 109
  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
110 111
  Global Instance is_Some_proper : Proper (() ==> iff) (@is_Some A).
  Proof. inversion_clear 1; split; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
112 113
End setoids.

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

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

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

181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
(** ** 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
205 206
Instance maybe_Some {A} : Maybe (@Some A) := id.
Arguments maybe_Some _ !_ /.
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 243 244 245 246 247
(** * 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 *)
248 249
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
250 251 252 253 254 255 256 257
  | 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
258 259 260
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
261

Robbert Krebbers's avatar
Robbert Krebbers committed
262
Lemma option_guard_True {A} P `{Decision P} (x : option A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
263 264
  P  guard P; x = x.
Proof. intros. by case_option_guard. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
265
Lemma option_guard_False {A} P `{Decision P} (x : option A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
266 267
  ¬P  guard P; x = None.
Proof. intros. by case_option_guard. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
268 269 270
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
271

Robbert Krebbers's avatar
Robbert Krebbers committed
272
Tactic Notation "simpl_option" "by" tactic3(tac) :=
273 274 275 276 277
  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
278 279 280
  | 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
281
  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
282
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
283
  | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
284 285 286
    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
287 288
  | 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
289 290 291
  | H : context [ match ?o with _ => _ end ] |- _ =>
    match type of o with
    | option ?A =>
292
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
293 294
    end
  | |- context [mbind (M:=option) (A:=?A) ?f ?o] =>
295
    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
296
  | |- context [fmap (M:=option) (A:=?A) ?f ?o] =>
297 298 299 300 301
    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
302 303 304
  | |- context [ match ?o with _ => _ end ] =>
    match type of o with
    | option ?A =>
305
      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
306
    end
307 308 309 310
  | 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
311 312 313 314
  | _ => rewrite decide_True by tac
  | _ => rewrite decide_False by tac
  | _ => rewrite option_guard_True by tac
  | _ => rewrite option_guard_False by tac
315 316 317 318
  | H : context [None  _] |- _ => rewrite (left_id_L None ()) in H
  | H : context [_  None] |- _ => rewrite (right_id_L None ()) in H
  | |- context [None  _] => rewrite (left_id_L None ())
  | |- context [_  None] => rewrite (right_id_L None ())
Robbert Krebbers's avatar
Robbert Krebbers committed
319 320
  end.
Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
321
  repeat match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
322
  | _ => progress simplify_equality'
Robbert Krebbers's avatar
Robbert Krebbers committed
323
  | _ => progress simpl_option by tac
324 325 326 327
  | _ : 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
328
  | H : _  _ = Some _ |- _ => apply option_union_Some in H; destruct H
329
  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
330 331
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
332 333 334
    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
335 336
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
337 338
    let y := fresh in destruct o as [y|] eqn:?;
      [change (x = f y) in H|change (x = None) in H]
339
  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
340 341
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
342 343 344
    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
345 346
    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
347 348
    let y := fresh in destruct o as [y|] eqn:?;
      [change (x = Some (f y)) in H|change (x = None) in H]
349
  | _ => progress case_decide
350
  | _ => progress case_option_guard
351
  end.
352
Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.