From d5697269991500ed1b4b3e6bbec6108ea3a059bb Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Fri, 29 Jul 2022 10:49:00 +0200
Subject: New case for vauto

---
 src/QInst.v                      | 10 +++++++++-
 unit-tests/Tests_verit_tactics.v | 27 +++++++++++++++++++++++++++
 2 files changed, 36 insertions(+), 1 deletion(-)

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
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 5164308..7be08d4 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1365,6 +1365,33 @@ Section Vauto.
 End Vauto.
 
 
+Require QInst.
+
+Section Vauto2.
+  Variable A : Type.
+  Variable Inv_A : Z -> A -> Prop.
+  Variable Inv_A_bool : Z -> A -> bool.
+  Variable y : Z.
+  Variable l : A.
+  Variable z : Z.
+  Variable H : Inv_A y l.
+  Variable H0 : z <= y.
+  Variable H2 : forall (H2 : A) (a b : Z),
+      Inv_A_bool a H2 ---> (b <=? a) ---> Inv_A_bool b H2 = true.
+  Variable H3 : Inv_A_bool y l = true.
+  Variable H4 : (z <=? y) = true.
+  Variable H5 : forall (c : A) (a b : Z),
+      Inv_A_bool a c ---> (b <=? a) ---> Inv_A_bool b c = true.
+  Variable CompDec0 : CompDec A.
+
+  Goal
+    (forall (c : A) (a b : Z),
+        Inv_A_bool a c ---> (b <=? a) ---> Inv_A_bool b c = true) ->
+    negb (Inv_A_bool y l) || negb (z <=? y) || Inv_A_bool z l.
+  Proof. QInst.vauto. Qed.
+End Vauto2.
+
+
 Section PropToBool.
   Goal (forall (x x0 : bool) (x1 x2 : list bool), x :: x1 = x0 :: x2 -> x = x0) -> true.
   Proof. verit. Qed.
-- 
cgit