Error message to state that tactics are not supported with native-coq (#47)

* Better error message for failing tactics with native-coq

8 files changed, 148 insertions, 64 deletions

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 <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 = 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/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/Tactics.v b/src/versions/standard/Tactics_standard.v
index 106e128..95b92d6 100644
--- a/src/Tactics.v
+++ b/src/versions/standard/Tactics_standard.v
@@ -12,68 +12,11 @@
 
 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.
+Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances QInst.
 
 Declare ML Module "smtcoq_plugin".
 
 
-(** Handling quantifiers with veriT **)
-
-(* 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 = 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.
 
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