diff options
Diffstat (limited to 'plugins/setoid_ring')
29 files changed, 128 insertions, 157 deletions
diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v index 1204bbd2e1..5f594d29cd 100644 --- a/plugins/setoid_ring/Algebra_syntax.v +++ b/plugins/setoid_ring/Algebra_syntax.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v index bb1eca49ce..727e99f0b4 100644 --- a/plugins/setoid_ring/ArithRing.v +++ b/plugins/setoid_ring/ArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v index b02b7484d5..958832274b 100644 --- a/plugins/setoid_ring/BinList.v +++ b/plugins/setoid_ring/BinList.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 7cb930ba5a..df0313a624 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -19,6 +19,7 @@ Require Export Algebra_syntax. Require Export Ncring. Require Export Ncring_initial. Require Export Ncring_tac. +Require Import InitialRing. Class Cring {R:Type}`{Rr:Ring R} := cring_mul_comm: forall x y:R, x * y == y * x. diff --git a/plugins/setoid_ring/Field.v b/plugins/setoid_ring/Field.v index a8ec1717f9..9ff07948df 100644 --- a/plugins/setoid_ring/Field.v +++ b/plugins/setoid_ring/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index 73acce2253..a5390efc7f 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 813c521ab0..3736bc47a5 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -730,7 +730,6 @@ Qed. (* The input: syntax of a field expression *) -#[universes(template)] Inductive FExpr : Type := | FEO : FExpr | FEI : FExpr @@ -763,7 +762,6 @@ Strategy expand [FEeval]. (* The result of the normalisation *) -#[universes(template)] Record linear : Type := mk_linear { num : PExpr C; denum : PExpr C; @@ -946,7 +944,6 @@ induction e2; intros p1 p2; now rewrite <- PEpow_mul_r. Qed. -#[universes(template)] Record rsplit : Type := mk_rsplit { rsplit_left : PExpr C; rsplit_common : PExpr C; @@ -1235,12 +1232,19 @@ Notation ring_correct := (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th). (* simplify a field expression into a fraction *) -(* TODO: simplify when den is constant... *) Definition display_linear l num den := - NPphi_dev l num / NPphi_dev l den. + let lnum := NPphi_dev l num in + match den with + | Pc c => if ceqb c cI then lnum else lnum / NPphi_dev l den + | _ => lnum / NPphi_dev l den + end. Definition display_pow_linear l num den := - NPphi_pow l num / NPphi_pow l den. + let lnum := NPphi_pow l num in + match den with + | Pc c => if ceqb c cI then lnum else lnum / NPphi_pow l den + | _ => lnum / NPphi_pow l den + end. Theorem Field_rw_correct n lpe l : Ninterp_PElist l lpe -> @@ -1252,7 +1256,18 @@ Theorem Field_rw_correct n lpe l : Proof. intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. rewrite (Fnorm_FEeval_PEeval _ _ H). - unfold display_linear; apply rdiv_ext; + unfold display_linear. + destruct (Nnorm _ _ _) as [c | | ] eqn: HN; + try ( apply rdiv_ext; + eapply ring_rw_correct; eauto). + destruct (ceqb_spec c cI). + set (nnum := NPphi_dev _ _). + apply eq_trans with (nnum / NPphi_dev l (Pc c)). + apply rdiv_ext; + eapply ring_rw_correct; eauto. + rewrite Pphi_dev_ok; try eassumption. + now simpl; rewrite H0, phi_1, <- rdiv1. + apply rdiv_ext; eapply ring_rw_correct; eauto. Qed. @@ -1266,8 +1281,19 @@ Theorem Field_rw_pow_correct n lpe l : Proof. intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. rewrite (Fnorm_FEeval_PEeval _ _ H). - unfold display_pow_linear; apply rdiv_ext; - eapply ring_rw_pow_correct;eauto. + unfold display_pow_linear. + destruct (Nnorm _ _ _) as [c | | ] eqn: HN; + try ( apply rdiv_ext; + eapply ring_rw_pow_correct; eauto). + destruct (ceqb_spec c cI). + set (nnum := NPphi_pow _ _). + apply eq_trans with (nnum / NPphi_pow l (Pc c)). + apply rdiv_ext; + eapply ring_rw_pow_correct; eauto. + rewrite Pphi_pow_ok; try eassumption. + now simpl; rewrite H0, phi_1, <- rdiv1. + apply rdiv_ext; + eapply ring_rw_pow_correct; eauto. Qed. Theorem Field_correct n l lpe fe1 fe2 : diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 4886c8b9aa..a98a963207 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -105,7 +105,7 @@ Section ZMORPHISM. Proof. constructor. destruct c;intros;try discriminate. - injection H as <-. + injection H as [= <-]. simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. Qed. @@ -740,7 +740,6 @@ Ltac abstract_ring_morphism set ext rspec := | _ => fail 1 "bad ring structure" end. -#[universes(template)] Record hypo : Type := mkhypo { hypo_type : Type; hypo_proof : hypo_type diff --git a/plugins/setoid_ring/Integral_domain.v b/plugins/setoid_ring/Integral_domain.v index 98407cb6d7..f1394c51d5 100644 --- a/plugins/setoid_ring/Integral_domain.v +++ b/plugins/setoid_ring/Integral_domain.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v index 36a92505eb..8cda4ad714 100644 --- a/plugins/setoid_ring/NArithRing.v +++ b/plugins/setoid_ring/NArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v index 2ca0d60948..8f3de26272 100644 --- a/plugins/setoid_ring/Ncring.v +++ b/plugins/setoid_ring/Ncring.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index aa0370b2ac..e40ef6056d 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 31182f51e2..048c8eecf9 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -32,7 +32,6 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. with coefficients in C : *) -#[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | PX : Pol -> positive -> positive -> Pol -> Pol. diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index c8d560cfe9..65233873b1 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index e12bf36339..d83fcf3781 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index b83e1c6704..35e308565f 100644 --- a/plugins/setoid_ring/Ring.v +++ b/plugins/setoid_ring/Ring.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v index 920b13ef49..36e7890fbb 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/plugins/setoid_ring/Ring_base.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index f7cb6b688b..092114ff0b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -121,7 +121,6 @@ Section MakeRingPol. - (Pinj i (Pc c)) is (Pc c) *) - #[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol @@ -894,7 +893,7 @@ Section MakeRingPol. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H as <-. rewrite <- PSubstL1_ok; intuition. + * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. @@ -909,7 +908,6 @@ Section MakeRingPol. (** Definition of polynomial expressions *) - #[universes(template)] Inductive PExpr : Type := | PEO : PExpr | PEI : PExpr diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 26fef99bb2..0a14c0ee5c 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 3e835f5c9f..dc45853458 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -540,7 +540,6 @@ Section AddRing. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). Variable req : R -> R -> Prop. *) -#[universes(template)] Inductive ring_kind : Type := | Abstract | Computational diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v index df3677e1c3..b3ed0be916 100644 --- a/plugins/setoid_ring/Rings_Q.v +++ b/plugins/setoid_ring/Rings_Q.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v index fe7558845d..ec91fa9e97 100644 --- a/plugins/setoid_ring/Rings_R.v +++ b/plugins/setoid_ring/Rings_R.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v index 75e77ab6ef..a0901202f7 100644 --- a/plugins/setoid_ring/Rings_Z.v +++ b/plugins/setoid_ring/Rings_Z.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v index 19eaddc123..833e19a698 100644 --- a/plugins/setoid_ring/ZArithRing.v +++ b/plugins/setoid_ring/ZArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg index 6be556b2ae..f2a3608d92 100644 --- a/plugins/setoid_ring/g_newring.mlg +++ b/plugins/setoid_ring/g_newring.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -13,8 +13,6 @@ open Ltac_plugin open Pp open Util -open Libnames -open Printer open Newring_ast open Newring open Stdarg @@ -85,21 +83,10 @@ 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 add_theory id t l } - | ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { - fun ~pstate -> - Feedback.msg_notice (strbrk "The following ring structures have been declared:"); - Spmap.iter (fun fn fi -> - (* We should use the global env here as this shouldn't contain proof - data, however preserving behavior as requested in review. *) - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - 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; - pstate } + { add_theory id t (Option.default [] l) } + | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { + print_rings () + } END TACTIC EXTEND ring_lookup @@ -135,20 +122,9 @@ 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 add_field_theory id t l } -| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { - fun ~pstate -> - Feedback.msg_notice (strbrk "The following field structures have been declared:"); - Spmap.iter (fun fn fi -> - (* We should use the global env here as this shouldn't - contain proof data. *) - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - 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; - pstate } +| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { + print_fields () + } END TACTIC EXTEND field_lookup diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 3f69701bd3..76c393450b 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -18,7 +18,6 @@ open EConstr open Vars open CClosure open Environ -open Libnames open Globnames open Glob_term open Locus @@ -29,7 +28,6 @@ open Tacinterp open Libobject open Printer open Declare -open Decl_kinds open Entries open Newring_ast open Proofview.Notations @@ -50,7 +48,7 @@ let global_head_of_constr sigma c = let global_of_constr_nofail c = try global_of_constr c - with Not_found -> VarRef (Id.of_string "dummy") + with Not_found -> GlobRef.VarRef (Id.of_string "dummy") let rec mk_clos_but f_map n t = let (f, args) = Constr.decompose_appvect t in @@ -89,10 +87,10 @@ let protect_red map env sigma c0 = EConstr.of_constr (eval 0 c) let protect_tac map = - Tactics.reduct_option (protect_red map,DEFAULTcast) None + Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) None let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)) + Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)) (****************************************************************************) @@ -152,11 +150,13 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in - let univs = UState.restrict_universe_context univs vars in - let univs = Monomorphic_entry univs in - mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true ~univs c), - IsProof Lemma)) + let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in + let () = Declare.declare_universe_context ~poly:false univs in + let types = (Typeops.infer (Global.env ()) c).uj_type in + let univs = Monomorphic_entry Univ.ContextSet.empty in + mkConst(declare_constant ~name:(Id.of_string na) + ~kind:Decls.(IsProof Lemma) + (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c))) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = @@ -325,7 +325,18 @@ let _ = add_map "ring" module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" -let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" + +let print_rings () = + Feedback.msg_notice (strbrk "The following ring structures have been declared:"); + Cmap.iter (fun _carrier ring -> + let env = Global.env () in + let sigma = Evd.from_env env in + Feedback.msg_notice + (hov 2 + (Ppconstr.pr_id ring.ring_name ++ spc() ++ + str"with carrier "++ pr_constr_env env sigma ring.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma ring.ring_req)) + ) !from_carrier let ring_for_carrier r = Cmap.find r !from_carrier @@ -348,9 +359,7 @@ let find_ring_structure env sigma l = | [] -> assert false let add_entry (sp,_kn) e = - from_carrier := Cmap.add e.ring_carrier e !from_carrier; - from_name := Spmap.add sp e !from_name - + from_carrier := Cmap.add e.ring_carrier e !from_carrier let subst_th (subst,th) = let c' = subst_mps subst th.ring_carrier in @@ -378,7 +387,8 @@ let subst_th (subst,th) = pretac' == th.ring_pre_tac && posttac' == th.ring_post_tac then th else - { ring_carrier = c'; + { ring_name = th.ring_name; + ring_carrier = c'; ring_req = eq'; ring_setoid = set'; ring_ext = ext'; @@ -415,59 +425,6 @@ let op_morph r add mul opp req m1 m2 m3 = let op_smorph r add mul req m1 m2 = lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] -(* let default_ring_equality (r,add,mul,opp,req) = *) -(* let is_setoid = function *) -(* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *) -(* eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *) -(* | _ -> false in *) -(* match default_relation_for_carrier ~filter:is_setoid r with *) -(* Leibniz _ -> *) -(* let setoid = lapp coq_eq_setoid [|r|] in *) -(* let op_morph = *) -(* match opp with *) -(* Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *) -(* | None -> lapp coq_eq_smorph [|r;add;mul|] in *) -(* (setoid,op_morph) *) -(* | Relation rel -> *) -(* let setoid = setoid_of_relation rel in *) -(* let is_endomorphism = function *) -(* { args=args } -> List.for_all *) -(* (function (var,Relation rel) -> *) -(* var=None && eq_constr_nounivs req rel *) -(* | _ -> false) args in *) -(* let add_m = *) -(* try default_morphism ~filter:is_endomorphism add *) -(* with Not_found -> *) -(* error "ring addition should be declared as a morphism" in *) -(* let mul_m = *) -(* try default_morphism ~filter:is_endomorphism mul *) -(* with Not_found -> *) -(* error "ring multiplication should be declared as a morphism" in *) -(* let op_morph = *) -(* match opp with *) -(* | Some opp -> *) -(* (let opp_m = *) -(* try default_morphism ~filter:is_endomorphism opp *) -(* with Not_found -> *) -(* error "ring opposite should be declared as a morphism" in *) -(* let op_morph = *) -(* op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *) -(* msgnl *) -(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ *) -(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) -(* str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *) -(* str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *) -(* str"\""); *) -(* op_morph) *) -(* | None -> *) -(* (msgnl *) -(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ *) -(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) -(* str"\""++spc()++str"and \""++ *) -(* pr_constr mul_m.morphism_theory++str"\""); *) -(* op_smorph r add mul req add_m.lem mul_m.lem) in *) -(* (setoid,op_morph) *) - let ring_equality env evd (r,add,mul,opp,req) = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> @@ -644,7 +601,8 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div let _ = Lib.add_leaf name (theory_to_obj - { ring_carrier = r; + { ring_name = name; + ring_carrier = r; ring_req = req; ring_setoid = sth; ring_ext = params.(1); @@ -822,7 +780,18 @@ let dest_field env evd th_spec = | _ -> error "bad field structure" let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table" -let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table" + +let print_fields () = + Feedback.msg_notice (strbrk "The following field structures have been declared:"); + Cmap.iter (fun _carrier fi -> + let env = Global.env () in + let sigma = Evd.from_env env in + Feedback.msg_notice + (hov 2 + (Id.print fi.field_name ++ spc() ++ + 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_carrier let field_for_carrier r = Cmap.find r !field_from_carrier @@ -846,8 +815,7 @@ let find_field_structure env sigma l = | [] -> assert false let add_field_entry (sp,_kn) e = - field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier; - field_from_name := Spmap.add sp e !field_from_name + field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier let subst_th (subst,th) = let c' = subst_mps subst th.field_carrier in @@ -873,7 +841,8 @@ let subst_th (subst,th) = pretac' == th.field_pre_tac && posttac' == th.field_post_tac then th else - { field_carrier = c'; + { field_name = th.field_name; + field_carrier = c'; field_req = eq'; field_cst_tac = tac'; field_pow_tac = pow_tac'; @@ -958,7 +927,8 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od let _ = Lib.add_leaf name (ftheory_to_obj - { field_carrier = r; + { field_name = name; + field_carrier = r; field_req = req; field_cst_tac = cst_tac; field_pow_tac = pow_tac; diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index fcd04a2e73..4c848d3f5b 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -10,7 +10,6 @@ open Names open EConstr -open Libnames open Constrexpr open Newring_ast @@ -23,7 +22,7 @@ val add_theory : constr_expr -> constr_expr ring_mod list -> unit -val from_name : ring_info Spmap.t ref +val print_rings : unit -> unit val ring_lookup : Geninterp.Val.t -> @@ -35,7 +34,7 @@ val add_field_theory : constr_expr -> constr_expr field_mod list -> unit -val field_from_name : field_info Spmap.t ref +val print_fields : unit -> unit val field_lookup : Geninterp.Val.t -> diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml index a83c79d11b..b81f5f7d14 100644 --- a/plugins/setoid_ring/newring_ast.ml +++ b/plugins/setoid_ring/newring_ast.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -40,7 +40,8 @@ type 'constr field_mod = | Inject of constr_expr type ring_info = - { ring_carrier : types; + { ring_name : Names.Id.t; + ring_carrier : types; ring_req : constr; ring_setoid : constr; ring_ext : constr; @@ -54,7 +55,8 @@ type ring_info = ring_post_tac : glob_tactic_expr } type field_info = - { field_carrier : types; + { field_name : Names.Id.t; + field_carrier : types; field_req : constr; field_cst_tac : glob_tactic_expr; field_pow_tac : glob_tactic_expr; diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index a83c79d11b..b81f5f7d14 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -40,7 +40,8 @@ type 'constr field_mod = | Inject of constr_expr type ring_info = - { ring_carrier : types; + { ring_name : Names.Id.t; + ring_carrier : types; ring_req : constr; ring_setoid : constr; ring_ext : constr; @@ -54,7 +55,8 @@ type ring_info = ring_post_tac : glob_tactic_expr } type field_info = - { field_carrier : types; + { field_name : Names.Id.t; + field_carrier : types; field_req : constr; field_cst_tac : glob_tactic_expr; field_pow_tac : glob_tactic_expr; |