diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
| commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
| tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /plugins/setoid_ring | |
| parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) | |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'plugins/setoid_ring')
31 files changed, 612 insertions, 347 deletions
diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v index e896554e..1204bbd2 100644 --- a/plugins/setoid_ring/Algebra_syntax.v +++ b/plugins/setoid_ring/Algebra_syntax.v @@ -1,3 +1,12 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Class Zero (A : Type) := zero : A. Notation "0" := zero. diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index 5f5b9792..bb1eca49 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Mult. @@ -41,9 +43,12 @@ Ltac Ss_to_add f acc := | _ => constr:((acc + f)%nat) end. +(* For internal use only *) +Local Definition protected_to_nat := N.to_nat. + Ltac natprering := match goal with - |- context C [S ?p] => + |- context C [S ?p] => match p with O => fail 1 (* avoid replacing 1 with 1+0 ! *) | p => match isnatcst p with @@ -52,9 +57,19 @@ Ltac natprering := fold v; natprering end end - | _ => idtac + | _ => change N.to_nat with protected_to_nat + end. + +Ltac natpostring := + match goal with + | |- context [N.to_nat ?x] => + let v := eval cbv in (N.to_nat x) in + change (N.to_nat x) with v; + natpostring + | _ => change protected_to_nat with N.to_nat end. Add Ring natr : natSRth - (morphism nat_morph_N, constants [natcst], preprocess [natprering]). + (morphism nat_morph_N, constants [natcst], + preprocess [natprering], postprocess [natpostring]). diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v index d639f608..b02b7484 100644 --- a/plugins/setoid_ring/BinList.v +++ b/plugins/setoid_ring/BinList.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import BinPos. diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 17a57e62..7cb930ba 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export List. diff --git a/plugins/setoid_ring/Field.v b/plugins/setoid_ring/Field.v index 73a13139..a8ec1717 100644 --- a/plugins/setoid_ring/Field.v +++ b/plugins/setoid_ring/Field.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export Field_theory. diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index babbb86a..73acce22 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Ring_tac BinList Ring_polynom InitialRing. diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 2932d379..d9e32dbb 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Ring. @@ -56,11 +58,16 @@ Let rI_neq_rO := AFth.(AF_1_neq_0). Let rdiv_def := AFth.(AFdiv_def). Let rinv_l := AFth.(AFinv_l). -Add Morphism radd : radd_ext. Proof. exact (Radd_ext Reqe). Qed. -Add Morphism rmul : rmul_ext. Proof. exact (Rmul_ext Reqe). Qed. -Add Morphism ropp : ropp_ext. Proof. exact (Ropp_ext Reqe). Qed. -Add Morphism rsub : rsub_ext. Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. -Add Morphism rinv : rinv_ext. Proof. exact SRinv_ext. Qed. +Add Morphism radd with signature (req ==> req ==> req) as radd_ext. +Proof. exact (Radd_ext Reqe). Qed. +Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. +Proof. exact (Rmul_ext Reqe). Qed. +Add Morphism ropp with signature (req ==> req) as ropp_ext. +Proof. exact (Ropp_ext Reqe). Qed. +Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. +Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. +Add Morphism rinv with signature (req ==> req) as rinv_ext. +Proof. exact SRinv_ext. Qed. Let eq_trans := Setoid.Seq_trans _ _ Rsth. Let eq_sym := Setoid.Seq_sym _ _ Rsth. @@ -1607,11 +1614,18 @@ Section Complete. Notation "x / y " := (rdiv x y). Notation "/ x" := (rinv x). Notation "x == y" := (req x y) (at level 70, no associativity). Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid3. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_setoid3. Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext3. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext3. + Proof. exact (Ropp_ext Reqe). Qed. Section AlmostField. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 9c690e2b..f5db2754 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Zbool. @@ -48,12 +50,19 @@ Section ZMORPHISM. Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). Notation "x == y" := (req x y). Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid3. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_setoid3. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext3. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext3. + Proof. exact (Ropp_ext Reqe). Qed. Fixpoint gen_phiPOS1 (p:positive) : R := match p with @@ -103,7 +112,8 @@ Section ZMORPHISM. Section ALMOST_RING. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. - Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. @@ -151,7 +161,8 @@ Section ZMORPHISM. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. Let ARth := Rth_ARth Rsth Reqe Rth. - Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext4. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. @@ -255,7 +266,11 @@ Section NMORPHISM. Notation "0" := rO. Notation "1" := rI. Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid4. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_setoid4. Ltac rrefl := gen_reflexivity Rsth. Variable SReqe : sring_eq_ext radd rmul req. Variable SRth : semi_ring_theory 0 1 radd rmul req. @@ -265,8 +280,10 @@ Section NMORPHISM. Let rsub := (@SRsub R radd). Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). Notation "x == y" := (req x y). - Add Morphism radd : radd_ext4. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext4. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4. + Proof. exact (Rmul_ext Reqe). Qed. Ltac norm := gen_srewrite_sr Rsth Reqe ARth. Definition gen_phiN1 x := @@ -374,15 +391,23 @@ Section NWORDMORPHISM. Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). Notation "x == y" := (req x y). Variable Rsth : Setoid_Theory R req. - Add Setoid R req Rsth as R_setoid5. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_setoid5. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext5. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext5. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext5. exact (Ropp_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext5. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext5. + Proof. exact (Ropp_ext Reqe). Qed. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. - Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. @@ -555,12 +580,20 @@ Section GEN_DIV. Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. (* Useful tactics *) - Add Setoid R req Rsth as R_set1. + Add Parametric Relation : R req + reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) + symmetry proved by Rsth.(@Equivalence_Symmetric _ _) + transitivity proved by Rsth.(@Equivalence_Transitive _ _) + as R_set1. Ltac rrefl := gen_reflexivity Rsth. - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext. + Proof. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac rsimpl := gen_srewrite Rsth Reqe ARth. Definition triv_div x y := @@ -859,8 +892,3 @@ Ltac isZcst t := (* *) | _ => constr:(false) end. - - - - - diff --git a/plugins/setoid_ring/Integral_domain.v b/plugins/setoid_ring/Integral_domain.v index 0c16fe1a..98407cb6 100644 --- a/plugins/setoid_ring/Integral_domain.v +++ b/plugins/setoid_ring/Integral_domain.v @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + Require Export Cring. diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v index 54e2789b..36a92505 100644 --- a/plugins/setoid_ring/NArithRing.v +++ b/plugins/setoid_ring/NArithRing.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export Ring. diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v index cd3bef43..2ca0d609 100644 --- a/plugins/setoid_ring/Ncring.v +++ b/plugins/setoid_ring/Ncring.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* non commutative rings *) diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 20022c00..523c7b02 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import ZArith_base. diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 109808ee..12208ff6 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* A <X1,...,Xn>: non commutative polynomials on a commutative ring A *) diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index 5e30a130..79585078 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import List. diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 29372212..38bc58a6 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + Require Import Nnat. Require Import ArithRing. Require Export Ring Field. @@ -59,11 +69,12 @@ Notation Rset := (Eqsth R). Notation Rext := (Eq_ext Rplus Rmult Ropp). Lemma Rlt_0_2 : 0 < 2. +Proof. apply Rlt_trans with (0 + 1). apply Rlt_n_Sn. rewrite Rplus_comm. apply Rplus_lt_compat_l. - replace 1 with (0 + 1). + replace R1 with (0 + 1). apply Rlt_n_Sn. apply Rplus_0_l. Qed. @@ -126,9 +137,17 @@ Ltac Rpow_tac t := | _ => constr:(N.of_nat t) end. -Add Field RField : Rfield - (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]). - - - +Ltac IZR_tac t := + match t with + | R0 => constr:(0%Z) + | R1 => constr:(1%Z) + | IZR ?u => + match isZcst u with + | true => u + | _ => constr:(InitialRing.NotConstant) + end + | _ => constr:(InitialRing.NotConstant) + end. +Add Field RField : Rfield + (completeness Zeq_bool_complete, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]). diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index 77576cb9..b83e1c67 100644 --- a/plugins/setoid_ring/Ring.v +++ b/plugins/setoid_ring/Ring.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Bool. diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v index dc7c10cc..a9b4d9d6 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/plugins/setoid_ring/Ring_base.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This module gathers the necessary base to build an instance of the diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index b6919667..33df36d8 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) @@ -59,10 +61,18 @@ Section MakeRingPol. Infix "?=!" := ceqb. Notation "[ x ]" := (phi x). (* Useful tactics *) - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext. + Proof. exact (Radd_ext Reqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. + Proof. exact (Rmul_ext Reqe). Qed. + + Add Morphism ropp with signature (req ==> req) as ropp_ext. + Proof. exact (Ropp_ext Reqe). Qed. + + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac rsimpl := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index fc02cef1..e8efb362 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + Set Implicit Arguments. Require Import Setoid. Require Import BinPos. @@ -427,19 +437,37 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= let t := type of H in let g := fresh "goal" in set (g:= G); - generalize H;clear H; + generalize H; ring_lookup (PackRing Ring_simplify) [] rl t; - intro H; + (* + Correction of bug 1859: + we want to leave H at its initial position + this is obtained by adding a copy of H (H'), + move it just after H, remove H and finally + rename H into H' + *) + let H' := fresh "H" in + intro H'; + move H' after H; + clear H;rename H' into H; unfold g;clear g. -Tactic Notation - "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):= +Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):= let G := Get_goal in let t := type of H in let g := fresh "goal" in set (g:= G); - generalize H;clear H; + generalize H; ring_lookup (PackRing Ring_simplify) [lH] rl t; - intro H; + (* + Correction of bug 1859: + we want to leave H at its initial position + this is obtained by adding a copy of H (H'), + move it just after H, remove H and finally + rename H into H' + *) + let H' := fresh "H" in + intro H'; + move H' after H; + clear H;rename H' into H; unfold g;clear g. - diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index f7757a18..d67a8d8d 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Setoid Morphisms BinPos BinNat. @@ -254,12 +256,16 @@ Section ALMOST_RING. Section SEMI_RING. Variable SReqe : sring_eq_ext radd rmul req. - Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed. - Add Morphism rmul : rmul_ext1. exact (SRmul_ext SReqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext1. + Proof. exact (SRadd_ext SReqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext1. + Proof. exact (SRmul_ext SReqe). Qed. + Variable SRth : semi_ring_theory 0 1 radd rmul req. (** Every semi ring can be seen as an almost ring, by taking : - -x = x and x - y = x + y *) + [-x = x] and [x - y = x + y] *) Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). Definition SRsub x y := x + -y. Infix "-" := SRsub. @@ -323,9 +329,15 @@ Section ALMOST_RING. Notation "- x" := (ropp x). Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext2. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext2. exact (Ropp_ext Reqe). Qed. + + Add Morphism radd with signature (req ==> req ==> req) as radd_ext2. + Proof. exact (Radd_ext Reqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext2. + Proof. exact (Rmul_ext Reqe). Qed. + + Add Morphism ropp with signature (req ==> req) as ropp_ext2. + Proof. exact (Ropp_ext Reqe). Qed. Section RING. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. @@ -393,14 +405,29 @@ Section ALMOST_RING. Notation "?=!" := ceqb. Notation "[ x ]" := (phi x). Variable Csth : Equivalence ceq. Variable Ceqe : ring_eq_ext cadd cmul copp ceq. - Add Setoid C ceq Csth as C_setoid. - Add Morphism cadd : cadd_ext. exact (Radd_ext Ceqe). Qed. - Add Morphism cmul : cmul_ext. exact (Rmul_ext Ceqe). Qed. - Add Morphism copp : copp_ext. exact (Ropp_ext Ceqe). Qed. + + Add Parametric Relation : C ceq + reflexivity proved by Csth.(@Equivalence_Reflexive _ _) + symmetry proved by Csth.(@Equivalence_Symmetric _ _) + transitivity proved by Csth.(@Equivalence_Transitive _ _) + as C_setoid. + + Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext. + Proof. exact (Radd_ext Ceqe). Qed. + + Add Morphism cmul with signature (ceq ==> ceq ==> ceq) as cmul_ext. + Proof. exact (Rmul_ext Ceqe). Qed. + + Add Morphism copp with signature (ceq ==> ceq) as copp_ext. + Proof. exact (Ropp_ext Ceqe). Qed. + Variable Cth : ring_theory cO cI cadd cmul csub copp ceq. Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi. Variable phi_ext : forall x y, ceq x y -> [x] == [y]. - Add Morphism phi : phi_ext1. exact phi_ext. Qed. + + Add Morphism phi with signature (ceq ==> req) as phi_ext1. + Proof. exact phi_ext. Qed. + Lemma Smorph_opp x : [-!x] == -[x]. Proof. rewrite <- (Rth.(Radd_0_l) [-!x]). diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v index fd765471..ae91ee16 100644 --- a/plugins/setoid_ring/Rings_Q.v +++ b/plugins/setoid_ring/Rings_Q.v @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + Require Export Cring. Require Export Integral_domain. diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v index fd219c23..901b36ed 100644 --- a/plugins/setoid_ring/Rings_R.v +++ b/plugins/setoid_ring/Rings_R.v @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + Require Export Cring. Require Export Integral_domain. diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v index 605a23a9..75e77ab6 100644 --- a/plugins/setoid_ring/Rings_Z.v +++ b/plugins/setoid_ring/Rings_Z.v @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + Require Export Cring. Require Export Integral_domain. Require Export Ncring_initial. diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v index 23784cf3..19eaddc1 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/plugins/setoid_ring/ZArithRing.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export Ring. diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 216eb8b3..5e4c9214 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -1,13 +1,14 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - +open Ltac_plugin open Pp open Util open Libnames @@ -15,9 +16,9 @@ open Printer open Newring_ast open Newring open Stdarg -open Constrarg +open Tacarg open Pcoq.Constr -open Pcoq.Tactic +open Pltac DECLARE PLUGIN "newring_plugin" @@ -77,22 +78,21 @@ END VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] -> - [ let l = match l with None -> [] | Some l -> l in - let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in - add_theory id (ic t) set k cst (pre,post) power sign div] + [ let l = match l with None -> [] | Some l -> l in add_theory id t l] | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.ring_req)) + str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) ) !from_name ] END TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] + [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t ] END let pr_field_mod = function @@ -114,16 +114,15 @@ END VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] -> - [ let l = match l with None -> [] | Some l -> l in - let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in - add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] + [ let l = match l with None -> [] | Some l -> l in add_field_theory id t l ] | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.field_req)) + str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) ) !field_from_name ] END diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 90f5f8e6..99bb8440 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -1,23 +1,25 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Ltac_plugin open Pp -open CErrors open Util open Names -open Term +open Constr +open EConstr open Vars open CClosure open Environ open Libnames open Globnames open Glob_term -open Tacticals open Tacexpr open Coqlib open Mod_subst @@ -31,6 +33,8 @@ open Misctypes open Newring_ast open Proofview.Notations +let error msg = CErrors.user_err Pp.(str msg) + (****************************************************************************) (* controlled reduction *) @@ -42,25 +46,27 @@ let tag_arg tag_rec map subs i c = | Prot -> mk_atom c | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c -let global_head_of_constr c = - let f, args = decompose_app c in - try global_of_constr f - with Not_found -> anomaly (str "global_head_of_constr") +let global_head_of_constr sigma c = + let f, args = decompose_app sigma c in + try fst (Termops.global_of_constr sigma f) + with Not_found -> CErrors.anomaly (str "global_head_of_constr.") let global_of_constr_nofail c = try global_of_constr c with Not_found -> VarRef (Id.of_string "dummy") let rec mk_clos_but f_map subs t = + let open Term in match f_map (global_of_constr_nofail t) with | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t | None -> - (match kind_of_term t with + (match Constr.kind t with App(f,args) -> mk_clos_app_but f_map subs f args 0 | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t | _ -> mk_atom t) and mk_clos_app_but f_map subs f args n = + let open Constr in if n >= Array.length args then mk_atom(mkApp(f, args)) else let fargs, args' = Array.chop n args in @@ -79,11 +85,13 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps with Not_found -> - errorlabstrm"lookup_map"(str"map "++qs map++str"not found") + CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") -let protect_red map env sigma c = - kl (create_clos_infos all env) - (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; +let protect_red map env sigma c0 = + let evars ev = Evarutil.safe_evar_value sigma ev in + let c = EConstr.Unsafe.to_constr c0 in + EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ()) + (mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));; let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None @@ -96,9 +104,10 @@ let protect_tac_in map id = let closed_term t l = let open Quote_plugin in + Proofview.tclEVARMAP >>= fun sigma -> let l = List.map Universes.constr_of_global l in let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in - if Quote.closed_under cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) + if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) (* TACTIC EXTEND echo | [ "echo" constr(t) ] -> @@ -121,11 +130,11 @@ let closed_term_ast l = mltac_name = tacname; mltac_index = 0; } in - let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in - TacFun([Some(Id.of_string"t")], - TacML(Loc.ghost,tacname, - [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None)); - TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)])) + let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in + TacFun([Name(Id.of_string"t")], + TacML(Loc.tag (tacname, + [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None)); + TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) @@ -135,33 +144,36 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" let ic c = let env = Global.env() in let sigma = Evd.from_env env in - Constrintern.interp_open_constr env sigma c + let sigma, c = Constrintern.interp_open_constr env sigma c in + (sigma, c) let ic_unsafe c = (*FIXME remove *) let env = Global.env() in let sigma = Evd.from_env env in - fst (Constrintern.interp_constr env sigma c) - -let decl_constant na ctx c = - let vars = Universes.universes_of_constr c in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in + fst (Constrintern.interp_constr env sigma c) + +let decl_constant na univs c = + let open Constr in + let env = Global.env () in + let vars = Univops.universes_of_constr env c in + let univs = Univops.restrict_universe_context univs vars in + let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true - ~univs:(Univ.ContextSet.to_context ctx) c), + (DefinitionEntry (definition_entry ~opaque:true ~univs c), IsProof Lemma)) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = - TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args)) + TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args))) (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args)) + TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args))) let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in - let x = Reference (ArgVar (Loc.ghost, id)) in + let x = Reference (ArgVar CAst.(make id)) in (succ i, x :: vars, Id.Map.add id arg lfun) in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in @@ -171,11 +183,11 @@ let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = let dummy_goal env sigma = let (gl,_,sigma) = - Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in + Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in {Evd.it = gl; Evd.sigma = sigma} let constr_of v = match Value.to_constr v with - | Some c -> c + | Some c -> EConstr.Unsafe.to_constr c | None -> failwith "Ring.exec_tactic: anomaly" let tactic_res = ref [||] @@ -196,7 +208,7 @@ let get_res = let exec_tactic env evd n f args = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in - let x = Reference (ArgVar (Loc.ghost, id)) in + let x = Reference (ArgVar CAst.(make id)) in (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun) in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in @@ -204,13 +216,14 @@ let exec_tactic env evd n f args = (** Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in - let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in - let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in + let get_res = TacML (Loc.tag (get_res, [TacGeneric n])) in + let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in (** Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - Array.map (fun x -> nf (constr_of x)) !tactic_res, snd (Evd.universe_context evd) + let nf c = nf (constr_of c) in + Array.map nf !tactic_res, Evd.universe_context_set evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; @@ -220,7 +233,7 @@ let stdlib_modules = ] let coq_constant c = - lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c) + lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)) let coq_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) @@ -238,19 +251,19 @@ let plapp evd f args = let fc = Evarutil.e_new_global evd (Lazy.force f) in mkApp(fc,args) -let dest_rel0 t = - match kind_of_term t with +let dest_rel0 sigma t = + match EConstr.kind sigma t with | App(f,args) when Array.length args >= 2 -> let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in - if closed0 rel then + if closed0 sigma rel then (rel,args.(Array.length args - 2),args.(Array.length args - 1)) else error "ring: cannot find relation (not closed)" | _ -> error "ring: cannot find relation" -let rec dest_rel t = - match kind_of_term t with - | Prod(_,_,c) -> dest_rel c - | _ -> dest_rel0 t +let rec dest_rel sigma t = + match EConstr.kind sigma t with + | Prod(_,_,c) -> dest_rel sigma c + | _ -> dest_rel0 sigma t (****************************************************************************) (* Library linking *) @@ -265,18 +278,16 @@ let plugin_modules = ] let my_constant c = - lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c) + lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) -let new_ring_path = - DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) let znew_ring_path = DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = - lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) + lazy(KerName.make (ModPath.MPfile znew_ring_path) DirPath.empty (Label.make s)) -let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);; +let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);; let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; (* Ring theory *) @@ -309,27 +320,29 @@ let coq_mkhypo = my_reference "mkhypo" let coq_hypo = my_reference "hypo" (* Equality: do not evaluate but make recursive call on both sides *) -let map_with_eq arg_map c = - let (req,_,_) = dest_rel c in +let map_with_eq arg_map sigma c = + let (req,_,_) = dest_rel sigma c in interp_map - ((global_head_of_constr req,(function -1->Prot|_->Rec)):: + ((global_head_of_constr sigma req,(function -1->Prot|_->Rec)):: List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) -let map_without_eq arg_map _ = +let map_without_eq arg_map _ _ = interp_map (List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) let _ = add_map "ring" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot); pol_cst "Pphi_pow", - (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring + (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot); + (* PEeval: evaluate polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)]) + pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot)]) (****************************************************************************) (* Ring database *) @@ -348,15 +361,15 @@ let find_ring_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - errorlabstrm "ring" + CErrors.user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") in List.iter check cl'; - (try ring_for_carrier ty + (try ring_for_carrier (EConstr.to_constr sigma ty) with Not_found -> - errorlabstrm "ring" + CErrors.user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\"")) | [] -> assert false let add_entry (sp,_kn) e = @@ -379,7 +392,7 @@ let subst_th (subst,th) = let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in if c' == th.ring_carrier && eq' == th.ring_req && - eq_constr set' th.ring_setoid && + Constr.equal set' th.ring_setoid && ext' == th.ring_ext && morph' == th.ring_morph && th' == th.ring_th && @@ -485,8 +498,8 @@ let op_smorph r add mul req m1 m2 = (* (setoid,op_morph) *) let ring_equality env evd (r,add,mul,opp,req) = - match kind_of_term req with - | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> + match EConstr.kind !evd req with + | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> let setoid = plapp evd coq_eq_setoid [|r|] in let op_morph = match opp with @@ -517,19 +530,19 @@ let ring_equality env evd (r,add,mul,opp,req) = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req++str"\""++spc()++ - str"and morphisms \""++pr_constr add_m_lem ++ - str"\","++spc()++ str"\""++pr_constr mul_m_lem++ - str"\""++spc()++str"and \""++pr_constr opp_m_lem++ + (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ + str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++ + str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++ str"\""); op_morph) | None -> (Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ - str"and morphisms \""++pr_constr add_m_lem ++ + (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ str"\""++spc()++str"and \""++ - pr_constr mul_m_lem++str"\""); + pr_econstr_env env !evd mul_m_lem++str"\""); op_smorph r add mul req add_m_lem mul_m_lem) in (setoid,op_morph) @@ -540,15 +553,15 @@ let build_setoid_params env evd r add mul opp req eqth = let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in - match kind_of_term th_typ with + match EConstr.kind sigma th_typ with App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) -> + when eq_constr_nounivs sigma f (Lazy.force coq_almost_ring_theory) -> (None,r,zero,one,add,mul,Some sub,Some opp,req) | App(f,[|r;zero;one;add;mul;req|]) - when eq_constr_nounivs f (Lazy.force coq_semi_ring_theory) -> + when eq_constr_nounivs sigma f (Lazy.force coq_semi_ring_theory) -> (Some true,r,zero,one,add,mul,None,None,req) | App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when eq_constr_nounivs f (Lazy.force coq_ring_theory) -> + when eq_constr_nounivs sigma f (Lazy.force coq_ring_theory) -> (Some false,r,zero,one,add,mul,Some sub,Some opp,req) | _ -> error "bad ring structure" @@ -566,8 +579,8 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = | Some (Closed lc) -> closed_term_ast (List.map Smartlocate.global_with_alias lc) | None -> - let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in - TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])) + let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in + TacArg(Loc.tag (TacCall(Loc.tag (t,[])))) let make_hyp env evd c = let t = Retyping.get_type_of env !evd c in @@ -581,14 +594,15 @@ let make_hyp_list env evd lH = (plapp evd coq_nil [|carrier|]) in let l' = Typing.e_solve_evars env evd l in + let l' = EConstr.Unsafe.to_constr l' in Evarutil.nf_evars_universes !evd l' let interp_power env evd pow = let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match pow with | None -> - let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in - (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|]) + let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in + (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with @@ -616,7 +630,7 @@ let interp_div env evd div = plapp evd coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = +let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div = check_required_library (cdir@["Ring_base"]); let env = Global.env() in let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in @@ -646,6 +660,9 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = match post with Some t -> Tacintern.glob_tactic t | _ -> TacId [] in + let r = EConstr.to_constr sigma r in + let req = EConstr.to_constr sigma req in + let sth = EConstr.to_constr sigma sth in let _ = Lib.add_leaf name (theory_to_obj @@ -693,13 +710,18 @@ let process_ring_mods l = let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) +let add_theory id rth l = + let (sigma, rth) = ic rth in + let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in + add_theory0 id (sigma, rth) set k cst (pre,post) power sign div + (*****************************************************************************) (* The tactics consist then only in a lookup in the ring database and call the appropriate ltac. *) -let make_args_list rl t = +let make_args_list sigma rl t = match rl with - | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2] + | [] -> let (_,t1,t2) = dest_rel0 sigma t in [t1;t2] | _ -> rl let make_term_list env evd carrier rl = @@ -708,7 +730,7 @@ let make_term_list env evd carrier rl = (plapp evd coq_nil [|carrier|]) in Typing.e_solve_evars env evd l -let carg = Tacinterp.Value.of_constr +let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c) let tacarg expr = Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr @@ -722,25 +744,25 @@ let ltac_ring_structure e = let pow_tac = tacarg e.ring_pow_tac in let lemma1 = carg e.ring_lemma1 in let lemma2 = carg e.ring_lemma2 in - let pretac = tacarg (TacFun([None],e.ring_pre_tac)) in - let posttac = tacarg (TacFun([None],e.ring_post_tac)) in + let pretac = tacarg (TacFun([Anonymous],e.ring_pre_tac)) in + let posttac = tacarg (TacFun([Anonymous],e.ring_post_tac)) in [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] let ring_lookup (f : Value.t) lH rl t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try (* find_ring_strucure can raise an exception *) + let rl = make_args_list sigma rl t in let evdref = ref sigma in - let rl = make_args_list rl t in let e = find_ring_structure env sigma rl in - let rl = carg (make_term_list env evdref e.ring_carrier rl) in + let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in let lH = carg (make_hyp_list env evdref lH) in let ring = ltac_ring_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end } + end (***********************************************************************) @@ -748,39 +770,42 @@ let new_field_path = DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) let field_ltac s = - lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s)) + lazy(KerName.make (ModPath.MPfile new_field_path) DirPath.empty (Label.make s)) let _ = add_map "field" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) my_reference "display_linear", - (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); + (function -1|9|10|11|13|15|16->Eval|12|14->Rec|_->Prot); my_reference "display_pow_linear", - (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot); + (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot); pol_cst "Pphi_pow", - (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); - (* PEeval: evaluate morphism and polynomial, protect ring + (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot); + (* PEeval: evaluate polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); - (* FEeval: evaluate morphism, protect field + pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot); + (* FEeval: evaluate polynomial, protect field operations and make recursive call on the var map *) - my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; + my_reference "FEeval", (function -1|12|15->Eval|10|14->Rec|_->Prot)]);; let _ = add_map "field_cond" (map_without_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); - (* PCond: evaluate morphism and denum list, protect ring + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); + (* PCond: evaluate denum list, protect ring operations and make recursive call on the var map *) - my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; -(* (function -1|9|11->Eval|10->Rec|_->Prot)]);;*) + my_reference "PCond", (function -1|11|14->Eval|9|13->Rec|_->Prot)]);; let _ = Redexpr.declare_reduction "simpl_field_expr" @@ -795,21 +820,22 @@ let af_ar = my_reference"AF_AR" let f_r = my_reference"F_R" let sf_sr = my_reference"SF_SR" let dest_field env evd th_spec = + let open Termops in let th_typ = Retyping.get_type_of env !evd th_spec in - match kind_of_term th_typ with + match EConstr.kind !evd th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when is_global (Lazy.force afield_theory) f -> + when is_global !evd (Lazy.force afield_theory) f -> let rth = plapp evd af_ar [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when is_global (Lazy.force field_theory) f -> + when is_global !evd (Lazy.force field_theory) f -> let rth = plapp evd f_r [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;div;inv;req|]) - when is_global (Lazy.force sfield_theory) f -> + when is_global !evd (Lazy.force sfield_theory) f -> let rth = plapp evd sf_sr [|r;zero;one;add;mul;div;inv;req;th_spec|] in (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) @@ -828,15 +854,15 @@ let find_field_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - errorlabstrm "field" + CErrors.user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") in List.iter check cl'; - (try field_for_carrier ty + (try field_for_carrier (EConstr.to_constr sigma ty) with Not_found -> - errorlabstrm "field" + CErrors.user_err ~hdr:"field" (str"cannot find a declared field structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc()++str"\""++pr_econstr_env env sigma ty++str"\"")) | [] -> assert false let add_field_entry (sp,_kn) e = @@ -889,9 +915,11 @@ let ftheory_to_obj : field_info -> obj = classify_function = (fun x -> Substitute x) } let field_equality evd r inv req = - match kind_of_term req with - | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> - mkApp(Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) + match EConstr.kind !evd req with + | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> + let c = Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr in + let c = EConstr.of_constr c in + mkApp(c,[|r;r;inv|]) | _ -> let _setoid = setoid_of_relation (Global.env ()) evd r req in let signature = [Some (r,Some req)],Some(r,Some req) in @@ -901,15 +929,17 @@ let field_equality evd r inv req = error "field inverse should be declared as a morphism" in inv_m_lem -let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv = +let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv = + let open Constr in check_required_library (cdir@["Field_tac"]); + let (sigma,fth) = ic fth in let env = Global.env() in let evd = ref sigma in let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = dest_field env evd fth in let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in let eqth = Some(sth,ext) in - let _ = add_theory name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in + let _ = add_theory0 name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in let (pow_tac, pspec) = interp_power env evd power in let sspec = interp_sign env evd sign in let dspec = interp_div env evd odiv in @@ -924,7 +954,7 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power let lemma4 = params.(6) in let cond_lemma = match inj with - | Some thm -> mkApp(params.(8),[|thm|]) + | Some thm -> mkApp(params.(8),[|EConstr.to_constr sigma thm|]) | None -> params.(7) in let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") ctx lemma1 in @@ -946,6 +976,8 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power match post with Some t -> Tacintern.glob_tactic t | _ -> TacId [] in + let r = EConstr.to_constr sigma r in + let req = EConstr.to_constr sigma req in let _ = Lib.add_leaf name (ftheory_to_obj @@ -985,6 +1017,10 @@ let process_field_mods l = let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) +let add_field_theory id t mods = + let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods mods in + add_field_theory0 id t set k cst_tac inj (pre,post) power sign div + let ltac_field_structure e = let req = carg e.field_req in let cst_tac = tacarg e.field_cst_tac in @@ -994,22 +1030,22 @@ let ltac_field_structure e = let field_simpl_eq_ok = carg e.field_simpl_eq_ok in let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in let cond_ok = carg e.field_cond in - let pretac = tacarg (TacFun([None],e.field_pre_tac)) in - let posttac = tacarg (TacFun([None],e.field_post_tac)) in + let pretac = tacarg (TacFun([Anonymous],e.field_pre_tac)) in + let posttac = tacarg (TacFun([Anonymous],e.field_post_tac)) in [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac] let field_lookup (f : Value.t) lH rl t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in try + let rl = make_args_list sigma rl t in let evdref = ref sigma in - let rl = make_args_list rl t in let e = find_field_structure env sigma rl in - let rl = carg (make_term_list env evdref e.field_carrier rl) in + let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in let lH = carg (make_hyp_list env evdref lH) in let field = ltac_field_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end } + end diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index f417c87c..1d1557b1 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -1,46 +1,30 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Constr +open EConstr open Libnames open Globnames open Constrexpr -open Tacexpr -open Proof_type open Newring_ast val protect_tac_in : string -> Id.t -> unit Proofview.tactic val protect_tac : string -> unit Proofview.tactic -val closed_term : constr -> global_reference list -> unit Proofview.tactic - -val process_ring_mods : - constr_expr ring_mod list -> - constr coeff_spec * (constr * constr) option * - cst_tac_spec option * raw_tactic_expr option * - raw_tactic_expr option * - (cst_tac_spec * constr_expr) option * - constr_expr option * constr_expr option +val closed_term : EConstr.constr -> global_reference list -> unit Proofview.tactic val add_theory : Id.t -> - Evd.evar_map * constr -> - (constr * constr) option -> - constr coeff_spec -> - cst_tac_spec option -> - raw_tactic_expr option * raw_tactic_expr option -> - (cst_tac_spec * constr_expr) option -> - constr_expr option -> - constr_expr option -> unit - -val ic : constr_expr -> Evd.evar_map * constr + constr_expr -> + constr_expr ring_mod list -> unit val from_name : ring_info Spmap.t ref @@ -49,26 +33,10 @@ val ring_lookup : constr list -> constr list -> constr -> unit Proofview.tactic -val process_field_mods : - constr_expr field_mod list -> - constr coeff_spec * - (constr * constr) option * constr option * - cst_tac_spec option * raw_tactic_expr option * - raw_tactic_expr option * - (cst_tac_spec * constr_expr) option * - constr_expr option * constr_expr option - val add_field_theory : Id.t -> - Evd.evar_map * constr -> - (constr * constr) option -> - constr coeff_spec -> - cst_tac_spec option -> - constr option -> - raw_tactic_expr option * raw_tactic_expr option -> - (cst_tac_spec * constr_expr) option -> - constr_expr option -> - constr_expr option -> unit + constr_expr -> + constr_expr field_mod list -> unit val field_from_name : field_info Spmap.t ref diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml new file mode 100644 index 00000000..3eb68b51 --- /dev/null +++ b/plugins/setoid_ring/newring_ast.ml @@ -0,0 +1,67 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Constr +open Libnames +open Constrexpr + +open Ltac_plugin +open Tacexpr + +type 'constr coeff_spec = + Computational of 'constr (* equality test *) + | Abstract (* coeffs = Z *) + | Morphism of 'constr (* general morphism *) + +type cst_tac_spec = + CstTac of raw_tactic_expr + | Closed of reference list + +type 'constr ring_mod = + Ring_kind of 'constr coeff_spec + | Const_tac of cst_tac_spec + | Pre_tac of raw_tactic_expr + | Post_tac of raw_tactic_expr + | Setoid of constr_expr * constr_expr + | Pow_spec of cst_tac_spec * constr_expr + (* Syntaxification tactic , correctness lemma *) + | Sign_spec of constr_expr + | Div_spec of constr_expr + +type 'constr field_mod = + Ring_mod of 'constr ring_mod + | Inject of constr_expr + +type ring_info = + { ring_carrier : types; + ring_req : constr; + ring_setoid : constr; + ring_ext : constr; + ring_morph : constr; + ring_th : constr; + ring_cst_tac : glob_tactic_expr; + ring_pow_tac : glob_tactic_expr; + ring_lemma1 : constr; + ring_lemma2 : constr; + ring_pre_tac : glob_tactic_expr; + ring_post_tac : glob_tactic_expr } + +type field_info = + { field_carrier : types; + field_req : constr; + field_cst_tac : glob_tactic_expr; + field_pow_tac : glob_tactic_expr; + field_ok : constr; + field_simpl_eq_ok : constr; + field_simpl_ok : constr; + field_simpl_eq_in_ok : constr; + field_cond : constr; + field_pre_tac : glob_tactic_expr; + field_post_tac : glob_tactic_expr } diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index c26fcc8d..3eb68b51 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -1,14 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr open Libnames open Constrexpr + +open Ltac_plugin open Tacexpr type 'constr coeff_spec = diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack index 23663b40..5aa79b58 100644 --- a/plugins/setoid_ring/newring_plugin.mlpack +++ b/plugins/setoid_ring/newring_plugin.mlpack @@ -1,2 +1,3 @@ +Newring_ast Newring G_newring diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget deleted file mode 100644 index 595ba55e..00000000 --- a/plugins/setoid_ring/vo.itarget +++ /dev/null @@ -1,24 +0,0 @@ -ArithRing.vo -BinList.vo -Field_tac.vo -Field_theory.vo -Field.vo -InitialRing.vo -NArithRing.vo -RealField.vo -Ring_base.vo -Ring_polynom.vo -Ring_tac.vo -Ring_theory.vo -Ring.vo -ZArithRing.vo -Algebra_syntax.vo -Cring.vo -Ncring.vo -Ncring_polynom.vo -Ncring_initial.vo -Ncring_tac.vo -Rings_Z.vo -Rings_R.vo -Rings_Q.vo -Integral_domain.vo
\ No newline at end of file |