From cdadc5d338e3c00c4cd22a3a3d7197f71d4d7a44 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Mon, 26 Apr 2021 18:27:37 +0200
Subject: Equality between Booleans should be changed for hypotheses

---
 src/PropToBool.v                 | 14 ++++++++++---
 src/QInst.v                      | 43 +++++++++++++++++++++++++++++++++++++++-
 unit-tests/Tests_verit_tactics.v | 11 ++++++++++
 3 files changed, 64 insertions(+), 4 deletions(-)

diff --git a/src/PropToBool.v b/src/PropToBool.v
index 64d88cf..8dc970f 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -42,12 +42,16 @@ Ltac prop2bool :=
     | [ |- context[ Z.ge _ _ ] ] => rewrite <- geb_ge
     | [ |- context[ Z.eq _ _ ] ] => rewrite <- Z.eqb_eq
 
-    | [ |- context[ @Logic.eq ?t _ _ ] ] =>
+    | [ |- context[ @Logic.eq ?t ?x ?y ] ] =>
       lazymatch t with
       | bitvector _ => rewrite <- bv_eq_reflect
       | farray _ _ => rewrite <- equal_iff_eq
       | Z => rewrite <- Z.eqb_eq
-      | bool => fail
+      | bool =>
+        lazymatch y with
+        | true => fail
+        | _ => rewrite <- eqb_true_iff
+        end
       | _ =>
         lazymatch goal with
         | [ p: (CompDec t) |- _ ] =>
@@ -107,6 +111,8 @@ Ltac bool2prop_true :=
     | [ |- context[ Z.geb _ _ ] ] => rewrite geb_ge
     | [ |- context[ Z.eqb _ _ = true ] ] => rewrite Z.eqb_eq
 
+    |  [ |- context[ Bool.eqb _ _ = true ] ] => rewrite eqb_true_iff
+
     | [ |- context[ eqb_of_compdec ?p _ _ = true ] ] => rewrite <- (@compdec_eq_eqb _ p)
 
     | [ |- context[ ?G0 || ?G1 = true ] ] =>
@@ -218,6 +224,7 @@ Section Test.
   Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = length l1 + length l2.
   Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z.
   Hypothesis uninterpreted_type : forall (a:A), a = a.
+  Hypothesis bool_eq : forall (b:bool), negb (negb b) = b.
 
   Goal True.
   Proof.
@@ -225,12 +232,13 @@ Section Test.
     prop2bool_hyp no_eq.
     prop2bool_hyp uninterpreted_type.
     admit.
+    prop2bool_hyp bool_eq.
     prop2bool_hyp plus_n_O.
   Abort.
 
   Goal True.
   Proof.
-    prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, plus_O_n).
+    prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, bool_eq, plus_O_n).
     admit.
   Abort.
 End Test.
diff --git a/src/QInst.v b/src/QInst.v
index 4ebdcc9..4a4ddc2 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -29,7 +29,7 @@ Qed.
 
 Hint Resolve impl_split.
 
-(* verit silently transforms an <implb (a || b) c> into a <or (not a) c>
+(** 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 *)
 Lemma impl_or_split_right a b c:
   implb (a || b) c = true -> negb b || c = true.
@@ -45,6 +45,35 @@ Proof.
   destruct a; destruct c; intuition.
 Qed.
 
+(** same for Boolean equivalence, modulo symmetry *)
+Lemma eqb_sym_or_split_right a b c:
+  Bool.eqb c (a || b) = true -> negb b || c = true.
+Proof.
+  intro H.
+  destruct a; destruct c; intuition.
+Qed.
+
+Lemma eqb_sym_or_split_left a b c:
+  Bool.eqb c (a || b) = true -> negb a || c = true.
+Proof.
+  intro H.
+  destruct a; destruct c; intuition.
+Qed.
+
+Lemma eqb_or_split_right a b c:
+  Bool.eqb (a || b) c = true -> negb b || c = true.
+Proof.
+  intro H.
+  destruct a; destruct c; intuition.
+Qed.
+
+Lemma eqb_or_split_left a b c:
+  Bool.eqb (a || b) c = true -> negb a || c = true.
+Proof.
+  intro H.
+  destruct a; 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 *)
@@ -159,6 +188,18 @@ Ltac vauto :=
                        | eapply impl_or_split_left;
                          first [ strategy1 H
                                | strategy2 H ]
+                       | eapply eqb_sym_or_split_right;
+                         first [ strategy1 H
+                               | strategy2 H ]
+                       | eapply eqb_sym_or_split_left;
+                         first [ strategy1 H
+                               | strategy2 H ]
+                       | eapply eqb_or_split_right;
+                         first [ strategy1 H
+                               | strategy2 H ]
+                       | eapply eqb_or_split_left;
+                         first [ strategy1 H
+                               | strategy2 H ]
                        ]
                end
              ]
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 73b59f4..d1c57f4 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1238,3 +1238,14 @@ Section Issue78.
   Proof. verit. Qed.
 
 End Issue78.
+
+
+Section SearchApp.
+  Variable search : Z -> list Z -> bool.
+  Hypothesis search_app : forall (x: Z) (l1 l2: list Z),
+    search x (l1 ++ l2) = orb (search x l1) (search x l2).
+
+  Lemma search_lemma : forall (x: Z) (l1 l2 l3: list Z),
+      search x (l1 ++ l2 ++ l3) = search x (l3 ++ l2 ++ l1).
+  Proof. verit. Qed.
+End SearchApp.
-- 
cgit