Equality between Booleans should be changed for hypotheses

1 files changed, 42 insertions, 1 deletions

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
              ]