option.v 16.3 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
From stdpp Require Export tactics.
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} (x : A) : None  Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
Proof. congruence. Qed.
15
Lemma Some_ne_None {A} (x : A) : Some x  None.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
Proof. congruence. Qed.
17
Lemma eq_None_ne_Some {A} (mx : option A) x : mx = None  mx  Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Proof. congruence. Qed.
19
Instance Some_inj {A} : Inj (=) (=) (@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 25
Definition default {A B} (y : B) (mx : option A) (f : A  B)  : B :=
  match mx with None => y | Some x => f x end.
Instance: Params (@default) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
26

Robbert Krebbers's avatar
Robbert Krebbers committed
27 28
(** The [from_option] function allows us to get the value out of the option
type by specifying a default value. *)
29 30 31
Definition from_option {A} (x : A) (mx : option A) : A :=
  match mx with None => x | Some y => y end.
Instance: Params (@from_option) 1.
32

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. *)
35 36 37
Lemma option_eq {A} (mx my: option A): mx = my   x, mx = Some x  my = Some x.
Proof. split; [by intros; by subst |]. destruct mx, my; naive_solver. Qed.
Lemma option_eq_1 {A} (mx my: option A) x : mx = my  mx = Some x  my = Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
Proof. congruence. Qed.
39 40
Lemma option_eq_1_alt {A} (mx my : option A) x :
  mx = my  my = Some x  mx = Some x.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
Proof. congruence. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
42

43 44 45 46
Definition is_Some {A} (mx : option A) :=  x, mx = Some x.
Instance: Params (@is_Some) 1.

Lemma mk_is_Some {A} (mx : option A) x : mx = Some x  is_Some mx.
47 48 49 50 51
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
52

53
Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx).
54
Proof.
55 56
  set (P (mx : option A) := match mx with Some _ => True | _ => False end).
  set (f mx := match mx return P mx  is_Some mx with
57
    Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
58 59 60 61
  set (g mx (H : is_Some mx) :=
    match H return P mx with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end).
  assert ( mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst).
  intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1.
62
Qed.
63 64
Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) :=
  match mx with
65 66
  | Some x => left (ex_intro _ x eq_refl)
  | None => right is_Some_None
67
  end.
68

69 70 71 72 73
Definition is_Some_proj {A} {mx : option A} : is_Some mx  A :=
  match mx with Some x => λ _, x | None => False_rect _  is_Some_None end.
Definition Some_dec {A} (mx : option A) : { x | mx = Some x } + { mx = None } :=
  match mx return { x | mx = Some x } + { mx = None } with
  | Some x => inleft (x  eq_refl _)
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75
  | None => inright eq_refl
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
76

77 78 79 80
Lemma eq_None_not_Some {A} (mx : option A) : mx = None  ¬is_Some mx.
Proof. destruct mx; unfold is_Some; naive_solver. Qed.
Lemma not_eq_None_Some {A} (mx : option A) : mx  None  is_Some mx.
Proof. rewrite eq_None_not_Some; apply dec_stable; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
81

