diff options
Diffstat (limited to 'lib/OptionMonad.v')
-rw-r--r-- | lib/OptionMonad.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/lib/OptionMonad.v b/lib/OptionMonad.v index 824a9c2f..18430e04 100644 --- a/lib/OptionMonad.v +++ b/lib/OptionMonad.v @@ -13,6 +13,27 @@ 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. |