diff options
Diffstat (limited to 'src/versions/standard/Tactics_standard.v')
| -rw-r--r-- | src/versions/standard/Tactics_standard.v | 40 |
1 files changed, 13 insertions, 27 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]). |