From dac2b6196b756c1566dc9889608d4ee8476d784d Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sat, 6 Nov 2021 17:46:02 +0100 Subject: option monad tactic --- lib/OptionMonad.v | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/OptionMonad.v b/lib/OptionMonad.v index 18430e04..f3566d5c 100644 --- a/lib/OptionMonad.v +++ b/lib/OptionMonad.v @@ -27,12 +27,13 @@ Ltac autodestruct := destruct t eqn:EQ; generalize EQ; clear EQ; congruence || trivial end. -(* deprecated version of "autodestruct". the new one seems a better replacement *) +(* 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)). @@ -61,6 +62,8 @@ Ltac simplify_someHyp := | 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 := @@ -68,3 +71,6 @@ Ltac simplify_someHyps := Ltac try_simplify_someHyps := try (intros; simplify_someHyps; eauto). + +Ltac simplify_option := repeat (try_simplify_someHyps; autodestruct); try_simplify_someHyps. + -- cgit