From d5697269991500ed1b4b3e6bbec6108ea3a059bb Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 29 Jul 2022 10:49:00 +0200 Subject: New case for vauto --- src/QInst.v | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'src/QInst.v') 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 -- cgit