Robbert Krebbers's avatar
Robbert Krebbers committed
82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
(** 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.
97
  Context `{Equiv A} `{!Equivalence (() : relation A)}.
98

Robbert Krebbers's avatar
Robbert Krebbers committed
99
  Global Instance option_equiv : Equiv (option A) := option_Forall2 ().
100 101 102 103

  Lemma equiv_option_Forall2 mx my : mx  my  option_Forall2 () mx my.
  Proof. split; destruct 1; constructor; auto. Qed.

104
  Global Instance option_equivalence : Equivalence (() : relation (option A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106
  Proof.
    split.
107 108
    - by intros []; constructor.
    - by destruct 1; constructor.
109
    - destruct 1; inversion 1; constructor; etrans; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111 112 113
  Qed.
  Global Instance Some_proper : Proper (() ==> ()) (@Some A).
  Proof. by constructor. Qed.
  Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
114
  Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
115

116 117
  Lemma equiv_None (mx : option A) : mx  None  mx = None.
  Proof. split; [by inversion_clear 1|by intros ->]. Qed.
118
  Lemma equiv_Some_inv_l (mx my : option A) x :
119 120
    mx  my  mx = Some x   y, my = Some y  x  y.
  Proof. destruct 1; naive_solver. Qed.
121 122 123 124
  Lemma equiv_Some_inv_r (mx my : option A) y :
    mx  my  mx = Some y   x, mx = Some x  x  y.
  Proof. destruct 1; naive_solver. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
  Global Instance is_Some_proper : Proper (() ==> iff) (@is_Some A).
  Proof. inversion_clear 1; split; eauto. Qed.
127 128 129
  Global Instance from_option_proper :
    Proper (() ==> () ==> ()) (@from_option A).
  Proof. by destruct 2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
130 131
End setoids.

132
(** Equality on [option] is decidable. *)
133 134 135 136 137 138
Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None) :=
  match mx with Some _ => right (Some_ne_None _) | None => left eq_refl end.
Instance option_None_eq_dec {A} (mx : option A) : Decision (None = mx) :=
  match mx with Some _ => right (None_ne_Some _) | None => left eq_refl end.
Instance option_eq_dec {A} {dec :  x y : A, Decision (x = y)}
  (mx my : option A) : Decision (mx = my).
139 140
Proof.
 refine
141 142
  match mx, my with
  | Some x, Some y => cast_if (decide (x = y))
143
  | None, None => left _ | _, _ => right _
Robbert Krebbers's avatar
Robbert Krebbers committed
144
  end; clear dec; abstract congruence.
145
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
146

147
(** * Monadic operations *)
148
Instance option_ret: MRet option := @Some.
149 150 151 152
Instance option_bind: MBind option := λ A B f mx,
  match mx with Some x => f x | None => None end.
Instance option_join: MJoin option := λ A mmx,
  match mmx with Some mx => mx | None => None end.
153
Instance option_fmap: FMap option := @option_map.
154 155
Instance option_guard: MGuard option := λ P dec A f,
  match dec with left H => f H | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
156

157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
Lemma fmap_is_Some {A B} (f : A  B) mx : is_Some (f <$> mx)  is_Some mx.
Proof. unfold is_Some; destruct mx; naive_solver. Qed.
Lemma fmap_Some {A B} (f : A  B) mx y :
  f <$> mx = Some y   x, mx = Some x  y = f x.
Proof. destruct mx; naive_solver. Qed.
Lemma fmap_None {A B} (f : A  B) mx : f <$> mx = None  mx = None.
Proof. by destruct mx. Qed.
Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
Proof. by destruct mx. Qed.
Lemma option_fmap_compose {A B} (f : A  B) {C} (g : B  C) mx :
  g  f <$> mx = g <$> f <$> mx.
Proof. by destruct mx. Qed.
Lemma option_fmap_ext {A B} (f g : A  B) mx :
  ( x, f x = g x)  f <$> mx = g <$> mx.
Proof. intros; destruct mx; f_equal/=; auto. Qed.
Lemma option_fmap_setoid_ext `{Equiv A, Equiv B} (f g : A  B) mx :
  ( x, f x  g x)  f <$> mx  g <$> mx.
Proof. destruct mx; constructor; auto. Qed.
Lemma option_fmap_bind {A B C} (f : A  B) (g : B  option C) mx :
  (f <$> mx) = g = mx = g  f.
Proof. by destruct mx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
Lemma option_bind_assoc {A B C} (f : A  option B)
179 180 181 182 183 184 185
  (g : B  option C) (mx : option A) : (mx = f) = g = mx = (mbind g  f).
Proof. by destruct mx; simpl. Qed.
Lemma option_bind_ext {A B} (f g : A  option B) mx my :
  ( x, f x = g x)  mx = my  mx = f = my = g.
Proof. destruct mx, my; naive_solver. Qed.
Lemma option_bind_ext_fun {A B} (f g : A  option B) mx :
  ( x, f x = g x)  mx = f = mx = g.
186
Proof. intros. by apply option_bind_ext. Qed.
187 188 189 190 191 192 193 194
Lemma bind_Some {A B} (f : A  option B) (mx : option A) y :
  mx = f = Some y   x, mx = Some x  f x = Some y.
Proof. destruct mx; naive_solver. Qed.
Lemma bind_None {A B} (f : A  option B) (mx : option A) :
  mx = f = None  mx = None   x, mx = Some x  f x = None.
Proof. destruct mx; naive_solver. Qed.
Lemma bind_with_Some {A} (mx : option A) : mx = Some = mx.
Proof. by destruct mx. Qed.
195

196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
(** ** 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
220 221
Instance maybe_Some {A} : Maybe (@Some A) := id.
Arguments maybe_Some _ !_ /.
222

223
(** * Union, intersection and difference *)
224 225 226 227 228
Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
  | None, Some y => Some y
229 230 231
  | None, None => None
  end.
Instance option_intersection_with {A} : IntersectionWith A (option A) :=
232 233 234 235 236
  λ f mx my, match mx, my with Some x, Some y => f x y | _, _ => None end.
Instance option_difference_with {A} : DifferenceWith A (option A) := λ f mx my,
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
237 238 239
  | None, _ => None
  end.
Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
240 241 242 243

Lemma option_union_Some {A} (mx my : option A) z :
  mx  my = Some z  mx = Some z  my = Some z.
Proof. destruct mx, my; naive_solver. Qed.
244 245 246 247 248 249 250

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.
251 252
  Global Instance: Comm (=) f  Comm (=) (union_with f).
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
253 254 255 256
  Global Instance: LeftAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
  Global Instance: RightAbsorb (=) None (intersection_with f).
  Proof. by intros [?|]. Qed.
257 258
  Global Instance: Comm (=) f  Comm (=) (intersection_with f).
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
259 260 261 262 263
  Global Instance: RightId (=) None (difference_with f).
  Proof. by intros [?|]. Qed.
End option_union_intersection_difference.

(** * Tactics *)
264 265
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
266
  | H : appcontext C [@mguard option _ ?P ?dec] |- _ =>
267 268
    change (@mguard option _ P dec) with (λ A (f : P  option A),
      match @decide P dec with left H' => f H' | _ => None end) in *;
269 270
    destruct_decide (@decide P dec) as Hx
  | |- appcontext C [@mguard option _ ?P ?dec] =>
271 272
    change (@mguard option _ P dec) with (λ A (f : P  option A),
      match @decide P dec with left H' => f H' | _ => None end) in *;
273
    destruct_decide (@decide P dec) as Hx
274 275 276
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
277

278 279
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
  P  guard P; mx = mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
Proof. intros. by case_option_guard. Qed.
281 282
Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
  ¬P  guard P; mx = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
Proof. intros. by case_option_guard. Qed.
284 285
Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
  (P  Q)  guard P; mx = guard Q; mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
Proof. intros [??]. repeat case_option_guard; intuition. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
287

Robbert Krebbers's avatar
Robbert Krebbers committed
288
Tactic Notation "simpl_option" "by" tactic3(tac) :=
289
  let assert_Some_None A mx H := first
290
    [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
291 292
      assert (mx = Some x') as H by tac
    | assert (mx = None) as H by tac ]
293
  in repeat match goal with
294 295 296
  | H : appcontext [@mret _ _ ?A] |- _ =>
     change (@mret _ _ A) with (@Some A) in H
  | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
297 298 299 300 301 302 303 304 305 306
  | H : context [mbind (M:=option) (A:=?A) ?f ?mx] |- _ =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
  | H : context [fmap (M:=option) (A:=?A) ?f ?mx] |- _ =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
  | H : context [default (A:=?A) _ ?mx _] |- _ =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
  | H : context [from_option (A:=?A) _ ?mx] |- _ =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
  | H : context [ match ?mx with _ => _ end ] |- _ =>
    match type of mx with
Robbert Krebbers's avatar
Robbert Krebbers committed
307
    | option ?A =>
308
      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
309
    end
310 311 312 313 314 315 316 317 318 319
  | |- context [mbind (M:=option) (A:=?A) ?f ?mx] =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
  | |- context [fmap (M:=option) (A:=?A) ?f ?mx] =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
  | |- context [default (A:=?A) _ ?mx _] =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
  | |- context [from_option (A:=?A) _ ?mx] =>
    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
  | |- context [ match ?mx with _ => _ end ] =>
    match type of mx with
Robbert Krebbers's avatar
Robbert Krebbers committed
320
    | option ?A =>
321
      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
322
    end
323 324 325 326
  | 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
327 328 329 330
  | _ => rewrite decide_True by tac
  | _ => rewrite decide_False by tac
  | _ => rewrite option_guard_True by tac
  | _ => rewrite option_guard_False by tac
331 332 333 334
  | 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
335
  end.
336
Tactic Notation "simplify_option_eq" "by" tactic3(tac) :=
337
  repeat match goal with
338
  | _ => progress simplify_eq/=
Robbert Krebbers's avatar
Robbert Krebbers committed
339
  | _ => progress simpl_option by tac
340 341 342 343
  | _ : 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
344
  | H : _  _ = Some _ |- _ => apply option_union_Some in H; destruct H
345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364
  | H : mbind (M:=option) ?f ?mx = ?my |- _ =>
    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
    let x := fresh in destruct mx as [x|] eqn:?;
      [change (f x = my) in H|change (None = my) in H]
  | H : ?my = mbind (M:=option) ?f ?mx |- _ =>
    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
    let x := fresh in destruct mx as [x|] eqn:?;
      [change (my = f x) in H|change (my = None) in H]
  | H : fmap (M:=option) ?f ?mx = ?my |- _ =>
    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
    let x := fresh in destruct mx as [x|] eqn:?;
      [change (Some (f x) = my) in H|change (None = my) in H]
  | H : ?my = fmap (M:=option) ?f ?mx |- _ =>
    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
    let x := fresh in destruct mx as [x|] eqn:?;
      [change (my = Some (f x)) in H|change (my = None) in H]
365
  | _ => progress case_decide
366
  | _ => progress case_option_guard
367
  end.
368
Tactic Notation "simplify_option_eq" := simplify_option_eq by eauto.