(* Declare Scope option_monad_scope. *)

Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
         (at level 200, X ident, A at level 100, B at level 200)
         : option_monad_scope.

Notation "'ASSERT' A 'IN' B" := (if A then B else None)
         (at level 200, A at level 100, B at level 200)
         : option_monad_scope.

Local Open Scope option_monad_scope.


(** Simple tactics for option-monad *)

Ltac deepest_match exp := 
  match exp with
  | context f [match ?expr with | _ => _ end] => ltac: (deepest_match expr)
  | _ => exp
  end.

Ltac autodestruct :=
  let EQ := fresh "EQ" in 
  match goal with
  | |- context f [match ?expr with | _ => _ end] => 
    let t := ltac: (deepest_match expr) in
    destruct t eqn:EQ; generalize EQ; clear EQ; congruence || trivial
  end.

(* deprecated version of "autodestruct". the new one seems a better replacement
Ltac dummy_autodestruct := 
  let EQ := fresh "EQ" in 
  match goal with
  | |- context f [match ?expr with | _ => _ end] => destruct expr eqn:EQ; generalize EQ; clear EQ; congruence || trivial
  end.
*)

Lemma destruct_SOME A B (P: option B -> Prop) (e: option A) (f: A -> option B):
  (forall x, e = Some x -> P (f x)) -> (e = None -> P None) -> (P (SOME x <- e IN f x)).
Proof.
  intros; destruct e; simpl; auto.
Qed.

Lemma destruct_ASSERT B (P: option B -> Prop) (e: bool) (x: option B):
  (e = true -> P x) -> (e = false -> P None) -> (P (ASSERT e IN x)).
Proof.
  intros; destruct e; simpl; auto.
Qed.

Ltac inversion_SOME x :=
  try (eapply destruct_SOME; [ let x := fresh x in intro x | simpl; try congruence ]).

Ltac inversion_ASSERT :=
  try (eapply destruct_ASSERT; [ idtac | simpl; try congruence ]).

Ltac simplify_someHyp :=
  match goal with
  | H: None = Some _ |- _  => inversion H; clear H; subst
  | H: Some _ = None |- _  => inversion H; clear H; subst
  | H: ?t = ?t |- _ => clear H
  | H: Some _ = Some _ |- _  => inversion H; clear H; subst
  | H: Some _ <> None |- _ => clear H
  | H: None <> Some _ |- _ => clear H
  | H: _ = Some _ |- _ => (try rewrite !H in * |- *); generalize H; clear H
  | H: _ = None |- _ => (try rewrite !H in * |- *); generalize H; clear H
  | H: None = _ |- _ => (try rewrite <- !H in * |- *); generalize H; clear H
  end.

Ltac simplify_someHyps := 
  repeat (simplify_someHyp; simpl in * |- *).

Ltac try_simplify_someHyps := 
  try (intros; simplify_someHyps; eauto).

Ltac simplify_option := repeat (try_simplify_someHyps; autodestruct); try_simplify_someHyps.