1 files changed, 76 insertions, 0 deletions
diff --git a/lib/OptionMonad.v b/lib/OptionMonad.v
new file mode 100644
index 00000000..f3566d5c
--- /dev/null
+++ b/lib/OptionMonad.v
@@ -0,0 +1,76 @@
+(* 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.
+