option.v 19 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
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
Set Default Proof Using "Type".
7

8 9 10 11
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.

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

23 24
(** The [from_option] is the eliminator for option. *)
Definition from_option {A B} (f : A  B) (y : B) (mx : option A) : B :=
25
  match mx with None => y | Some x => f x end.
26
Instance: Params (@from_option) 3.
27
Arguments from_option {_ _} _ _ !_ / : assert.
Robbert Krebbers's avatar
Robbert Krebbers committed
28

29 30 31
(* The eliminator again, but with the arguments in different order, which is
sometimes more convenient. *)
Notation default y mx f := (from_option f y mx) (only parsing).
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
Definition is_Some {A} (mx : option A) :=  x, mx = Some x.
Instance: Params (@is_Some) 1.

46 47 48 49
Lemma is_Some_alt {A} (mx : option A) :
  is_Some mx  match mx with Some _ => True | None => False end.
Proof. unfold is_Some. destruct mx; naive_solver. Qed.

50
Lemma mk_is_Some {A} (mx : option A) x : mx = Some x  is_Some mx.
51 52 53 54 55
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
56

57 58 59 60 61
Lemma eq_None_not_Some {A} (mx : option A) : mx = None  ¬is_Some mx.
Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed.
Lemma not_eq_None_Some {A} (mx : option A) : mx  None  is_Some mx.
Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed.

62
Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx).
63
Proof.
64 65
  set (P (mx : option A) := match mx with Some _ => True | _ => False end).
  set (f mx := match mx return P mx  is_Some mx with
66
    Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
67
  set (g mx (H : is_Some mx) :=
Ralf Jung's avatar
Ralf Jung committed
68
    match H return P mx with ex_intro _ _ p => eq_rect _ _ I _ (eq_sym p) end).
69 70
  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.
71
Qed.
72

73 74
Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) :=
  match mx with
75 76
  | Some x => left (ex_intro _ x eq_refl)
  | None => right is_Some_None
77
  end.
78

79 80
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.
81

82 83 84
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
85 86
  | None => inright eq_refl
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
87

Robbert Krebbers's avatar
Robbert Krebbers committed
88
(** Lifting a relation point-wise to option *)
89 90 91
Inductive option_Forall2 {A B} (R: A  B  Prop) : option A  option B  Prop :=
  | Some_Forall2 x y : R x y  option_Forall2 R (Some x) (Some y)
  | None_Forall2 : option_Forall2 R None None.
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93 94 95 96 97 98 99 100
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.

101 102 103 104 105 106 107 108 109 110 111 112 113
Section Forall2.
  Context {A} (R : relation A).

  Global Instance option_Forall2_refl : Reflexive R  Reflexive (option_Forall2 R).
  Proof. intros ? [?|]; by constructor. Qed.
  Global Instance option_Forall2_sym : Symmetric R  Symmetric (option_Forall2 R).
  Proof. destruct 2; by constructor. Qed.
  Global Instance option_Forall2_trans : Transitive R  Transitive (option_Forall2 R).
  Proof. destruct 2; inversion_clear 1; constructor; etrans; eauto. Qed.
  Global Instance option_Forall2_equiv : Equivalence R  Equivalence (option_Forall2 R).
  Proof. destruct 1; split; apply _. Qed.
End Forall2.

Robbert Krebbers's avatar
Robbert Krebbers committed
114
(** Setoids *)
115 116
Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 ().

Robbert Krebbers's avatar
Robbert Krebbers committed
117
Section setoids.
118
  Context `{Equiv A}.
119
  Implicit Types mx my : option A.
120 121

  Lemma equiv_option_Forall2 mx my : mx  my  option_Forall2 () mx my.
122
  Proof. done. Qed.
123

124
  Global Instance option_equivalence :
125
    Equivalence (@{A})  Equivalence (@{option A}).
126
  Proof. apply _. Qed.
127
  Global Instance Some_proper : Proper (() ==> (@{option A})) Some.
128
  Proof. by constructor. Qed.
129
  Global Instance Some_equiv_inj : Inj () (@{option A}) Some.
130
  Proof. by inversion_clear 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
  Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
132
  Proof. intros x y; destruct 1; f_equal; by apply leibniz_equiv. Qed.
133

134
  Lemma equiv_None mx : mx  None  mx = None.
135
  Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed.
136
  Lemma equiv_Some_inv_l mx my x :
137
    mx  my  mx = Some x   y, my = Some y  x  y.
138
  Proof. destruct 1; naive_solver. Qed.
139 140
  Lemma equiv_Some_inv_r mx my y :
    mx  my  my = Some y   x, mx = Some x  x  y.
141
  Proof. destruct 1; naive_solver. Qed.
142
  Lemma equiv_Some_inv_l' my x : Some x  my   x', Some x' = my  x  x'.
143
  Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
144
  Lemma equiv_Some_inv_r' `{!Equivalence (@{A})} mx y :
