option.v 17.8 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* 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 iris.prelude Require Export tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
8
9
10
11
12

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.

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

28
29
30
(* 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).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33

(** An alternative, but equivalent, definition of equality on the option
data type. This theorem is useful to prove that two options are the same. *)
34
35
36
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
37
Proof. congruence. Qed.
38
39
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
40
41
Proof. congruence. Qed.

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

45
46
47
48
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.

49
Lemma mk_is_Some {A} (mx : option A) x : mx = Some x  is_Some mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
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.

56
57
58
59
60
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.

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

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

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

81
82
83
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
84
85
86
87
  | None => inright eq_refl
  end.

(** Lifting a relation point-wise to option *)
88
89
90
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
91
92
93
94
95
96
97
98
99
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.

100
101
102
103
104
105
106
107
108
109
110
111
112
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
113
(** Setoids *)
114
115
Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 ().

Robbert Krebbers's avatar
Robbert Krebbers committed
116
Section setoids.
117
  Context `{Equiv A} `{!Equivalence (() : relation A)}.
118
  Implicit Types mx my : option A.
119
120

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

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

132
  Lemma equiv_None mx : mx  None  mx = None.
133
  Proof. split; [by inversion_clear 1|by intros ->]. Qed.
134
  Lemma equiv_Some_inv_l mx my x :
135
136
    mx  my  mx = Some x   y, my = Some y  x  y.
  Proof. destruct 1; naive_solver. Qed.
137
138
  Lemma equiv_Some_inv_r mx my y :
    mx  my  my = Some y   x, mx = Some x  x  y.
139
  Proof. destruct 1; naive_solver. Qed.
140
141
142
143
  Lemma equiv_Some_inv_l' my x : Some x  my   x', Some x' = my  x  x'.
  Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
  Lemma equiv_Some_inv_r' mx y : mx  Some y   y', mx = Some y'  y  y'.
  Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
144

Robbert Krebbers's avatar
Robbert Krebbers committed
145
146
  Global Instance is_Some_proper : Proper (() ==> iff) (@is_Some A).
  Proof. inversion_clear 1; split; eauto. Qed.
147
148
149
  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
150
151
End setoids.

152
153
Typeclasses Opaque option_equiv.

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

(** * Monadic operations *)
Instance option_ret: MRet option := @Some.
170
171
172
173
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
Instance option_fmap: FMap option := @option_map.
175
176
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
177

178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
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
199
Lemma option_bind_assoc {A B C} (f : A  option B)
200
201
202
203
204
205
206
  (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.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Proof. intros. by apply option_bind_ext. Qed.
208
209
210
211
212
213
214
215
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
216

217
218
219
220
Instance option_fmap_proper `{Equiv A, Equiv B} (f : A  B) :
  Proper (() ==> ()) f  Proper (() ==> ()) (fmap (M:=option) f).
Proof. destruct 2; constructor; auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
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
248
(** ** 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.
Instance maybe_Some {A} : Maybe (@Some A) := id.
Arguments maybe_Some _ !_ /.

(** * Union, intersection and difference *)
249
250
251
252
253
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
Robbert Krebbers's avatar
Robbert Krebbers committed
254
255
256
  | None, None => None
  end.
Instance option_intersection_with {A} : IntersectionWith A (option A) :=
257
258
259
260
261
  λ 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
Robbert Krebbers's avatar
Robbert Krebbers committed
262
263
264
  | None, _ => None
  end.
Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
265
266
267
268

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.
Robbert Krebbers's avatar
Robbert Krebbers committed
269

270
271
272
273
Class DiagNone {A B C} (f : option A  option B  option C) :=
  diag_none : f None None = None.

Section union_intersection_difference.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
  Context {A} (f : A  A  option A).
275
276
277
278
279
280
281
282

  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).
Robbert Krebbers's avatar
Robbert Krebbers committed
283
  Proof. by intros [?|]. Qed.
284
  Global Instance union_with_right_id : RightId (=) None (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
285
  Proof. by intros [?|]. Qed.
286
  Global Instance union_with_comm : Comm (=) f  Comm (=) (union_with f).
287
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
288
  Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
289
  Proof. by intros [?|]. Qed.
290
  Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  Proof. by intros [?|]. Qed.
292
  Global Instance difference_with_comm : Comm (=) f  Comm (=) (intersection_with f).
293
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
294
  Global Instance difference_with_right_id : RightId (=) None (difference_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
295
  Proof. by intros [?|]. Qed.
296
End union_intersection_difference.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
298
299
300

(** * Tactics *)
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
301
  | H : context C [@mguard option _ ?P ?dec] |- _ =>
302
303
    change (@mguard option _ P dec) with (λ A (f : P  option A),
      match @decide P dec with left H' => f H' | _ => None end) in *;
Robbert Krebbers's avatar
Robbert Krebbers committed
304
    destruct_decide (@decide P dec) as Hx
305
  | |- context C [@mguard option _ ?P ?dec] =>
306
307
    change (@mguard option _ P dec) with (λ A (f : P  option A),
      match @decide P dec with left H' => f H' | _ => None end) in *;
Robbert Krebbers's avatar
Robbert Krebbers committed
308
309
310
311
312
    destruct_decide (@decide P dec) as Hx
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.

313
314
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
  P  guard P; mx = mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
315
Proof. intros. by case_option_guard. Qed.
316
317
Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
  ¬P  guard P; mx = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
318
Proof. intros. by case_option_guard. Qed.
319
320
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
321
322
Proof. intros [??]. repeat case_option_guard; intuition. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
323
Tactic Notation "simpl_option" "by" tactic3(tac) :=
324
  let assert_Some_None A mx H := first
Robbert Krebbers's avatar
Robbert Krebbers committed
325
    [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
326
327
      assert (mx = Some x') as H by tac
    | assert (mx = None) as H by tac ]
Robbert Krebbers's avatar
Robbert Krebbers committed
328
  in repeat match goal with
329
  | H : context [@mret _ _ ?A] |- _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
330
     change (@mret _ _ A) with (@Some A) in H
331
  | |- context [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
332
333
334
335
  | 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
336
  | H : context [from_option (A:=?A) _ _ ?mx] |- _ =>
337
338
339
    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
340
    | option ?A =>
341
      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
342
    end
343
344
345
346
  | |- 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
347
  | |- context [from_option (A:=?A) _ _ ?mx] =>
348
349
350
    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
351
    | option ?A =>
352
      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
Robbert Krebbers's avatar
Robbert Krebbers committed
353
354
355
356
357
358
359
360
361
    end
  | 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
  | _ => rewrite decide_True by tac
  | _ => rewrite decide_False by tac
  | _ => rewrite option_guard_True by tac
  | _ => rewrite option_guard_False by tac
362
363
364
365
  | 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
366
  end.
367
Tactic Notation "simplify_option_eq" "by" tactic3(tac) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
368
  repeat match goal with
369
  | _ => progress simplify_eq/=
Robbert Krebbers's avatar
Robbert Krebbers committed
370
  | _ => progress simpl_option by tac
Robbert Krebbers's avatar
Robbert Krebbers committed
371
372
373
374
375
  | _ : 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
  | H : _  _ = Some _ |- _ => apply option_union_Some in H; destruct H
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
  | 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]
Robbert Krebbers's avatar
Robbert Krebbers committed
396
397
398
  | _ => progress case_decide
  | _ => progress case_option_guard
  end.
399
Tactic Notation "simplify_option_eq" := simplify_option_eq by eauto.