From 4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 Mon Sep 17 00:00:00 2001 From: ckeller Date: Wed, 21 Apr 2021 09:46:30 +0200 Subject: 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 . --- src/versions/standard/Tactics_standard.v | 40 ++++++++++------------------- src/versions/standard/_CoqProject | 1 - src/versions/standard/g_smtcoq_standard.ml4 | 4 +-- 3 files changed, 15 insertions(+), 30 deletions(-) (limited to 'src/versions') 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 -- cgit