Adding support for lemmas in the command verit

1 files changed, 61 insertions, 0 deletions

diff --git a/src/SMTCoq.v b/src/SMTCoq.v
index c7588af..a17c840 100644
--- a/src/SMTCoq.v
+++ b/src/SMTCoq.v
@@ -20,3 +20,64 @@ Require Export Conversion_tactics.
 Export Atom Form Sat_Checker Cnf_Checker Euf_Checker.
 
 Declare ML Module "smtcoq_plugin".
+
+Require Import Bool.
+Open Scope Z_scope.
+
+(* verit silently transforms an <implb a b> into a <or (not a) b> when
+ instantiating a quantified theorem with <implb> *)
+Lemma impl_split a b:
+  implb a b = true -> orb (negb a) b = 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.
+
+Hint Resolve impl_split.
+
+(* 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 -> negb b || c.
+Proof.
+  intro H.
+  destruct a; destruct c; intuition.
+Qed.
+
+Lemma impl_or_split_left a b c:
+  implb (a || b) c -> negb a || c.
+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 *)
+Definition hidden_eq a b := a =? b.
+Ltac all_rew :=
+  repeat match goal with
+         | [ |- context [ ?A =? ?B]] =>
+           change (A =? B) with (hidden_eq A B)
+         end;
+  repeat match goal with
+         | [ |- context [ hidden_eq ?A ?B] ] =>
+           replace (hidden_eq A B) with (B =? A);
+           [ | now rewrite Z.eqb_sym]
+         end.
+
+(* An automatic tactic that takes into account all those transformations *)
+Ltac vauto :=
+  try (let H := fresh "H" in
+       intro H; try (all_rew; apply H);
+       match goal with
+       | [ |- is_true (negb ?A || ?B) ] =>
+         try (eapply impl_or_split_right; apply H);
+         eapply impl_or_split_left; apply H
+       end;
+       apply H);
+  auto.
+
+Ltac verit :=
+  verit_base; vauto.