diff options
52 files changed, 801 insertions, 782 deletions
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index ceb390c02c..340b66bbd0 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -96,6 +96,8 @@ in time. - [ ] Delay non-blocking issues to the appropriate milestone and ensure blocking issues are solved. If required to solve some blocking issues, it is possible to revert some feature PRs in the version branch only. +- [ ] Add a new link to the ``'versions'`` list of the refman (in + ``html_context`` in ``doc/sphinx/conf.py``). ## Before the beta release date ## diff --git a/doc/LICENSE b/doc/LICENSE index 9f3a6b3f4c..a327156144 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -6,13 +6,16 @@ copyright (c) 1999-2019, Inria, CNRS and contributors, with the exception of the Ubuntu font file UbuntuMono-B.ttf, which is Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font license, version 1.0 -(https://www.ubuntu.com/legal/terms-and-policies/font-licence), and +(https://www.ubuntu.com/legal/terms-and-policies/font-licence), its derivative CoqNotations.ttf distributed under the same -license. The material connected to the Reference Manual may be -distributed only subject to the terms and conditions set forth in the -Open Publication License, v1.0 or later (the latest version is -presently available at http://www.opencontent.org/openpub/). Options -A and B are *not* elected. +license, and the _templates/versions.html file derived from +sphinx_rtd_theme, which is Copyright 2013-2018 Dave Snider, Read the +Docs, Inc. & contributors and distributed under the MIT License +included in that file. The material connected to the Reference Manual +may be distributed only subject to the terms and conditions set forth in +the Open Publication License, v1.0 or later (the latest version is +presently available at http://www.opencontent.org/openpub/). Options A +and B are *not* elected. The Coq Standard Library is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index b94b1fc657..e9e866c5fb 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,6 +1,6 @@ let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let scope = Declare.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - DeclareDef.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl + Declare.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly ~types:None ~body sigma diff --git a/doc/sphinx/_templates/versions.html b/doc/sphinx/_templates/versions.html new file mode 100644 index 0000000000..967d00d2bf --- /dev/null +++ b/doc/sphinx/_templates/versions.html @@ -0,0 +1,48 @@ +{# Forked from versions.html in sphinx_rtd_theme 0.4.3 #} + +{# +The MIT License (MIT) + +Copyright (c) 2013-2018 Dave Snider, Read the Docs, Inc. & contributors + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of +the Software, and to permit persons to whom the Software is furnished to do so, +subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR +COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER +IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +#} + +{% if not READTHEDOCS %} + <div class="rst-versions" data-toggle="rst-versions" role="note" aria-label="versions"> + <span class="rst-current-version" data-toggle="rst-current-version"> + <span class="fa fa-book"> Other versions</span> + v: {{ version }} + <span class="fa fa-caret-down"></span> + </span> + <div class="rst-other-versions"> + <dl> + <dt>{{ _('Versions') }}</dt> + {% for slug, url in versions %} + <dd><a href="{{ url }}">{{ slug }}</a></dd> + {% endfor %} + </dl> + <dl> + <dt>{{ _('Downloads') }}</dt> + {% for type, url in downloads %} + <dd><a href="{{ url }}">{{ type }}</a></dd> + {% endfor %} + </dl> + </div> + </div> +{% endif %} diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index dbe582df95..4136b406de 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -202,6 +202,7 @@ html_theme = 'sphinx_rtd_theme' # Theme options are theme-specific and customize the look and feel of a theme # further. For a list of options available for each theme, see the # documentation. +PDF_URL = "https://github.com/coq/coq/releases/download/V{version}/coq-{version}-reference-manual.pdf" html_theme_options = { 'collapse_navigation': False } @@ -210,7 +211,26 @@ html_context = { 'github_user': 'coq', 'github_repo': 'coq', 'github_version': 'master', - 'conf_py_path': '/doc/sphinx/' + 'conf_py_path': '/doc/sphinx/', + # Versions and downloads listed in the versions menu (see _templates/versions.html) + 'versions': [ + ("master", "https://coq.github.io/doc/master/refman/"), + ("stable", "https://coq.inria.fr/distrib/current/refman/"), + ("v8.11", "https://coq.github.io/doc/v8.11/refman/"), + ("v8.10", "https://coq.github.io/doc/v8.10/refman/"), + ("v8.9", "https://coq.github.io/doc/v8.9/refman/"), + ("8.8", "https://coq.inria.fr/distrib/V8.8.2/refman/"), + ("8.7", "https://coq.inria.fr/distrib/V8.7.2/refman/"), + ("8.6", "https://coq.inria.fr/distrib/V8.6.1/refman/"), + ("8.5", "https://coq.inria.fr/distrib/V8.5pl3/refman/"), + ("8.4", "https://coq.inria.fr/distrib/V8.4pl6/refman/"), + ("8.3", "https://coq.inria.fr/distrib/V8.3pl5/refman/"), + ("8.2", "https://coq.inria.fr/distrib/V8.2pl3/refman/"), + ("8.1", "https://coq.inria.fr/distrib/V8.1pl6/refman/"), + ("8.0", "https://coq.inria.fr/distrib/V8.0/doc/") + ], + 'downloads': ([("PDF", PDF_URL.format(version=version))] + if coq_config.is_a_released_version else []) } # Add any paths that contain custom themes here, relative to this directory. diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index c53dcc7edd..608155eb71 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -218,7 +218,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac in (* uctx was ignored before *) - let hook = DeclareDef.Hook.make (hook new_principle_type) in + let hook = Declare.Hook.make (hook new_principle_type) in (body, typ, univs, hook, sigma) let change_property_sort evd toSort princ princName = @@ -318,8 +318,8 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts let uctx = Evd.evar_universe_context sigma in let entry = Declare.definition_entry ~univs ?types body in let (_ : Names.GlobRef.t) = - DeclareDef.declare_entry ~name:new_princ_name ~hook - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + Declare.declare_entry ~name:new_princ_name ~hook + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) ~impargs:[] ~uctx entry in @@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl = Pp.(str "Body of Function must be given") in ComDefinition.do_definition ~name:fname.CAst.v ~poly:false - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~kind:Decls.Definition univs binders None body (Some rtype); let evd, rev_pconstants = List.fold_left @@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl = (None, evd, List.rev rev_pconstants) | _ -> ComFixpoint.do_fixpoint - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd, rev_pconstants = List.fold_left diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ffb9a7e69b..5c82ed38bb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1483,7 +1483,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name let lemma = build_proof env (Evd.from_env env) start_tac end_tac in Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in - let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in + let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in let lemma = Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type in @@ -1721,7 +1721,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook {DeclareDef.Hook.S.uctx; _} = + let hook {Declare.Hook.S.uctx; _} = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref @@ -1767,5 +1767,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls functional_ref (EConstr.of_constr rec_arg_type) relation rec_arg_num term_id using_lemmas (List.length res_vars) evd - (DeclareDef.Hook.make hook)) + (Declare.Hook.make hook)) () diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 5baa23b3e9..aef5f645f4 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; tac = Pltac.tactic -> - { ComHints.HintsExtern (n,c, in_tac tac) } ] ] + { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ] ; operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3834b21a14..3b8fb48eb0 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1894,10 +1894,10 @@ let declare_projection name instance_id r = in it_mkProd_or_LetIn ccl ctx in let types = Some (it_mkProd_or_LetIn typ ctx) in - let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let _r : GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma + Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma in () let build_morphism_signature env sigma m = @@ -1961,10 +1961,10 @@ let add_morphism_as_parameter atts m n : unit = let env = Global.env () in let evd = Evd.from_env env in let poly = atts.polymorphic in - let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let evd, types = build_morphism_signature env evd m in - let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in + let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in let cst = GlobRef.ConstRef cst in Classes.add_instance @@ -1981,7 +1981,7 @@ let add_morphism_interactive atts m n : Lemmas.t = let poly = atts.polymorphic in let kind = Decls.(IsDefinition Instance) in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in - let hook { DeclareDef.Hook.S.dref; _ } = dref |> function + let hook { Declare.Hook.S.dref; _ } = dref |> function | GlobRef.ConstRef cst -> Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info @@ -1989,7 +1989,7 @@ let add_morphism_interactive atts m n : Lemmas.t = declare_projection n instance_id (GlobRef.ConstRef cst) | _ -> assert false in - let hook = DeclareDef.Hook.make hook in + let hook = Declare.Hook.make hook in let info = Lemmas.Info.make ~hook ~kind () in Flags.silently (fun () -> diff --git a/theories/Reals/Abstract/ConstructiveAbs.v b/theories/Reals/Abstract/ConstructiveAbs.v index d357ad2d54..31397cbddd 100644 --- a/theories/Reals/Abstract/ConstructiveAbs.v +++ b/theories/Reals/Abstract/ConstructiveAbs.v @@ -57,11 +57,11 @@ Proof. - pose proof (CRabs_def R x (CRabs R x)) as [_ H1]. apply H1, CRle_refl. - rewrite <- CRabs_def. split. apply CRle_refl. - apply (CRle_trans _ (CRzero R)). 2: exact H. - apply (CRle_trans _ (CRopp R (CRzero R))). + apply (CRle_trans _ 0). 2: exact H. + apply (CRle_trans _ (CRopp R 0)). intro abs. apply CRopp_lt_cancel in abs. contradiction. - apply (CRplus_le_reg_l (CRzero R)). - apply (CRle_trans _ (CRzero R)). apply CRplus_opp_r. + apply (CRplus_le_reg_l 0). + apply (CRle_trans _ 0). apply CRplus_opp_r. apply CRplus_0_r. Qed. @@ -164,8 +164,7 @@ Lemma CR_of_Q_abs : forall {R : ConstructiveReals} (q : Q), Proof. intros. destruct (Qlt_le_dec 0 q). - apply (CReq_trans _ (CR_of_Q R q)). - apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)). - apply CR_of_Q_zero. apply CR_of_Q_le. apply Qlt_le_weak, q0. + apply CRabs_right. apply CR_of_Q_le. apply Qlt_le_weak, q0. apply CR_of_Q_morph. symmetry. apply Qabs_pos, Qlt_le_weak, q0. - apply (CReq_trans _ (CR_of_Q R (-q))). apply (CReq_trans _ (CRabs R (CRopp R (CR_of_Q R q)))). @@ -173,8 +172,7 @@ Proof. 2: apply CR_of_Q_morph; symmetry; apply Qabs_neg, q0. apply (CReq_trans _ (CRopp R (CR_of_Q R q))). 2: apply CReq_sym, CR_of_Q_opp. - apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)). - apply CR_of_Q_zero. + apply CRabs_right. apply (CRle_trans _ (CR_of_Q R (-q))). apply CR_of_Q_le. apply (Qplus_le_l _ _ q). ring_simplify. exact q0. apply CR_of_Q_opp. @@ -206,14 +204,14 @@ Proof. destruct (CR_Q_dense R _ _ neg) as [q [H0 H1]]. destruct (Qlt_le_dec 0 q). - destruct (s (CR_of_Q R (-q)) x 0). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. + apply CR_of_Q_lt. apply (Qplus_lt_l _ _ q). ring_simplify. exact q0. exfalso. pose proof (CRabs_def R x (CR_of_Q R q)) as [H2 _]. apply H2. clear H2. split. apply CRlt_asym, H0. 2: exact H1. rewrite <- Qopp_involutive, CR_of_Q_opp. apply CRopp_ge_le_contravar, CRlt_asym, c. exact c. - apply (CRlt_le_trans _ _ _ H0). - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. exact q0. + apply CR_of_Q_le. exact q0. Qed. @@ -339,24 +337,23 @@ Proof. left; apply CR_of_Q_pos; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_right. unfold CRminus. rewrite CRopp_plus_distr, CRplus_assoc, <- (CRplus_assoc y). rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. reflexivity. apply (CRmult_lt_compat_r (CR_of_Q R 2)) in H. 2: apply CR_of_Q_pos; reflexivity. - rewrite CRmult_assoc, <- CR_of_Q_mult in H. - setoid_replace ((1 # 2) * 2)%Q with 1%Q in H. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r in H. - rewrite CRmult_comm, (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_r, - CRmult_1_l in H. - intro abs. rewrite CRabs_left in H. - unfold CRminus in H. - rewrite CRopp_involutive, CRplus_comm in H. - rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l in H. - rewrite CRplus_0_l in H. exact (CRlt_asym _ _ H H). - apply CRlt_asym, abs. + intro abs. contradict H. + apply (CRle_trans _ (x + y - CRabs R (y - x))). + rewrite CRabs_left. 2: apply CRlt_asym, abs. + unfold CRminus. rewrite CRopp_involutive, CRplus_comm. + rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l. + rewrite CRplus_0_l, (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. + rewrite CRmult_1_r. apply CRle_refl. + rewrite CRmult_assoc, <- CR_of_Q_mult. + setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. + rewrite CRmult_1_r. apply CRle_refl. Qed. Add Parametric Morphism {R : ConstructiveReals} : CRmin @@ -383,11 +380,11 @@ Lemma CRmin_l : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_r (CRabs _ (y + - x)+ -x)). rewrite CRplus_assoc, <- (CRplus_assoc (-CRabs _ (y + - x))). @@ -401,11 +398,11 @@ Lemma CRmin_r : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite (CRplus_comm x). unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). @@ -451,15 +448,15 @@ Proof. intros. unfold CRmin. unfold CRminus. setoid_replace (x + z + - (x + y)) with (z-y). apply (CRmult_eq_reg_r (CR_of_Q _ 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_plus_distr_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. do 3 rewrite (CRplus_assoc x). apply CRplus_morph. reflexivity. do 2 rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. rewrite (CRplus_comm x). apply CRplus_assoc. @@ -474,11 +471,11 @@ Lemma CRmin_left : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_right. unfold CRminus. rewrite CRopp_plus_distr. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. apply CRopp_involutive. @@ -491,11 +488,11 @@ Lemma CRmin_right : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_left. unfold CRminus. do 2 rewrite CRopp_plus_distr. rewrite (CRplus_comm x y). rewrite CRplus_assoc. apply CRplus_morph. reflexivity. @@ -510,10 +507,10 @@ Lemma CRmin_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_lt_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_lt_reg_l _ (CRabs _ (y - x) - (z*CR_of_Q R 2))). unfold CRminus. rewrite CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_r. rewrite (CRplus_comm (CRabs R (y + - x))). @@ -526,7 +523,7 @@ Proof. apply (CRplus_lt_reg_l R (-x)). rewrite CRopp_mult_distr_l. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym. apply CRopp_gt_lt_contravar, H. @@ -537,7 +534,7 @@ Proof. apply (CRplus_lt_reg_l R (-y)). rewrite CRopp_mult_distr_l. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym. apply CRopp_gt_lt_contravar, H0. @@ -552,12 +549,12 @@ Proof. rewrite (CRabs_morph _ ((x - y + (CRabs _ (a - y) - CRabs _ (a - x))) * CR_of_Q R (1 # 2))). rewrite CRabs_mult, (CRabs_right (CR_of_Q R (1 # 2))). - 2: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate. + 2: apply CR_of_Q_le; discriminate. apply (CRle_trans _ ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1) * CR_of_Q R (1 # 2))). apply CRmult_le_compat_r. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. apply (CRle_trans _ (CRabs _ (x - y) + CRabs _ (CRabs _ (a - y) - CRabs _ (a - x)))). apply CRabs_triang. rewrite CRmult_1_r. apply CRplus_le_compat_l. @@ -568,11 +565,11 @@ Proof. rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l. reflexivity. - rewrite <- CRmult_plus_distr_l, <- CR_of_Q_one. + rewrite <- CRmult_plus_distr_l. rewrite <- (CR_of_Q_plus R 1 1). rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl. + rewrite CRmult_1_r. apply CRle_refl. unfold CRminus. apply CRmult_morph. 2: reflexivity. do 4 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc. rewrite CRplus_comm, CRopp_plus_distr. @@ -587,10 +584,10 @@ Lemma CRmin_glb : forall {R : ConstructiveReals} (x y z:CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_le_reg_l (CRabs _ (y-x) - (z*CR_of_Q R 2))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite (CRplus_comm (CRabs R (y + - x) + - (z * CR_of_Q R 2))). @@ -601,13 +598,13 @@ Proof. rewrite CRopp_involutive, (CRplus_comm y), CRplus_assoc. apply CRplus_le_compat_l, (CRplus_le_reg_l y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_compat; exact H0. - rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite CRopp_mult_distr_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_compat; apply CRopp_ge_le_contravar; exact H. Qed. @@ -673,11 +670,11 @@ Lemma CRmax_lub : forall {R : ConstructiveReals} (x y z:CRcarrier R), x <= z -> y <= z -> CRmax x y <= z. Proof. intros. unfold CRmax. - apply (CRmult_le_reg_r (CR_of_Q _ 2)). rewrite <- CR_of_Q_zero. + apply (CRmult_le_reg_r (CR_of_Q _ 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_le_reg_l (-x-y)). rewrite <- CRplus_assoc. unfold CRminus. rewrite <- CRopp_plus_distr, CRplus_opp_l, CRplus_0_l. @@ -687,14 +684,14 @@ Proof. rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRopp_plus_distr. apply CRplus_le_compat; apply CRopp_ge_le_contravar; assumption. - rewrite (CRplus_comm y), CRopp_plus_distr, CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. apply CRplus_le_compat; assumption. Qed. @@ -702,12 +699,12 @@ Lemma CRmax_l : forall {R : ConstructiveReals} (x y : CRcarrier R), x <= CRmax x y. Proof. intros. unfold CRmax. - apply (CRmult_le_reg_r (CR_of_Q R 2)). rewrite <- CR_of_Q_zero. + apply (CRmult_le_reg_r (CR_of_Q R 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - setoid_replace 2%Q with (1+1)%Q. rewrite CR_of_Q_plus, CR_of_Q_one. + rewrite CRmult_1_r. + setoid_replace 2%Q with (1+1)%Q. rewrite CR_of_Q_plus. rewrite CRmult_plus_distr_l, CRmult_1_r, CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-y)). @@ -720,12 +717,12 @@ Lemma CRmax_r : forall {R : ConstructiveReals} (x y : CRcarrier R), y <= CRmax x y. Proof. intros. unfold CRmax. - apply (CRmult_le_reg_r (CR_of_Q _ 2)). rewrite <- CR_of_Q_zero. + apply (CRmult_le_reg_r (CR_of_Q _ 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite (CRplus_comm x). rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). @@ -754,14 +751,14 @@ Proof. intros. unfold CRmax. setoid_replace (x + z - (x + y)) with (z-y). apply (CRmult_eq_reg_r (CR_of_Q _ 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_plus_distr_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRmult_1_r. do 3 rewrite (CRplus_assoc x). apply CRplus_morph. reflexivity. do 2 rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. @@ -777,11 +774,11 @@ Lemma CRmax_left : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmax. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRabs_left. unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. reflexivity. @@ -793,11 +790,11 @@ Lemma CRmax_right : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmax. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite (CRplus_comm x y). rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRabs_right. unfold CRminus. rewrite CRplus_comm. @@ -812,12 +809,12 @@ Proof. rewrite (CRabs_morph _ ((x - y + (CRabs _ (a - x) - CRabs _ (a - y))) * CR_of_Q R (1 # 2))). rewrite CRabs_mult, (CRabs_right (CR_of_Q R (1 # 2))). - 2: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate. + 2: apply CR_of_Q_le; discriminate. apply (CRle_trans _ ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1) * CR_of_Q R (1 # 2))). apply CRmult_le_compat_r. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. apply (CRle_trans _ (CRabs _ (x - y) + CRabs _ (CRabs _ (a - x) - CRabs _ (a - y)))). apply CRabs_triang. rewrite CRmult_1_r. apply CRplus_le_compat_l. @@ -829,11 +826,11 @@ Proof. rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l. reflexivity. - rewrite <- CRmult_plus_distr_l, <- CR_of_Q_one. + rewrite <- CRmult_plus_distr_l. rewrite <- (CR_of_Q_plus R 1 1). rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl. + rewrite CRmult_1_r. apply CRle_refl. unfold CRminus. rewrite CRopp_mult_distr_l. rewrite <- CRmult_plus_distr_r. apply CRmult_morph. 2: reflexivity. do 4 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. @@ -849,10 +846,10 @@ Lemma CRmax_lub_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R), Proof. intros. unfold CRmax. apply (CRmult_lt_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_lt_reg_l _ (-y -x)). unfold CRminus. rewrite CRplus_assoc, <- (CRplus_assoc (-x)), <- (CRplus_assoc (-x)). rewrite CRplus_opp_l, CRplus_0_l, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. @@ -861,14 +858,14 @@ Proof. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l _ y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym, H0. exact H0. - rewrite CRopp_plus_distr, CRopp_involutive. rewrite CRplus_assoc. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l _ x). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym, H. exact H. Qed. diff --git a/theories/Reals/Abstract/ConstructiveLUB.v b/theories/Reals/Abstract/ConstructiveLUB.v index 4ae24de154..1c19c6aa40 100644 --- a/theories/Reals/Abstract/ConstructiveLUB.v +++ b/theories/Reals/Abstract/ConstructiveLUB.v @@ -108,7 +108,7 @@ Proof. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply le_S, H0. discriminate. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. Qed. Lemma is_upper_bound_dec : @@ -272,7 +272,7 @@ Proof. apply CR_of_Q_pos. reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult, (CR_of_Q_plus R 1 1). setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r. + rewrite CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r. apply CRplus_lt_compat_r. exact H0. } destruct (CR_cv_open_below _ _ l lcv H1) as [p pmaj]. assert (0 < (l-CR_of_Q R r) * CR_of_Q R (1#2)). @@ -280,7 +280,6 @@ Proof. apply CRplus_lt_compat_r. exact H0. apply CR_of_Q_pos. reflexivity. } destruct (CRup_nat (CRinv R _ (inr H2))) as [i imaj]. destruct i. exfalso. simpl in imaj. - rewrite CR_of_Q_zero in imaj. exact (CRlt_asym _ _ imaj (CRinv_0_lt_compat R _ (inr H2) H2)). specialize (pmaj (max (S i) (S p)) (le_trans p (S p) _ (le_S p p (le_refl p)) (Nat.le_max_r (S i) (S p)))). unfold proj1_sig in pmaj. @@ -309,7 +308,7 @@ Proof. CR_of_Q R (1 # Pos.of_nat (S i)))). apply CRlt_asym, imaj. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.of_nat (S i) # 1) * (1 # Pos.of_nat (S i)))%Q with 1%Q. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. unfold CRminus. rewrite CRmult_plus_distr_r, (CRplus_comm (-CR_of_Q R r)). rewrite (CRplus_comm (CR_of_Q R r)), CRmult_plus_distr_r. rewrite CRplus_assoc. apply CRplus_le_compat_l. diff --git a/theories/Reals/Abstract/ConstructiveLimits.v b/theories/Reals/Abstract/ConstructiveLimits.v index 4a40cc8cb3..64dcd2e1ec 100644 --- a/theories/Reals/Abstract/ConstructiveLimits.v +++ b/theories/Reals/Abstract/ConstructiveLimits.v @@ -89,7 +89,7 @@ Lemma CR_cv_unique : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) -> CR_cv R xn b -> a == b. Proof. - intros. assert (CR_cv R (fun _ => CRzero R) (CRminus R b a)). + intros. assert (CR_cv R (fun _ => 0) (CRminus R b a)). { apply (CR_cv_extens (fun n => CRminus R (xn n) (xn n))). intro n. unfold CRminus. apply CRplus_opp_r. apply CR_cv_plus. exact H0. apply CR_cv_opp, H. } @@ -111,8 +111,7 @@ Proof. rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl. do 2 rewrite Pos.mul_1_r. reflexivity. apply (Qplus_lt_l _ _ q). ring_simplify. - apply (lt_CR_of_Q R q 0). apply (CRlt_le_trans _ (CRzero R) _ H). - apply CR_of_Q_zero. + apply (lt_CR_of_Q R q 0). exact H. apply (CRlt_le_trans _ (CRopp R z)). apply (CRle_lt_trans _ (CRopp R (CR_of_Q R q))). apply CR_of_Q_opp. apply CRopp_gt_lt_contravar, H0. @@ -131,8 +130,7 @@ Proof. setoid_replace ((Z.pos p # 1) * (1 # p))%Q with 1%Q in pmaj. rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl. do 2 rewrite Pos.mul_1_r. reflexivity. - apply (lt_CR_of_Q R 0 q). apply (CRle_lt_trans _ (CRzero R)). - 2: exact H0. apply CR_of_Q_zero. + apply (lt_CR_of_Q R 0 q). exact H0. apply (CRlt_le_trans _ _ _ H). apply (CRle_trans _ (CRabs R (CRopp R z))). apply (CRle_trans _ (CRabs R z)). @@ -140,10 +138,7 @@ Proof. apply H1. apply CRle_refl. apply CRabs_opp. apply CRabs_morph. unfold CRminus. symmetry. apply CRplus_0_l. - subst z. apply (CRplus_eq_reg_l (CRopp R a)). - apply (CReq_trans _ (CRzero R)). apply CRplus_opp_l. - destruct (CRisRing R). - apply (CReq_trans _ (CRplus R b (CRopp R a))). apply CReq_sym, H. - apply Radd_comm. + rewrite CRplus_opp_l, CRplus_comm. symmetry. exact H. Qed. Lemma CR_cv_eq : forall {R : ConstructiveReals} @@ -196,7 +191,7 @@ Lemma Un_cv_nat_real : forall {R : ConstructiveReals} Proof. intros. destruct (CR_archimedean R (CRinv R eps (inr H0))) as [k kmaj]. assert (0 < CR_of_Q R (Z.pos k # 1)). - { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. } + { apply CR_of_Q_lt. reflexivity. } specialize (H k) as [p pmaj]. exists p. intros. apply (CRle_lt_trans _ (CR_of_Q R (1 # k))). @@ -204,7 +199,7 @@ Proof. apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos k # 1))). exact H1. rewrite <- CR_of_Q_mult. apply (CRle_lt_trans _ 1). - rewrite <- CR_of_Q_one. apply CR_of_Q_le. + apply CR_of_Q_le. unfold Qle; simpl. do 2 rewrite Pos.mul_1_r. apply Z.le_refl. apply (CRmult_lt_reg_r (CRinv R eps (inr H0))). apply CRinv_0_lt_compat, H0. rewrite CRmult_1_l, CRmult_assoc. @@ -220,7 +215,7 @@ Lemma Un_cv_real_nat : forall {R : ConstructiveReals} Proof. intros. intros n. specialize (H (CR_of_Q R (1#n))) as [p pmaj]. - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply CR_of_Q_lt. reflexivity. exists p. intros. apply CRlt_asym. apply pmaj. apply H. Qed. @@ -288,12 +283,12 @@ Proof. setoid_replace (1 # n * x)%Q with ((1 # n) *(1# x))%Q. 2: reflexivity. rewrite <- (CRmult_1_r (CR_of_Q R (1#n))). rewrite CR_of_Q_mult, CRmult_assoc. - apply CRmult_le_compat_l. rewrite <- CR_of_Q_zero. + apply CRmult_le_compat_l. apply CR_of_Q_le. discriminate. intro abs. apply (CRmult_lt_compat_l (CR_of_Q R (Z.pos x #1))) in abs. rewrite CRmult_1_r, <- CRmult_assoc, <- CR_of_Q_mult in abs. rewrite (CR_of_Q_morph R ((Z.pos x # 1) * (1 # x))%Q 1%Q) in abs. - rewrite CR_of_Q_one, CRmult_1_l in abs. + rewrite CRmult_1_l in abs. apply (CRlt_asym _ _ abs), (CRlt_trans _ (1 + CRabs R a)). 2: exact c. rewrite <- CRplus_0_l, <- CRplus_assoc. apply CRplus_lt_compat_r. rewrite CRplus_0_r. apply CRzero_lt_one. @@ -310,7 +305,7 @@ Lemma CR_cv_const : forall {R : ConstructiveReals} (a : CRcarrier R), Proof. intros a p. exists O. intros. unfold CRminus. rewrite CRplus_opp_r. - rewrite CRabs_right. rewrite <- CR_of_Q_zero. + rewrite CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. Qed. @@ -633,7 +628,7 @@ Lemma CR_double : forall {R : ConstructiveReals} (x:CRcarrier R), CR_of_Q R 2 * x == x + x. Proof. intros R x. rewrite (CR_of_Q_morph R 2 (1+1)). - 2: reflexivity. rewrite CR_of_Q_plus, CR_of_Q_one. + 2: reflexivity. rewrite CR_of_Q_plus. rewrite CRmult_plus_distr_r, CRmult_1_l. reflexivity. Qed. @@ -641,7 +636,7 @@ Lemma GeoCvZero : forall {R : ConstructiveReals}, CR_cv R (fun n:nat => CRpow (CR_of_Q R (1#2)) n) 0. Proof. intro R. assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n). - { induction n. unfold INR; simpl. rewrite CR_of_Q_zero. + { induction n. unfold INR; simpl. apply CRzero_lt_one. unfold INR. fold (1+n)%nat. rewrite Nat2Z.inj_add. rewrite (CR_of_Q_morph R _ ((Z.of_nat 1 # 1) + (Z.of_nat n #1))). @@ -651,29 +646,29 @@ Proof. with (CR_of_Q R 2 * CRpow (CR_of_Q R 2) n). 2: reflexivity. rewrite CR_double. apply CRplus_le_lt_compat. - 2: exact IHn. simpl. rewrite CR_of_Q_one. - apply pow_R1_Rle. rewrite <- CR_of_Q_one. apply CR_of_Q_le. discriminate. } + 2: exact IHn. simpl. + apply pow_R1_Rle. apply CR_of_Q_le. discriminate. } intros p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0. rewrite CRplus_0_r. rewrite CRabs_right. - 2: apply pow_le; rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate. + 2: apply pow_le; apply CR_of_Q_le; discriminate. apply CRlt_asym. apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos p # 1))). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. rewrite <- CR_of_Q_mult. + apply CR_of_Q_lt. reflexivity. rewrite <- CR_of_Q_mult. rewrite (CR_of_Q_morph R ((Z.pos p # 1) * (1 # p)) 1). 2: unfold Qmult, Qeq, Qnum, Qden; ring_simplify; reflexivity. apply (CRmult_lt_reg_r (CRpow (CR_of_Q R 2) i)). - apply pow_lt. simpl. rewrite <- CR_of_Q_zero. + apply pow_lt. simpl. apply CR_of_Q_lt. reflexivity. rewrite CRmult_assoc. rewrite pow_mult. rewrite (pow_proper (CR_of_Q R (1 # 2) * CR_of_Q R 2) 1), pow_one. - rewrite CRmult_1_r, CR_of_Q_one, CRmult_1_l. + rewrite CRmult_1_r, CRmult_1_l. apply (CRle_lt_trans _ (INR i)). 2: exact (H i). clear H. apply CR_of_Q_le. unfold Qle,Qnum,Qden. do 2 rewrite Z.mul_1_r. rewrite <- positive_nat_Z. apply Nat2Z.inj_le, H0. rewrite <- CR_of_Q_mult. setoid_replace ((1#2)*2)%Q with 1%Q. - apply CR_of_Q_one. reflexivity. + reflexivity. reflexivity. Qed. Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat), @@ -681,9 +676,9 @@ Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat), Proof. induction n. - unfold CRsum, CRpow. simpl (1%ConstructiveReals). - unfold CRminus. rewrite (CR_of_Q_morph R _ (1+1)). - rewrite CR_of_Q_plus, CR_of_Q_one, CRplus_assoc. - rewrite CRplus_opp_r, CRplus_0_r. reflexivity. reflexivity. + unfold CRminus. rewrite (CR_of_Q_plus R 1 1). + rewrite CRplus_assoc. + rewrite CRplus_opp_r, CRplus_0_r. reflexivity. - setoid_replace (CRsum (CRpow (CR_of_Q R (1 # 2))) (S n)) with (CRsum (CRpow (CR_of_Q R (1 # 2))) n + CRpow (CR_of_Q R (1 # 2)) (S n)). 2: reflexivity. @@ -701,7 +696,7 @@ Proof. 2: reflexivity. rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. - rewrite CR_of_Q_one. apply CRmult_1_l. reflexivity. + apply CRmult_1_l. reflexivity. Qed. Lemma GeoHalfBelowTwo : forall {R : ConstructiveReals} (n:nat), @@ -710,7 +705,7 @@ Proof. intros. rewrite <- (CRplus_0_r (CR_of_Q R 2)), GeoFiniteSum. apply CRplus_lt_compat_l. rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. - apply pow_lt. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply pow_lt. apply CR_of_Q_lt. reflexivity. Qed. Lemma GeoHalfTwo : forall {R : ConstructiveReals}, @@ -720,35 +715,35 @@ Proof. apply (CR_cv_eq _ (fun n => CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) n)). - intro n. rewrite GeoFiniteSum. reflexivity. - assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n). - { induction n. unfold INR; simpl. rewrite CR_of_Q_zero. + { induction n. unfold INR; simpl. apply CRzero_lt_one. apply (CRlt_le_trans _ (CRpow (CR_of_Q R 2) n + 1)). unfold INR. rewrite Nat2Z.inj_succ, <- Z.add_1_l. rewrite (CR_of_Q_morph R _ (1 + (Z.of_nat n #1))). 2: symmetry; apply Qinv_plus_distr. rewrite CR_of_Q_plus. - rewrite CRplus_comm. rewrite CR_of_Q_one. + rewrite CRplus_comm. apply CRplus_lt_compat_r, IHn. setoid_replace (CRpow (CR_of_Q R 2) (S n)) with (CRpow (CR_of_Q R 2) n + CRpow (CR_of_Q R 2) n). apply CRplus_le_compat. apply CRle_refl. - apply pow_R1_Rle. rewrite <- CR_of_Q_one. apply CR_of_Q_le. discriminate. + apply pow_R1_Rle. apply CR_of_Q_le. discriminate. rewrite <- CR_double. reflexivity. } intros n. exists (Pos.to_nat n). intros. setoid_replace (CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) i - CR_of_Q R 2) with (- CRpow (CR_of_Q R (1 # 2)) i). rewrite CRabs_opp. rewrite CRabs_right. assert (0 < CR_of_Q R 2). - { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. } + { apply CR_of_Q_lt. reflexivity. } rewrite (pow_proper _ (CRinv R (CR_of_Q R 2) (inr H1))). rewrite pow_inv. apply CRlt_asym. apply (CRmult_lt_reg_l (CRpow (CR_of_Q R 2) i)). apply pow_lt, H1. rewrite CRinv_r. apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n#1))). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply CR_of_Q_lt. reflexivity. rewrite CRmult_1_l, CRmult_assoc. rewrite <- CR_of_Q_mult. rewrite (CR_of_Q_morph R ((1 # n) * (Z.pos n # 1)) 1). 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. apply (CRle_lt_trans _ (INR i)). + rewrite CRmult_1_r. apply (CRle_lt_trans _ (INR i)). 2: apply H. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. destruct i. exfalso. inversion H0. pose proof (Pos2Nat.is_pos n). @@ -758,8 +753,8 @@ Proof. apply (CRmult_eq_reg_l (CR_of_Q R 2)). right. exact H1. rewrite CRinv_r. rewrite <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. - apply CR_of_Q_one. reflexivity. - apply CRlt_asym, pow_lt. rewrite <- CR_of_Q_zero. + reflexivity. reflexivity. + apply CRlt_asym, pow_lt. apply CR_of_Q_lt. reflexivity. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. @@ -929,5 +924,5 @@ Proof. intros n. exists (Pos.to_nat n). intros. unfold CRminus. simpl. rewrite CRopp_involutive, CRplus_opp_l. rewrite CRabs_right. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. apply CRle_refl. + apply CR_of_Q_le. discriminate. apply CRle_refl. Qed. diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v index d91fd1183a..019428a5b0 100644 --- a/theories/Reals/Abstract/ConstructiveReals.v +++ b/theories/Reals/Abstract/ConstructiveReals.v @@ -101,9 +101,15 @@ Structure ConstructiveReals : Type := CRltDisjunctEpsilon : forall a b c d : CRcarrier, (CRltProp a b \/ CRltProp c d) -> CRlt a b + CRlt c d; - (* Constants *) - CRzero : CRcarrier; - CRone : CRcarrier; + (* The initial field morphism (in characteristic zero). + The abstract definition by iteration of addition is + probably the slowest. Let each instance implement + a faster (and often simpler) version. *) + CR_of_Q : Q -> CRcarrier; + CR_of_Q_lt : forall q r : Q, + Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r); + lt_CR_of_Q : forall q r : Q, + CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r; (* Addition and multiplication *) CRplus : CRcarrier -> CRcarrier -> CRcarrier; @@ -111,19 +117,22 @@ Structure ConstructiveReals : Type := stronger than Prop-existence of opposite *) CRmult : CRcarrier -> CRcarrier -> CRcarrier; - CRisRing : ring_theory CRzero CRone CRplus CRmult + CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r)) + (CRplus (CR_of_Q q) (CR_of_Q r)); + CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r)) + (CRmult (CR_of_Q q) (CR_of_Q r)); + CRisRing : ring_theory (CR_of_Q 0) (CR_of_Q 1) CRplus CRmult (fun x y => CRplus x (CRopp y)) CRopp CReq; CRisRingExt : ring_eq_ext CRplus CRmult CRopp CReq; (* Compatibility with order *) - CRzero_lt_one : CRlt CRzero CRone; (* 0 # 1 would only allow 0 < 1 because - of Fmult_lt_0_compat so request 0 < 1 directly. *) + CRzero_lt_one : CRlt (CR_of_Q 0) (CR_of_Q 1); CRplus_lt_compat_l : forall r r1 r2 : CRcarrier, CRlt r1 r2 -> CRlt (CRplus r r1) (CRplus r r2); CRplus_lt_reg_l : forall r r1 r2 : CRcarrier, CRlt (CRplus r r1) (CRplus r r2) -> CRlt r1 r2; CRmult_lt_0_compat : forall x y : CRcarrier, - CRlt CRzero x -> CRlt CRzero y -> CRlt CRzero (CRmult x y); + CRlt (CR_of_Q 0) x -> CRlt (CR_of_Q 0) y -> CRlt (CR_of_Q 0) (CRmult x y); (* A constructive total inverse function on F would need to be continuous, which is impossible because we cannot connect plus and minus infinities. @@ -132,26 +141,11 @@ Structure ConstructiveReals : Type := To implement Finv by Cauchy sequences we need orderAppart, ~orderEq is not enough. *) - CRinv : forall x : CRcarrier, CRapart x CRzero -> CRcarrier; - CRinv_l : forall (r:CRcarrier) (rnz : CRapart r CRzero), - CReq (CRmult (CRinv r rnz) r) CRone; - CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r CRzero), - CRlt CRzero r -> CRlt CRzero (CRinv r rnz); - - (* The initial field morphism (in characteristic zero). - The abstract definition by iteration of addition is - probably the slowest. Let each instance implement - a faster (and often simpler) version. *) - CR_of_Q : Q -> CRcarrier; - CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r)) - (CRplus (CR_of_Q q) (CR_of_Q r)); - CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r)) - (CRmult (CR_of_Q q) (CR_of_Q r)); - CR_of_Q_one : CReq (CR_of_Q 1) CRone; - CR_of_Q_lt : forall q r : Q, - Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r); - lt_CR_of_Q : forall q r : Q, - CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r; + CRinv : forall x : CRcarrier, CRapart x (CR_of_Q 0) -> CRcarrier; + CRinv_l : forall (r:CRcarrier) (rnz : CRapart r (CR_of_Q 0)), + CReq (CRmult (CRinv r rnz) r) (CR_of_Q 1); + CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r (CR_of_Q 0)), + CRlt (CR_of_Q 0) r -> CRlt (CR_of_Q 0) (CRinv r rnz); (* This function is very fast in both the Cauchy and Dedekind instances, because this rational number q is almost what @@ -213,8 +207,17 @@ Notation "x <= y <= z" := (CRle _ x y /\ CRle _ y z) : ConstructiveReals. Notation "x < y < z" := (prod (CRlt _ x y) (CRlt _ y z)) : ConstructiveReals. Notation "x == y" := (CReq _ x y) : ConstructiveReals. Notation "x ≶ y" := (CRapart _ x y) (at level 70, no associativity) : ConstructiveReals. -Notation "0" := (CRzero _) : ConstructiveReals. -Notation "1" := (CRone _) : ConstructiveReals. +Notation "0" := (CR_of_Q _ 0) : ConstructiveReals. +Notation "1" := (CR_of_Q _ 1) : ConstructiveReals. +Notation "2" := (CR_of_Q _ 2) : ConstructiveReals. +Notation "3" := (CR_of_Q _ 3) : ConstructiveReals. +Notation "4" := (CR_of_Q _ 4) : ConstructiveReals. +Notation "5" := (CR_of_Q _ 5) : ConstructiveReals. +Notation "6" := (CR_of_Q _ 6) : ConstructiveReals. +Notation "7" := (CR_of_Q _ 7) : ConstructiveReals. +Notation "8" := (CR_of_Q _ 8) : ConstructiveReals. +Notation "9" := (CR_of_Q _ 9) : ConstructiveReals. +Notation "10" := (CR_of_Q _ 10) : ConstructiveReals. Notation "x + y" := (CRplus _ x y) : ConstructiveReals. Notation "- x" := (CRopp _ x) : ConstructiveReals. Notation "x - y" := (CRminus _ x y) : ConstructiveReals. @@ -567,7 +570,7 @@ Lemma CRopp_involutive : forall {R : ConstructiveReals} (r : CRcarrier R), - - r == r. Proof. intros. apply (CRplus_eq_reg_l (CRopp R r)). - transitivity (CRzero R). apply CRisRing. + transitivity (CR_of_Q R 0). apply CRisRing. apply CReq_sym. transitivity (r + - r). apply CRisRing. apply CRisRing. Qed. @@ -578,7 +581,7 @@ Lemma CRopp_gt_lt_contravar Proof. intros. apply (CRplus_lt_reg_l R r1). destruct (CRisRing R). - apply (CRle_lt_trans _ (CRzero R)). apply Ropp_def. + apply (CRle_lt_trans _ 0). apply Ropp_def. apply (CRplus_lt_compat_l R (CRopp R r2)) in H. apply (CRle_lt_trans _ (CRplus R (CRopp R r2) r2)). apply (CRle_trans _ (CRplus R r2 (CRopp R r2))). @@ -611,13 +614,13 @@ Lemma CRopp_plus_distr : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), Proof. intros. destruct (CRisRing R), (CRisRingExt R). apply (CRplus_eq_reg_l (CRplus R r1 r2)). - transitivity (CRzero R). apply Ropp_def. + transitivity (CR_of_Q R 0). apply Ropp_def. transitivity (r2 + r1 + (-r1 + -r2)). transitivity (r2 + (r1 + (-r1 + -r2))). transitivity (r2 + - r2). apply CReq_sym. apply Ropp_def. apply Radd_ext. apply CReq_refl. - transitivity (CRzero R + - r2). + transitivity (0 + - r2). apply CReq_sym, Radd_0_l. transitivity (r1 + - r1 + - r2). apply Radd_ext. 2: apply CReq_refl. apply CReq_sym, Ropp_def. @@ -701,7 +704,7 @@ Lemma CRopp_mult_distr_r : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), - (r1 * r2) == r1 * (- r2). Proof. intros. apply (CRplus_eq_reg_l (CRmult R r1 r2)). - destruct (CRisRing R). transitivity (CRzero R). apply Ropp_def. + destruct (CRisRing R). transitivity (CR_of_Q R 0). apply Ropp_def. transitivity (r1 * (r2 + - r2)). 2: apply CRmult_plus_distr_l. transitivity (r1 * 0). @@ -725,7 +728,7 @@ Lemma CRmult_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R 0 < r -> r1 < r2 -> r1 * r < r2 * r. Proof. intros. apply (CRplus_lt_reg_r (CRopp R (CRmult R r1 r))). - apply (CRle_lt_trans _ (CRzero R)). + apply (CRle_lt_trans _ 0). apply (Ropp_def (CRisRing R)). apply (CRlt_le_trans _ (CRplus R (CRmult R r2 r) (CRmult R (CRopp R r1) r))). apply (CRlt_le_trans _ (CRmult R (CRplus R r2 (CRopp R r1)) r)). @@ -734,7 +737,7 @@ Proof. apply (CRle_lt_trans _ r1). apply (Radd_0_l (CRisRing R)). apply (CRlt_le_trans _ r2 _ H0). apply (CRle_trans _ (CRplus R r2 (CRplus R (CRopp R r1) r1))). - apply (CRle_trans _ (CRplus R r2 (CRzero R))). + apply (CRle_trans _ (CRplus R r2 0)). destruct (CRplus_0_r r2). exact H1. apply CRplus_le_compat_l. destruct (CRplus_opp_l r1). exact H1. destruct (Radd_assoc (CRisRing R) r2 (CRopp R r1) r1). exact H2. @@ -752,7 +755,7 @@ Proof. Qed. Lemma CRinv_r : forall {R : ConstructiveReals} (r:CRcarrier R) - (rnz : r ≶ (CRzero R)), + (rnz : r ≶ 0), r * (/ r) rnz == 1. Proof. intros. transitivity ((/ r) rnz * r). @@ -765,7 +768,7 @@ Proof. intros. apply (CRmult_lt_compat_r ((/ r) (inr H))) in H0. 2: apply CRinv_0_lt_compat, H. apply (CRle_lt_trans _ ((r1 * r) * ((/ r) (inr H)))). - - clear H0. apply (CRle_trans _ (CRmult R r1 (CRone R))). + - clear H0. apply (CRle_trans _ (CRmult R r1 1)). destruct (CRmult_1_r r1). exact H0. apply (CRle_trans _ (CRmult R r1 (CRmult R r ((/ r) (inr H))))). destruct (Rmul_ext (CRisRingExt R) r1 r1 (CReq_refl r1) @@ -779,7 +782,7 @@ Proof. apply (CRle_trans _ (r2 * (r * ((/ r) (inr H))))). destruct (Rmul_assoc (CRisRing R) r2 r ((/ r) (inr H))). exact H0. destruct (Rmul_ext (CRisRingExt R) r2 r2 (CReq_refl r2) - (r * ((/ r) (inr H))) (CRone R)). + (r * ((/ r) (inr H))) 1). apply CRinv_r. exact H1. Qed. @@ -829,7 +832,7 @@ Proof. apply CRmult_lt_compat_r. 2: exact abs. apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r). apply (Radd_0_l (CRisRing R)). - apply (CRlt_le_trans _ (CRzero R) _ c). + apply (CRlt_le_trans _ 0 _ c). apply CRplus_opp_l. + intro abs. apply H0. apply CRopp_lt_cancel. apply (CRle_lt_trans _ (CRmult R r2 (CRopp R r))). @@ -839,7 +842,7 @@ Proof. apply CRmult_lt_compat_r. 2: exact abs. apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r). apply (Radd_0_l (CRisRing R)). - apply (CRlt_le_trans _ (CRzero R) _ c). + apply (CRlt_le_trans _ 0 _ c). apply CRplus_opp_l. Qed. @@ -920,31 +923,21 @@ Proof. intros R x y H. apply CR_of_Q_morph; assumption. Qed. -Lemma CR_of_Q_zero : forall {R : ConstructiveReals}, - CR_of_Q R 0 == 0. -Proof. - intros. apply CRzero_double. - transitivity (CR_of_Q R (0+0)). apply CR_of_Q_morph. - reflexivity. apply CR_of_Q_plus. -Qed. - Lemma CR_of_Q_opp : forall {R : ConstructiveReals} (q : Q), CR_of_Q R (-q) == - CR_of_Q R q. Proof. intros. apply (CRplus_eq_reg_l (CR_of_Q R q)). - transitivity (CRzero R). + transitivity (CR_of_Q R 0). transitivity (CR_of_Q R (q-q)). apply CReq_sym, CR_of_Q_plus. - transitivity (CR_of_Q R 0). - apply CR_of_Q_morph. ring. apply CR_of_Q_zero. + apply CR_of_Q_morph. ring. apply CReq_sym. apply (CRisRing R). Qed. Lemma CR_of_Q_pos : forall {R : ConstructiveReals} (q:Q), Qlt 0 q -> 0 < CR_of_Q R q. Proof. - intros. apply (CRle_lt_trans _ (CR_of_Q R 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. exact H. + intros. apply CR_of_Q_lt. exact H. Qed. Lemma CR_of_Q_inv : forall {R : ConstructiveReals} (q : Q) (qPos : Qlt 0 q), @@ -954,7 +947,7 @@ Proof. intros. apply (CRmult_eq_reg_l (CR_of_Q R q)). right. apply CR_of_Q_pos, qPos. - rewrite CRinv_r, <- CR_of_Q_mult, <- CR_of_Q_one. + rewrite CRinv_r, <- CR_of_Q_mult. apply CR_of_Q_morph. field. intro abs. rewrite abs in qPos. exact (Qlt_irrefl 0 qPos). Qed. @@ -969,7 +962,7 @@ Proof. destruct (CR_archimedean R (b * ((/ -(a*b)) (inr epsPos)))) as [n maj]. assert (0 < CR_of_Q R (Z.pos n #1)) as nPos. - { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. } + { apply CR_of_Q_lt. reflexivity. } assert (b * (/ CR_of_Q R (Z.pos n #1)) (inr nPos) < -(a*b)). { apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n #1))). apply nPos. rewrite <- (Rmul_assoc (CRisRing R)), CRinv_l, CRmult_1_r. @@ -1082,7 +1075,7 @@ Definition CRfloor {R : ConstructiveReals} (a : CRcarrier R) Proof. destruct (CR_Q_dense R (a - CR_of_Q R (1#2)) a) as [q qmaj]. - apply (CRlt_le_trans _ (a-0)). apply CRplus_lt_compat_l. - apply CRopp_gt_lt_contravar. rewrite <- CR_of_Q_zero. + apply CRopp_gt_lt_contravar. apply CR_of_Q_lt. reflexivity. unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl. - exists (Qfloor q). destruct qmaj. split. diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v index bc44668e2f..cf302dc847 100644 --- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v +++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v @@ -163,9 +163,8 @@ Lemma CRmorph_zero : forall {R1 R2 : ConstructiveReals} CRmorph f 0 == 0. Proof. intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 0))). - apply CRmorph_proper. apply CReq_sym, CR_of_Q_zero. - apply (CReq_trans _ (CR_of_Q R2 0)). - apply CRmorph_rat. apply CR_of_Q_zero. + apply CRmorph_proper. reflexivity. + apply CRmorph_rat. Qed. Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals} @@ -173,9 +172,8 @@ Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals} CRmorph f 1 == 1. Proof. intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 1))). - apply CRmorph_proper. apply CReq_sym, CR_of_Q_one. - apply (CReq_trans _ (CR_of_Q R2 1)). - apply CRmorph_rat. apply CR_of_Q_one. + apply CRmorph_proper. reflexivity. + apply CRmorph_rat. Qed. Lemma CRmorph_opp : forall {R1 R2 : ConstructiveReals} @@ -228,9 +226,9 @@ Lemma CRplus_pos_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Qlt 0 q -> CRlt R x (CRplus R x (CR_of_Q R q)). Proof. intros. - apply (CRle_lt_trans _ (CRplus R x (CRzero R))). apply CRplus_0_r. + apply (CRle_lt_trans _ (CRplus R x 0)). apply CRplus_0_r. apply CRplus_lt_compat_l. - apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CR_of_Q_zero. + apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CRle_refl. apply CR_of_Q_lt. exact H. Defined. @@ -238,10 +236,10 @@ Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x. Proof. intros. - apply (CRlt_le_trans _ (CRplus R x (CRzero R))). 2: apply CRplus_0_r. + apply (CRlt_le_trans _ (CRplus R x 0)). 2: apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRlt_le_trans _ (CR_of_Q R 0)). - apply CR_of_Q_lt. exact H. apply CR_of_Q_zero. + apply CR_of_Q_lt. exact H. apply CRle_refl. Qed. Lemma CRmorph_plus_rat : forall {R1 R2 : ConstructiveReals} @@ -276,7 +274,7 @@ Proof. destruct (CRisRing R1). apply (CRle_trans _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))). - apply (CRle_trans _ (CRplus R1 x (CRzero R1))). + apply (CRle_trans _ (CRplus R1 x 0)). destruct (CRplus_0_r x). exact H. apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H. destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))). @@ -294,7 +292,7 @@ Proof. _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))). destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))). exact H0. - apply (CRle_trans _ (CRplus R1 x (CRzero R1))). + apply (CRle_trans _ (CRplus R1 x 0)). apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H1. destruct (CRplus_0_r x). exact H1. apply (CRlt_le_trans _ (CR_of_Q R1 (r-q))). @@ -379,12 +377,12 @@ Proof. apply CRmorph_proper. destruct (CRisRing R1). apply (CReq_trans _ (CRplus R1 x (CRplus R1 y (CRopp R1 y)))). apply CReq_sym, Radd_assoc. - apply (CReq_trans _ (CRplus R1 x (CRzero R1))). 2: apply CRplus_0_r. + apply (CReq_trans _ (CRplus R1 x 0)). 2: apply CRplus_0_r. destruct (CRisRingExt R1). apply Radd_ext. apply CReq_refl. apply Ropp_def. apply (CRplus_lt_reg_r (CRmorph f y)). apply (CRlt_le_trans _ _ _ abs). clear abs. - apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) (CRzero R2))). + apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) 0)). destruct (CRplus_0_r (CRmorph f (CRplus R1 x y))). exact H. apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) (CRplus R2 (CRmorph f (CRopp R1 y)) (CRmorph f y)))). @@ -407,29 +405,26 @@ Lemma CRmorph_mult_pos : forall {R1 R2 : ConstructiveReals} Proof. induction n. - simpl. destruct (CRisRingExt R1). - apply (CReq_trans _ (CRzero R2)). - + apply (CReq_trans _ (CRmorph f (CRzero R1))). + apply (CReq_trans _ 0). + + apply (CReq_trans _ (CRmorph f 0)). 2: apply CRmorph_zero. apply CRmorph_proper. - apply (CReq_trans _ (CRmult R1 x (CRzero R1))). - 2: apply CRmult_0_r. apply Rmul_ext. apply CReq_refl. apply CR_of_Q_zero. - + apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRzero R2))). + apply (CReq_trans _ (CRmult R1 x 0)). + 2: apply CRmult_0_r. apply Rmul_ext. apply CReq_refl. reflexivity. + + apply (CReq_trans _ (CRmult R2 (CRmorph f x) 0)). apply CReq_sym, CRmult_0_r. destruct (CRisRingExt R2). - apply Rmul_ext0. apply CReq_refl. apply CReq_sym, CR_of_Q_zero. + apply Rmul_ext0. apply CReq_refl. reflexivity. - destruct (CRisRingExt R1), (CRisRingExt R2). - apply (CReq_trans - _ (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))). + transitivity (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))). apply CRmorph_proper. - apply (CReq_trans - _ (CRmult R1 x (CRplus R1 (CRone R1) (CR_of_Q R1 (Z.of_nat n # 1))))). - apply Rmul_ext. apply CReq_refl. - apply (CReq_trans _ (CR_of_Q R1 (1 + (Z.of_nat n # 1)))). + transitivity (CRmult R1 x (CRplus R1 1 (CR_of_Q R1 (Z.of_nat n # 1)))). + apply Rmul_ext. reflexivity. + transitivity (CR_of_Q R1 (1 + (Z.of_nat n # 1))). apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity. - apply (CReq_trans _ (CRplus R1 (CR_of_Q R1 1) (CR_of_Q R1 (Z.of_nat n # 1)))). - apply CR_of_Q_plus. apply Radd_ext. apply CR_of_Q_one. apply CReq_refl. - apply (CReq_trans _ (CRplus R1 (CRmult R1 x (CRone R1)) - (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))). - apply CRmult_plus_distr_l. apply Radd_ext. apply CRmult_1_r. apply CReq_refl. + rewrite CR_of_Q_plus. reflexivity. + transitivity (CRplus R1 (CRmult R1 x 1) + (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))). + apply CRmult_plus_distr_l. apply Radd_ext. apply CRmult_1_r. reflexivity. apply (CReq_trans _ (CRplus R2 (CRmorph f x) (CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))). @@ -439,16 +434,16 @@ Proof. (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))). apply Radd_ext0. apply CReq_refl. exact IHn. apply (CReq_trans - _ (CRmult R2 (CRmorph f x) (CRplus R2 (CRone R2) (CR_of_Q R2 (Z.of_nat n # 1))))). + _ (CRmult R2 (CRmorph f x) (CRplus R2 1 (CR_of_Q R2 (Z.of_nat n # 1))))). apply (CReq_trans - _ (CRplus R2 (CRmult R2 (CRmorph f x) (CRone R2)) + _ (CRplus R2 (CRmult R2 (CRmorph f x) 1) (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))). apply Radd_ext0. 2: apply CReq_refl. apply CReq_sym, CRmult_1_r. apply CReq_sym, CRmult_plus_distr_l. apply Rmul_ext0. apply CReq_refl. apply (CReq_trans _ (CR_of_Q R2 (1 + (Z.of_nat n # 1)))). apply (CReq_trans _ (CRplus R2 (CR_of_Q R2 1) (CR_of_Q R2 (Z.of_nat n # 1)))). - apply Radd_ext0. apply CReq_sym, CR_of_Q_one. apply CReq_refl. + apply Radd_ext0. reflexivity. reflexivity. apply CReq_sym, CR_of_Q_plus. apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity. @@ -501,7 +496,7 @@ Lemma CRmorph_mult_inv : forall {R1 R2 : ConstructiveReals} Proof. intros. apply (CRmult_eq_reg_r (CR_of_Q R2 (Z.pos p # 1))). left. apply (CRle_lt_trans _ (CR_of_Q R2 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply CRle_refl. apply CR_of_Q_lt. reflexivity. apply (CReq_trans _ (CRmorph f x)). - apply (CReq_trans _ (CRmorph f (CRmult R1 (CRmult R1 x (CR_of_Q R1 (1 # p))) @@ -511,22 +506,22 @@ Proof. _ (CRmult R1 x (CRmult R1 (CR_of_Q R1 (1 # p)) (CR_of_Q R1 (Z.pos p # 1))))). destruct (CRisRing R1). apply CReq_sym, Rmul_assoc. - apply (CReq_trans _ (CRmult R1 x (CRone R1))). + apply (CReq_trans _ (CRmult R1 x 1)). apply (Rmul_ext (CRisRingExt R1)). apply CReq_refl. apply (CReq_trans _ (CR_of_Q R1 ((1#p) * (Z.pos p # 1)))). apply CReq_sym, CR_of_Q_mult. apply (CReq_trans _ (CR_of_Q R1 1)). - apply CR_of_Q_morph. reflexivity. apply CR_of_Q_one. + apply CR_of_Q_morph. reflexivity. reflexivity. apply CRmult_1_r. - apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRmult R2 (CR_of_Q R2 (1 # p)) (CR_of_Q R2 (Z.pos p # 1))))). 2: apply (Rmul_assoc (CRisRing R2)). - apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRone R2))). + apply (CReq_trans _ (CRmult R2 (CRmorph f x) 1)). apply CReq_sym, CRmult_1_r. apply (Rmul_ext (CRisRingExt R2)). apply CReq_refl. apply (CReq_trans _ (CR_of_Q R2 1)). - apply CReq_sym, CR_of_Q_one. + reflexivity. apply (CReq_trans _ (CR_of_Q R2 ((1#p)*(Z.pos p # 1)))). apply CR_of_Q_morph. reflexivity. apply CR_of_Q_mult. Qed. @@ -571,7 +566,7 @@ Qed. Lemma CRmorph_mult_pos_pos_le : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), - CRlt R1 (CRzero R1) y + CRlt R1 0 y -> CRmult R2 (CRmorph f x) (CRmorph f y) <= CRmorph f (CRmult R1 x y). Proof. @@ -590,20 +585,20 @@ Proof. apply Qlt_minus_iff in H1. rewrite H4 in H1. inversion H1. } destruct (CR_Q_dense R1 (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A)))) x) as [s [H4 H5]]. - - apply (CRlt_le_trans _ (CRplus R1 x (CRzero R1))). + - apply (CRlt_le_trans _ (CRplus R1 x 0)). 2: apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l R1 (CR_of_Q R1 ((r-q) * (1#A)))). - apply (CRle_lt_trans _ (CRzero R1)). + apply (CRle_lt_trans _ 0). apply (CRle_trans _ (CR_of_Q R1 ((r-q)*(1#A) + (q-r)*(1#A)))). destruct (CR_of_Q_plus R1 ((r-q)*(1#A)) ((q-r)*(1#A))). exact H0. apply (CRle_trans _ (CR_of_Q R1 0)). - 2: destruct (@CR_of_Q_zero R1); exact H4. + 2: apply CRle_refl. intro H4. apply lt_CR_of_Q in H4. ring_simplify in H4. inversion H4. apply (CRlt_le_trans _ (CR_of_Q R1 ((r - q) * (1 # A)))). 2: apply CRplus_0_r. apply (CRle_lt_trans _ (CR_of_Q R1 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. + apply CRle_refl. apply CR_of_Q_lt. rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l. apply Qlt_minus_iff in H1. exact H1. reflexivity. - apply (CRmorph_increasing f) in H4. @@ -637,7 +632,7 @@ Proof. apply (CRlt_le_trans _ (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))). apply (CRmult_lt_reg_l (CR_of_Q R2 (/((r-q)*(1#A))))). - apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero. + apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CRle_refl. apply CR_of_Q_lt, Qinv_lt_0_compat. rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l. apply Qlt_minus_iff in H1. exact H1. reflexivity. @@ -655,24 +650,24 @@ Proof. apply (CRlt_le_trans _ (CRmorph f (CR_of_Q R1 (Z.pos A # 1)))). apply CRmorph_increasing. exact Amaj. destruct (CRmorph_rat f (Z.pos A # 1)). exact H4. - apply (CRle_trans _ (CRmult R2 (CRopp R2 (CRone R2)) (CRmorph f y))). - apply (CRle_trans _ (CRopp R2 (CRmult R2 (CRone R2) (CRmorph f y)))). + apply (CRle_trans _ (CRmult R2 (CRopp R2 1) (CRmorph f y))). + apply (CRle_trans _ (CRopp R2 (CRmult R2 1 (CRmorph f y)))). destruct (Ropp_ext (CRisRingExt R2) (CRmorph f y) - (CRmult R2 (CRone R2) (CRmorph f y))). + (CRmult R2 1 (CRmorph f y))). apply CReq_sym, (Rmul_1_l (CRisRing R2)). exact H4. - destruct (CRopp_mult_distr_l (CRone R2) (CRmorph f y)). exact H4. + destruct (CRopp_mult_distr_l 1 (CRmorph f y)). exact H4. apply (CRle_trans _ (CRmult R2 (CRmult R2 (CR_of_Q R2 (/ ((r - q) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A)))) (CRmorph f y))). apply CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. apply (CRle_trans _ (CR_of_Q R2 ((/ ((r - q) * (1 # A))) * ((q - r) * (1 # A))))). apply (CRle_trans _ (CR_of_Q R2 (-1))). apply (CRle_trans _ (CRopp R2 (CR_of_Q R2 1))). - destruct (Ropp_ext (CRisRingExt R2) (CRone R2) (CR_of_Q R2 1)). - apply CReq_sym, CR_of_Q_one. exact H4. + destruct (Ropp_ext (CRisRingExt R2) 1 (CR_of_Q R2 1)). + reflexivity. exact H4. destruct (@CR_of_Q_opp R2 1). exact H0. destruct (CR_of_Q_morph R2 (-1) (/ ((r - q) * (1 # A)) * ((q - r) * (1 # A)))). field. split. @@ -685,7 +680,7 @@ Proof. (CRmorph f y)). exact H0. apply CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H0. + apply (CRle_trans _ (CRmorph f (CRmult R1 y (CR_of_Q R1 s)))). @@ -696,14 +691,14 @@ Proof. destruct (CRmorph_proper f (CRmult R1 y (CR_of_Q R1 s)) (CRmult R1 (CR_of_Q R1 s) y)). apply (Rmul_comm (CRisRing R1)). exact H4. - + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. Qed. Lemma CRmorph_mult_pos_pos : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), - CRlt R1 (CRzero R1) y + CRlt R1 0 y -> CRmorph f (CRmult R1 x y) == CRmult R2 (CRmorph f x) (CRmorph f y). Proof. @@ -718,10 +713,10 @@ Proof. destruct (CR_archimedean R1 y) as [A Amaj]. destruct (CR_Q_dense R1 x (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A))))) as [s [H4 H5]]. - - apply (CRle_lt_trans _ (CRplus R1 x (CRzero R1))). + - apply (CRle_lt_trans _ (CRplus R1 x 0)). apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRle_lt_trans _ (CR_of_Q R1 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. + apply CRle_refl. apply CR_of_Q_lt. rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l. apply Qlt_minus_iff in H3. exact H3. reflexivity. - apply (CRmorph_increasing f) in H5. @@ -763,14 +758,14 @@ Proof. (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y)))). apply CRplus_le_compat_l, CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H2. apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 r) (CR_of_Q R2 ((q - r))))). apply CRplus_lt_compat_l. * apply (CRmult_lt_reg_l (CR_of_Q R2 (/((q - r) * (1 # A))))). - apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero. + apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CRle_refl. apply CR_of_Q_lt, Qinv_lt_0_compat. rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l. apply Qlt_minus_iff in H3. exact H3. reflexivity. @@ -781,9 +776,9 @@ Proof. exact (proj2 (Rmul_assoc (CRisRing R2) (CR_of_Q R2 (/ ((q - r) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))). - apply (CRle_trans _ (CRmult R2 (CRone R2) (CRmorph f y))). + apply (CRle_trans _ (CRmult R2 1 (CRmorph f y))). apply CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. apply (CRle_trans _ (CR_of_Q R2 ((/ ((q - r) * (1 # A))) * ((q - r) * (1 # A))))). @@ -793,7 +788,7 @@ Proof. field_simplify. reflexivity. split. intro H5. inversion H5. intro H5. apply Qlt_minus_iff in H3. rewrite H5 in H3. inversion H3. exact H2. - destruct (CR_of_Q_one R2). exact H2. + apply CRle_refl. destruct (Rmul_1_l (CRisRing R2) (CRmorph f y)). intro H5. contradiction. apply (CRlt_le_trans _ (CR_of_Q R2 (Z.pos A # 1))). @@ -809,7 +804,7 @@ Proof. * apply (CRle_trans _ (CR_of_Q R2 (r + (q-r)))). exact (proj1 (CR_of_Q_plus R2 r (q-r))). destruct (CR_of_Q_morph R2 (r + (q-r)) q). ring. exact H2. - + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. Qed. @@ -867,10 +862,10 @@ Lemma CRmorph_appart_zero : forall {R1 R2 : ConstructiveReals} CRmorph f x ≶ 0. Proof. intros. destruct app. - - left. apply (CRlt_le_trans _ (CRmorph f (CRzero R1))). + - left. apply (CRlt_le_trans _ (CRmorph f 0)). apply CRmorph_increasing. exact c. exact (proj2 (CRmorph_zero f)). - - right. apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + - right. apply (CRle_lt_trans _ (CRmorph f 0)). exact (proj1 (CRmorph_zero f)). apply CRmorph_increasing. exact c. Defined. @@ -885,7 +880,7 @@ Lemma CRmorph_inv : forall {R1 R2 : ConstructiveReals} Proof. intros. apply (CRmult_eq_reg_r (CRmorph f x)). destruct fxnz. right. exact c. left. exact c. - apply (CReq_trans _ (CRone R2)). + apply (CReq_trans _ 1). 2: apply CReq_sym, CRinv_l. apply (CReq_trans _ (CRmorph f (CRmult R1 ((/ x) xnz) x))). apply CReq_sym, CRmorph_mult. @@ -915,11 +910,11 @@ Proof. - simpl. unfold INR. rewrite (CRmorph_proper f _ (1 + CR_of_Q R1 (Z.of_nat n # 1))). rewrite CRmorph_plus. unfold INR in IHn. - rewrite IHn. rewrite CRmorph_one, <- CR_of_Q_one, <- CR_of_Q_plus. + rewrite IHn. rewrite CRmorph_one, <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity. - rewrite <- CR_of_Q_one, <- CR_of_Q_plus. + rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity. @@ -1047,7 +1042,7 @@ Proof. apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. exact H0. destruct i. inversion H0. pose proof (Pos2Nat.is_pos p). rewrite H2 in H1. inversion H1. discriminate. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. rewrite CRplus_0_r. reflexivity. } pose proof (CR_cv_open_above _ _ _ H0 H) as [n nmaj]. apply (CRle_lt_trans _ (CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in diff --git a/theories/Reals/Abstract/ConstructiveSum.v b/theories/Reals/Abstract/ConstructiveSum.v index 11c8e5d8a2..3be03bf615 100644 --- a/theories/Reals/Abstract/ConstructiveSum.v +++ b/theories/Reals/Abstract/ConstructiveSum.v @@ -60,11 +60,11 @@ Lemma sum_const : forall {R : ConstructiveReals} (a : CRcarrier R) (n : nat), CRsum (fun _ => a) n == a * INR (S n). Proof. induction n. - - unfold INR. simpl. rewrite CR_of_Q_one, CRmult_1_r. reflexivity. + - unfold INR. simpl. rewrite CRmult_1_r. reflexivity. - simpl. rewrite IHn. unfold INR. replace (Z.of_nat (S (S n))) with (Z.of_nat (S n) + 1)%Z. rewrite <- Qinv_plus_distr, CR_of_Q_plus, CRmult_plus_distr_l. - apply CRplus_morph. reflexivity. rewrite CR_of_Q_one, CRmult_1_r. reflexivity. + apply CRplus_morph. reflexivity. rewrite CRmult_1_r. reflexivity. replace 1%Z with (Z.of_nat 1). rewrite <- Nat2Z.inj_add. apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity. Qed. diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index be844c413a..754f9be5fe 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -309,12 +309,11 @@ Definition CRealConstructive : ConstructiveReals := Build_ConstructiveReals CReal CRealLt CRealLtIsLinear CRealLtProp CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon - (inject_Q 0) (inject_Q 1) + inject_Q inject_Q_lt lt_inject_Q CReal_plus CReal_opp CReal_mult + inject_Q_plus inject_Q_mult CReal_isRing CReal_isRingExt CRealLt_0_1 CReal_plus_lt_compat_l CReal_plus_lt_reg_l CReal_mult_lt_0_compat CReal_inv CReal_inv_l CReal_inv_0_lt_compat - inject_Q inject_Q_plus inject_Q_mult - inject_Q_one inject_Q_lt lt_inject_Q CRealQ_dense Rup_pos CReal_abs CRealAbsLUB CRealComplete. diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v index 373654e6db..390b39bab1 100644 --- a/user-contrib/Ltac2/Notations.v +++ b/user-contrib/Ltac2/Notations.v @@ -146,7 +146,7 @@ match ev with end. Ltac2 intros0 ev p := - Control.enter (fun () => Std.intros false p). + Control.enter (fun () => Std.intros ev p). Ltac2 Notation "intros" p(intropatterns) := intros0 false p. Ltac2 Notation intros := intros. diff --git a/vernac/classes.ml b/vernac/classes.ml index eb735b7cdf..55af2e1a7d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,8 +313,8 @@ let instance_hook info global ?hook cst = let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs + let scope = Declare.Global Declare.ImportDefaultBehavior in + let kn = Declare.declare_definition ~name ~kind ~scope ~impargs ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in instance_hook info global ?hook kn @@ -325,7 +325,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma, entry = DeclareDef.prepare_parameter ~poly sigma ~udecl ~types:termtype in + let sigma, entry = Declare.prepare_parameter ~poly sigma ~udecl ~types:termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); @@ -334,7 +334,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst instance_hook pri global cst let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype = - let hook { DeclareDef.Hook.S.scope; dref; _ } = + let hook { Declare.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in let pri = intern_info pri in let env = Global.env () in @@ -342,9 +342,9 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst) in let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in - let hook = DeclareDef.Hook.make hook in + let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in - let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in + let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in let _ : DeclareObl.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () @@ -357,7 +357,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let kind = Decls.(IsDefinition Instance) in - let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in + let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in let info = Lemmas.Info.make ~hook ~kind () in (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) diff --git a/vernac/classes.mli b/vernac/classes.mli index f410cddfef..1b6deb3b28 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -22,7 +22,7 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map -> Does nothing — or emit a “not-a-class” warning if the [warn] argument is set — when said type is not a registered type class. *) -val existing_instance : bool -> qualid -> ComHints.hint_info_expr option -> unit +val existing_instance : bool -> qualid -> Vernacexpr.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val new_instance_interactive @@ -34,7 +34,7 @@ val new_instance_interactive -> ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) - -> ComHints.hint_info_expr + -> Vernacexpr.hint_info_expr -> (bool * constr_expr) option -> Id.t * Lemmas.t @@ -47,7 +47,7 @@ val new_instance -> (bool * constr_expr) -> ?generalize:bool -> ?hook:(GlobRef.t -> unit) - -> ComHints.hint_info_expr + -> Vernacexpr.hint_info_expr -> Id.t val new_instance_program @@ -59,7 +59,7 @@ val new_instance_program -> (bool * constr_expr) option -> ?generalize:bool -> ?hook:(GlobRef.t -> unit) - -> ComHints.hint_info_expr + -> Vernacexpr.hint_info_expr -> Id.t val declare_new_instance @@ -69,7 +69,7 @@ val declare_new_instance -> ident_decl -> local_binder_expr list -> constr_expr - -> ComHints.hint_info_expr + -> Vernacexpr.hint_info_expr -> unit (** {6 Low level interface used by Add Morphism, do not use } *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 776ffd6b9f..023d76ce3b 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -87,8 +87,7 @@ let context_set_of_entry = function | Monomorphic_entry uctx -> uctx let declare_assumptions ~poly ~scope ~kind univs nl l = - let open DeclareDef in - let () = match scope with + let () = let open Declare in match scope with | Discharge -> (* declare universes separately for variables *) DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs)) @@ -100,10 +99,10 @@ let declare_assumptions ~poly ~scope ~kind univs nl l = let univs,subst' = List.fold_left_map (fun univs id -> let refu = match scope with - | Discharge -> + | Declare.Discharge -> declare_variable is_coe ~kind typ imps Glob_term.Explicit id; GlobRef.VarRef id.CAst.v, Univ.Instance.empty - | Global local -> + | Declare.Global local -> declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id in next_univs univs, (id.CAst.v, Constr.mkRef refu)) @@ -130,7 +129,7 @@ let process_assumptions_udecls ~scope l = udecl, id | (_, ([], _))::_ | [] -> assert false in - let open DeclareDef in + let open Declare in let () = match scope, udecl with | Discharge, Some _ -> let loc = first_id.CAst.loc in @@ -208,7 +207,7 @@ let context_insection sigma ~poly ctx = let uctx = Evd.evar_universe_context sigma in let kind = Decls.(IsDefinition Definition) in let _ : GlobRef.t = - DeclareDef.declare_entry ~name ~scope:DeclareDef.Discharge + Declare.declare_entry ~name ~scope:Declare.Discharge ~kind ~impargs:[] ~uctx entry in () diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 4b953c8869..989015a9f3 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -17,7 +17,7 @@ open Constrexpr val do_assumptions : program_mode:bool -> poly:bool - -> scope:DeclareDef.locality + -> scope:Declare.locality -> kind:Decls.assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 4a8e217fc1..d6be02245c 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -352,8 +352,8 @@ let try_add_new_identity_coercion id ~local ~poly ~source ~target = let try_add_new_coercion_with_source ref ~local ~poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false -let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } = - let open DeclareDef in +let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } = + let open Declare in let local = match scope with | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) | Global ImportNeedQualified -> true @@ -363,10 +363,10 @@ let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } = let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg -let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly) +let add_coercion_hook ~poly = Declare.Hook.make (add_coercion_hook poly) -let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } = - let open DeclareDef in +let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } = + let open Declare in let stre = match scope with | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) | Global ImportNeedQualified -> true @@ -375,4 +375,4 @@ let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } = let cl = class_of_global dref in try_add_new_coercion_subclass cl ~local:stre ~poly -let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly) +let add_subclass_hook ~poly = Declare.Hook.make (add_subclass_hook ~poly) diff --git a/vernac/comCoercion.mli b/vernac/comCoercion.mli index 3b44bdaf8a..dee693232f 100644 --- a/vernac/comCoercion.mli +++ b/vernac/comCoercion.mli @@ -46,8 +46,8 @@ val try_add_new_identity_coercion -> local:bool -> poly:bool -> source:cl_typ -> target:cl_typ -> unit -val add_coercion_hook : poly:bool -> DeclareDef.Hook.t +val add_coercion_hook : poly:bool -> Declare.Hook.t -val add_subclass_hook : poly:bool -> DeclareDef.Hook.t +val add_subclass_hook : poly:bool -> Declare.Hook.t val class_of_global : GlobRef.t -> cl_typ diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 66d5a4f7f5..95f3955309 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -117,7 +117,7 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = in let kind = Decls.IsDefinition kind in let _ : Names.GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs + Declare.declare_definition ~name ~scope ~kind ?hook ~impargs ~opaque:false ~poly evd ~udecl ~types ~body in () @@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in + let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in let _ : DeclareObl.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 337da22018..2e8fe16252 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -15,9 +15,9 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : ?hook:DeclareDef.Hook.t + : ?hook:Declare.Hook.t -> name:Id.t - -> scope:DeclareDef.locality + -> scope:Declare.locality -> poly:bool -> kind:Decls.definition_object_kind -> universe_decl_expr option @@ -28,9 +28,9 @@ val do_definition -> unit val do_definition_program - : ?hook:DeclareDef.Hook.t + : ?hook:Declare.Hook.t -> name:Id.t - -> scope:DeclareDef.locality + -> scope:Declare.locality -> poly:bool -> kind:Decls.definition_object_kind -> universe_decl_expr option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index d3c1d2e767..80ca85e9a6 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -257,7 +257,7 @@ let build_recthms ~indexes fixnames fixtypes fiximps = in let thms = List.map3 (fun name typ (ctx,impargs,_) -> - { DeclareDef.Recthm.name + { Declare.Recthm.name ; typ ; args = List.map Context.Rel.Declaration.get_name ctx ; impargs}) @@ -284,7 +284,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in let fix_kind = Decls.IsDefinition fix_kind in let _ : GlobRef.t list = - DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx + Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration fixitems in diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index dcb61d38d9..62a9d10bae 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -16,16 +16,16 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t + scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t val do_fixpoint : - scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t + scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t val do_cofixpoint : - scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/comHints.ml b/vernac/comHints.ml index 5a48e9c16c..2fd6fe2b29 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -13,23 +13,6 @@ open Util (** (Partial) implementation of the [Hint] command; some more functionality still lives in tactics/hints.ml *) -type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen - -type reference_or_constr = - | HintsReference of Libnames.qualid - | HintsConstr of Constrexpr.constr_expr - -type hints_expr = - | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * Libnames.qualid list * int option - | HintsImmediate of reference_or_constr list - | HintsUnfold of Libnames.qualid list - | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool - | HintsMode of Libnames.qualid * Hints.hint_mode list - | HintsConstructors of Libnames.qualid list - | HintsExtern of - int * Constrexpr.constr_expr option * Genarg.raw_generic_argument - let project_hint ~poly pri l2r r = let open EConstr in let open Coqlib in @@ -108,6 +91,7 @@ let interp_hints ~poly h = let fr r = Tacred.evaluable_of_global_reference env (fref r) in let fi c = let open Hints in + let open Vernacexpr in match c with | HintsReference c -> let gr = Smartlocate.global_with_alias c in @@ -126,15 +110,14 @@ let interp_hints ~poly h = in (info, poly, b, path, gr) in - let ft = - let open Hints in - function + let open Hints in + let open Vernacexpr in + let ft = function | HintsVariables -> HintsVariables | HintsConstants -> HintsConstants | HintsReferences lhints -> HintsReferences (List.map fr lhints) in let fp = Constrintern.intern_constr_pattern (Global.env ()) in - let open Hints in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) | HintsResolveIFF (l2r, lc, n) -> diff --git a/vernac/comHints.mli b/vernac/comHints.mli index 77fbef5387..20894eecf1 100644 --- a/vernac/comHints.mli +++ b/vernac/comHints.mli @@ -8,22 +8,4 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Typeclasses - -type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen - -type reference_or_constr = - | HintsReference of Libnames.qualid - | HintsConstr of Constrexpr.constr_expr - -type hints_expr = - | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * Libnames.qualid list * int option - | HintsImmediate of reference_or_constr list - | HintsUnfold of Libnames.qualid list - | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool - | HintsMode of Libnames.qualid * Hints.hint_mode list - | HintsConstructors of Libnames.qualid list - | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument - -val interp_hints : poly:bool -> hints_expr -> Hints.hints_entry +val interp_hints : poly:bool -> Vernacexpr.hints_expr -> Hints.hints_entry diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index bf38088f71..4e9e24b119 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -230,7 +230,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let name = add_suffix recname "_func" in (* XXX: Mutating the evar_map in the hook! *) (* XXX: Likely the sigma is out of date when the hook is called .... *) - let hook sigma { DeclareDef.Hook.S.dref; _ } = + let hook sigma { Declare.Hook.S.dref; _ } = let sigma, h_body = Evarutil.new_global sigma dref in let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in @@ -248,13 +248,13 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = hook, name, typ else let typ = it_mkProd_or_LetIn top_arity binders_rel in - let hook sigma { DeclareDef.Hook.S.dref; _ } = + let hook sigma { Declare.Hook.S.dref; _ } = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false dref impls in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) - let hook = DeclareDef.Hook.make (hook sigma) in + let hook = Declare.Hook.make (hook sigma) in RetrieveObl.check_evars env sigma; let evars, _, evars_def, evars_typ = RetrieveObl.retrieve_obligations env recname sigma 0 def typ @@ -290,7 +290,7 @@ let do_program_recursive ~scope ~poly fixkind fixl = let evars, _, def, typ = RetrieveObl.retrieve_obligations env name evm (List.length rec_sign) def typ in - ({ DeclareDef.Recthm.name; typ; impargs; args = [] }, def, evars) + ({ Declare.Recthm.name; typ; impargs; args = [] }, def, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index 6851c9f69e..8b1fa6c202 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -14,8 +14,8 @@ open Vernacexpr val do_fixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit diff --git a/vernac/declare.ml b/vernac/declare.ml index f4636c5724..c3f95c5297 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -16,7 +16,7 @@ open Names open Safe_typing module NamedDecl = Context.Named.Declaration -type opacity_flag = Opaque | Transparent +type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent type t = { endline_tactic : Genarg.glob_generic_argument option @@ -120,17 +120,6 @@ let get_open_goals ps = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf -(* object_kind , id *) -exception AlreadyDeclared of (string option * Id.t) - -let _ = CErrors.register_handler (function - | AlreadyDeclared (kind, id) -> - Some - (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind - ; Id.print id; str " already exists."]) - | _ -> - None) - type import_status = ImportDefaultBehavior | ImportNeedQualified (** Declaration of constants and parameters *) @@ -267,7 +256,7 @@ type constant_obj = { let load_constant i ((sp,kn), obj) = if Nametab.exists_cci sp then - raise (AlreadyDeclared (None, Libnames.basename sp)); + raise (DeclareUniv.AlreadyDeclared (None, Libnames.basename sp)); let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con); Dumpglob.add_constant_kind con obj.cst_kind @@ -287,7 +276,7 @@ let exists_name id = let check_exists id = if exists_name id then - raise (AlreadyDeclared (None, id)) + raise (DeclareUniv.AlreadyDeclared (None, id)) let cache_constant ((sp,kn), obj) = (* Invariant: the constant must exist in the logical environment *) @@ -495,6 +484,17 @@ let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = register_constant kn kind local in kn +let get_cd_fix_exn = function + | DefinitionEntry de -> + Future.fix_exn_of de.proof_entry_body + | _ -> fun x -> x + +let declare_constant ?local ~name ~kind cd = + try declare_constant ?local ~name ~kind cd + with exn -> + let exn = Exninfo.capture exn in + Exninfo.iraise (get_cd_fix_exn cd exn) + let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de = let kn, eff = let de = @@ -537,7 +537,7 @@ let inVariable v = Libobject.Dyn.Easy.inj v objVariable let declare_variable ~name ~kind d = (* Variables are distinguished by only short names *) if Decls.variable_exists name then - raise (AlreadyDeclared (None, name)); + raise (DeclareUniv.AlreadyDeclared (None, name)); let impl,opaque = match d with (* Fails if not well-typed *) | SectionLocalAssum {typ;impl} -> @@ -620,8 +620,6 @@ module Internal = struct let set_opacity ~opaque entry = { entry with proof_entry_opaque = opaque } - let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body - let rec decompose len c t accu = let open Constr in let open Context.Rel.Declaration in @@ -877,3 +875,181 @@ let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme let _ = Abstract.declare_abstract := declare_abstract let declare_universe_context = DeclareUctx.declare_universe_context + +type locality = Discharge | Global of import_status + +(* Hooks naturally belong here as they apply to both definitions and lemmas *) +module Hook = struct + module S = struct + type t = + { uctx : UState.t + (** [ustate]: universe constraints obtained when the term was closed *) + ; obls : (Names.Id.t * Constr.t) list + (** [(n1,t1),...(nm,tm)]: association list between obligation + name and the corresponding defined term (might be a constant, + but also an arbitrary term in the Expand case of obligations) *) + ; scope : locality + (** [locality]: Locality of the original declaration *) + ; dref : Names.GlobRef.t + (** [ref]: identifier of the original declaration *) + } + end + + type t = (S.t -> unit) CEphemeron.key + + let make hook = CEphemeron.create hook + + let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook + +end + +(* Locality stuff *) +let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = + let should_suggest = entry.proof_entry_opaque && + Option.is_empty entry.proof_entry_secctx in + let ubind = UState.universe_binders uctx in + let dref = match scope with + | Discharge -> + let () = declare_variable ~name ~kind (SectionLocalDef entry) in + if should_suggest then Proof_using.suggest_variable (Global.env ()) name; + Names.GlobRef.VarRef name + | Global local -> + let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in + let gr = Names.GlobRef.ConstRef kn in + if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; + let () = DeclareUniv.declare_univ_binders gr ubind in + gr + in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = definition_message name in + Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; + dref + +let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = + match possible_indexes with + | Some possible_indexes -> + let env = Global.env() in + let indexes = Pretyping.search_guard env possible_indexes rec_declaration in + let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in + let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in + vars, fixdecls, Some indexes + | None -> + let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in + let vars = Vars.universes_of_constr (List.hd fixdecls) in + vars, fixdecls, None + +module Recthm = struct + type t = + { name : Names.Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Names.Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = + let vars, fixdecls, indexes = + mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in + let uctx, univs = + (* XXX: Obligations don't do this, this seems like a bug? *) + if restrict_ucontext + then + let uctx = UState.restrict uctx vars in + let univs = UState.check_univ_decl ~poly uctx udecl in + uctx, univs + else + let univs = UState.univ_entry ~poly uctx in + uctx, univs + in + let csts = CList.map2 + (fun Recthm.{ name; typ; impargs } body -> + let entry = definition_entry ~opaque ~types:typ ~univs body in + declare_entry ~name ~scope ~kind ~impargs ~uctx entry) + fixitems fixdecls + in + let isfix = Option.has_some possible_indexes in + let fixnames = List.map (fun { Recthm.name } -> name) fixitems in + recursive_message isfix indexes fixnames; + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; + csts + +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" + Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ + spc () ++ strbrk "declared as an axiom.") + +let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = + let local = match scope with + | Discharge -> warn_let_as_axiom name; ImportNeedQualified + | Global local -> local + in + let kind = Decls.(IsAssumption Conjectural) in + let decl = ParameterEntry pe in + let kn = declare_constant ~name ~local ~kind decl in + let dref = Names.GlobRef.ConstRef kn in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = assumption_message name in + let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in + let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in + dref + +let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = + try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + with exn -> + let exn = Exninfo.capture exn in + let exn = Option.cata (fun fix -> fix exn) exn fix_exn in + Exninfo.iraise exn + +(* Preparing proof entries *) + +let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma = + let env = Global.env () in + Pretyping.check_evars_are_solved ~program_mode:false env sigma; + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true + sigma (fun nf -> nf body, Option.map nf types) + in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in + let uctx = Evd.evar_universe_context sigma in + entry, uctx + +let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook + ?obls ~poly ?inline ~types ~body ?fix_exn sigma = + let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in + declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry + +let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false + sigma (fun nf -> nf body, Option.map nf types) + in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let ce = definition_entry ?opaque ?inline ?types ~univs body in + let env = Global.env () in + let (c,ctx), sideff = Future.force ce.proof_entry_body in + assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private); + assert(Univ.ContextSet.is_empty ctx); + RetrieveObl.check_evars env sigma; + let c = EConstr.of_constr c in + let typ = match ce.proof_entry_type with + | Some t -> EConstr.of_constr t + | None -> Retyping.get_type_of env sigma c + in + let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in + let uctx = Evd.evar_universe_context sigma in + c, cty, uctx, obls + +let prepare_parameter ~poly ~udecl ~types sigma = + let env = Global.env () in + Pretyping.check_evars_are_solved ~program_mode:false env sigma; + let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true + sigma (fun nf -> nf types) + in + let univs = Evd.check_univ_decl ~poly sigma udecl in + sigma, (None(*proof using*), (typ, univs), None(*inline*)) + +(* Compat: will remove *) +exception AlreadyDeclared = DeclareUniv.AlreadyDeclared diff --git a/vernac/declare.mli b/vernac/declare.mli index a297f25868..340c035d1d 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -69,7 +69,7 @@ module Proof : sig end -type opacity_flag = Opaque | Transparent +type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent (** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of name [name] with goals [goals] (a list of pairs of environment and @@ -194,14 +194,9 @@ val inline_private_constants val definition_message : Id.t -> unit val assumption_message : Id.t -> unit val fixpoint_message : int array option -> Id.t list -> unit -val recursive_message : bool (** true = fixpoint *) -> - int array option -> Id.t list -> unit val check_exists : Id.t -> unit -(* Used outside this module only in indschemes *) -exception AlreadyDeclared of (string option * Id.t) - (** {6 For legacy support, do not use} *) module Internal : sig @@ -211,10 +206,6 @@ module Internal : sig (* Overriding opacity is indeed really hacky *) val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry - (* TODO: This is only used in DeclareDef to forward the fix to - hooks, should eventually go away *) - val get_fix_exn : 'a proof_entry -> Future.fix_exn - val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list type constant_obj @@ -282,3 +273,127 @@ val build_constant_by_tactic : val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit [@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"] + +type locality = Discharge | Global of import_status + +(** Declaration hooks *) +module Hook : sig + type t + + (** Hooks allow users of the API to perform arbitrary actions at + proof/definition saving time. For example, to register a constant + as a Coercion, perform some cleanup, update the search database, + etc... *) + module S : sig + type t = + { uctx : UState.t + (** [ustate]: universe constraints obtained when the term was closed *) + ; obls : (Id.t * Constr.t) list + (** [(n1,t1),...(nm,tm)]: association list between obligation + name and the corresponding defined term (might be a constant, + but also an arbitrary term in the Expand case of obligations) *) + ; scope : locality + (** [scope]: Locality of the original declaration *) + ; dref : GlobRef.t + (** [dref]: identifier of the original declaration *) + } + end + + val make : (S.t -> unit) -> t + val call : ?hook:t -> S.t -> unit +end + +(** Declare an interactively-defined constant *) +val declare_entry + : name:Id.t + -> scope:locality + -> kind:Decls.logical_kind + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list + -> impargs:Impargs.manual_implicits + -> uctx:UState.t + -> Evd.side_effects proof_entry + -> GlobRef.t + +(** Declares a non-interactive constant; [body] and [types] will be + normalized w.r.t. the passed [evar_map] [sigma]. Universes should + be handled properly, including minimization and restriction. Note + that [sigma] is checked for unresolved evars, thus you should be + careful not to submit open terms or evar maps with stale, + unresolved existentials *) +val declare_definition + : name:Id.t + -> scope:locality + -> kind:Decls.logical_kind + -> opaque:bool + -> impargs:Impargs.manual_implicits + -> udecl:UState.universe_decl + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list + -> poly:bool + -> ?inline:bool + -> types:EConstr.t option + -> body:EConstr.t + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> Evd.evar_map + -> GlobRef.t + +val declare_assumption + : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> name:Id.t + -> scope:locality + -> hook:Hook.t option + -> impargs:Impargs.manual_implicits + -> uctx:UState.t + -> Entries.parameter_entry + -> GlobRef.t + +module Recthm : sig + type t = + { name : Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +val declare_mutually_recursive + : opaque:bool + -> scope:locality + -> kind:Decls.logical_kind + -> poly:bool + -> uctx:UState.t + -> udecl:UState.universe_decl + -> ntns:Vernacexpr.decl_notation list + -> rec_declaration:Constr.rec_declaration + -> possible_indexes:int list list option + -> ?restrict_ucontext:bool + (** XXX: restrict_ucontext should be always true, this seems like a + bug in obligations, so this parameter should go away *) + -> Recthm.t list + -> Names.GlobRef.t list + +val prepare_obligation + : ?opaque:bool + -> ?inline:bool + -> name:Id.t + -> poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map + -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info + +val prepare_parameter + : poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.types + -> Evd.evar_map + -> Evd.evar_map * Entries.parameter_entry + +(* Compat: will remove *) +exception AlreadyDeclared of (string option * Names.Id.t) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 1809c2bc91..83bb1dae71 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -1,193 +1,9 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \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 Declare - -type locality = Discharge | Global of Declare.import_status - -(* Hooks naturally belong here as they apply to both definitions and lemmas *) -module Hook = struct - module S = struct - type t = - { uctx : UState.t - (** [ustate]: universe constraints obtained when the term was closed *) - ; obls : (Names.Id.t * Constr.t) list - (** [(n1,t1),...(nm,tm)]: association list between obligation - name and the corresponding defined term (might be a constant, - but also an arbitrary term in the Expand case of obligations) *) - ; scope : locality - (** [locality]: Locality of the original declaration *) - ; dref : Names.GlobRef.t - (** [ref]: identifier of the original declaration *) - } - end - - type t = (S.t -> unit) CEphemeron.key - - let make hook = CEphemeron.create hook - - let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook - -end - -(* Locality stuff *) -let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = - let should_suggest = entry.Declare.proof_entry_opaque && - Option.is_empty entry.Declare.proof_entry_secctx in - let ubind = UState.universe_binders uctx in - let dref = match scope with - | Discharge -> - let () = declare_variable ~name ~kind (SectionLocalDef entry) in - if should_suggest then Proof_using.suggest_variable (Global.env ()) name; - Names.GlobRef.VarRef name - | Global local -> - let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in - let gr = Names.GlobRef.ConstRef kn in - if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; - let () = DeclareUniv.declare_univ_binders gr ubind in - gr - in - let () = Impargs.maybe_declare_manual_implicits false dref impargs in - let () = definition_message name in - Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; - dref - -let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry = - try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry - with exn -> - let exn = Exninfo.capture exn in - let fix_exn = Declare.Internal.get_fix_exn entry in - Exninfo.iraise (fix_exn exn) - -let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = - match possible_indexes with - | Some possible_indexes -> - let env = Global.env() in - let indexes = Pretyping.search_guard env possible_indexes rec_declaration in - let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in - let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in - vars, fixdecls, Some indexes - | None -> - let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in - let vars = Vars.universes_of_constr (List.hd fixdecls) in - vars, fixdecls, None - -module Recthm = struct - type t = - { name : Names.Id.t - (** Name of theorem *) - ; typ : Constr.t - (** Type of theorem *) - ; args : Names.Name.t list - (** Names to pre-introduce *) - ; impargs : Impargs.manual_implicits - (** Explicitily declared implicit arguments *) - } -end - -let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = - let vars, fixdecls, indexes = - mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in - let uctx, univs = - (* XXX: Obligations don't do this, this seems like a bug? *) - if restrict_ucontext - then - let uctx = UState.restrict uctx vars in - let univs = UState.check_univ_decl ~poly uctx udecl in - uctx, univs - else - let univs = UState.univ_entry ~poly uctx in - uctx, univs - in - let csts = CList.map2 - (fun Recthm.{ name; typ; impargs } body -> - let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in - declare_entry ~name ~scope ~kind ~impargs ~uctx entry) - fixitems fixdecls - in - let isfix = Option.has_some possible_indexes in - let fixnames = List.map (fun { Recthm.name } -> name) fixitems in - Declare.recursive_message isfix indexes fixnames; - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; - csts - -let warn_let_as_axiom = - CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ - spc () ++ strbrk "declared as an axiom.") - -let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = - let local = match scope with - | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified - | Global local -> local - in - let kind = Decls.(IsAssumption Conjectural) in - let decl = Declare.ParameterEntry pe in - let kn = Declare.declare_constant ~name ~local ~kind decl in - let dref = Names.GlobRef.ConstRef kn in - let () = Impargs.maybe_declare_manual_implicits false dref impargs in - let () = Declare.assumption_message name in - let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in - let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in - dref - -let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = - try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe - with exn -> - let exn = Exninfo.capture exn in - let exn = Option.cata (fun fix -> fix exn) exn fix_exn in - Exninfo.iraise exn - -(* Preparing proof entries *) - -let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma = - let env = Global.env () in - Pretyping.check_evars_are_solved ~program_mode:false env sigma; - let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true - sigma (fun nf -> nf body, Option.map nf types) - in - let univs = Evd.check_univ_decl ~poly sigma udecl in - let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in - let uctx = Evd.evar_universe_context sigma in - entry, uctx - -let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook - ?obls ~poly ?inline ~types ~body ?fix_exn sigma = - let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in - declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry - -let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = - let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false - sigma (fun nf -> nf body, Option.map nf types) - in - let univs = Evd.check_univ_decl ~poly sigma udecl in - let ce = definition_entry ?opaque ?inline ?types ~univs body in - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in - assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private); - assert(Univ.ContextSet.is_empty ctx); - RetrieveObl.check_evars env sigma; - let c = EConstr.of_constr c in - let typ = match ce.Declare.proof_entry_type with - | Some t -> EConstr.of_constr t - | None -> Retyping.get_type_of env sigma c - in - let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in - let uctx = Evd.evar_universe_context sigma in - c, cty, uctx, obls - -let prepare_parameter ~poly ~udecl ~types sigma = - let env = Global.env () in - Pretyping.check_evars_are_solved ~program_mode:false env sigma; - let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true - sigma (fun nf -> nf types) - in - let univs = Evd.check_univ_decl ~poly sigma udecl in - sigma, (None(*proof using*), (typ, univs), None(*inline*)) +type locality = Declare.locality = + | Discharge [@ocaml.deprecated "Use [Declare.Discharge]"] + | Global of Declare.import_status [@ocaml.deprecated "Use [Declare.Global]"] +[@@ocaml.deprecated "Use [Declare.locality]"] + +let declare_definition = Declare.declare_definition +[@@ocaml.deprecated "Use [Declare.declare_definition]"] +module Hook = Declare.Hook +[@@ocaml.deprecated "Use [Declare.Hook]"] diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli deleted file mode 100644 index 3bc1e25f19..0000000000 --- a/vernac/declareDef.mli +++ /dev/null @@ -1,132 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \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 Names - -type locality = Discharge | Global of Declare.import_status - -(** Declaration hooks *) -module Hook : sig - type t - - (** Hooks allow users of the API to perform arbitrary actions at - proof/definition saving time. For example, to register a constant - as a Coercion, perform some cleanup, update the search database, - etc... *) - module S : sig - type t = - { uctx : UState.t - (** [ustate]: universe constraints obtained when the term was closed *) - ; obls : (Id.t * Constr.t) list - (** [(n1,t1),...(nm,tm)]: association list between obligation - name and the corresponding defined term (might be a constant, - but also an arbitrary term in the Expand case of obligations) *) - ; scope : locality - (** [scope]: Locality of the original declaration *) - ; dref : GlobRef.t - (** [dref]: identifier of the original declaration *) - } - end - - val make : (S.t -> unit) -> t - val call : ?hook:t -> S.t -> unit -end - -(** Declare an interactively-defined constant *) -val declare_entry - : name:Id.t - -> scope:locality - -> kind:Decls.logical_kind - -> ?hook:Hook.t - -> ?obls:(Id.t * Constr.t) list - -> impargs:Impargs.manual_implicits - -> uctx:UState.t - -> Evd.side_effects Declare.proof_entry - -> GlobRef.t - -(** Declares a non-interactive constant; [body] and [types] will be - normalized w.r.t. the passed [evar_map] [sigma]. Universes should - be handled properly, including minimization and restriction. Note - that [sigma] is checked for unresolved evars, thus you should be - careful not to submit open terms or evar maps with stale, - unresolved existentials *) -val declare_definition - : name:Id.t - -> scope:locality - -> kind:Decls.logical_kind - -> opaque:bool - -> impargs:Impargs.manual_implicits - -> udecl:UState.universe_decl - -> ?hook:Hook.t - -> ?obls:(Id.t * Constr.t) list - -> poly:bool - -> ?inline:bool - -> types:EConstr.t option - -> body:EConstr.t - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> Evd.evar_map - -> GlobRef.t - -val declare_assumption - : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> name:Id.t - -> scope:locality - -> hook:Hook.t option - -> impargs:Impargs.manual_implicits - -> uctx:UState.t - -> Entries.parameter_entry - -> GlobRef.t - -module Recthm : sig - type t = - { name : Id.t - (** Name of theorem *) - ; typ : Constr.t - (** Type of theorem *) - ; args : Name.t list - (** Names to pre-introduce *) - ; impargs : Impargs.manual_implicits - (** Explicitily declared implicit arguments *) - } -end - -val declare_mutually_recursive - : opaque:bool - -> scope:locality - -> kind:Decls.logical_kind - -> poly:bool - -> uctx:UState.t - -> udecl:UState.universe_decl - -> ntns:Vernacexpr.decl_notation list - -> rec_declaration:Constr.rec_declaration - -> possible_indexes:int list list option - -> ?restrict_ucontext:bool - (** XXX: restrict_ucontext should be always true, this seems like a - bug in obligations, so this parameter should go away *) - -> Recthm.t list - -> Names.GlobRef.t list - -val prepare_obligation - : ?opaque:bool - -> ?inline:bool - -> name:Id.t - -> poly:bool - -> udecl:UState.universe_decl - -> types:EConstr.t option - -> body:EConstr.t - -> Evd.evar_map - -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info - -val prepare_parameter - : poly:bool - -> udecl:UState.universe_decl - -> types:EConstr.types - -> Evd.evar_map - -> Evd.evar_map * Entries.parameter_entry diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index bba3687256..ab11472dec 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -55,10 +55,10 @@ module ProgramDecl = struct ; prg_implicits : Impargs.manual_implicits ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool - ; prg_scope : DeclareDef.locality + ; prg_scope : Declare.locality ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr - ; prg_hook : DeclareDef.Hook.t option + ; prg_hook : Declare.Hook.t option ; prg_opaque : bool } @@ -373,7 +373,7 @@ let declare_definition prg = (* XXX: This is doing normalization twice *) let () = progmap_remove prg in let kn = - DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls + Declare.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in kn @@ -426,7 +426,7 @@ let declare_mutual_definition l = let fixdefs, fixrs, fixtypes, fixitems = List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) -> d :: a1, r :: a2, typ :: a3, - DeclareDef.Recthm.{ name; typ; impargs; args = [] } :: a4 + Declare.Recthm.{ name; typ; impargs; args = [] } :: a4 ) defs first.prg_deps ([],[],[],[]) in let fixkind = Option.get first.prg_fixkind in @@ -446,13 +446,13 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let udecl = UState.default_univ_decl in let kns = - DeclareDef.declare_mutually_recursive ~scope ~opaque ~kind + Declare.declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly ~restrict_ucontext:false fixitems in (* Only for the first constant *) let dref = List.hd kns in - DeclareDef.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref }); + Declare.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref }); List.iter progmap_remove l; dref @@ -556,7 +556,7 @@ let obligation_terminator entries uctx { name; num; auto } = (* Similar to the terminator but for interactive paths, as the terminator is only called in interactive proof mode *) -let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } = +let obligation_hook prg obl num auto { Declare.Hook.S.uctx = ctx'; dref; _ } = let { obls; remaining=rem } = prg.prg_obligations in let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 16c0413caf..03f0a57bcb 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -52,22 +52,22 @@ module ProgramDecl : sig ; prg_implicits : Impargs.manual_implicits ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool - ; prg_scope : DeclareDef.locality + ; prg_scope : Declare.locality ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr - ; prg_hook : DeclareDef.Hook.t option + ; prg_hook : Declare.Hook.t option ; prg_opaque : bool } val make : ?opaque:bool - -> ?hook:DeclareDef.Hook.t + -> ?hook:Declare.Hook.t -> Names.Id.t -> udecl:UState.universe_decl -> uctx:UState.t -> impargs:Impargs.manual_implicits -> poly:bool - -> scope:DeclareDef.locality + -> scope:Declare.locality -> kind:Decls.definition_object_kind -> Constr.constr option -> Constr.types @@ -126,7 +126,7 @@ val obligation_hook -> Obligation.t -> Int.t -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b) - -> DeclareDef.Hook.S.t + -> Declare.Hook.S.t -> unit (** [obligation_hook] part 2 of saving an obligation, non-interactive mode *) diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 89f3503f4d..1705915e70 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -10,6 +10,17 @@ open Names +(* object_kind , id *) +exception AlreadyDeclared of (string option * Id.t) + +let _ = CErrors.register_handler (function + | AlreadyDeclared (kind, id) -> + Some + Pp.(seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind + ; Id.print id; str " already exists."]) + | _ -> + None) + type universe_source = | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) | QualifiedUniv of Id.t (* global universe introduced by some global value *) @@ -19,7 +30,7 @@ type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list let check_exists_universe sp = if Nametab.exists_universe sp then - raise (Declare.AlreadyDeclared (Some "Universe", Libnames.basename sp)) + raise (AlreadyDeclared (Some "Universe", Libnames.basename sp)) else () let qualify_univ i dp src id = diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli index 51f3f5e0fb..e4d1d5dc65 100644 --- a/vernac/declareUniv.mli +++ b/vernac/declareUniv.mli @@ -10,6 +10,9 @@ open Names +(* object_kind , id *) +exception AlreadyDeclared of (string option * Id.t) + (** Global universe contexts, names and constraints *) val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index e84fce5504..058fa691ee 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -14,7 +14,6 @@ open Glob_term open Constrexpr open Vernacexpr open Hints -open ComHints open Pcoq open Pcoq.Prim diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 6ffa88874b..356ccef06b 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -142,7 +142,7 @@ let try_declare_scheme what f internal names kn = | UndefinedCst s -> alarm what internal (strbrk "Required constant " ++ str s ++ str " undefined.") - | AlreadyDeclared (kind, id) as exn -> + | DeclareUniv.AlreadyDeclared (kind, id) as exn -> let msg = CErrors.print exn in alarm what internal msg | DecidabilityMutualNotSupported -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index b13e5bf653..838496c595 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -39,17 +39,17 @@ end module Info = struct type t = - { hook : DeclareDef.Hook.t option + { hook : Declare.Hook.t option ; proof_ending : Proof_ending.t CEphemeron.key (* This could be improved and the CEphemeron removed *) - ; scope : DeclareDef.locality + ; scope : Declare.locality ; kind : Decls.logical_kind (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *) - ; thms : DeclareDef.Recthm.t list + ; thms : Declare.Recthm.t list ; compute_guard : lemma_possible_guards } - let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) + let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.(IsProof Lemma)) () = { hook ; compute_guard = [] @@ -98,7 +98,7 @@ let initialize_named_context_for_proof () = let add_first_thm ~info ~name ~typ ~impargs = let thms = - { DeclareDef.Recthm.name + { Declare.Recthm.name ; impargs ; typ = EConstr.Unsafe.to_constr typ ; args = [] } :: info.Info.thms @@ -128,7 +128,7 @@ let start_dependent_lemma ~name ~poly let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun { DeclareDef.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with + match List.map (fun { Declare.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -136,12 +136,12 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun { DeclareDef.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with + in match List.map2 (fun { Declare.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl = - let intro_tac { DeclareDef.Recthm.args; _ } = Tactics.auto_intros_tac args in + let intro_tac { Declare.Recthm.args; _ } = Tactics.auto_intros_tac args in let init_tac, compute_guard = match recguard with | Some (finite,guard,init_terms) -> let rec_tac = rec_tac_initializer finite guard thms snl in @@ -161,7 +161,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua intro_tac (List.hd thms), [] in match thms with | [] -> CErrors.anomaly (Pp.str "No proof to start.") - | { DeclareDef.Recthm.name; typ; impargs; _} :: thms -> + | { Declare.Recthm.name; typ; impargs; _} :: thms -> let info = Info.{ hook ; compute_guard @@ -200,7 +200,7 @@ module MutualEntry : sig end = struct - (* XXX: Refactor this with the code in [DeclareDef.declare_mutdef] *) + (* XXX: Refactor this with the code in [Declare.declare_mutdef] *) let guess_decreasing env possible_indexes ((body, ctx), eff) = let open Constr in match Constr.kind body with @@ -220,7 +220,7 @@ end = struct Pp.(str "Not a proof by induction: " ++ Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") - let declare_mutdef ~uctx ~info pe i DeclareDef.Recthm.{ name; impargs; typ; _} = + let declare_mutdef ~uctx ~info pe i Declare.Recthm.{ name; impargs; typ; _} = let { Info.hook; scope; kind; compute_guard; _ } = info in (* if i = 0 , we don't touch the type; this is for compat but not clear it is the right thing to do. @@ -238,7 +238,7 @@ end = struct Declare.Internal.map_entry_body pe ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in - DeclareDef.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe + Declare.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe let declare_mutdef ~info ~uctx const = let pe = match info.Info.compute_guard with @@ -256,8 +256,8 @@ end = struct let declare_variable ~info ~uctx pe = let { Info.scope; hook } = info in List.map_i ( - fun i { DeclareDef.Recthm.name; typ; impargs } -> - DeclareDef.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + fun i { Declare.Recthm.name; typ; impargs } -> + Declare.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe ) 0 info.Info.thms end @@ -395,8 +395,8 @@ let process_idopt_for_save ~idopt info = (* Save foo was used; we override the info in the first theorem *) let thms = match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with - | [ { DeclareDef.Recthm.name; _} as decl ], Proof_ending.Regular -> - [ { decl with DeclareDef.Recthm.name = save_name } ] + | [ { Declare.Recthm.name; _} as decl ], Proof_ending.Regular -> + [ { decl with Declare.Recthm.name = save_name } ] | _ -> err_save_forbidden_in_place_of_qed () in { info with Info.thms } diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index bd2e87ac3a..b1462f1ce5 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -49,11 +49,11 @@ module Info : sig type t val make - : ?hook: DeclareDef.Hook.t + : ?hook: Declare.Hook.t (** Callback to be executed at the end of the proof *) -> ?proof_ending : Proof_ending.t (** Info for special constants *) - -> ?scope : DeclareDef.locality + -> ?scope : Declare.locality (** locality *) -> ?kind:Decls.logical_kind (** Theorem, etc... *) @@ -85,14 +85,14 @@ type lemma_possible_guards = int list list (** Pretty much internal, used by the Lemma / Fixpoint vernaculars *) val start_lemma_with_initialization - : ?hook:DeclareDef.Hook.t + : ?hook:Declare.Hook.t -> poly:bool - -> scope:DeclareDef.locality + -> scope:Declare.locality -> kind:Decls.logical_kind -> udecl:UState.universe_decl -> Evd.evar_map -> (bool * lemma_possible_guards * Constr.t option list option) option - -> DeclareDef.Recthm.t list + -> Declare.Recthm.t list -> int list option -> t diff --git a/vernac/locality.ml b/vernac/locality.ml index 9e784c8bb3..f62eed5e41 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -34,7 +34,7 @@ let warn_local_declaration = strbrk "available without qualification when imported.") let enforce_locality_exp locality_flag discharge = - let open DeclareDef in + let open Declare in let open Vernacexpr in match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) diff --git a/vernac/locality.mli b/vernac/locality.mli index 26149cb394..bf65579efd 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -20,7 +20,7 @@ val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality_exp : bool option -> Vernacexpr.discharge -> DeclareDef.locality +val enforce_locality_exp : bool option -> Vernacexpr.discharge -> Declare.locality val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: diff --git a/vernac/obligations.ml b/vernac/obligations.ml index bed593234b..5e746afc74 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -162,13 +162,13 @@ let rec solve_obligation prg num tac = ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); in let obl = subst_deps_obl obls obl in - let scope = DeclareDef.(Global Declare.ImportNeedQualified) in + let scope = Declare.(Global Declare.ImportNeedQualified) in let kind = kind_of_obligation (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in - let hook = DeclareDef.Hook.make (DeclareObl.obligation_hook prg obl num auto) in + let hook = Declare.Hook.make (DeclareObl.obligation_hook prg obl num auto) in let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in let poly = prg.prg_poly in let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in @@ -309,7 +309,7 @@ let show_term n = ++ Printer.pr_constr_env env sigma prg.prg_body) let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl) - ?(impargs=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic + ?(impargs=[]) ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = let info = Id.print name ++ str " has type-checked" in let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in @@ -328,11 +328,11 @@ let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl) | _ -> res) let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic - ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) + ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = - let deps = List.map (fun ({ DeclareDef.Recthm.name; _ }, _, _) -> name) l in + let deps = List.map (fun ({ Declare.Recthm.name; _ }, _, _) -> name) l in List.iter - (fun ({ DeclareDef.Recthm.name; typ; impargs; _ }, b, obls) -> + (fun ({ Declare.Recthm.name; typ; impargs; _ }, b, obls) -> let prg = ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce ?hook in progmap_add name (CEphemeron.create prg)) l; diff --git a/vernac/obligations.mli b/vernac/obligations.mli index f42d199e18..89ed4c3498 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -77,11 +77,11 @@ val add_definition : -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?impargs:Impargs.manual_implicits -> poly:bool - -> ?scope:DeclareDef.locality + -> ?scope:Declare.locality -> ?kind:Decls.definition_object_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) - -> ?hook:DeclareDef.Hook.t + -> ?hook:Declare.Hook.t -> ?opaque:bool -> RetrieveObl.obligation_info -> DeclareObl.progress @@ -91,15 +91,15 @@ val add_definition : (** Start a [Program Fixpoint] declaration, similar to the above, except it takes a list now. *) val add_mutual_definitions : - (DeclareDef.Recthm.t * Constr.t * RetrieveObl.obligation_info) list + (Declare.Recthm.t * Constr.t * RetrieveObl.obligation_info) list -> uctx:UState.t -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?tactic:unit Proofview.tactic -> poly:bool - -> ?scope:DeclareDef.locality + -> ?scope:Declare.locality -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) - -> ?hook:DeclareDef.Hook.t + -> ?hook:Declare.Hook.t -> ?opaque:bool -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f1aae239aa..b97cdfa51c 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -185,7 +185,7 @@ open Pputils | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z - let pr_reference_or_constr pr_c = let open ComHints in function + let pr_reference_or_constr pr_c = function | HintsReference r -> pr_qualid r | HintsConstr c -> pr_c c @@ -202,7 +202,6 @@ open Pputils let opth = pr_opt_hintbases db in let pph = let open Hints in - let open ComHints in match h with | HintsResolve l -> keyword "Resolve " ++ prlist_with_sep sep @@ -792,7 +791,6 @@ let string_of_definition_object_kind = let open Decls in function return (keyword "Admitted") | VernacEndProof (Proved (opac,o)) -> return ( - let open Declare in match o with | None -> (match opac with | Transparent -> keyword "Defined" diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 2b6beaf2e3..1718024edd 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -28,7 +28,7 @@ module Vernac_ : val command_entry : vernac_expr Entry.t val main_entry : vernac_control option Entry.t val red_expr : raw_red_expr Entry.t - val hint_info : ComHints.hint_info_expr Entry.t + val hint_info : hint_info_expr Entry.t end (* To be removed when the parser is made functional wrt the tactic diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 6d5d16d94a..618a61f487 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -9,16 +9,15 @@ Himsg Locality Egramml Vernacextend -Declare -ComHints Ppvernac Proof_using Egramcoq Metasyntax DeclareUniv RetrieveObl -DeclareDef +Declare DeclareObl +ComHints Canonical RecLemmas Library @@ -48,3 +47,4 @@ Vernacstate Vernacinterp Proof_global Pfedit +DeclareDef diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index df94f69cf6..aac0b54ed4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -460,7 +460,7 @@ let vernac_custom_entry ~module_local s = let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable id || - locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) + locality <> Declare.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) then user_err ?loc (Id.print id ++ str " already exists.") @@ -504,7 +504,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in let thms = List.map (fun (name, (typ, (args, impargs))) -> - { DeclareDef.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in + { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in let () = let open UState in if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then @@ -521,13 +521,13 @@ let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in | Coercion -> Some (ComCoercion.add_coercion_hook ~poly) | CanonicalStructure -> - Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) + Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | SubClass -> Some (ComCoercion.add_subclass_hook ~poly) | Definition when canonical_instance -> - Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) + Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | Let when canonical_instance -> - Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) + Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) | _ -> None let default_thm_id = Id.of_string "Unnamed_thm" @@ -542,7 +542,7 @@ let vernac_definition_name lid local = CAst.make ?loc (fresh_name_for_anonymous_theorem ()) | { v = Name.Name n; loc } -> CAst.make ?loc n in let () = - let open DeclareDef in + let open Declare in match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Global _ -> Dumpglob.dump_definition lid false "def" @@ -603,8 +603,8 @@ let vernac_assumption ~atts discharge kind l nl = if Dumpglob.dump () then List.iter (fun (lid, _) -> match scope with - | DeclareDef.Global _ -> Dumpglob.dump_definition lid false "ax" - | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; + | Declare.Global _ -> Dumpglob.dump_definition lid false "ax" + | Declare.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l let is_polymorphic_inductive_cumulativity = diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b65a0da1cc..b622fd9801 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -195,10 +195,12 @@ type syntax_modifier = | SetOnlyPrinting | SetFormat of string * lstring +type opacity_flag = Opaque | Transparent + type proof_end = | Admitted (* name in `Save ident` when closing goal *) - | Proved of Declare.opacity_flag * lident option + | Proved of opacity_flag * lident option type scheme = | InductionScheme of bool * qualid or_by_notation * sort_expr @@ -286,6 +288,22 @@ type extend_name = type discharge = DoDischarge | NoDischarge +type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen + +type reference_or_constr = + | HintsReference of Libnames.qualid + | HintsConstr of Constrexpr.constr_expr + +type hints_expr = + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * Libnames.qualid list * int option + | HintsImmediate of reference_or_constr list + | HintsUnfold of Libnames.qualid list + | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool + | HintsMode of Libnames.qualid * Hints.hint_mode list + | HintsConstructors of Libnames.qualid list + | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument + type nonrec vernac_expr = | VernacLoad of verbose_flag * string @@ -336,18 +354,18 @@ type nonrec vernac_expr = local_binder_expr list * (* binders *) constr_expr * (* type *) (bool * constr_expr) option * (* body (bool=true when using {}) *) - ComHints.hint_info_expr + hint_info_expr | VernacDeclareInstance of ident_decl * (* name *) local_binder_expr list * (* binders *) constr_expr * (* type *) - ComHints.hint_info_expr + hint_info_expr | VernacContext of local_binder_expr list | VernacExistingInstance of - (qualid * ComHints.hint_info_expr) list (* instances names, priorities and patterns *) + (qualid * hint_info_expr) list (* instances names, priorities and patterns *) | VernacExistingClass of qualid (* inductive or definition name *) @@ -387,7 +405,7 @@ type nonrec vernac_expr = (* Commands *) | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * qualid list - | VernacHints of string list * ComHints.hints_expr + | VernacHints of string list * hints_expr | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag |