From 0a459d80f75f0abbc60936c3e5b99d993272ce6b Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Mon, 15 Nov 2021 17:35:34 +0100
Subject: More bad instanciations by verit

---
 src/QInst.v                      | 34 +++++++++++++++++++++++++++++++++-
 unit-tests/Tests_verit_tactics.v | 26 ++++++++++++++++++++++++++
 2 files changed, 59 insertions(+), 1 deletion(-)

diff --git a/src/QInst.v b/src/QInst.v
index 16a4d5f..a683bcd 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -27,6 +27,15 @@ Proof.
    installed when we compile SMTCoq. *)
 Qed.
 
+Lemma impl_split2 a b c:
+  implb a (b || c) = true -> (negb a) || b || c = true.
+Proof.
+  intro H.
+  destruct a; destruct b; trivial.
+(* alternatively we could do <now verit_base H.> but it forces us to have veriT
+   installed when we compile SMTCoq. *)
+Qed.
+
 
 (** verit silently transforms an <implb (a || b) c> into a <or (not a) c>
    or into a <or (not b) c> when instantiating such a quantified theorem *)
@@ -80,6 +89,25 @@ Proof.
   destruct a; destruct b; destruct c; intuition.
 Qed.
 
+(** verit silently transforms an <implb a (b && c)> into a <or (not a)
+    b> or into a <or (not a) c> when instantiating such a quantified
+    theorem. *)
+Lemma impl_and_split_right a b c:
+  implb a (b && c) = true -> negb a || c = true.
+Proof.
+  intro H.
+  destruct a; destruct c; intuition.
+  now rewrite andb_false_r in H.
+Qed.
+
+Lemma impl_and_split_left a b c:
+  implb a (b && c) = true -> negb a || b = true.
+Proof.
+  intro H.
+  destruct a; destruct b; 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 *)
@@ -120,9 +148,13 @@ Ltac vauto :=
                        | eapply eqb_sym_or_split_left; apply_sym H
                        | eapply eqb_or_split_right; apply_sym H
                        | eapply eqb_or_split_left; apply_sym H
+                       | eapply impl_and_split_right; apply_sym H
+                       | eapply impl_and_split_left; apply_sym H
                        ]
                | [ |- (negb ?A || ?B || ?C) = true ] =>
-                 eapply eqb_or_split; apply_sym H
+                 first [ eapply eqb_or_split; apply_sym H
+                       | eapply impl_split2; apply_sym H
+                       ]
                end
              ]
       );
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 2f080a8..ce530bd 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1449,3 +1449,29 @@ Section NonPrenexDependentTypes.
 
 End NonPrenexDependentTypes.
 *)
+
+
+Section QInstAnd.
+
+  Variable A : Type.
+  Hypothesis HA : CompDec A.
+
+  Hypothesis H : forall (a1 a2:A) l1 l2,
+      eqb_of_compdec _ (a1::l1) (a2::l2) --->
+        (eqb_of_compdec HA a1 a2) && (eqb_of_compdec _ l1 l2).
+
+  Variables a1 a2 : A.
+  Variables l1 l2 : list A.
+  Hypothesis H1 : eqb_of_compdec _ (a1::l1) (a2::l2).
+
+  Goal eqb_of_compdec _ a1 a2.
+  Proof. verit. Qed.
+
+  Variable inb : A -> list A -> bool.
+
+  Hypothesis H2 : forall (a:A) l1 l2, inb a (l1++l2) ---> (inb a l1 || inb a l2).
+
+  Goal negb (inb a1 (l1++l2)) || inb a1 l1 || inb a1 l2.
+  Proof. verit. Qed.
+
+End QInstAnd.
-- 
cgit