From 02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b Mon Sep 17 00:00:00 2001 From: ckeller Date: Fri, 12 Apr 2019 14:13:00 +0200 Subject: Error message to state that tactics are not supported with native-coq (#47) * Better error message for failing tactics with native-coq --- src/QInst.v | 80 ++++++++++++++++++ src/Tactics.v | 122 --------------------------- src/configure.sh | 3 + src/versions/native/Make | 2 +- src/versions/native/Makefile | 2 +- src/versions/native/Tactics_native.v | 55 ++++++++++++ src/versions/native/smtcoq_plugin_native.ml4 | 10 ++- src/versions/standard/Tactics_standard.v | 65 ++++++++++++++ src/versions/standard/_CoqProject | 1 + 9 files changed, 212 insertions(+), 128 deletions(-) create mode 100644 src/QInst.v delete mode 100644 src/Tactics.v create mode 100644 src/versions/native/Tactics_native.v create mode 100644 src/versions/standard/Tactics_standard.v (limited to 'src') diff --git a/src/QInst.v b/src/QInst.v new file mode 100644 index 0000000..724a482 --- /dev/null +++ b/src/QInst.v @@ -0,0 +1,80 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +Require Import Bool ZArith. +Require Import State. + + +(** Handling quantifiers with veriT **) + +(* verit silently transforms an into a when + instantiating a quantified theorem with *) +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 but it forces us to have veriT + installed when we compile SMTCoq. *) +Qed. + +Hint Resolve impl_split. + +(* verit silently transforms an into a + or into a when instantiating such a quantified theorem *) +Lemma impl_or_split_right a b c: + implb (a || b) c = true -> negb b || c = true. +Proof. + intro H. + destruct a; destruct c; intuition. +Qed. + +Lemma impl_or_split_left a b c: + implb (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 *) +Definition hidden_eq (a b : Z) := (a =? b)%Z. +Ltac all_rew := + repeat match goal with + | [ |- context [ (?A =? ?B)%Z]] => + change (A =? B)%Z with (hidden_eq A B) + end; + repeat match goal with + | [ |- context [ hidden_eq ?A ?B] ] => + replace (hidden_eq A B) with (B =? A)%Z; + [ | 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. + + + +(* + Local Variables: + coq-load-path: ((rec "." "SMTCoq")) + End: +*) diff --git a/src/Tactics.v b/src/Tactics.v deleted file mode 100644 index 106e128..0000000 --- a/src/Tactics.v +++ /dev/null @@ -1,122 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2019 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -Require Import PropToBool BoolToProp. (* Before SMTCoq.State *) -Require Import Int63 List PArray Bool ZArith. -Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances. - -Declare ML Module "smtcoq_plugin". - - -(** Handling quantifiers with veriT **) - -(* verit silently transforms an into a when - instantiating a quantified theorem with *) -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 but it forces us to have veriT - installed when we compile SMTCoq. *) -Qed. - -Hint Resolve impl_split. - -(* verit silently transforms an into a - or into a when instantiating such a quantified theorem *) -Lemma impl_or_split_right a b c: - implb (a || b) c = true -> negb b || c = true. -Proof. - intro H. - destruct a; destruct c; intuition. -Qed. - -Lemma impl_or_split_left a b c: - implb (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 *) -Definition hidden_eq (a b : Z) := (a =? b)%Z. -Ltac all_rew := - repeat match goal with - | [ |- context [ (?A =? ?B)%Z]] => - change (A =? B)%Z with (hidden_eq A B) - end; - repeat match goal with - | [ |- context [ hidden_eq ?A ?B] ] => - replace (hidden_eq A B) with (B =? A)%Z; - [ | 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. - -Tactic Notation "verit_bool" constr_list(h) := - verit_bool_base h; vauto. - -Tactic Notation "verit_bool_no_check" constr_list(h) := - verit_bool_no_check_base h; vauto. - - -(** Tactics in Prop **) - -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. - -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). - - - -(* - Local Variables: - coq-load-path: ((rec "." "SMTCoq")) - End: -*) diff --git a/src/configure.sh b/src/configure.sh index 3def21c..21b7232 100755 --- a/src/configure.sh +++ b/src/configure.sh @@ -10,6 +10,7 @@ rm -f ${pre}smtcoq_plugin.ml4 rm -f ${pre}versions/native/Structures.v rm -f ${pre}g_smtcoq.ml4 rm -f ${pre}smtcoq_plugin.mlpack +rm -f ${pre}Tactics.v rm -f ${pre}versions/standard/Int63/Int63.v rm -f ${pre}versions/standard/Int63/Int63Native.v rm -f ${pre}versions/standard/Int63/Int63Op.v @@ -23,6 +24,7 @@ if [ $@ -a $@ = -native ]; then cp ${pre}versions/native/Makefile ${pre}Makefile cp ${pre}versions/native/smtcoq_plugin_native.ml4 ${pre}smtcoq_plugin.ml4 cp ${pre}versions/native/Structures_native.v ${pre}versions/native/Structures.v + cp ${pre}versions/native/Tactics_native.v ${pre}Tactics.v else cp ${pre}versions/standard/_CoqProject ${pre}_CoqProject cp ${pre}versions/standard/Makefile.local ${pre}Makefile.local @@ -35,5 +37,6 @@ else cp ${pre}versions/standard/Int63/Int63Properties_standard.v ${pre}versions/standard/Int63/Int63Properties.v cp ${pre}versions/standard/Array/PArray_standard.v ${pre}versions/standard/Array/PArray.v cp ${pre}versions/standard/Structures_standard.v ${pre}versions/standard/Structures.v + cp ${pre}versions/standard/Tactics_standard.v ${pre}Tactics.v coq_makefile -f _CoqProject -o Makefile fi diff --git a/src/versions/native/Make b/src/versions/native/Make index 63c95b2..a9e60e4 100644 --- a/src/versions/native/Make +++ b/src/versions/native/Make @@ -51,7 +51,7 @@ CMXA = smtcoq.cmxa CMXS = smtcoq_plugin.cmxs -VCMXS = "versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi" +VCMXS = "versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs classes/NSMTCoq_SMT_classes.cmxs classes/NSMTCoq_SMT_classes_instances.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_Tactics.cmxs NSMTCoq_Conversion_tactics.cmxs NSMTCoq_PropToBool.cmxs NSMTCoq_BoolToProp.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi classes/NSMTCoq_SMT_classes.cmi classes/NSMTCoq_SMT_classes_instances.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_Tactics.cmi NSMTCoq_Conversion_tactics.cmi NSMTCoq_PropToBool.cmi NSMTCoq_BoolToProp.cmi NSMTCoq_SMTCoq.cmi" CAMLLEX = $(CAMLBIN)ocamllex CAMLYACC = $(CAMLBIN)ocamlyacc diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile index afc5523..4683956 100644 --- a/src/versions/native/Makefile +++ b/src/versions/native/Makefile @@ -73,7 +73,7 @@ COQDOCLIBS?=-R . SMTCoq CAMLYACC=$(CAMLBIN)ocamlyacc CAMLLEX=$(CAMLBIN)ocamllex -VCMXS=versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi +VCMXS=versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs classes/NSMTCoq_SMT_classes.cmxs classes/NSMTCoq_SMT_classes_instances.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_Tactics.cmxs NSMTCoq_Conversion_tactics.cmxs NSMTCoq_PropToBool.cmxs NSMTCoq_BoolToProp.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi classes/NSMTCoq_SMT_classes.cmi classes/NSMTCoq_SMT_classes_instances.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_Tactics.cmi NSMTCoq_Conversion_tactics.cmi NSMTCoq_PropToBool.cmi NSMTCoq_BoolToProp.cmi NSMTCoq_SMTCoq.cmi CMXS=smtcoq_plugin.cmxs CMXA=smtcoq.cmxa diff --git a/src/versions/native/Tactics_native.v b/src/versions/native/Tactics_native.v new file mode 100644 index 0000000..d2b2400 --- /dev/null +++ b/src/versions/native/Tactics_native.v @@ -0,0 +1,55 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +Require Import Psatz. + +Declare ML Module "smtcoq_plugin". + + + +Tactic Notation "verit_bool" constr_list(h) := + fail "Tactics are not supported with native-coq". + +Tactic Notation "verit_bool_no_check" constr_list(h) := + fail "Tactics are not supported with native-coq". + + +(** Tactics in Prop **) + +Ltac zchaff := + fail "Tactics are not supported with native-coq". +Ltac zchaff_no_check := + fail "Tactics are not supported with native-coq". + +Tactic Notation "verit" constr_list(h) := + fail "Tactics are not supported with native-coq". +Tactic Notation "verit_no_check" constr_list(h) := + fail "Tactics are not supported with native-coq". + +Ltac cvc4 := + fail "Tactics are not supported with native-coq". +Ltac cvc4_no_check := + fail "Tactics are not supported with native-coq". + + +Tactic Notation "smt" constr_list(h) := + fail "Tactics are not supported with native-coq". +Tactic Notation "smt_no_check" constr_list(h) := + fail "Tactics are not supported with native-coq". + + + +(* + Local Variables: + coq-load-path: ((rec "../.." "SMTCoq")) + End: +*) diff --git a/src/versions/native/smtcoq_plugin_native.ml4 b/src/versions/native/smtcoq_plugin_native.ml4 index d6954b5..7d78731 100644 --- a/src/versions/native/smtcoq_plugin_native.ml4 +++ b/src/versions/native/smtcoq_plugin_native.ml4 @@ -86,12 +86,14 @@ VERNAC COMMAND EXTEND Add_lemma END +let error () = Structures.error "Tactics are not supported with native-coq" + TACTIC EXTEND Tactic_verit -| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic lpl !lemmas_list ] -| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check lpl !lemmas_list ] +| [ "verit_bool_base" constr_list(lpl) ] -> [ error () ] +| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ error () ] END TACTIC EXTEND Tactic_cvc4 -| [ "cvc4_bool" ] -> [ Lfsc.tactic () ] -| [ "cvc4_bool_no_check" ] -> [ Lfsc.tactic_no_check () ] +| [ "cvc4_bool" ] -> [ error () ] +| [ "cvc4_bool_no_check" ] -> [ error () ] END diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v new file mode 100644 index 0000000..95b92d6 --- /dev/null +++ b/src/versions/standard/Tactics_standard.v @@ -0,0 +1,65 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +Require Import PropToBool BoolToProp. (* Before SMTCoq.State *) +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_no_check" constr_list(h) := + verit_bool_no_check_base h; vauto. + + +(** Tactics in Prop **) + +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. + +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). + + + +(* + Local Variables: + coq-load-path: ((rec "." "SMTCoq")) + End: +*) diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject index a71f500..f283e00 100644 --- a/src/versions/standard/_CoqProject +++ b/src/versions/standard/_CoqProject @@ -146,6 +146,7 @@ SMTCoq.v ReflectFacts.v PropToBool.v BoolToProp.v +QInst.v Tactics.v SMT_terms.v State.v -- cgit