From cfadb667ba2c9904ff0d94bf186cf9f89e370515 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Thu, 6 May 2021 18:44:01 +0200
Subject: Another silent change of veriT...

---
 src/QInst.v                      | 11 +++++++++++
 unit-tests/Tests_verit_tactics.v | 22 ++++++++++++++++++++++
 2 files changed, 33 insertions(+)

diff --git a/src/QInst.v b/src/QInst.v
index 4a4ddc2..2684dea 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -74,6 +74,13 @@ Proof.
   destruct a; destruct c; intuition.
 Qed.
 
+Lemma eqb_or_split a b c:
+  Bool.eqb c (a || b) = true -> negb c || a || b = true.
+Proof.
+  intro H.
+  destruct a; destruct b; destruct c; intuition.
+Qed.
+
 (** verit considers equality modulo its symmetry, so we have to recover the
     right direction in the instances of the theorems *)
 (* TODO: currently incomplete *)
@@ -201,6 +208,10 @@ Ltac vauto :=
                          first [ strategy1 H
                                | strategy2 H ]
                        ]
+               | [ |- (negb ?A || ?B || ?C) = true ] =>
+                 eapply eqb_or_split;
+                 first [ strategy1 H
+                       | strategy2 H ]
                end
              ]
       );
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 0e2509a..9c5e7f4 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1341,3 +1341,25 @@ Section Issue92.
   Goal 0 = 2.
   Proof. verit_no_check. Abort.
 End Issue92.
+
+
+Section Vauto.
+  Variable A : Type.
+  Variable HA : CompDec A.
+  Variable H0 : forall (x y : A) (x0 y0 : list A), x :: x0 = y :: y0 -> y = x /\ y0 = x0.
+  Variable H1 : forall (H : A) (H0 : list A), nil = H :: H0 -> False.
+  Variable search : forall {A : Type} {H: CompDec A}, A -> list A -> bool.
+  Arguments search {_ _} _ _.
+  Variable H4_A : forall (H : CompDec A) (H0 H1 : A) (H2 : list A),
+         search H0 (H1 :: H2) = eqb_of_compdec H H0 H1 || search H0 H2.
+  Variable H2 : forall (H : CompDec (list A)) (H0 H1 : list A) (H2 : list (list A)),
+       search H0 (H1 :: H2) = eqb_of_compdec H H0 H1 || search H0 H2.
+  Variable H3_A : forall (H : CompDec A) (H0 : A), search H0 nil = false.
+  Variable H4 : forall (H : CompDec (list A)) (H0 : list A), search H0 nil = false.
+  Variables a b : A.
+  Variable l : list A.
+  Variable H : search b (a :: l).
+
+  Goal eqb_of_compdec HA a b \/ search b l.
+  Proof. verit_no_check. Qed.
+End Vauto.
-- 
cgit