145
    mx  Some y   y', mx = Some y'  y  y'.
146
  Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
147

148
  Global Instance is_Some_proper : Proper ((@{option A}) ==> iff) is_Some.
149
  Proof. inversion_clear 1; split; eauto. Qed.
150 151 152
  Global Instance from_option_proper {B} (R : relation B) (f : A  B) :
    Proper (() ==> R) f  Proper (R ==> () ==> R) (from_option f).
  Proof. destruct 3; simpl; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
153 154
End setoids.

155 156
Typeclasses Opaque option_equiv.

157
(** Equality on [option] is decidable. *)
158 159 160 161
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.
162
Instance option_eq_dec `{dec : EqDecision A} : EqDecision (option A).
163
Proof.
164
 refine (λ mx my,
165 166
  match mx, my with
  | Some x, Some y => cast_if (decide (x = y))
167
  | None, None => left _ | _, _ => right _
168
  end); clear dec; abstract congruence.
169
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
170

171
(** * Monadic operations *)
172
Instance option_ret: MRet option := @Some.
173 174 175 176
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.
177
Instance option_fmap: FMap option := @option_map.
178 179
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
180

181 182 183 184 185
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.
186 187 188 189 190
Lemma fmap_Some_1 {A B} (f : A  B) mx y :
  f <$> mx = Some y   x, mx = Some x  y = f x.
Proof. apply fmap_Some. Qed.
Lemma fmap_Some_2 {A B} (f : A  B) mx x : mx = Some x  f <$> mx = Some (f x).
Proof. intros. apply fmap_Some; eauto. Qed.
191
Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (@{B})} (f : A  B) mx y :
Ralf Jung's avatar
Ralf Jung committed
192 193 194 195 196 197 198 199
  f <$> mx  Some y   x, mx = Some x  y  f x.
Proof.
  destruct mx; simpl; split.
  - intros ?%Some_equiv_inj. eauto.
  - intros (? & ->%Some_inj & ?). constructor. done.
  - intros ?%symmetry%equiv_None. done.
  - intros (? & ? & ?). done.
Qed.
200
Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence (@{B})} (f : A  B) mx y :
201
  f <$> mx  Some y   x, mx = Some x  y  f x.
202
Proof. by rewrite fmap_Some_equiv. Qed.
203 204 205 206 207
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 :
208
  g  f <$> mx = g <$> (f <$> mx).
209 210 211 212
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.
213
Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A  B) (mx : option A) :
214 215 216 217 218
  ( 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
219
Lemma option_bind_assoc {A B C} (f : A  option B)
220 221 222 223 224 225 226
  (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.
227
Proof. intros. by apply option_bind_ext. Qed.
228 229 230 231 232 233 234 235
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.
236

237
Instance option_fmap_proper `{Equiv A, Equiv B} :
238
  Proper ((() ==> ()) ==> (@{option A}) ==> (@{option B})) fmap.
239
Proof. destruct 2; constructor; auto. Qed.
240
Instance option_mbind_proper `{Equiv A, Equiv B} :
241
  Proper ((() ==> ()) ==> (@{option A}) ==> (@{option B})) mbind.
242 243
Proof. destruct 2; simpl; try constructor; auto. Qed.
Instance option_mjoin_proper `{Equiv A} :
244
  Proper (() ==> (@{option (option A)})) mjoin.
245
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
246

247 248 249 250 251
(** ** 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.
252
Arguments maybe {_ _} _ {_} !_ / : assert.
253 254
Class Maybe2 {A1 A2 B : Type} (c : A1  A2  B) :=
  maybe2 : B  option (A1 * A2).
255
Arguments maybe2 {_ _ _} _ {_} !_ / : assert.
256 257
Class Maybe3 {A1 A2 A3 B : Type} (c : A1  A2  A3  B) :=
  maybe3 : B  option (A1 * A2 * A3).
258
Arguments maybe3 {_ _ _ _} _ {_} !_ / : assert.
259 260
Class Maybe4 {A1 A2 A3 A4 B : Type} (c : A1  A2  A3  A4  B) :=
  maybe4 : B  option (A1 * A2 * A3 * A4).
261
Arguments maybe4 {_ _ _ _ _} _ {_} !_ / : assert.
262 263 264

Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1  c2) := λ x,
  maybe c1 x = maybe c2.
