diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-07-29 10:49:00 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-07-29 10:49:00 +0200 |
| commit | d5697269991500ed1b4b3e6bbec6108ea3a059bb (patch) | |
| tree | 89c189decec919ebd852a6a22c974472d52ae673 /src | |
| parent | f36bf11e994cc269c2ec92b061b082e3516f472f (diff) | |
| download | smtcoq-d5697269991500ed1b4b3e6bbec6108ea3a059bb.tar.gz smtcoq-d5697269991500ed1b4b3e6bbec6108ea3a059bb.zip | |
New case for vauto
Diffstat (limited to 'src')
| -rw-r--r-- | src/QInst.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/QInst.v b/src/QInst.v index d891fe2..5e88a0b 100644 --- a/src/QInst.v +++ b/src/QInst.v @@ -27,6 +27,13 @@ Proof. installed when we compile SMTCoq. *) Qed. +Lemma impl2_split a b c: + implb a (implb b c) = true -> (negb a) || (negb b) || c = true. +Proof. + intro H. + destruct a; destruct b; destruct c; trivial. +Qed. + Lemma impl_split2 a b c: implb a (b || c) = true -> (negb a) || b || c = true. Proof. @@ -180,7 +187,8 @@ Ltac vauto := | eapply impl_and_split_left; apply_sym H ] | [ |- (negb ?A || ?B || ?C) = true ] => - first [ eapply eqb_or_split; apply_sym H + first [ eapply impl2_split; apply_sym H + | eapply eqb_or_split; apply_sym H | eapply impl_split2; apply_sym H | eapply impl_split211; apply_sym H | eapply impl_split212; apply_sym H |