Convert hypotheses from Prop to bool (#89)

* This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed.

* Some current limitations are detailed in src/PropToBool.v.

* Partially enhances #30 .

3 files changed, 15 insertions, 30 deletions

diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v
index 4162f13..6ddf5a5 100644
--- a/src/versions/standard/Tactics_standard.v
+++ b/src/versions/standard/Tactics_standard.v
@@ -10,18 +10,18 @@
 (**************************************************************************)
 
 
-Require Import PropToBool BoolToProp.  (* Before SMTCoq.State *)
+Require Import PropToBool.
 Require Import Int63 List PArray Bool ZArith.
 Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances QInst.
 
 Declare ML Module "smtcoq_plugin".
 
 
-Tactic Notation "verit_bool" constr_list(h) :=
-  verit_bool_base h; vauto.
+Tactic Notation "verit_bool" constr(h) := verit_bool_base (Some h); vauto.
+Tactic Notation "verit_bool"           := verit_bool_base (@None nat); vauto.
 
-Tactic Notation "verit_bool_no_check" constr_list(h) :=
-  verit_bool_no_check_base h; vauto.
+Tactic Notation "verit_bool_no_check" constr(h) := verit_bool_no_check_base (Some h); vauto.
+Tactic Notation "verit_bool_no_check"           := verit_bool_no_check_base (@None nat); vauto.
 
 
 (** Tactics in Prop **)
@@ -29,32 +29,18 @@ Tactic Notation "verit_bool_no_check" constr_list(h) :=
 Ltac zchaff          := prop2bool; zchaff_bool; bool2prop.
 Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop.
 
-Tactic Notation "verit" constr_list(h) := prop2bool; [ .. | verit_bool h; bool2prop ].
-Tactic Notation "verit_no_check" constr_list(h) := prop2bool; [ .. | verit_bool_no_check h; bool2prop ].
+Tactic Notation "verit" constr(h) := prop2bool; [ .. | prop2bool_hyps h; [ .. | verit_bool h; bool2prop ] ].
+Tactic Notation "verit"           := prop2bool; [ .. | verit_bool  ; bool2prop ].
+Tactic Notation "verit_no_check" constr(h) := prop2bool; [ .. | prop2bool_hyps h; [ .. | verit_bool_no_check h; bool2prop ] ].
+Tactic Notation "verit_no_check"           := prop2bool; [ .. | verit_bool_no_check  ; bool2prop ].
 
 Ltac cvc4            := prop2bool; [ .. | cvc4_bool; bool2prop ].
 Ltac cvc4_no_check   := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ].
 
-
-(* Ltac smt := prop2bool; *)
-(*             repeat *)
-(*               match goal with *)
-(*                 | [ |- context[ CompDec ?t ] ] => try assumption *)
-(*                 | [ |- _ : bool] => verit_bool *)
-(*                 | [ |- _ : bool] => try (cvc4_bool; verit_bool) *)
-(*               end; *)
-(*             bool2prop. *)
-(* Ltac smt_no_check := prop2bool; *)
-(*             repeat *)
-(*               match goal with *)
-(*                 | [ |- context[ CompDec ?t ] ] => try assumption *)
-(*                 | [ |- _ : bool] => verit_bool_no_check *)
-(*                 | [ |- _ : bool] => try (cvc4_bool_no_check; verit_bool_no_check) *)
-(*               end; *)
-(*             bool2prop. *)
-
-Tactic Notation "smt" constr_list(h) := (prop2bool; [ .. | try verit_bool h; cvc4_bool; try verit_bool h; bool2prop ]).
-Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; [ .. | try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; bool2prop]).
+Tactic Notation "smt" constr(h) := (prop2bool; [ .. | try (prop2bool_hyps h; [ .. | verit_bool h ]); cvc4_bool; try (prop2bool_hyps h; [ .. | verit_bool h ]); bool2prop ]).
+Tactic Notation "smt"           := (prop2bool; [ .. | try verit_bool  ; cvc4_bool; try verit_bool  ; bool2prop ]).
+Tactic Notation "smt_no_check" constr(h) := (prop2bool; [ .. | try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); cvc4_bool_no_check; try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); bool2prop]).
+Tactic Notation "smt_no_check"           := (prop2bool; [ .. | try verit_bool_no_check  ; cvc4_bool_no_check; try verit_bool_no_check  ; bool2prop]).
 
 
 
diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject
index e067da8..86dd443 100644
--- a/src/versions/standard/_CoqProject
+++ b/src/versions/standard/_CoqProject
@@ -149,7 +149,6 @@ Misc.v
 SMTCoq.v
 ReflectFacts.v
 PropToBool.v
-BoolToProp.v
 QInst.v
 Tactics.v
 SMT_terms.v
diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4
index 6c3b8cf..2411316 100644
--- a/src/versions/standard/g_smtcoq_standard.ml4
+++ b/src/versions/standard/g_smtcoq_standard.ml4
@@ -109,8 +109,8 @@ END
 
 
 TACTIC EXTEND Tactic_verit
-| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ]
-| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ]
+| [ "verit_bool_base" constr(lpl) ] -> [ Verit.tactic lpl (get_lemmas ()) ]
+| [ "verit_bool_no_check_base" constr(lpl) ] -> [ Verit.tactic_no_check lpl (get_lemmas ()) ]
 END
 
 TACTIC EXTEND Tactic_cvc4