Module OptionMonad

Require Import List.

Declare Scope option_monad_scope.

Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
         (at level 200, X name, 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.



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.

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


Fixpoint map_opt {A B} (f : A -> option B) (l : list A) : option (list B) :=
  match l with
  | nil => Some nil
  | cons x xs => SOME y <- f x IN
                 SOME ys <- map_opt f xs IN
                 Some (cons y ys)
  end.


Inductive elim_SOME_someT [A B] (a : option A) (f : A -> option B) (y : B) : Prop :=
  | Elim_SOME_someT (x : A) (SOME_x : a = Some x) (SOME_y : f x = Some y).

Lemma elim_SOME_Some [A B] [a : option A] [f : A -> option B] [y : B]:
  (SOME x <- a IN f x) = Some y ->
  elim_SOME_someT a f y.