option.v 18.4 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.
6
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10 11 12 13

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. *)
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 27
Instance: Params (@from_option) 3.
Arguments from_option {_ _} _ _ !_ /.
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
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 42
Proof. congruence. Qed.

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.
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54 55 56
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.

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).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Robbert Krebbers's avatar
Robbert Krebbers committed
66
    Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
67 68 69 70
  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
71
Qed.
72

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

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 87 88
  | None => inright eq_refl
  end.

(** 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 125
  Global Instance option_equivalence :
    Equivalence (() : relation A)  Equivalence (() : relation (option A)).
126
  Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  Global Instance Some_proper : Proper (() ==> ()) (@Some A).
128
  Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  Global Instance Some_equiv_inj : Inj () () (@Some A).
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 144 145
  Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
  Lemma equiv_Some_inv_r' `{!Equivalence (() : relation A)} mx y :
    mx  Some y   y', mx = Some y'  y  y'.
146
  Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
147

Robbert Krebbers's avatar
Robbert Krebbers committed
148
  Global Instance is_Some_proper : Proper (() ==> iff) (@is_Some A).
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.

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

(** * Monadic operations *)
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (() : relation B)}
Ralf Jung's avatar
Ralf Jung committed
187 188 189 190 191 192 193 194 195
      (f : A  B) mx y :
  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.
196
Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence (() : relation B)}
197 198
      (f : A  B) mx y :
  f <$> mx  Some y   x, mx = Some x  y  f x.
199
Proof. by rewrite fmap_Some_equiv. Qed.
200 201 202 203 204 205 206 207 208 209
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.
210
Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A  B) mx :
211 212 213 214 215
  ( 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
216
Lemma option_bind_assoc {A B C} (f : A  option B)
217 218 219 220 221 222 223
  (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
224
Proof. intros. by apply option_bind_ext. Qed.
225 226 227 228 229 230 231 232
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
233

234 235 236 237
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
238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265
(** ** 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 *)
266 267 268 269 270
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
271 272 273
  | None, None => None
  end.
Instance option_intersection_with {A} : IntersectionWith A (option A) :=
274 275 276 277 278
  λ 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
279 280 281
  | None, _ => None
  end.
Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
282 283 284 285

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
286

287 288 289 290
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
291
  Context {A} (f : A  A  option A).
292 293 294 295 296 297 298 299

  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
300
  Proof. by intros [?|]. Qed.
301
  Global Instance union_with_right_id : RightId (=) None (union_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
302
  Proof. by intros [?|]. Qed.
303
  Global Instance union_with_comm : Comm (=) f  Comm (=) (union_with f).
304
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
305
  Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
306
  Proof. by intros [?|]. Qed.
307
  Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
308
  Proof. by intros [?|]. Qed.
309
  Global Instance difference_with_comm : Comm (=) f  Comm (=) (intersection_with f).
310
  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
311
  Global Instance difference_with_right_id : RightId (=) None (difference_with f).
Robbert Krebbers's avatar
Robbert Krebbers committed
312
  Proof. by intros [?|]. Qed.
313
End union_intersection_difference.
Robbert Krebbers's avatar
Robbert Krebbers committed
314 315 316 317

(** * Tactics *)
Tactic Notation "case_option_guard" "as" ident(Hx) :=
  match goal with
318
  | H : context C [@mguard option _ ?P ?dec] |- _ =>
319 320
    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
321
    destruct_decide (@decide P dec) as Hx
322
  | |- context C [@mguard option _ ?P ?dec] =>
323 324
    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
325 326 327 328 329
    destruct_decide (@decide P dec) as Hx
  end.
Tactic Notation "case_option_guard" :=
  let H := fresh in case_option_guard as H.

330 331
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
  P  guard P; mx = mx.
Robbert Krebbers's avatar
Robbert Krebbers committed
332
Proof. intros. by case_option_guard. Qed.
333 334
Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
  ¬P  guard P; mx = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
335
Proof. intros. by case_option_guard. Qed.
336 337
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
338 339
Proof. intros [??]. repeat case_option_guard; intuition. Qed.

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