265
Arguments maybe_comp _ _ _ _ _ _ _ !_ / : assert.
266 267 268 269 270

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
271
Instance maybe_Some {A} : Maybe (@Some A) := id.
272
Arguments maybe_Some _ !_ / : assert.
273

274
(** * Union, intersection and difference *)
275
Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
276 277 278 279
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
  | None, Some y => Some y
280 281
  | None, None => None
  end.
282 283 284
Instance option_intersection_with {A} : IntersectionWith A (option A) :=
  λ 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,
285 286 287
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
288 289 290
  | None, _ => None
  end.
Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
291 292 293 294

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.
295

296 297 298 299
Class DiagNone {A B C} (f : option A  option B  option C) :=
  diag_none : f None None = None.

Section union_intersection_difference.
300
  Context {A} (f : A  A  option A).
301 302 303 304 305 306 307 308

  Global Instance union_with_diag_none : DiagNone (union_with f).
  Proof. reflexivity. Qed.
  Global Instance intersection_with_diag_none : DiagNone (intersection_with f).
  Proof. reflexivity. Qed.
  Global Instance difference_with_diag_none : DiagNone (difference_with f).
  Proof. reflexivity. Qed.
  Global Instance union_with_left_id : LeftId (=) None (union_with f).
309
  Proof. by intros [?|]. Qed.
310
  Global Instance union_with_right_id : RightId (=) None (union_with f).
311
  Proof. by intros [?|]. Qed.
312
  Global Instance union_with_comm :
313
    Comm (=) f  Comm (=@{option A}) (union_with f).
314
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
315
  Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f).
316
  Proof. by intros [?|]. Qed.
317
  Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
318
  Proof. by intros [?|]. Qed.
319
  Global Instance difference_with_comm :
320
    Comm (=) f  Comm (=@{option A}) (intersection_with f).
321
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
322
  Global Instance difference_with_right_id : RightId (=) None (difference_with f).
323
  Proof. by intros [?|]. Qed.
324
End union_intersection_difference.
325 326

(** * Tactics *)
327 328
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
329
  | H : context C [@mguard option _ ?P ?dec] |- _ =>
330 331
    change (@mguard option _ P dec) with (λ A (f : P  option A),
      match @decide P dec with left H' => f H' | _ => None end) in *;
332
    destruct_decide (@decide P dec) as Hx
333
  | |- context C [@mguard option _ ?P ?dec] =>
334 335
    change (@mguard option _ P dec) with (λ A (f : P  option A),
      match @decide P dec with left H' => f H' | _ => None end) in *;
336
    destruct_decide (@decide P dec) as Hx
337 338 339
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
340

341
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
342
  P  (guard P; mx) = mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
Proof. intros. by case_option_guard. Qed.
344
Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
345
  ¬P  (guard P; mx) = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
346
Proof. intros. by case_option_guard. Qed.
347
Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
348
  (P  Q)  (guard P; mx) = guard Q; mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
Proof. intros [??]. repeat case_option_guard; intuition. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
350

Robbert Krebbers's avatar
Robbert Krebbers committed
351
Tactic Notation "simpl_option" "by" tactic3(tac) :=
352
  let assert_Some_None A mx H := first
353
    [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
354 355
      assert (mx = Some x') as H by tac
    | assert (mx = None) as H by tac ]
356
  in repeat match goal with
357
  | H : context [@mret _ _ ?A] |- _ =>
358
     change (@mret _ _ A) with (@Some A) in H
359
  | |- context [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
360 361 362 363
  | 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
364
  | H : context [from_option (A:=?A) _ _ ?mx] |- _ =>
365 366 367
    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
368
    | option ?A =>
369
      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
370
    end
371 372 373 374
  | |- 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
375
  | |- context [from_option (A:=?A) _ _ ?mx] =>
376 377 378
    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
379
    | option ?A =>
380
      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
381
    end
382 383 384 385
  | 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
386 387 388 389
  | _ => rewrite decide_True by tac
  | _ => rewrite decide_False by tac
  | _ => rewrite option_guard_True by tac
  | _ => rewrite option_guard_False by tac
390 391 392 393
  | 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
394
  end.
395
Tactic Notation "simplify_option_eq" "by" tactic3(tac) :=
396
  repeat match goal with
397
  | _ => progress simplify_eq/=
Robbert Krebbers's avatar
Robbert Krebbers committed
398
  | _ => progress simpl_option by tac
399 400 401 402
  | _ : 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
403
  | H : _  _ = Some _ |- _ => apply option_union_Some in H; destruct H
404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
  | 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]
424
  | _ => progress case_decide
425
  | _ => progress case_option_guard
426
  end.
427
Tactic Notation "simplify_option_eq" := simplify_option_eq by eauto.