option.v 17.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
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 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).
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
Proof. congruence. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
41

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.
50 51 52 53 54
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
55

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).
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
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.
70
Qed.
71

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
87
(** 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.

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).
160
Proof.
161
 refine (λ mx my,
162 163
  match mx, my with
  | Some x, Some y => cast_if (decide (x = y))
164
  | None, None => left _ | _, _ => right _
165
  end); clear dec; abstract congruence.
166
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
167

168
(** * Monadic operations *)
169
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.
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.
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.
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.

221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244
(** ** 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
245 246
Instance maybe_Some {A} : Maybe (@Some A) := id.
Arguments maybe_Some _ !_ /.
247

248
(** * Union, intersection and difference *)
249
Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
250 251 252 253
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
  | None, Some y => Some y
254 255
  | None, None => None
  end.
256 257 258
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,
259 260 261
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
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.
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.
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).
283
  Proof. by intros [?|]. Qed.
284
  Global Instance union_with_right_id : RightId (=) None (union_with f).
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).
289
  Proof. by intros [?|]. Qed.
290
  Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
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).
295
  Proof. by intros [?|]. Qed.
296
End union_intersection_difference.
297 298

(** * Tactics *)
299 300
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
301
  | H : appcontext 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 *;
304 305
    destruct_decide (@decide P dec) as Hx
  | |- appcontext 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 *;
308
    destruct_decide (@decide P dec) as Hx
309 310 311
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
312

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
Proof. intros [??]. repeat case_option_guard; intuition. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
322

Robbert Krebbers's avatar
Robbert Krebbers committed
323
Tactic Notation "simpl_option" "by" tactic3(tac) :=
324
  let assert_Some_None A mx H := first
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 ]
328
  in repeat match goal with
329 330 331
  | H : appcontext [@mret _ _ ?A] |- _ =>
     change (@mret _ _ A) with (@Some A) in H
  | |- appcontext [@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
    end
354 355 356 357
  | 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
358 359 360 361
  | _ => 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) :=
368
  repeat match goal with
369
  | _ => progress simplify_eq/=
Robbert Krebbers's avatar
Robbert Krebbers committed
370
  | _ => progress simpl_option by tac
371 372 373 374
  | _ : 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
375
  | 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]
396
  | _ => progress case_decide
397
  | _ => progress case_option_guard
398
  end.
399
Tactic Notation "simplify_option_eq" := simplify_option_eq by eauto.