diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-11-06 17:46:02 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-11-06 17:46:02 +0100 |
| commit | dac2b6196b756c1566dc9889608d4ee8476d784d (patch) | |
| tree | 4b90e345da8cd01b58ea9615e4730d2d56986e05 /lib | |
| parent | 17b1ec4333af8120ab6867baf9c5c9139541c6b7 (diff) | |
| download | compcert-kvx-dac2b6196b756c1566dc9889608d4ee8476d784d.tar.gz compcert-kvx-dac2b6196b756c1566dc9889608d4ee8476d784d.zip | |
option monad tactic
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/OptionMonad.v | 8 |
1 files changed, 7 insertions, 1 deletions
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. + |