diff options
53 files changed, 1595 insertions, 3512 deletions
diff --git a/META.coq.in b/META.coq.in index 0baacbc82e..9869e7f575 100644 --- a/META.coq.in +++ b/META.coq.in @@ -288,6 +288,8 @@ package "plugins" ( archive(byte) = "ltac_plugin.cmo" archive(native) = "ltac_plugin.cmx" + plugin(byte) = "ltac_plugin.cmo" + plugin(native) = "ltac_plugin.cmxs" ) package "tauto" ( @@ -300,6 +302,9 @@ package "plugins" ( archive(byte) = "tauto_plugin.cmo" archive(native) = "tauto_plugin.cmx" + + plugin(byte) = "tauto_plugin.cmo" + plugin(native) = "tauto_plugin.cmxs" ) package "omega" ( @@ -312,6 +317,9 @@ package "plugins" ( archive(byte) = "omega_plugin.cmo" archive(native) = "omega_plugin.cmx" + + plugin(byte) = "omega_plugin.cmo" + plugin(native) = "omega_plugin.cmxs" ) package "micromega" ( @@ -324,6 +332,24 @@ package "plugins" ( archive(byte) = "micromega_plugin.cmo" archive(native) = "micromega_plugin.cmx" + + plugin(byte) = "micromega_plugin.cmo" + plugin(native) = "micromega_plugin.cmxs" + ) + + package "zify" ( + + description = "Coq Zify plugin" + version = "8.11" + + requires = "coq.plugins.ltac" + directory = "micromega" + + archive(byte) = "zify_plugin.cmo" + archive(native) = "zify_plugin.cmx" + + plugin(byte) = "zify_plugin.cmo" + plugin(native) = "zify_plugin.cmxs" ) package "setoid_ring" ( @@ -336,6 +362,9 @@ package "plugins" ( archive(byte) = "newring_plugin.cmo" archive(native) = "newring_plugin.cmx" + + plugin(byte) = "newring_plugin.cmo" + plugin(native) = "newring_plugin.cmxs" ) package "extraction" ( @@ -348,6 +377,9 @@ package "plugins" ( archive(byte) = "extraction_plugin.cmo" archive(native) = "extraction_plugin.cmx" + + plugin(byte) = "extraction_plugin.cmo" + plugin(native) = "extraction_plugin.cmxs" ) package "cc" ( @@ -360,6 +392,9 @@ package "plugins" ( archive(byte) = "cc_plugin.cmo" archive(native) = "cc_plugin.cmx" + + plugin(byte) = "cc_plugin.cmo" + plugin(native) = "cc_plugin.cmxs" ) package "firstorder" ( @@ -372,6 +407,9 @@ package "plugins" ( archive(byte) = "ground_plugin.cmo" archive(native) = "ground_plugin.cmx" + + plugin(byte) = "ground_plugin.cmo" + plugin(native) = "ground_plugin.cmxs" ) package "rtauto" ( @@ -384,6 +422,9 @@ package "plugins" ( archive(byte) = "rtauto_plugin.cmo" archive(native) = "rtauto_plugin.cmx" + + plugin(byte) = "rtauto_plugin.cmo" + plugin(native) = "rtauto_plugin.cmxs" ) package "btauto" ( @@ -396,6 +437,9 @@ package "plugins" ( archive(byte) = "btauto_plugin.cmo" archive(native) = "btauto_plugin.cmx" + + plugin(byte) = "btauto_plugin.cmo" + plugin(native) = "btauto_plugin.cmxs" ) package "funind" ( @@ -408,6 +452,9 @@ package "plugins" ( archive(byte) = "recdef_plugin.cmo" archive(native) = "recdef_plugin.cmx" + + plugin(byte) = "recdef_plugin.cmo" + plugin(native) = "recdef_plugin.cmxs" ) package "nsatz" ( @@ -420,6 +467,9 @@ package "plugins" ( archive(byte) = "nsatz_plugin.cmo" archive(native) = "nsatz_plugin.cmx" + + plugin(byte) = "nsatz_plugin.cmo" + plugin(native) = "nsatz_plugin.cmxs" ) package "rsyntax" ( @@ -432,6 +482,9 @@ package "plugins" ( archive(byte) = "r_syntax_plugin.cmo" archive(native) = "r_syntax_plugin.cmx" + + plugin(byte) = "r_syntax_plugin.cmo" + plugin(native) = "r_syntax_plugin.cmxs" ) package "int63syntax" ( @@ -444,6 +497,9 @@ package "plugins" ( archive(byte) = "int63_syntax_plugin.cmo" archive(native) = "int63_syntax_plugin.cmx" + + plugin(byte) = "int63_syntax_plugin.cmo" + plugin(native) = "int63_syntax_plugin.cmxs" ) package "string_notation" ( @@ -456,6 +512,9 @@ package "plugins" ( archive(byte) = "string_notation_plugin.cmo" archive(native) = "string_notation_plugin.cmx" + + plugin(byte) = "string_notation_plugin.cmo" + plugin(native) = "string_notation_plugin.cmxs" ) package "derive" ( @@ -468,6 +527,9 @@ package "plugins" ( archive(byte) = "derive_plugin.cmo" archive(native) = "derive_plugin.cmx" + + plugin(byte) = "derive_plugin.cmo" + plugin(native) = "derive_plugin.cmxs" ) package "ssrmatching" ( @@ -480,6 +542,9 @@ package "plugins" ( archive(byte) = "ssrmatching_plugin.cmo" archive(native) = "ssrmatching_plugin.cmx" + + plugin(byte) = "ssrmatching_plugin.cmo" + plugin(native) = "ssrmatching_plugin.cmxs" ) package "ssreflect" ( @@ -492,5 +557,8 @@ package "plugins" ( archive(byte) = "ssreflect_plugin.cmo" archive(native) = "ssreflect_plugin.cmx" + + plugin(byte) = "ssreflect_plugin.cmo" + plugin(native) = "ssreflect_plugin.cmxs" ) ) diff --git a/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh b/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh new file mode 100644 index 0000000000..7001c3d0c8 --- /dev/null +++ b/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10516" ] || [ "$CI_BRANCH" = "proof+dup_save" ]; then + + elpi_CI_REF=proof+dup_save + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 042093a14c..0fc0a413ba 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -9,7 +9,7 @@ with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming versions of Proof General. A somewhat out-of-date description of the async state machine is -[documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). +[documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md). OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml). Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md). diff --git a/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst b/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst deleted file mode 100644 index 6cab6a1c13..0000000000 --- a/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Fix proof of False when using |SProp| (incorrect De Bruijn handling - when inferring the relevance mark of a function) (`#10904 - <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot). diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst new file mode 100644 index 0000000000..327a39bdb6 --- /dev/null +++ b/doc/changelog/03-notations/10963-simplify-parser.rst @@ -0,0 +1,6 @@ +- A simplification of parsing rules could cause a slight change of + parsing precedences for the very rare users who defined notations + with `constr` at level strictly between 100 and 200 and used these + notations on the right-hand side of a cast operator (`:`, `:>`, + `:>>`) (`#10963 <https://github.com/coq/coq/pull/10963>`_, by Théo + Zimmermann, simplification initially noticed by Jim Fehrle). diff --git a/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst b/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst deleted file mode 100644 index 9d15b7126f..0000000000 --- a/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst +++ /dev/null @@ -1 +0,0 @@ -- Fixed bug #10894: Ltac1 regression in binding free names in uconstr (`#10899 <https://github.com/coq/coq/pull/10899>`_, by Hugo Herbelin). diff --git a/doc/changelog/08-tools/10947-coq-makefile-dep.rst b/doc/changelog/08-tools/10947-coq-makefile-dep.rst new file mode 100644 index 0000000000..f620b32cb8 --- /dev/null +++ b/doc/changelog/08-tools/10947-coq-makefile-dep.rst @@ -0,0 +1,5 @@ +- Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` + utility, where `<CoqMakefile>` is the name of the output file given by the + `-o` option. In this way two generated makefiles can coexist in the same + directory. + (`#10947 <https://github.com/coq/coq/pull/10947>`_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst new file mode 100644 index 0000000000..5d8467025b --- /dev/null +++ b/doc/changelog/10-standard-library/10827-dedekind-reals.rst @@ -0,0 +1,11 @@ +- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers + as boolean-values functions along with 3 logical axioms: limited principle + of omniscience, excluded middle of negations and functional extensionality. + The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those + Dedekind reals, hidden behind an opaque module. + Classical Dedekind reals are a quotient of constructive reals, which allows + to transport many constructive proofs to the classical case. + + See `#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria, + based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, + code review by Hugo Herbelin. diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 9dd4700db5..307214089f 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -9,4 +9,4 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.Definition ~opaque:false sigma udecl body None [] + ~kind:Decls.(IsDefinition Definition) ~opaque:false sigma udecl body None [] diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index b6fcf9da22..80a24b997c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -726,6 +726,45 @@ Changes in 8.10.0 fixes `#9512 <https://github.com/coq/coq/issues/9512>`_ by Vincent Laporte). +Changes in 8.10.1 +~~~~~~~~~~~~~~~~~ + +A few bug fixes and documentation improvements, in particular: + +**Kernel** + +- Fix proof of False when using |SProp| (incorrect De Bruijn handling + when inferring the relevance mark of a function) (`#10904 + <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot). + +**Tactics** + +- Fix an anomaly when unsolved evar in :cmd:`Add Ring` + (`#10891 <https://github.com/coq/coq/pull/10891>`_, + fixes `#9851 <https://github.com/coq/coq/issues/9851>`_, + by Gaëtan Gilbert). + +**Tactic language** + +- Fix Ltac regression in binding free names in uconstr + (`#10899 <https://github.com/coq/coq/pull/10899>`_, + fixes `#10894 <https://github.com/coq/coq/issues/10894>`_, + by Hugo Herbelin). + +**CoqIDE** + +- Fix handling of unicode input before space + (`#10852 <https://github.com/coq/coq/pull/10852>`_, + fixes `#10842 <https://github.com/coq/coq/issues/10842>`_, + by Arthur Charguéraud). + +**Extraction** + +- Fix custom extraction of inductives to JSON + (`#10897 <https://github.com/coq/coq/pull/10897>`_, + fixes `#4741 <https://github.com/coq/coq/issues/4741>`_, + by Helge Bahmann). + Version 8.9 ----------- diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 03b30d5d97..57a54bc0ad 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -538,13 +538,11 @@ Requesting information .. cmdv:: Show Proof :name: Show Proof - It displays the proof term generated by the tactics - that have been applied. If the proof is not completed, this term - contain holes, which correspond to the sub-terms which are still to be - constructed. These holes appear as a question mark indexed by an - integer, and applied to the list of variables in the context, since it - may depend on them. The types obtained by abstracting away the context - from the type of each placeholder are also printed. + Displays the proof term generated by the tactics + that have been applied so far. If the proof is incomplete, the term + will contain holes, which correspond to subterms which are still to be + constructed. Each hole is an existential variable, which appears as a + question mark followed by an identifier. .. cmdv:: Show Conjectures :name: Show Conjectures @@ -574,9 +572,8 @@ Requesting information .. cmdv:: Show Existentials :name: Show Existentials - It displays the set of all uninstantiated - existential variables in the current proof tree, along with the type - and the context of each variable. + Displays all open goals / existential variables in the current proof + along with the type and the context of each variable. .. cmdv:: Show Match @ident diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1d08001e34..75897fec45 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2670,7 +2670,7 @@ context entry name. Lemma test n m (H : m + 1 < n) : True. have @i : 'I_n by apply: (Sub m); omega. -Note that the sub-term produced by :tacn:`omega` is in general huge and +Note that the subterm produced by :tacn:`omega` is in general huge and uninteresting, and hence one may want to hide it. For this purpose the ``[: name ]`` intro pattern and the tactic ``abstract`` (see :ref:`abstract_ssr`) are provided. @@ -4583,7 +4583,7 @@ The ``elim/`` tactic distinguishes two cases: passed to the eliminator as the last argument (``x`` in ``foo_ind``) and ``en−1 … e1`` are used as patterns to select in the goal the occurrences that will be bound by the predicate ``P``, thus it must be possible to unify - the sub-term of the goal matched by ``en−1`` with ``pm`` , the one matched + the subterm of the goal matched by ``en−1`` with ``pm`` , the one matched by ``en−2`` with ``pm−1`` and so on. :regular eliminator: in all the other cases. Here it must be possible to unify the term matched by ``en`` with ``pm`` , the one matched by diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index bcc5e914ac..a28ce600ca 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -750,12 +750,12 @@ level is otherwise given explicitly by using the syntax Levels are cumulative: a notation at level ``n`` of which the left end is a term shall use rules at level less than ``n`` to parse this -sub-term. More precisely, it shall use rules at level strictly less +subterm. More precisely, it shall use rules at level strictly less than ``n`` if the rule is declared with ``right associativity`` and rules at level less or equal than ``n`` if the rule is declared with ``left associativity``. Similarly, a notation at level ``n`` of which the right end is a term shall use by default rules at level strictly -less than ``n`` to parse this sub-term if the rule is declared left +less than ``n`` to parse this subterm if the rule is declared left associative and rules at level less or equal than ``n`` if the rule is declared right associative. This is what happens for instance in the rule diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 75c8c6c1ea..f0ada745e7 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -68,6 +68,7 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/WKL.v theories/Logic/FinFun.v theories/Logic/PropFacts.v + theories/Logic/HLevels.v </dd> <dt> <b>Structures</b>: @@ -518,8 +519,8 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/ConstructiveRealsMorphisms.v theories/Reals/ConstructiveCauchyReals.v theories/Reals/ConstructiveCauchyRealsMult.v + theories/Reals/ClassicalDedekindReals.v theories/Reals/Raxioms.v - theories/Reals/ConstructiveRIneq.v theories/Reals/ConstructiveRealsLUB.v theories/Reals/RIneq.v theories/Reals/DiscrR.v diff --git a/library/lib.ml b/library/lib.ml index 80b50b26d0..630c860a61 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -408,18 +408,12 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type abstr_info = Section.abstr_info = private { - abstr_ctx : Constr.named_context; - abstr_subst : Univ.Instance.t; - abstr_uctx : Univ.AUContext.t; -} - let instance_from_variable_context = List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list let extract_worklist info = - let args = instance_from_variable_context info.abstr_ctx in - info.abstr_subst, args + let args = instance_from_variable_context info.Section.abstr_ctx in + info.Section.abstr_subst, args let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () @@ -441,7 +435,7 @@ let section_segment_of_reference = let open GlobRef in function | VarRef _ -> empty_segment let variable_section_segment_of_reference gr = - (section_segment_of_reference gr).abstr_ctx + (section_segment_of_reference gr).Section.abstr_ctx let is_in_section ref = Section.is_in_section (Global.env ()) ref (sections ()) @@ -557,7 +551,7 @@ let discharge_proj_repr = let _, newpars = Mindmap.find mind (snd modlist) in mind, npars + Array.length newpars) -let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx = +let discharge_abstract_universe_context { Section.abstr_subst = subst; abstr_uctx = abs_ctx } auctx = let open Univ in let ainst = make_abstract_instance auctx in let subst = Instance.append subst ainst in diff --git a/library/lib.mli b/library/lib.mli index cef50a5f3b..a313a62c2e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -164,18 +164,9 @@ val drop_objects : frozen -> frozen val init : unit -> unit (** {6 Section management for discharge } *) -type abstr_info = Section.abstr_info = private { - abstr_ctx : Constr.named_context; - (** Section variables of this prefix *) - abstr_subst : Univ.Instance.t; - (** Actual names of the abstracted variables *) - abstr_uctx : Univ.AUContext.t; - (** Universe quantification, same length as the substitution *) -} - -val section_segment_of_constant : Constant.t -> abstr_info -val section_segment_of_mutual_inductive: MutInd.t -> abstr_info -val section_segment_of_reference : GlobRef.t -> abstr_info +val section_segment_of_constant : Constant.t -> Section.abstr_info +val section_segment_of_mutual_inductive: MutInd.t -> Section.abstr_info +val section_segment_of_reference : GlobRef.t -> Section.abstr_info val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context @@ -190,4 +181,4 @@ val replacement_context : unit -> Opaqueproof.work_list val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t val discharge_abstract_universe_context : - abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t + Section.abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index ea44e748c9..87b9a8eea3 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -196,17 +196,11 @@ GRAMMAR EXTEND Gram [ "200" RIGHTA [ c = binder_constr -> { c } ] | "100" RIGHTA - [ c1 = operconstr; "<:"; c2 = binder_constr -> + [ c1 = operconstr; "<:"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastVM c2) } - | c1 = operconstr; "<:"; c2 = SELF -> - { CAst.make ~loc @@ CCast(c1, CastVM c2) } - | c1 = operconstr; "<<:"; c2 = binder_constr -> - { CAst.make ~loc @@ CCast(c1, CastNative c2) } - | c1 = operconstr; "<<:"; c2 = SELF -> + | c1 = operconstr; "<<:"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastNative c2) } - | c1 = operconstr; ":";c2 = binder_constr -> - { CAst.make ~loc @@ CCast(c1, CastConv c2) } - | c1 = operconstr; ":"; c2 = SELF -> + | c1 = operconstr; ":"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastConv c2) } | c1 = operconstr; ":>" -> { CAst.make ~loc @@ CCast(c1, CastCoerce) } ] @@ -407,9 +401,7 @@ GRAMMAR EXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; ":"; ty = binder_constr -> - {CAst.make ~loc @@ CPatCast (p, ty) } - | p = pattern; ":"; ty = operconstr LEVEL "100" -> + [ p = pattern; ":"; ty = operconstr LEVEL "200" -> {CAst.make ~loc @@ CPatCast (p, ty) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 6011af74e5..0452665585 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -234,23 +234,6 @@ let change_property_sort evd toSort princ princName = ) (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params) -(* XXX: To be cleaned up soon in favor of common save path. *) -let save name const ?hook uctx scope kind = - let open Declare in - let open DeclareDef in - let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in - let r = match scope with - | Discharge -> - let c = SectionLocalDef const in - let () = declare_variable ~name ~kind c in - GlobRef.VarRef name - | Global local -> - let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in - GlobRef.ConstRef kn - in - DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); - definition_message name - let generate_functional_principle (evd: Evd.evar_map ref) interactive_proof old_princ_type sorts new_princ_name funs i proof_tac @@ -307,7 +290,14 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(IsProof Theorem) + let hook_data = hook, uctx, [] in + let _ : Names.GlobRef.t = DeclareDef.declare_definition + ~name:new_princ_name ~hook_data + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~kind:Decls.(IsProof Theorem) + UnivNames.empty_binders + entry [] in + () with e when CErrors.noncritical e -> raise (Defining_principle e) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 80fc64fe65..b55d8537d6 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -10,8 +10,6 @@ let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct" let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete" let mk_equation_id id = Nameops.add_suffix id "_equation" -let msgnl m = () - let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid) let fresh_name avoid s = Name (fresh_id avoid s) diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index cd5202a6c7..550f727951 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -9,9 +9,6 @@ val mk_correct_id : Id.t -> Id.t val mk_complete_id : Id.t -> Id.t val mk_equation_id : Id.t -> Id.t - -val msgnl : Pp.t -> unit - val fresh_id : Id.t list -> string -> Id.t val fresh_name : Id.t list -> string -> Name.t val get_name : Id.t list -> ?default:string -> Name.t -> Name.t diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4c5eab1a9b..29356df81d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1539,13 +1539,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type generate_induction_principle f_ref tcc_lemma_constr functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) - (nb_prod evd (EConstr.of_constr res)) relation; - Flags.if_verbose - msgnl (h 1 (Ppconstr.pr_id function_name ++ - spc () ++ str"is defined" )++ fnl () ++ - h 1 (Ppconstr.pr_id equation_id ++ - spc () ++ str"is defined" ) - ) + (nb_prod evd (EConstr.of_constr res)) relation in (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v index 03a7774a31..b94b74097b 100644 --- a/plugins/micromega/ZifyBool.v +++ b/plugins/micromega/ZifyBool.v @@ -42,6 +42,16 @@ Instance Op_orb : BinOp orb := TBOpInj := ltac:(destruct n,m; reflexivity)}. Add BinOp Op_orb. +Instance Op_implb : BinOp implb := + { TBOp := fun x y => Z.max (1 - x) y; + TBOpInj := ltac:(destruct n,m; reflexivity) }. +Add BinOp Op_implb. + +Instance Op_xorb : BinOp xorb := + { TBOp := fun x y => Z.max (x - y) (y - x); + TBOpInj := ltac:(destruct n,m; reflexivity) }. +Add BinOp Op_xorb. + Instance Op_negb : UnOp negb := { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}. Add UnOp Op_negb. diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 66db924051..70c1077106 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -102,7 +102,7 @@ let bigint_of_z c = match DAst.get c with let rdefinitions = ["Coq";"Reals";"Rdefinitions"] let r_modpath = MPfile (make_dir rdefinitions) let r_base_modpath = MPdot (r_modpath, Label.make "RbaseSymbolsImpl") -let r_path = make_path rdefinitions "R" +let r_path = make_path ["Coq";"Reals";"Rdefinitions";"RbaseSymbolsImpl"] "R" let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR") let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult") diff --git a/tactics/declare.ml b/tactics/declare.ml index 7d32f1a7e8..57eeddb847 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -266,6 +266,7 @@ let get_roles export eff = List.map map export let feedback_axiom () = Feedback.(feedback AddedAxiom) + let is_unsafe_typing_flags () = let flags = Environ.typing_flags (Global.env()) in not (flags.check_universes && flags.check_guarded && flags.check_positive) @@ -375,132 +376,6 @@ let declare_variable ~name ~kind d = Impargs.declare_var_implicits ~impl name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) -(** Declaration of inductive blocks *) -let declare_inductive_argument_scopes kn mie = - List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope Evd.empty (GlobRef.IndRef (kn,i)); - for j=1 to List.length lc do - Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j)); - done) mie.mind_entry_inds - -type inductive_obj = { - ind_names : (Id.t * Id.t list) list - (* For each block, name of the type + name of constructors *) -} - -let inductive_names sp kn obj = - let (dp,_) = Libnames.repr_path sp in - let kn = Global.mind_of_delta_kn kn in - let names, _ = - List.fold_left - (fun (names, n) (typename, consnames) -> - let ind_p = (kn,n) in - let names, _ = - List.fold_left - (fun (names, p) l -> - let sp = - Libnames.make_path dp l - in - ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1)) - (names, 1) consnames in - let sp = Libnames.make_path dp typename - in - ((sp, GlobRef.IndRef ind_p) :: names, n+1)) - ([], 0) obj.ind_names - in names - -let load_inductive i ((sp, kn), names) = - let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names - -let open_inductive i ((sp, kn), names) = - let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names - -let cache_inductive ((sp, kn), names) = - let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names - -let discharge_inductive ((sp, kn), names) = - Some names - -let inInductive : inductive_obj -> obj = - declare_object {(default_object "INDUCTIVE") with - cache_function = cache_inductive; - load_function = load_inductive; - open_function = open_inductive; - classify_function = (fun a -> Substitute a); - subst_function = ident_subst_function; - discharge_function = discharge_inductive; - } - -let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c - -let load_prim _ p = cache_prim p - -let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c - -let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) - -let inPrim : (Projection.Repr.t * Constant.t) -> obj = - declare_object { - (default_object "PRIMPROJS") with - cache_function = cache_prim ; - load_function = load_prim; - subst_function = subst_prim; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_prim } - -let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) - -let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = - let name = Label.to_id label in - let univs, u = match univs with - | Monomorphic_entry _ -> - (* Global constraints already defined through the inductive *) - default_univ_entry, Univ.Instance.empty - | Polymorphic_entry (nas, ctx) -> - Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx - in - let term = Vars.subst_instance_constr u term in - let types = Vars.subst_instance_constr u types in - let entry = definition_entry ~types ~univs term in - let cst = declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (DefinitionEntry entry) in - let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - declare_primitive_projection p cst - -let declare_projections univs mind = - let env = Global.env () in - let mib = Environ.lookup_mind mind env in - match mib.mind_record with - | PrimRecord info -> - let iter_ind i (_, labs, _, _) = - let ind = (mind, i) in - let projs = Inductiveops.compute_projections env ind in - Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs - in - let () = Array.iteri iter_ind info in - true - | FakeRecord -> false - | NotRecord -> false - -(* for initial declaration *) -let declare_mind mie = - let id = match mie.mind_entry_inds with - | ind::_ -> ind.mind_entry_typename - | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in - let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in - let names = List.map map_names mie.mind_entry_inds in - List.iter (fun (typ, cons) -> check_exists typ; List.iter check_exists cons) names; - let _kn' = Global.add_mind id mie in - let (sp,kn as oname) = add_leaf id (inInductive { ind_names = names }) in - if is_unsafe_typing_flags() then feedback_axiom(); - let mind = Global.mind_of_delta_kn kn in - let isprim = declare_projections mie.mind_entry_universes mind in - Impargs.declare_mib_implicits mind; - declare_inductive_argument_scopes mind mie; - oname, isprim - (* Declaration messages *) let pr_rank i = pr_nth (i+1) @@ -538,106 +413,3 @@ let assumption_message id = the type of the object than to the name of the object (see discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") - -(** Global universes are not substitutive objects but global objects - bound at the *library* or *module* level. The polymorphic flag is - used to distinguish universes declared in polymorphic sections, which - are discharged and do not remain in scope. *) - -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 *) - | UnqualifiedUniv (* other global universe *) - -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 (AlreadyDeclared (Some "Universe", Libnames.basename sp)) - else () - -let qualify_univ i dp src id = - match src with - | BoundUniv | UnqualifiedUniv -> - i, Libnames.make_path dp id - | QualifiedUniv l -> - let dp = DirPath.repr dp in - Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id - -let do_univ_name ~check i dp src (id,univ) = - let i, sp = qualify_univ i dp src id in - if check then check_exists_universe sp; - Nametab.push_universe i sp univ - -let cache_univ_names ((sp, _), (src, univs)) = - let depth = sections_depth () in - let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in - List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs - -let load_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs - -let open_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs - -let discharge_univ_names = function - | _, (BoundUniv, _) -> None - | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x - -let input_univ_names : universe_name_decl -> Libobject.obj = - declare_object - { (default_object "Global universe name state") with - cache_function = cache_univ_names; - load_function = load_univ_names; - open_function = open_univ_names; - discharge_function = discharge_univ_names; - subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); - classify_function = (fun a -> Substitute a) } - -let declare_univ_binders gr pl = - if Global.is_polymorphic gr then - () - else - let l = let open GlobRef in match gr with - | ConstRef c -> Label.to_id @@ Constant.label c - | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> - CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") - | ConstructRef _ -> - CErrors.anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on an constructor reference") - in - let univs = Id.Map.fold (fun id univ univs -> - match Univ.Level.name univ with - | None -> assert false (* having Prop/Set/Var as binders is nonsense *) - | Some univ -> (id,univ)::univs) pl [] - in - Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) - -let do_universe ~poly l = - let in_section = Global.sections_are_opened () in - let () = - if poly && not in_section then - CErrors.user_err ~hdr:"Constraint" - (str"Cannot declare polymorphic universes outside sections") - in - let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in - let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) - Univ.LSet.empty l, Univ.Constraint.empty - in - let src = if poly then BoundUniv else UnqualifiedUniv in - let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in - declare_universe_context ~poly ctx - -let do_constraint ~poly l = - let open Univ in - let u_of_id x = - Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x - in - let constraints = List.fold_left (fun acc (l, d, r) -> - let lu = u_of_id l and ru = u_of_id r in - Constraint.add (lu, d, ru) acc) - Constraint.empty l - in - let uctx = ContextSet.add_constraints constraints ContextSet.empty in - declare_universe_context ~poly uctx diff --git a/tactics/declare.mli b/tactics/declare.mli index a6c1374a77..1a037ef937 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -43,6 +43,8 @@ type 'a constant_entry = | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry +val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit + val declare_variable : name:variable -> kind:Decls.logical_kind @@ -86,11 +88,6 @@ val declare_private_constant val set_declare_scheme : (string -> (inductive * Constant.t) array -> unit) -> unit -(** [declare_mind me] declares a block of inductive types with - their constructors in the current section; it returns the path of - the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool - (** Declaration messages *) val definition_message : Id.t -> unit @@ -100,15 +97,7 @@ val cofixpoint_message : Id.t list -> unit val recursive_message : bool (** true = fixpoint *) -> int array option -> Id.t list -> unit -val exists_name : Id.t -> bool - -(** Global universe contexts, names and constraints *) -val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit - -val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit - -val do_universe : poly:bool -> lident list -> unit -val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit +val check_exists : Id.t -> unit (* Used outside this module only in indschemes *) exception AlreadyDeclared of (string option * Id.t) diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index 381fbabe72..998f3f7dd1 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -419,13 +419,13 @@ Qed. -Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point, +Lemma Desargues: forall A B C A1 B1 C1 P Q T S:point, X S = 0 -> Y S = 0 -> Y A = 0 -> collinear A S A1 -> collinear B S B1 -> collinear C S C1 -> collinear B1 C1 P -> collinear B C P -> collinear A1 C1 Q -> collinear A C Q -> - collinear A1 B1 R -> collinear A B R -> - collinear P Q R + collinear A1 B1 T -> collinear A B T -> + collinear P Q T \/ X A = X B \/ X A = X C \/ X B = X C \/ X A = 0 \/ Y B = 0 \/ Y C = 0 \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1. Proof. @@ -440,8 +440,8 @@ let lv := rev (X A :: Y A1 :: X A1 :: Y B1 :: Y C1 - :: X R - :: Y R + :: X T + :: Y T :: X Q :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in nsatz with radicalmax :=1%N strategy:=0%Z diff --git a/theories/Logic/HLevels.v b/theories/Logic/HLevels.v new file mode 100644 index 0000000000..010c4aad6f --- /dev/null +++ b/theories/Logic/HLevels.v @@ -0,0 +1,146 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** The first three levels of homotopy type theory: homotopy propositions, + homotopy sets and homotopy one types. For more information, + https://github.com/HoTT/HoTT + and + https://homotopytypetheory.org/book + + Univalence is not assumed here, and equality is Coq's usual inductive + type eq in sort Prop. This is a little different from HoTT, where + sort Prop does not exist and equality is directly in sort Type. *) + + +(* It is almost impossible to prove that a type is a homotopy proposition + without funext, so we assume it here. *) +Require Import Coq.Logic.FunctionalExtensionality. + +(* A homotopy proposition is a type that has at most one element. + Its unique inhabitant, when it exists, is to be interpreted as the + proof of the homotopy proposition. + Homotopy propositions are therefore an alternative to the sort Prop, + to select which types represent mathematical propositions. *) +Definition IsHProp (P : Type) : Prop + := forall p q : P, p = q. + +(* A homotopy set is a type such as each equality type x = y is a + homotopy proposition. For example, any type which equality is + decidable in sort Prop is a homotopy set, as shown in file + Coq.Logic.Eqdep_dec.v. *) +Definition IsHSet (X : Type) : Prop + := forall (x y : X) (p q : x = y), p = q. + +Definition IsHOneType (X : Type) : Prop + := forall (x y : X) (p q : x = y) (r s : p = q), r = s. + +Lemma forall_hprop : forall (A : Type) (P : A -> Prop), + (forall x:A, IsHProp (P x)) + -> IsHProp (forall x:A, P x). +Proof. + intros A P H p q. apply functional_extensionality_dep. + intro x. apply H. +Qed. + +(* Homotopy propositions are stable by conjunction, but not by disjunction, + which can have a proof by the left and another proof by the right. *) +Lemma and_hprop : forall P Q : Prop, + IsHProp P -> IsHProp Q -> IsHProp (P /\ Q). +Proof. + intros. intros p q. destruct p,q. + replace p0 with p. replace q0 with q. reflexivity. + apply H0. apply H. +Qed. + +Lemma impl_hprop : forall P Q : Prop, + IsHProp Q -> IsHProp (P -> Q). +Proof. + intros P Q H p q. apply functional_extensionality. + intros. apply H. +Qed. + +Lemma false_hprop : IsHProp False. +Proof. + intros p q. contradiction. +Qed. + +Lemma true_hprop : IsHProp True. +Proof. + intros p q. destruct p,q. reflexivity. +Qed. + +(* All negations are homotopy propositions. *) +Lemma not_hprop : forall P : Type, IsHProp (P -> False). +Proof. + intros P p q. apply functional_extensionality. + intros. contradiction. +Qed. + +(* Homotopy propositions are included in homotopy sets. + They are the first 2 levels of a cumulative hierarchy of types + indexed by the natural numbers. In homotopy type theory, + homotopy propositions are call (-1)-types and homotopy + sets 0-types. *) +Lemma hset_hprop : forall X : Type, + IsHProp X -> IsHSet X. +Proof. + intros X H. + assert (forall (x y z:X) (p : y = z), eq_trans (H x y) p = H x z). + { intros. unfold eq_trans, eq_ind. destruct p. reflexivity. } + assert (forall (x y z:X) (p : y = z), + p = eq_trans (eq_sym (H x y)) (H x z)). + { intros. rewrite <- (H0 x y z p). unfold eq_trans, eq_sym, eq_ind. + destruct p, (H x y). reflexivity. } + intros x y p q. + rewrite (H1 x x y p), (H1 x x y q). reflexivity. +Qed. + +Lemma eq_trans_cancel : forall {X : Type} {x y z : X} (p : x = y) (q r : y = z), + (eq_trans p q = eq_trans p r) -> q = r. +Proof. + intros. destruct p. simpl in H. destruct r. + simpl in H. rewrite eq_trans_refl_l in H. exact H. +Qed. + +Lemma hset_hOneType : forall X : Type, + IsHSet X -> IsHOneType X. +Proof. + intros X f x y p q. + pose (fun a => f x y p a) as g. + assert (forall a (r : q = a), eq_trans (g q) r = g a). + { intros. destruct a. subst q. reflexivity. } + intros r s. pose proof (H p (eq_sym r)). + pose proof (H p (eq_sym s)). + rewrite <- H1 in H0. apply eq_trans_cancel in H0. + rewrite <- eq_sym_involutive. rewrite <- (eq_sym_involutive r). + rewrite H0. reflexivity. +Qed. + +(* "IsHProp X" sounds like a proposition, because it asserts + a property of the type X. And indeed: *) +Lemma hprop_hprop : forall X : Type, + IsHProp (IsHProp X). +Proof. + intros X p q. + apply forall_hprop. intro x. + apply forall_hprop. intro y. intros f g. + apply (hset_hprop X p). +Qed. + +Lemma hprop_hset : forall X : Type, + IsHProp (IsHSet X). +Proof. + intros X f g. + apply functional_extensionality_dep. intro x. + apply functional_extensionality_dep. intro y. + apply functional_extensionality_dep. intro a. + apply functional_extensionality_dep. intro b. + apply (hset_hOneType). exact f. +Qed. diff --git a/theories/Reals/ClassicalDedekindReals.v b/theories/Reals/ClassicalDedekindReals.v new file mode 100644 index 0000000000..e32def29b8 --- /dev/null +++ b/theories/Reals/ClassicalDedekindReals.v @@ -0,0 +1,465 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Coq.Logic.Eqdep_dec. +Require Import Coq.Logic.FunctionalExtensionality. +Require Import Coq.Logic.HLevels. +Require Import QArith. +Require Import Qabs. +Require Import ConstructiveCauchyReals. +Require Import ConstructiveRcomplete. + +(** + Classical Dedekind reals. With the 3 logical axioms funext, + sig_forall_dec and sig_not_dec, the lower cuts defined as + functions Q -> bool have all the classical properties of the + real numbers. + + We could prove operations and theorems about them directly, + but instead we notice that they are a quotient of the + constructive Cauchy reals, from which they inherit many properties. +*) + +(* The limited principle of omniscience *) +Axiom sig_forall_dec + : forall (P : nat -> Prop), + (forall n, {P n} + {~P n}) + -> {n | ~P n} + {forall n, P n}. + +Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }. + +(* Try to find a surjection CReal -> lower cuts. *) +Definition isLowerCut (f : Q -> bool) : Prop + := (forall q r:Q, Qle q r -> f r = true -> f q = true) (* interval *) + /\ ~(forall q:Q, f q = true) (* avoid positive infinity *) + /\ ~(forall q:Q, f q = false) (* avoid negative infinity *) + (* openness, the cut contains rational numbers + strictly lower than a real number. *) + /\ (forall q:Q, f q = true -> ~(forall r:Q, Qle r q \/ f r = false)). + +Lemma isLowerCut_hprop : forall (f : Q -> bool), + IsHProp (isLowerCut f). +Proof. + intro f. apply and_hprop. + 2: apply and_hprop. 2: apply not_hprop. + 2: apply and_hprop. 2: apply not_hprop. + - apply forall_hprop. intro x. + apply forall_hprop. intro y. + apply impl_hprop. apply impl_hprop. + intros p q. apply eq_proofs_unicity_on. + intro b. destruct (f x), b. + left. reflexivity. right. discriminate. + right. discriminate. left. reflexivity. + - apply forall_hprop. intro q. apply impl_hprop. apply not_hprop. +Qed. + +Lemma lowerCutBelow : forall f : Q -> bool, + isLowerCut f -> { q : Q | f q = true }. +Proof. + intros. + destruct (sig_forall_dec (fun n:nat => f (-(Z.of_nat n # 1))%Q = false)). + - intro n. destruct (f (-(Z.of_nat n # 1))%Q). + right. discriminate. left. reflexivity. + - destruct s. exists (-(Z.of_nat x # 1))%Q. + destruct (f (-(Z.of_nat x # 1))%Q). + reflexivity. exfalso. apply n. reflexivity. + - exfalso. destruct H, H0, H1. apply H1. intro q. + destruct (f q) eqn:des. 2: reflexivity. exfalso. + destruct (Qarchimedean (-q)) as [p pmaj]. + rewrite <- (Qplus_lt_l _ _ (q-(Z.pos p # 1))) in pmaj. + ring_simplify in pmaj. + specialize (H (- (Z.pos p#1))%Q q). + specialize (e (Pos.to_nat p)). + rewrite positive_nat_Z in e. rewrite H in e. discriminate. + 2: exact des. ring_simplify. apply Qlt_le_weak, pmaj. +Qed. + +Lemma lowerCutAbove : forall f : Q -> bool, + isLowerCut f -> { q : Q | f q = false }. +Proof. + intros. + destruct (sig_forall_dec (fun n => f (Z.of_nat n # 1)%Q = true)). + - intro n. destruct (f (Z.of_nat n # 1)%Q). + left. reflexivity. right. discriminate. + - destruct s. exists (Z.of_nat x # 1)%Q. destruct (f (Z.of_nat x # 1)%Q). + exfalso. apply n. reflexivity. reflexivity. + - exfalso. destruct H, H0, H1. apply H0. intro q. + destruct (Qarchimedean q) as [p pmaj]. + apply (H q (Z.of_nat (Pos.to_nat p) # 1)%Q). + rewrite positive_nat_Z. apply Qlt_le_weak, pmaj. apply e. +Qed. + +Definition DReal : Set + := { f : Q -> bool | isLowerCut f }. + +Fixpoint DRealQlim_rec (f : Q -> bool) (low : isLowerCut f) (n p : nat) { struct p } + : f (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q = false + -> { q : Q | f q = true /\ f (q + (1 # Pos.of_nat (S n)))%Q = false }. +Proof. + intros. destruct p. + - exfalso. destruct (lowerCutBelow f low); unfold proj1_sig in H. + destruct low. rewrite (H0 _ x) in H. discriminate. simpl. + apply (Qplus_le_l _ _ (-x)). ring_simplify. discriminate. exact e. + - destruct (f (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q) eqn:des. + + exists (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q. + split. exact des. + destruct (f (proj1_sig (lowerCutBelow f low) + + (Z.of_nat p # Pos.of_nat (S n)) + (1 # Pos.of_nat (S n)))%Q) eqn:d. + 2: reflexivity. exfalso. + destruct low. + rewrite (e _ (proj1_sig (lowerCutBelow f (conj e a)) + (Z.of_nat p # Pos.of_nat (S n)) + (1 # Pos.of_nat (S n))))%Q in H. + discriminate. 2: exact d. rewrite <- Qplus_assoc, Qplus_le_r. + rewrite Qinv_plus_distr. + replace (Z.of_nat p + 1)%Z with (Z.of_nat (S p))%Z. apply Qle_refl. + replace 1%Z with (Z.of_nat 1). rewrite <- (Nat2Z.inj_add p 1). + apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity. + + destruct (DRealQlim_rec f low n p des) as [q qmaj]. + exists q. exact qmaj. +Qed. + +Definition DRealQlim (x : DReal) (n : nat) + : { q : Q | proj1_sig x q = true /\ proj1_sig x (q + (1# Pos.of_nat (S n)))%Q = false }. +Proof. + destruct x as [f low]. + destruct (lowerCutAbove f low). + destruct (Qarchimedean (x - proj1_sig (lowerCutBelow f low))) as [p pmaj]. + apply (DRealQlim_rec f low n ((S n) * Pos.to_nat p)). + destruct (lowerCutBelow f low); unfold proj1_sig; unfold proj1_sig in pmaj. + destruct (f (x0 + (Z.of_nat (S n * Pos.to_nat p) # Pos.of_nat (S n)))%Q) eqn:des. + 2: reflexivity. exfalso. destruct low. + rewrite (H _ (x0 + (Z.of_nat (S n * Pos.to_nat p) # Pos.of_nat (S n)))%Q) in e. + discriminate. 2: exact des. + setoid_replace (Z.of_nat (S n * Pos.to_nat p) # Pos.of_nat (S n))%Q with (Z.pos p # 1)%Q. + apply (Qplus_lt_l _ _ x0) in pmaj. ring_simplify in pmaj. + apply Qlt_le_weak, pmaj. rewrite Nat2Z.inj_mul, positive_nat_Z. + unfold Qeq, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_comm. + replace (Z.of_nat (S n)) with (Z.pos (Pos.of_nat (S n))). reflexivity. + simpl. destruct n. reflexivity. apply f_equal. + apply Pos.succ_of_nat. discriminate. +Qed. + +Definition DRealAbstr : CReal -> DReal. +Proof. + intro x. + assert (forall (q : Q) (n : nat), + {(fun n0 : nat => (proj1_sig x (S n0) <= q + (1 # Pos.of_nat (S n0)))%Q) n} + + {~ (fun n0 : nat => (proj1_sig x (S n0) <= q + (1 # Pos.of_nat (S n0)))%Q) n}). + { intros. destruct (Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (proj1_sig x (S n))). + right. apply (Qlt_not_le _ _ q0). left. exact q0. } + + exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (proj1_sig x (S n)) (q + (1#Pos.of_nat (S n)))) (H q) + then true else false). + repeat split. + - intros. + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q) + (H q)). + reflexivity. exfalso. + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= r + (1 # Pos.of_nat (S n)))%Q) + (H r)). + destruct s. apply n. + apply (Qle_trans _ _ _ (q0 x0)). + apply Qplus_le_l. exact H0. discriminate. + - intro abs. destruct (Rfloor x) as [z [_ zmaj]]. + specialize (abs (z+3 # 1)%Q). + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= (z+3 # 1) + (1 # Pos.of_nat (S n)))%Q) + (H (z+3 # 1)%Q)). + 2: exfalso; discriminate. clear abs. destruct s as [n nmaj]. apply nmaj. + rewrite <- (inject_Q_plus (z#1) 2) in zmaj. + apply CRealLt_asym in zmaj. rewrite <- CRealLe_not_lt in zmaj. + specialize (zmaj (Pos.of_nat (S n))). unfold inject_Q, proj1_sig in zmaj. + rewrite Nat2Pos.id in zmaj. 2: discriminate. + destruct x as [xn xcau]; unfold proj1_sig. + rewrite Qinv_plus_distr in zmaj. + apply (Qplus_le_l _ _ (-(z + 2 # 1))). apply (Qle_trans _ _ _ zmaj). + apply (Qplus_le_l _ _ (-(1 # Pos.of_nat (S n)))). apply (Qle_trans _ 1). + unfold Qopp, Qnum, Qden. rewrite Qinv_plus_distr. + unfold Qle, Qnum, Qden. apply Z2Nat.inj_le. discriminate. discriminate. + do 2 rewrite Z.mul_1_l. unfold Z.to_nat. rewrite Nat2Pos.id. 2: discriminate. + apply le_n_S, le_0_n. setoid_replace (- (z + 2 # 1))%Q with (-(z+2) #1)%Q. + 2: reflexivity. ring_simplify. rewrite Qinv_plus_distr. + replace (z + 3 + - (z + 2))%Z with 1%Z. apply Qle_refl. ring. + - intro abs. destruct (Rfloor x) as [z [zmaj _]]. + specialize (abs (z-4 # 1)%Q). + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= (z-4 # 1) + (1 # Pos.of_nat (S n)))%Q) + (H (z-4 # 1)%Q)). + exfalso; discriminate. clear abs. + apply CRealLt_asym in zmaj. apply zmaj. clear zmaj. + exists 1%positive. unfold inject_Q, proj1_sig. + specialize (q O). + destruct x as [xn xcau]; unfold proj1_sig; unfold proj1_sig in q. + unfold Pos.of_nat in q. rewrite Qinv_plus_distr in q. + unfold Pos.to_nat; simpl. apply (Qplus_lt_l _ _ (xn 1%nat - 2)). + ring_simplify. rewrite Qinv_plus_distr. + apply (Qle_lt_trans _ _ _ q). apply Qlt_minus_iff. + unfold Qopp, Qnum, Qden. rewrite Qinv_plus_distr. + replace (z + -2 + - (z - 4 + 1))%Z with 1%Z. 2: ring. reflexivity. + - intros q H0 abs. + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q) (H q)). + 2: exfalso; discriminate. clear H0. + destruct x as [xn xcau]; unfold proj1_sig in abs, s. + destruct s as [n nmaj]. + (* We have that q < x as real numbers. The middle + (q + xSn - 1/Sn)/2 is also lower than x, witnessed by the same index n. *) + specialize (abs ((q + xn (S n) - (1 # Pos.of_nat (S n))%Q)/2)%Q). + destruct abs. + + apply (Qmult_le_r _ _ 2) in H0. field_simplify in H0. + apply (Qplus_le_r _ _ ((1 # Pos.of_nat (S n)) - q)) in H0. + ring_simplify in H0. apply nmaj. rewrite Qplus_comm. exact H0. reflexivity. + + destruct (sig_forall_dec + (fun n0 : nat => + (xn (S n0) <= (q + xn (S n) - (1 # Pos.of_nat (S n))) / 2 + (1 # Pos.of_nat (S n0)))%Q) + (H ((q + xn (S n) - (1 # Pos.of_nat (S n))) / 2)%Q)). + discriminate. clear H0. specialize (q0 n). + apply (Qmult_le_l _ _ 2) in q0. field_simplify in q0. + apply (Qplus_le_l _ _ (-xn (S n))) in q0. ring_simplify in q0. + contradiction. reflexivity. +Defined. + +Lemma UpperAboveLower : forall (f : Q -> bool) (q r : Q), + isLowerCut f + -> f q = true + -> f r = false + -> Qlt q r. +Proof. + intros. destruct H. apply Qnot_le_lt. intro abs. + rewrite (H r q abs) in H1. discriminate. exact H0. +Qed. + +Definition DRealRepr : DReal -> CReal. +Proof. + intro x. exists (fun n => proj1_sig (DRealQlim x n)). + intros n p q H H0. + destruct (DRealQlim x p), (DRealQlim x q); unfold proj1_sig. + destruct x as [f low]; unfold proj1_sig in a0, a. + apply Qabs_case. + - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (S q))). + apply (Qplus_lt_l _ _ x1). ring_simplify. apply (UpperAboveLower f). + exact low. apply a. apply a0. unfold Qle, Qnum, Qden. + do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. + apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply (le_trans _ _ _ H0), le_S, le_refl. + discriminate. + - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (S p))). + apply (Qplus_lt_l _ _ x0). ring_simplify. apply (UpperAboveLower f). + exact low. apply a0. apply a. unfold Qle, Qnum, Qden. + do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. + apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply (le_trans _ _ _ H), le_S, le_refl. + discriminate. +Defined. + +Definition Rle (x y : DReal) + := forall q:Q, proj1_sig x q = true -> proj1_sig y q = true. + +Lemma Rle_antisym : forall x y : DReal, + Rle x y + -> Rle y x + -> x = y. +Proof. + intros [f cf] [g cg] H H0. unfold Rle in H,H0; simpl in H, H0. + assert (f = g). + { apply functional_extensionality. intro q. + specialize (H q). specialize (H0 q). + destruct (f q), (g q). reflexivity. + exfalso. specialize (H (eq_refl _)). discriminate. + exfalso. specialize (H0 (eq_refl _)). discriminate. + reflexivity. } + subst g. replace cg with cf. reflexivity. + apply isLowerCut_hprop. +Qed. + +Lemma lowerUpper : forall (f : Q -> bool) (q r : Q), + isLowerCut f -> Qle q r -> f q = false -> f r = false. +Proof. + intros. destruct H. specialize (H q r H0). destruct (f r) eqn:desR. + 2: reflexivity. exfalso. specialize (H (eq_refl _)). + rewrite H in H1. discriminate. +Qed. + +Lemma DRealOpen : forall (x : DReal) (q : Q), + proj1_sig x q = true + -> { r : Q | Qlt q r /\ proj1_sig x r = true }. +Proof. + intros. + destruct (sig_forall_dec (fun n => Qle (proj1_sig (DRealQlim x n)) q)). + - intro n. destruct (DRealQlim x n); unfold proj1_sig. + destruct (Qlt_le_dec q x0). right. exact (Qlt_not_le _ _ q0). + left. exact q0. + - destruct s. apply Qnot_le_lt in n. + destruct (DRealQlim x x0); unfold proj1_sig in n. + exists x1. split. exact n. apply a. + - exfalso. destruct x as [f low]. unfold proj1_sig in H, q0. + destruct low, a, a. apply (n1 q H). intros. + destruct (Qlt_le_dec q r). 2: left; exact q1. right. + destruct (Qarchimedean (/(r - q))) as [p pmaj]. + specialize (q0 (Pos.to_nat p)). + destruct (DRealQlim (exist _ f (conj e (conj n (conj n0 n1)))) (Pos.to_nat p)) + as [s smaj]. + unfold proj1_sig in smaj. + apply (lowerUpper f (s + (1 # Pos.of_nat (S (Pos.to_nat p))))). + exact (conj e (conj n (conj n0 n1))). + 2: apply smaj. apply (Qle_trans _ (s + (r-q))). + apply Qplus_le_r. apply (Qle_trans _ (1 # p)). + unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. + apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. + rewrite Nat2Pos.id. apply le_S, le_refl. discriminate. + apply (Qmult_le_l _ _ ( (Z.pos p # 1) / (r-q))). + rewrite <- (Qmult_0_r (Z.pos p #1)). apply Qmult_lt_l. + reflexivity. apply Qinv_lt_0_compat. + unfold Qminus. rewrite <- Qlt_minus_iff. exact q1. + unfold Qdiv. rewrite Qmult_comm, <- Qmult_assoc. + rewrite (Qmult_comm (/(r-q))), Qmult_inv_r, Qmult_assoc. + setoid_replace ((1 # p) * (Z.pos p # 1))%Q with 1%Q. + 2: reflexivity. rewrite Qmult_1_l, Qmult_1_r. + apply Qlt_le_weak, pmaj. intro abs. apply Qlt_minus_iff in q1. + rewrite abs in q1. apply (Qlt_not_le _ _ q1), Qle_refl. + apply (Qplus_le_l _ _ (q-r)). ring_simplify. exact q0. +Qed. + +Lemma DRealReprQ : forall (x : DReal) (q : Q), + proj1_sig x q = true + -> CRealLt (inject_Q q) (DRealRepr x). +Proof. + intros. + destruct (DRealOpen x q H) as [r rmaj]. + destruct (Qarchimedean (4/(r - q))) as [p pmaj]. + exists p. + destruct x as [f low]; unfold DRealRepr, inject_Q, proj1_sig. + destruct (DRealQlim (exist _ f low) (Pos.to_nat p)) as [s smaj]. + unfold proj1_sig in smaj, rmaj. + apply (Qplus_lt_l _ _ (q+ (1 # Pos.of_nat (S (Pos.to_nat p))))). + ring_simplify. rewrite <- (Qplus_comm s). + apply (UpperAboveLower f _ _ low). 2: apply smaj. + destruct low. apply (e _ r). 2: apply rmaj. + rewrite <- (Qplus_comm q). + apply (Qle_trans _ (q + (4#p))). + - rewrite <- Qplus_assoc. apply Qplus_le_r. + apply (Qle_trans _ ((2#p) + (1#p))). + apply Qplus_le_r. + unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. + apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. + rewrite Nat2Pos.id. apply le_S, le_refl. discriminate. + rewrite Qinv_plus_distr. unfold Qle, Qnum, Qden. + apply Z.mul_le_mono_nonneg_r. discriminate. discriminate. + - apply (Qle_trans _ (q + (r-q))). 2: ring_simplify; apply Qle_refl. + apply Qplus_le_r. + apply (Qmult_le_l _ _ ( (Z.pos p # 1) / (r-q))). + rewrite <- (Qmult_0_r (Z.pos p #1)). apply Qmult_lt_l. + reflexivity. apply Qinv_lt_0_compat. + unfold Qminus. rewrite <- Qlt_minus_iff. apply rmaj. + unfold Qdiv. rewrite Qmult_comm, <- Qmult_assoc. + rewrite (Qmult_comm (/(r-q))), Qmult_inv_r, Qmult_assoc. + setoid_replace ((4 # p) * (Z.pos p # 1))%Q with 4%Q. + 2: reflexivity. rewrite Qmult_1_r. + apply Qlt_le_weak, pmaj. intro abs. destruct rmaj. + apply Qlt_minus_iff in H0. + rewrite abs in H0. apply (Qlt_not_le _ _ H0), Qle_refl. +Qed. + +Lemma DRealReprQup : forall (x : DReal) (q : Q), + proj1_sig x q = false + -> CRealLe (DRealRepr x) (inject_Q q). +Proof. + intros x q H [p pmaj]. + unfold inject_Q, DRealRepr, proj1_sig in pmaj. + destruct (DRealQlim x (Pos.to_nat p)) as [r rmaj], rmaj. + clear H1. destruct x as [f low], low; unfold proj1_sig in H, H0. + apply (Qplus_lt_l _ _ q) in pmaj. ring_simplify in pmaj. + rewrite (e _ r) in H. discriminate. 2: exact H0. + apply Qlt_le_weak. apply (Qlt_trans _ ((2#p)+q)). 2: exact pmaj. + apply (Qplus_lt_l _ _ (-q)). ring_simplify. reflexivity. +Qed. + +Lemma DRealQuot1 : forall x y:DReal, CRealEq (DRealRepr x) (DRealRepr y) -> x = y. +Proof. + intros. destruct H. apply Rle_antisym. + - clear H. intros q H1. destruct (proj1_sig y q) eqn:des. + reflexivity. exfalso. apply H0. + apply (CReal_le_lt_trans _ (inject_Q q)). apply DRealReprQup. + exact des. apply DRealReprQ. exact H1. + - clear H0. intros q H1. destruct (proj1_sig x q) eqn:des. + reflexivity. exfalso. apply H. + apply (CReal_le_lt_trans _ (inject_Q q)). apply DRealReprQup. + exact des. apply DRealReprQ. exact H1. +Qed. + +Lemma DRealAbstrFalse : forall (x : CReal) (q : Q) (n : nat), + proj1_sig (DRealAbstr x) q = false + -> (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q. +Proof. + intros. destruct x as [xn xcau]. + unfold DRealAbstr, proj1_sig in H. + destruct ( + sig_forall_dec (fun n : nat => (xn (S n) <= q + (1 # Pos.of_nat (S n)))%Q) + (fun n : nat => + match Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (xn (S n)) with + | left q0 => right (Qlt_not_le (q + (1 # Pos.of_nat (S n))) (xn (S n)) q0) + | right q0 => left q0 + end)). + discriminate. apply q0. +Qed. + +Lemma DRealQuot2 : forall x:CReal, CRealEq (DRealRepr (DRealAbstr x)) x. +Proof. + split. + - intros [p pmaj]. unfold DRealRepr, proj1_sig in pmaj. + destruct x as [xn xcau]. + destruct (DRealQlim (DRealAbstr (exist _ xn xcau)) (Pos.to_nat p)) + as [q [_ qmaj]]. + (* By pmaj, q + 1/p < x as real numbers. + But by qmaj x <= q + 1/(p+1), contradiction. *) + apply (DRealAbstrFalse _ _ (pred (Pos.to_nat p))) in qmaj. + unfold proj1_sig in qmaj. + rewrite Nat.succ_pred in qmaj. + apply (Qlt_not_le _ _ pmaj), (Qplus_le_l _ _ q). + ring_simplify. apply (Qle_trans _ _ _ qmaj). + rewrite <- Qplus_assoc. apply Qplus_le_r. + rewrite Pos2Nat.id. apply (Qle_trans _ ((1#p)+(1#p))). + apply Qplus_le_l. unfold Qle, Qnum, Qden. + do 2 rewrite Z.mul_1_l. + apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. + rewrite Nat2Pos.id. apply le_S, le_refl. discriminate. + rewrite Qinv_plus_distr. apply Qle_refl. + intro abs. pose proof (Pos2Nat.is_pos p). + rewrite abs in H. inversion H. + - intros [p pmaj]. unfold DRealRepr, proj1_sig in pmaj. + destruct x as [xn xcau]. + destruct (DRealQlim (DRealAbstr (exist _ xn xcau)) (Pos.to_nat p)) + as [q [qmaj _]]. + (* By pmaj, x < q - 1/p *) + unfold DRealAbstr, proj1_sig in qmaj. + destruct ( + sig_forall_dec (fun n : nat => (xn (S n) <= q + (1 # Pos.of_nat (S n)))%Q) + (fun n : nat => + match Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (xn (S n)) with + | left q0 => + right (Qlt_not_le (q + (1 # Pos.of_nat (S n))) (xn (S n)) q0) + | right q0 => left q0 + end)). + 2: discriminate. clear qmaj. + destruct s as [n nmaj]. apply nmaj. + apply (Qplus_lt_l _ _ (xn (Pos.to_nat p) + (1#Pos.of_nat (S n)))) in pmaj. + ring_simplify in pmaj. apply Qlt_le_weak. rewrite Qplus_comm. + apply (Qlt_trans _ ((2 # p) + xn (Pos.to_nat p) + (1 # Pos.of_nat (S n)))). + 2: exact pmaj. + apply (Qplus_lt_l _ _ (-xn (Pos.to_nat p))). + apply (Qle_lt_trans _ _ _ (Qle_Qabs _)). + destruct (le_lt_dec (S n) (Pos.to_nat p)). + + specialize (xcau (Pos.of_nat (S n)) (S n) (Pos.to_nat p)). + apply (Qlt_trans _ (1# Pos.of_nat (S n))). apply xcau. + rewrite Nat2Pos.id. apply le_refl. discriminate. + rewrite Nat2Pos.id. exact l. discriminate. + apply (Qplus_lt_l _ _ (-(1#Pos.of_nat (S n)))). + ring_simplify. reflexivity. + + apply (Qlt_trans _ (1#p)). apply xcau. + apply le_S_n in l. apply le_S, l. apply le_refl. + ring_simplify. apply (Qlt_trans _ (2#p)). + unfold Qlt, Qnum, Qden. + apply Z.mul_lt_mono_pos_r. reflexivity. reflexivity. + apply (Qplus_lt_l _ _ (-(2#p))). ring_simplify. reflexivity. +Qed. diff --git a/theories/Reals/ConstructiveCauchyReals.v b/theories/Reals/ConstructiveCauchyReals.v index 965d31d403..b83f8581d0 100644 --- a/theories/Reals/ConstructiveCauchyReals.v +++ b/theories/Reals/ConstructiveCauchyReals.v @@ -16,15 +16,7 @@ Require Import Logic.ConstructiveEpsilon. Require CMorphisms. (** The constructive Cauchy real numbers, ie the Cauchy sequences - of rational numbers. This file is not supposed to be imported, - except in Rdefinitions.v, Raxioms.v, Rcomplete_constr.v - and ConstructiveRIneq.v. - - Constructive real numbers should be considered abstractly, - forgetting the fact that they are implemented as rational sequences. - All useful lemmas of this file are exposed in ConstructiveRIneq.v, - under more abstract names, like Rlt_asym instead of CRealLt_asym. - + of rational numbers. Cauchy reals are Cauchy sequences of rational numbers, equipped with explicit moduli of convergence and @@ -705,6 +697,17 @@ Proof. right. rewrite H0, H. exact c. Qed. +Add Parametric Morphism : CRealLtProp + with signature CRealEq ==> CRealEq ==> iff + as CRealLtProp_morph. +Proof. + intros x y H x0 y0 H0. split. + - intro. apply CRealLtForget. apply CRealLtEpsilon in H1. + rewrite <- H, <- H0. exact H1. + - intro. apply CRealLtForget. apply CRealLtEpsilon in H1. + rewrite H, H0. exact H1. +Qed. + Add Parametric Morphism : CRealLe with signature CRealEq ==> CRealEq ==> iff as CRealLe_morph. @@ -772,6 +775,9 @@ Proof. intro q. exists (fun n => q). apply ConstCauchy. Defined. +Definition inject_Z : Z -> CReal + := fun n => inject_Q (n # 1). + Notation "0" := (inject_Q 0) : CReal_scope. Notation "1" := (inject_Q 1) : CReal_scope. Notation "2" := (inject_Q 2) : CReal_scope. @@ -1324,3 +1330,19 @@ Proof. apply (Qlt_not_le _ _ maj). apply (Qle_trans _ 0). apply (Qplus_le_l _ _ r). ring_simplify. exact H. discriminate. Qed. + +Lemma inject_Z_plus : forall q r : Z, + inject_Z (q + r) == inject_Z q + inject_Z r. +Proof. + intros. unfold inject_Z. + setoid_replace (q + r # 1)%Q with ((q#1) + (r#1))%Q. + apply inject_Q_plus. rewrite Qinv_plus_distr. reflexivity. +Qed. + +Lemma opp_inject_Z : forall n : Z, + inject_Z (-n) == - inject_Z n. +Proof. + intros. unfold inject_Z. + setoid_replace (-n # 1)%Q with (-(n#1))%Q. + rewrite opp_inject_Q. reflexivity. reflexivity. +Qed. diff --git a/theories/Reals/ConstructiveRIneq.v b/theories/Reals/ConstructiveRIneq.v deleted file mode 100644 index e0f08d2fbe..0000000000 --- a/theories/Reals/ConstructiveRIneq.v +++ /dev/null @@ -1,2817 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(************************************************************************) - -(*********************************************************) -(** * Basic lemmas for the contructive real numbers *) -(*********************************************************) - -(* Implement interface ConstructiveReals opaquely with - Cauchy reals and prove basic results. - Those are therefore true for any implementation of - ConstructiveReals (for example with Dedekind reals). - - This file is the recommended import for working with - constructive reals, do not use ConstructiveCauchyReals - directly. *) - -Require Import ConstructiveCauchyRealsMult. -Require Import ConstructiveRcomplete. -Require Export ConstructiveReals. -Require Import Zpower. -Require Export ZArithRing. -Require Import Omega. -Require Import QArith_base. -Require Import Qring. - -Declare Scope R_scope_constr. - -Local Open Scope Z_scope. -Local Open Scope R_scope_constr. - -Definition CRealImplem : ConstructiveReals. -Proof. - assert (isLinearOrder CReal CRealLt) as lin. - { repeat split. exact CRealLt_asym. - exact CReal_lt_trans. - intros. destruct (CRealLt_dec x z y H). - left. exact c. right. exact c. } - apply (Build_ConstructiveReals - CReal CRealLt lin CRealLtProp - CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon - (inject_Q 0) (inject_Q 1) - CReal_plus CReal_opp CReal_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). - - intros. destruct (Rcauchy_complete xn) as [l cv]. - intro n. destruct (H n). exists x. intros. - specialize (a i j H0 H1) as [a b]. split. 2: exact b. - rewrite <- opp_inject_Q. - setoid_replace (-(1#n))%Q with (-1#n). exact a. reflexivity. - exists l. intros p. destruct (cv p). - exists x. intros. specialize (a i H0). split. 2: apply a. - unfold orderLe. - intro abs. setoid_replace (-1#p) with (-(1#p))%Q in abs. - rewrite opp_inject_Q in abs. destruct a. contradiction. - reflexivity. -Defined. - -Definition CR : ConstructiveReals. -Proof. - exact CRealImplem. -Qed. (* Keep it opaque to possibly change the implementation later *) - -Definition R := CRcarrier CR. - -Definition Req := orderEq R (CRlt CR). -Definition Rle (x y : R) := CRlt CR y x -> False. -Definition Rge (x y : R) := CRlt CR x y -> False. -Definition Rlt := CRlt CR. -Definition RltProp := CRltProp CR. -Definition Rgt (x y : R) := CRlt CR y x. -Definition Rappart := orderAppart R (CRlt CR). - -Infix "==" := Req : R_scope_constr. -Infix "#" := Rappart : R_scope_constr. -Infix "<" := Rlt : R_scope_constr. -Infix ">" := Rgt : R_scope_constr. -Infix "<=" := Rle : R_scope_constr. -Infix ">=" := Rge : R_scope_constr. - -Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope_constr. -Notation "x <= y < z" := (prod (x <= y) (y < z)) : R_scope_constr. -Notation "x < y < z" := (prod (x < y) (y < z)) : R_scope_constr. -Notation "x < y <= z" := (prod (x < y) (y <= z)) : R_scope_constr. - -Lemma Rlt_epsilon : forall x y : R, RltProp x y -> x < y. -Proof. - exact (CRltEpsilon CR). -Qed. - -Lemma Rlt_forget : forall x y : R, x < y -> RltProp x y. -Proof. - exact (CRltForget CR). -Qed. - -Lemma Rle_refl : forall x : R, x <= x. -Proof. - intros. intro abs. - destruct (CRltLinear CR), p. - exact (f x x abs abs). -Qed. -Hint Immediate Rle_refl: rorders. - -Lemma Req_refl : forall x : R, x == x. -Proof. - intros. split; apply Rle_refl. -Qed. - -Lemma Req_sym : forall x y : R, x == y -> y == x. -Proof. - intros. destruct H. split; intro abs; contradiction. -Qed. - -Lemma Req_trans : forall x y z : R, x == y -> y == z -> x == z. -Proof. - intros. destruct H,H0. destruct (CRltLinear CR), p. split. - - intro abs. destruct (s _ y _ abs); contradiction. - - intro abs. destruct (s _ y _ abs); contradiction. -Qed. - -Add Parametric Relation : R Req - reflexivity proved by Req_refl - symmetry proved by Req_sym - transitivity proved by Req_trans - as Req_rel. - -Instance Req_relT : CRelationClasses.Equivalence Req. -Proof. - split. exact Req_refl. exact Req_sym. exact Req_trans. -Qed. - -Lemma linear_order_T : forall x y z : R, - x < z -> (x < y) + (y < z). -Proof. - intros. destruct (CRltLinear CR). apply s. exact H. -Qed. - -Instance Rlt_morph - : CMorphisms.Proper - (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rlt. -Proof. - intros x y H x0 y0 H0. destruct H, H0. split. - - intro. destruct (linear_order_T x y x0). assumption. - contradiction. destruct (linear_order_T y y0 x0). - assumption. assumption. contradiction. - - intro. destruct (linear_order_T y x y0). assumption. - contradiction. destruct (linear_order_T x x0 y0). - assumption. assumption. contradiction. -Qed. - -Instance RltProp_morph - : Morphisms.Proper - (Morphisms.respectful Req (Morphisms.respectful Req iff)) RltProp. -Proof. - intros x y H x0 y0 H0. destruct H, H0. split. - - intro. destruct (linear_order_T x y x0). - apply Rlt_epsilon. assumption. - contradiction. destruct (linear_order_T y y0 x0). - assumption. apply Rlt_forget. assumption. contradiction. - - intro. destruct (linear_order_T y x y0). - apply Rlt_epsilon. assumption. - contradiction. destruct (linear_order_T x x0 y0). - assumption. apply Rlt_forget. assumption. contradiction. -Qed. - -Instance Rgt_morph - : CMorphisms.Proper - (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rgt. -Proof. - intros x y H x0 y0 H0. unfold Rgt. apply Rlt_morph; assumption. -Qed. - -Instance Rappart_morph - : CMorphisms.Proper - (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rappart. -Proof. - split. - - intros. destruct H1. left. rewrite <- H0, <- H. exact c. - right. rewrite <- H0, <- H. exact c. - - intros. destruct H1. left. rewrite H0, H. exact c. - right. rewrite H0, H. exact c. -Qed. - -Add Parametric Morphism : Rle - with signature Req ==> Req ==> iff - as Rle_morph. -Proof. - intros. split. - - intros H1 H2. unfold CRealLe in H1. - rewrite <- H0 in H2. rewrite <- H in H2. contradiction. - - intros H1 H2. unfold CRealLe in H1. - rewrite H0 in H2. rewrite H in H2. contradiction. -Qed. - -Add Parametric Morphism : Rge - with signature Req ==> Req ==> iff - as Rge_morph. -Proof. - intros. unfold Rge. apply Rle_morph; assumption. -Qed. - - -Definition Rplus := CRplus CR. -Definition Rmult := CRmult CR. -Definition Rinv := CRinv CR. -Definition Ropp := CRopp CR. - -Add Parametric Morphism : Rplus - with signature Req ==> Req ==> Req - as Rplus_morph. -Proof. - apply CRisRingExt. -Qed. - -Instance Rplus_morph_T - : CMorphisms.Proper - (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rplus. -Proof. - apply CRisRingExt. -Qed. - -Add Parametric Morphism : Rmult - with signature Req ==> Req ==> Req - as Rmult_morph. -Proof. - apply CRisRingExt. -Qed. - -Instance Rmult_morph_T - : CMorphisms.Proper - (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rmult. -Proof. - apply CRisRingExt. -Qed. - -Add Parametric Morphism : Ropp - with signature Req ==> Req - as Ropp_morph. -Proof. - apply CRisRingExt. -Qed. - -Instance Ropp_morph_T - : CMorphisms.Proper - (CMorphisms.respectful Req Req) Ropp. -Proof. - apply CRisRingExt. -Qed. - -Infix "+" := Rplus : R_scope_constr. -Notation "- x" := (Ropp x) : R_scope_constr. -Definition Rminus (r1 r2:R) : R := r1 + - r2. -Infix "-" := Rminus : R_scope_constr. -Infix "*" := Rmult : R_scope_constr. -Notation "/ x" := (CRinv CR x) (at level 35, right associativity) : R_scope_constr. - -Notation "0" := (CRzero CR) : R_scope_constr. -Notation "1" := (CRone CR) : R_scope_constr. - -Add Parametric Morphism : Rminus - with signature Req ==> Req ==> Req - as Rminus_morph. -Proof. - intros. unfold Rminus, CRminus. rewrite H,H0. reflexivity. -Qed. - - -(* Help Add Ring to find the correct equality *) -Lemma RisRing : ring_theory 0 1 - Rplus Rmult - Rminus Ropp - Req. -Proof. - exact (CRisRing CR). -Qed. - -Add Ring CRealRing : RisRing. - -Lemma Rplus_comm : forall x y:R, x + y == y + x. -Proof. intros. ring. Qed. - -Lemma Rplus_assoc : forall x y z:R, (x + y) + z == x + (y + z). -Proof. intros. ring. Qed. - -Lemma Rplus_opp_r : forall x:R, x + -x == 0. -Proof. intros. ring. Qed. - -Lemma Rplus_0_l : forall x:R, 0 + x == x. -Proof. intros. ring. Qed. - -Lemma Rmult_0_l : forall x:R, 0 * x == 0. -Proof. intros. ring. Qed. - -Lemma Rmult_1_l : forall x:R, 1 * x == x. -Proof. intros. ring. Qed. - -Lemma Rmult_comm : forall x y:R, x * y == y * x. -Proof. intros. ring. Qed. - -Lemma Rmult_assoc : forall x y z:R, (x * y) * z == x * (y * z). -Proof. intros. ring. Qed. - -Definition Rinv_l := CRinv_l CR. - -Lemma Rmult_plus_distr_l : forall r1 r2 r3 : R, - r1 * (r2 + r3) == (r1 * r2) + (r1 * r3). -Proof. intros. ring. Qed. - -Definition Rlt_0_1 := CRzero_lt_one CR. - -Lemma Rlt_asym : forall x y :R, x < y -> y < x -> False. -Proof. - intros. destruct (CRltLinear CR), p. - apply (f x y); assumption. -Qed. - -Lemma Rlt_trans : forall x y z : R, x < y -> y < z -> x < z. -Proof. - intros. destruct (CRltLinear CR), p. - apply (c x y); assumption. -Qed. - -Lemma Rplus_lt_compat_l : forall x y z : R, - y < z -> x + y < x + z. -Proof. - intros. apply CRplus_lt_compat_l. exact H. -Qed. - -Lemma Ropp_mult_distr_l - : forall r1 r2 : R, -(r1 * r2) == (- r1) * r2. -Proof. - intros. ring. -Qed. - -Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. -Proof. - intros. apply CRplus_lt_reg_l in H. exact H. -Qed. - -Lemma Rmult_lt_compat_l : forall x y z : R, - 0 < x -> y < z -> x * y < x * z. -Proof. - intros. apply (CRplus_lt_reg_l CR (- (x * y))). - rewrite Rplus_comm. pose proof Rplus_opp_r. - rewrite H1. - rewrite Rmult_comm, Ropp_mult_distr_l, Rmult_comm. - rewrite <- Rmult_plus_distr_l. - apply CRmult_lt_0_compat. exact H. - apply (Rplus_lt_reg_l y). - rewrite Rplus_comm, Rplus_0_l. - rewrite <- Rplus_assoc, H1, Rplus_0_l. exact H0. -Qed. - -Hint Resolve Rplus_comm Rplus_assoc Rplus_opp_r Rplus_0_l - Rmult_comm Rmult_assoc Rinv_l Rmult_1_l Rmult_plus_distr_l - Rlt_0_1 Rlt_asym Rlt_trans Rplus_lt_compat_l Rmult_lt_compat_l - Rmult_0_l : creal. - -Fixpoint INR (n:nat) : R := - match n with - | O => 0 - | S O => 1 - | S n => INR n + 1 - end. -Arguments INR n%nat. - -(* compact representation for 2*p *) -Fixpoint IPR_2 (p:positive) : R := - match p with - | xH => 1 + 1 - | xO p => (1 + 1) * IPR_2 p - | xI p => (1 + 1) * (1 + IPR_2 p) - end. - -Definition IPR (p:positive) : R := - match p with - | xH => 1 - | xO p => IPR_2 p - | xI p => 1 + IPR_2 p - end. -Arguments IPR p%positive : simpl never. - -(**********) -Definition IZR (z:Z) : R := - match z with - | Z0 => 0 - | Zpos n => IPR n - | Zneg n => - IPR n - end. -Arguments IZR z%Z : simpl never. - -Notation "2" := (IZR 2) : R_scope_constr. - - -(*********************************************************) -(** ** Relation between orders and equality *) -(*********************************************************) - -Lemma Rge_refl : forall r, r <= r. -Proof. exact Rle_refl. Qed. -Hint Immediate Rge_refl: rorders. - -(** Irreflexivity of the strict order *) - -Lemma Rlt_irrefl : forall r, r < r -> False. -Proof. - intros r H; eapply Rlt_asym; eauto. -Qed. -Hint Resolve Rlt_irrefl: creal. - -Lemma Rgt_irrefl : forall r, r > r -> False. -Proof. exact Rlt_irrefl. Qed. - -Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 H). -Qed. - -Lemma Rgt_not_eq : forall r1 r2, r1 > r2 -> r1 <> r2. -Proof. - intros; apply not_eq_sym; apply Rlt_not_eq; auto with creal. -Qed. - -(**********) -Lemma Rlt_dichotomy_converse : forall r1 r2, ((r1 < r2) + (r1 > r2)) -> r1 <> r2. -Proof. - intros. destruct H. - - intro abs. subst r2. exact (Rlt_irrefl r1 r). - - intro abs. subst r2. exact (Rlt_irrefl r1 r). -Qed. -Hint Resolve Rlt_dichotomy_converse: creal. - -(** Reasoning by case on equality and order *) - - -(*********************************************************) -(** ** Relating [<], [>], [<=] and [>=] *) -(*********************************************************) - -(*********************************************************) -(** ** Order *) -(*********************************************************) - -(** *** Relating strict and large orders *) - -Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2. -Proof. - intros. intro abs. apply (Rlt_asym r1 r2); assumption. -Qed. -Hint Resolve Rlt_le: creal. - -Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2. -Proof. - intros. intro abs. apply (Rlt_asym r1 r2); assumption. -Qed. - -(**********) -Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1. -Proof. - intros. intros abs. contradiction. -Qed. -Hint Immediate Rle_ge: creal. -Hint Resolve Rle_ge: rorders. - -Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1. -Proof. - intros. intro abs. contradiction. -Qed. -Hint Resolve Rge_le: creal. -Hint Immediate Rge_le: rorders. - -(**********) -Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1. -Proof. - trivial. -Qed. -Hint Resolve Rlt_gt: rorders. - -Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1. -Proof. - trivial. -Qed. -Hint Immediate Rgt_lt: rorders. - -(**********) - -Lemma Rnot_lt_le : forall r1 r2, (r1 < r2 -> False) -> r2 <= r1. -Proof. - intros. exact H. -Qed. - -Lemma Rnot_gt_le : forall r1 r2, (r1 > r2 -> False) -> r1 <= r2. -Proof. - intros. intro abs. contradiction. -Qed. - -Lemma Rnot_gt_ge : forall r1 r2, (r1 > r2 -> False) -> r2 >= r1. -Proof. - intros. intro abs. contradiction. -Qed. - -Lemma Rnot_lt_ge : forall r1 r2, (r1 < r2 -> False) -> r1 >= r2. -Proof. - intros. intro abs. contradiction. -Qed. - -(**********) -Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2. -Proof. - generalize Rlt_asym Rlt_dichotomy_converse; unfold CRealLe. - unfold not; intuition eauto 3. -Qed. -Hint Immediate Rlt_not_le: creal. - -Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2. -Proof. exact Rlt_not_le. Qed. - -Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2. -Proof. red; intros; eapply Rlt_not_le; eauto with creal. Qed. -Hint Immediate Rlt_not_ge: creal. - -Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2. -Proof. exact Rlt_not_ge. Qed. - -Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> r1 < r2 -> False. -Proof. - intros r1 r2. generalize (Rlt_asym r1 r2) (Rlt_dichotomy_converse r1 r2). - unfold CRealLe; intuition. -Qed. - -Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> r1 < r2 -> False. -Proof. intros; apply (Rle_not_lt r1 r2); auto with creal. Qed. - -Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> r1 > r2 -> False. -Proof. do 2 intro; apply Rle_not_lt. Qed. - -Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> r1 > r2 -> False. -Proof. do 2 intro; apply Rge_not_lt. Qed. - -(**********) -Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs). -Qed. -Hint Immediate Req_le: creal. - -Lemma Req_ge : forall r1 r2, r1 = r2 -> r1 >= r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs). -Qed. -Hint Immediate Req_ge: creal. - -Lemma Req_le_sym : forall r1 r2, r2 = r1 -> r1 <= r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs). -Qed. -Hint Immediate Req_le_sym: creal. - -Lemma Req_ge_sym : forall r1 r2, r2 = r1 -> r1 >= r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs). -Qed. -Hint Immediate Req_ge_sym: creal. - -(** *** Asymmetry *) - -(** Remark: [Rlt_asym] is an axiom *) - -Lemma Rgt_asym : forall r1 r2, r1 > r2 -> r2 > r1 -> False. -Proof. do 2 intro; apply Rlt_asym. Qed. - - -(** *** Compatibility with equality *) - -Lemma Rlt_eq_compat : - forall r1 r2 r3 r4, r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3. -Proof. - intros x x' y y'; intros; replace x with x'; replace y with y'; assumption. -Qed. - -Lemma Rgt_eq_compat : - forall r1 r2 r3 r4, r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3. -Proof. intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed. - -(** *** Transitivity *) - -Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3. -Proof. - intros. intro abs. - destruct (linear_order_T r3 r2 r1 abs); contradiction. -Qed. - -Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3. -Proof. - intros. apply (Rle_trans _ r2); assumption. -Qed. - -Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3. -Proof. - intros. apply (Rlt_trans _ r2); assumption. -Qed. - -(**********) -Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3. -Proof. - intros. - destruct (linear_order_T r2 r1 r3 H0). contradiction. apply r. -Qed. - -Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3. -Proof. - intros. - destruct (linear_order_T r1 r3 r2 H). apply r. contradiction. -Qed. - -Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3. -Proof. - intros. apply (Rlt_le_trans _ r2); assumption. -Qed. - -Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3. -Proof. - intros. apply (Rle_lt_trans _ r2); assumption. -Qed. - - -(*********************************************************) -(** ** Addition *) -(*********************************************************) - -(** Remark: [Rplus_0_l] is an axiom *) - -Lemma Rplus_0_r : forall r, r + 0 == r. -Proof. - intros. rewrite Rplus_comm. rewrite Rplus_0_l. reflexivity. -Qed. -Hint Resolve Rplus_0_r: creal. - -Lemma Rplus_ne : forall r, r + 0 == r /\ 0 + r == r. -Proof. - split. apply Rplus_0_r. apply Rplus_0_l. -Qed. -Hint Resolve Rplus_ne: creal. - -(**********) - -(** Remark: [Rplus_opp_r] is an axiom *) - -Lemma Rplus_opp_l : forall r, - r + r == 0. -Proof. - intros. rewrite Rplus_comm. apply Rplus_opp_r. -Qed. -Hint Resolve Rplus_opp_l: creal. - -(**********) -Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 == 0 -> r2 == - r1. -Proof. - intros x y H. rewrite <- (Rplus_0_l y). - rewrite <- (Rplus_opp_l x). rewrite Rplus_assoc. - rewrite H. rewrite Rplus_0_r. reflexivity. -Qed. - -Lemma Rplus_eq_compat_l : forall r r1 r2, r1 == r2 -> r + r1 == r + r2. -Proof. - intros. rewrite H. reflexivity. -Qed. - -Lemma Rplus_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 + r == r2 + r. -Proof. - intros. rewrite H. reflexivity. -Qed. - - -(**********) -Lemma Rplus_eq_reg_l : forall r r1 r2, r + r1 == r + r2 -> r1 == r2. -Proof. - intros; transitivity (- r + r + r1). - rewrite Rplus_opp_l. rewrite Rplus_0_l. reflexivity. - transitivity (- r + r + r2). - repeat rewrite Rplus_assoc; rewrite <- H; reflexivity. - rewrite Rplus_opp_l. rewrite Rplus_0_l. reflexivity. -Qed. -Hint Resolve Rplus_eq_reg_l: creal. - -Lemma Rplus_eq_reg_r : forall r r1 r2, r1 + r == r2 + r -> r1 == r2. -Proof. - intros r r1 r2 H. - apply Rplus_eq_reg_l with r. - now rewrite 2!(Rplus_comm r). -Qed. - -(**********) -Lemma Rplus_0_r_uniq : forall r r1, r + r1 == r -> r1 == 0. -Proof. - intros. apply (Rplus_eq_reg_l r). rewrite Rplus_0_r. exact H. -Qed. - - -(*********************************************************) -(** ** Multiplication *) -(*********************************************************) - -(**********) -Lemma Rinv_r : forall r (rnz : r # 0), - r # 0 -> r * ((/ r) rnz) == 1. -Proof. - intros. rewrite Rmult_comm. rewrite Rinv_l. - reflexivity. -Qed. -Hint Resolve Rinv_r: creal. - -Lemma Rinv_l_sym : forall r (rnz: r # 0), 1 == (/ r) rnz * r. -Proof. - intros. symmetry. apply Rinv_l. -Qed. -Hint Resolve Rinv_l_sym: creal. - -Lemma Rinv_r_sym : forall r (rnz : r # 0), 1 == r * (/ r) rnz. -Proof. - intros. symmetry. apply Rinv_r. apply rnz. -Qed. -Hint Resolve Rinv_r_sym: creal. - -(**********) -Lemma Rmult_0_r : forall r, r * 0 == 0. -Proof. - intro; ring. -Qed. -Hint Resolve Rmult_0_r: creal. - -(**********) -Lemma Rmult_ne : forall r, r * 1 == r /\ 1 * r == r. -Proof. - intro; split; ring. -Qed. -Hint Resolve Rmult_ne: creal. - -(**********) -Lemma Rmult_1_r : forall r, r * 1 == r. -Proof. - intro; ring. -Qed. -Hint Resolve Rmult_1_r: creal. - -(**********) -Lemma Rmult_eq_compat_l : forall r r1 r2, r1 == r2 -> r * r1 == r * r2. -Proof. - intros. rewrite H. reflexivity. -Qed. - -Lemma Rmult_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 * r == r2 * r. -Proof. - intros. rewrite H. reflexivity. -Qed. - -(**********) -Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 == r * r2 -> r # 0 -> r1 == r2. -Proof. - intros. transitivity ((/ r) H0 * r * r1). - rewrite Rinv_l. ring. - transitivity ((/ r) H0 * r * r2). - repeat rewrite Rmult_assoc; rewrite H; reflexivity. - rewrite Rinv_l. ring. -Qed. - -Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2. -Proof. - intros. - apply Rmult_eq_reg_l with (2 := H0). - now rewrite 2!(Rmult_comm r). -Qed. - -(**********) -Lemma Rmult_eq_0_compat : forall r1 r2, r1 == 0 \/ r2 == 0 -> r1 * r2 == 0. -Proof. - intros r1 r2 [H| H]; rewrite H; auto with creal. -Qed. - -Hint Resolve Rmult_eq_0_compat: creal. - -(**********) -Lemma Rmult_eq_0_compat_r : forall r1 r2, r1 == 0 -> r1 * r2 == 0. -Proof. - auto with creal. -Qed. - -(**********) -Lemma Rmult_eq_0_compat_l : forall r1 r2, r2 == 0 -> r1 * r2 == 0. -Proof. - auto with creal. -Qed. - -(**********) -Lemma Rmult_integral_contrapositive : - forall r1 r2, (prod (r1 # 0) (r2 # 0)) -> (r1 * r2) # 0. -Proof. - assert (forall r, 0 > r -> 0 < - r). - { intros. rewrite <- (Rplus_opp_l r), <- (Rplus_0_r (-r)), Rplus_assoc. - apply Rplus_lt_compat_l. rewrite Rplus_0_l. apply H. } - intros. destruct H0, r, r0. - - right. setoid_replace (r1*r2) with (-r1 * -r2). 2: ring. - rewrite <- (Rmult_0_r (-r1)). apply Rmult_lt_compat_l; apply H; assumption. - - left. rewrite <- (Rmult_0_r r2). - rewrite Rmult_comm. apply (Rmult_lt_compat_l). apply c0. apply c. - - left. rewrite <- (Rmult_0_r r1). apply (Rmult_lt_compat_l). apply c. apply c0. - - right. rewrite <- (Rmult_0_r r1). apply Rmult_lt_compat_l; assumption. -Qed. -Hint Resolve Rmult_integral_contrapositive: creal. - -Lemma Rmult_integral_contrapositive_currified : - forall r1 r2, r1 # 0 -> r2 # 0 -> (r1 * r2) # 0. -Proof. - intros. apply Rmult_integral_contrapositive. - split; assumption. -Qed. - -(**********) -Lemma Rmult_plus_distr_r : - forall r1 r2 r3, (r1 + r2) * r3 == r1 * r3 + r2 * r3. -Proof. - intros; ring. -Qed. - -(*********************************************************) -(** ** Square function *) -(*********************************************************) - -(***********) -Definition Rsqr (r : R) := r * r. - -Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope_constr. - -(***********) -Lemma Rsqr_0 : Rsqr 0 == 0. - unfold Rsqr; auto with creal. -Qed. - -(*********************************************************) -(** ** Opposite *) -(*********************************************************) - -(**********) -Lemma Ropp_eq_compat : forall r1 r2, r1 == r2 -> - r1 == - r2. -Proof. - intros. rewrite H. reflexivity. -Qed. -Hint Resolve Ropp_eq_compat: creal. - -(**********) -Lemma Ropp_0 : -0 == 0. -Proof. - ring. -Qed. -Hint Resolve Ropp_0: creal. - -(**********) -Lemma Ropp_eq_0_compat : forall r, r == 0 -> - r == 0. -Proof. - intros; rewrite H; auto with creal. -Qed. -Hint Resolve Ropp_eq_0_compat: creal. - -(**********) -Lemma Ropp_involutive : forall r, - - r == r. -Proof. - intro; ring. -Qed. -Hint Resolve Ropp_involutive: creal. - -(**********) -Lemma Ropp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2. -Proof. - intros; ring. -Qed. -Hint Resolve Ropp_plus_distr: creal. - -(*********************************************************) -(** ** Opposite and multiplication *) -(*********************************************************) - -Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 == - (r1 * r2). -Proof. - intros; ring. -Qed. -Hint Resolve Ropp_mult_distr_l_reverse: creal. - -(**********) -Lemma Rmult_opp_opp : forall r1 r2, - r1 * - r2 == r1 * r2. -Proof. - intros; ring. -Qed. -Hint Resolve Rmult_opp_opp: creal. - -Lemma Ropp_mult_distr_r : forall r1 r2, - (r1 * r2) == r1 * - r2. -Proof. - intros; ring. -Qed. - -Lemma Ropp_mult_distr_r_reverse : forall r1 r2, r1 * - r2 == - (r1 * r2). -Proof. - intros; ring. -Qed. - -(*********************************************************) -(** ** Subtraction *) -(*********************************************************) - -Lemma Rminus_0_r : forall r, r - 0 == r. -Proof. - intro r. unfold Rminus. ring. -Qed. -Hint Resolve Rminus_0_r: creal. - -Lemma Rminus_0_l : forall r, 0 - r == - r. -Proof. - intro r. unfold Rminus. ring. -Qed. -Hint Resolve Rminus_0_l: creal. - -(**********) -Lemma Ropp_minus_distr : forall r1 r2, - (r1 - r2) == r2 - r1. -Proof. - intros; ring. -Qed. -Hint Resolve Ropp_minus_distr: creal. - -Lemma Ropp_minus_distr' : forall r1 r2, - (r2 - r1) == r1 - r2. -Proof. - intros; ring. -Qed. - -(**********) -Lemma Rminus_diag_eq : forall r1 r2, r1 == r2 -> r1 - r2 == 0. -Proof. - intros; rewrite H; unfold Rminus; ring. -Qed. -Hint Resolve Rminus_diag_eq: creal. - -(**********) -Lemma Rminus_diag_uniq : forall r1 r2, r1 - r2 == 0 -> r1 == r2. -Proof. - intros r1 r2. unfold Rminus,CRminus; rewrite Rplus_comm; intro. - rewrite <- (Ropp_involutive r2); apply (Rplus_opp_r_uniq (- r2) r1 H). -Qed. -Hint Immediate Rminus_diag_uniq: creal. - -Lemma Rminus_diag_uniq_sym : forall r1 r2, r2 - r1 == 0 -> r1 == r2. -Proof. - intros; generalize (Rminus_diag_uniq r2 r1 H); clear H; - intro H; rewrite H; reflexivity. -Qed. -Hint Immediate Rminus_diag_uniq_sym: creal. - -Lemma Rplus_minus : forall r1 r2, r1 + (r2 - r1) == r2. -Proof. - intros; ring. -Qed. -Hint Resolve Rplus_minus: creal. - -(**********) -Lemma Rmult_minus_distr_l : - forall r1 r2 r3, r1 * (r2 - r3) == r1 * r2 - r1 * r3. -Proof. - intros; ring. -Qed. - - -(*********************************************************) -(** ** Order and addition *) -(*********************************************************) - -(** *** Compatibility *) - -(** Remark: [Rplus_lt_compat_l] is an axiom *) - -Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2. -Proof. - intros. apply Rplus_lt_compat_l. apply H. -Qed. -Hint Resolve Rplus_gt_compat_l: creal. - -(**********) -Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r. -Proof. - intros. - rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r). - apply Rplus_lt_compat_l. exact H. -Qed. -Hint Resolve Rplus_lt_compat_r: creal. - -Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r. -Proof. do 3 intro; apply Rplus_lt_compat_r. Qed. - -(**********) - -Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2. -Proof. - intros. - apply (Rplus_lt_reg_l r). - now rewrite 2!(Rplus_comm r). -Qed. - -Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2. -Proof. - intros. intro abs. apply Rplus_lt_reg_l in abs. contradiction. -Qed. - -Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2. -Proof. - intros. apply Rplus_le_compat_l. apply H. -Qed. -Hint Resolve Rplus_ge_compat_l: creal. - -(**********) -Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r. -Proof. - intros. intro abs. apply Rplus_lt_reg_r in abs. contradiction. -Qed. - -Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: creal. - -Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r. -Proof. - intros. apply Rplus_le_compat_r. apply H. -Qed. - -(*********) -Lemma Rplus_lt_compat : - forall r1 r2 r3 r4, r1 < r2 -> r3 < r4 -> r1 + r3 < r2 + r4. -Proof. - intros; apply Rlt_trans with (r2 + r3); auto with creal. -Qed. -Hint Immediate Rplus_lt_compat: creal. - -Lemma Rplus_le_compat : - forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4. -Proof. - intros; apply Rle_trans with (r2 + r3); auto with creal. -Qed. -Hint Immediate Rplus_le_compat: creal. - -Lemma Rplus_gt_compat : - forall r1 r2 r3 r4, r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4. -Proof. - intros. apply Rplus_lt_compat; assumption. -Qed. - -Lemma Rplus_ge_compat : - forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4. -Proof. - intros. apply Rplus_le_compat; assumption. -Qed. - -(*********) -Lemma Rplus_lt_le_compat : - forall r1 r2 r3 r4, r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4. -Proof. - intros; apply Rlt_le_trans with (r2 + r3); auto with creal. -Qed. - -Lemma Rplus_le_lt_compat : - forall r1 r2 r3 r4, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4. -Proof. - intros; apply Rle_lt_trans with (r2 + r3); auto with creal. -Qed. - -Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: creal. - -Lemma Rplus_gt_ge_compat : - forall r1 r2 r3 r4, r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4. -Proof. - intros. apply Rplus_lt_le_compat; assumption. -Qed. - -Lemma Rplus_ge_gt_compat : - forall r1 r2 r3 r4, r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4. -Proof. - intros. apply Rplus_le_lt_compat; assumption. -Qed. - -(**********) -Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2. -Proof. - intros. apply (Rlt_trans _ (r1+0)). rewrite Rplus_0_r. exact H. - apply Rplus_lt_compat_l. exact H0. -Qed. - -Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2. -Proof. - intros. apply (Rle_lt_trans _ (r1+0)). rewrite Rplus_0_r. exact H. - apply Rplus_lt_compat_l. exact H0. -Qed. - -Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2. -Proof. - intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat; - assumption. -Qed. - -Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2. -Proof. - intros. apply (Rle_trans _ (r1+0)). rewrite Rplus_0_r. exact H. - apply Rplus_le_compat_l. exact H0. -Qed. - -(**********) -Lemma sum_inequa_Rle_lt : - forall a x b c y d, - a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d. -Proof. - intros; split. - apply Rlt_le_trans with (a + y); auto with creal. - apply Rlt_le_trans with (b + y); auto with creal. -Qed. - -(** *** Cancellation *) - -Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. -Proof. - intros. intro abs. apply (Rplus_lt_compat_l r) in abs. contradiction. -Qed. - -Lemma Rplus_le_reg_r : forall r r1 r2, r1 + r <= r2 + r -> r1 <= r2. -Proof. - intros. - apply (Rplus_le_reg_l r). - now rewrite 2!(Rplus_comm r). -Qed. - -Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2. -Proof. - unfold CRealGt; intros; apply (Rplus_lt_reg_l r r2 r1 H). -Qed. - -Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2. -Proof. - intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with creal. -Qed. - -(**********) -Lemma Rplus_le_reg_pos_r : - forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3. -Proof. - intros. apply (Rle_trans _ (r1+r2)). 2: exact H0. - rewrite <- (Rplus_0_r r1), Rplus_assoc. - apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H. -Qed. - -Lemma Rplus_lt_reg_pos_r : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3. -Proof. - intros. apply (Rle_lt_trans _ (r1+r2)). 2: exact H0. - rewrite <- (Rplus_0_r r1), Rplus_assoc. - apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H. -Qed. - -Lemma Rplus_ge_reg_neg_r : - forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3. -Proof. - intros. apply (Rge_trans _ (r1+r2)). 2: exact H0. - apply Rle_ge. rewrite <- (Rplus_0_r r1), Rplus_assoc. - apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H. -Qed. - -Lemma Rplus_gt_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 > r3 -> r1 > r3. -Proof. - intros. apply (Rlt_le_trans _ (r1+r2)). exact H0. - rewrite <- (Rplus_0_r r1), Rplus_assoc. - apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H. -Qed. - -(***********) -Lemma Rplus_eq_0_l : - forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 == 0 -> r1 == 0. -Proof. - intros. split. - - intro abs. rewrite <- (Rplus_opp_r r1) in H1. - apply Rplus_eq_reg_l in H1. rewrite H1 in H0. clear H1. - apply (Rplus_le_compat_l r1) in H0. - rewrite Rplus_opp_r in H0. rewrite Rplus_0_r in H0. - contradiction. - - intro abs. clear H. rewrite <- (Rplus_opp_r r1) in H1. - apply Rplus_eq_reg_l in H1. rewrite H1 in H0. clear H1. - apply (Rplus_le_compat_l r1) in H0. - rewrite Rplus_opp_r in H0. rewrite Rplus_0_r in H0. - contradiction. -Qed. - -Lemma Rplus_eq_R0 : - forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 == 0 -> r1 == 0 /\ r2 == 0. -Proof. - intros a b; split. - apply Rplus_eq_0_l with b; auto with creal. - apply Rplus_eq_0_l with a; auto with creal. - rewrite Rplus_comm; auto with creal. -Qed. - - -(*********************************************************) -(** ** Order and opposite *) -(*********************************************************) - -(** *** Contravariant compatibility *) - -Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2. -Proof. - unfold CRealGt; intros. - apply (Rplus_lt_reg_l (r2 + r1)). - setoid_replace (r2 + r1 + - r1) with r2 by ring. - setoid_replace (r2 + r1 + - r2) with r1 by ring. - exact H. -Qed. -Hint Resolve Ropp_gt_lt_contravar : creal. - -Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2. -Proof. - intros. apply Ropp_gt_lt_contravar. exact H. -Qed. -Hint Resolve Ropp_lt_gt_contravar: creal. - -(**********) -Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2. -Proof. - auto with creal. -Qed. -Hint Resolve Ropp_lt_contravar: creal. - -Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2. -Proof. auto with creal. Qed. - -(**********) - -Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2. -Proof. - intros x y H'. - rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); - auto with creal. -Qed. -Hint Immediate Ropp_lt_cancel: creal. - -Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2. -Proof. - intros. apply Ropp_lt_cancel. apply H. -Qed. - -Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2. -Proof. - intros. intro abs. apply Ropp_lt_cancel in abs. contradiction. -Qed. -Hint Resolve Ropp_le_ge_contravar: creal. - -Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2. -Proof. - intros. intro abs. apply Ropp_lt_cancel in abs. contradiction. -Qed. -Hint Resolve Ropp_ge_le_contravar: creal. - -(**********) -Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2. -Proof. - intros. intro abs. apply Ropp_lt_cancel in abs. contradiction. -Qed. -Hint Resolve Ropp_le_contravar: creal. - -Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2. -Proof. - intros. apply Ropp_le_contravar. apply H. -Qed. - -(**********) -Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r. -Proof. - intros; setoid_replace 0 with (-0); auto with creal. ring. -Qed. -Hint Resolve Ropp_0_lt_gt_contravar: creal. - -Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r. -Proof. - intros; setoid_replace 0 with (-0); auto with creal. ring. -Qed. -Hint Resolve Ropp_0_gt_lt_contravar: creal. - -(**********) -Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0. -Proof. - intros; rewrite <- Ropp_0; auto with creal. -Qed. -Hint Resolve Ropp_lt_gt_0_contravar: creal. - -Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0. -Proof. - intros; rewrite <- Ropp_0; auto with creal. -Qed. -Hint Resolve Ropp_gt_lt_0_contravar: creal. - -(**********) -Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r. -Proof. - intros; setoid_replace 0 with (-0); auto with creal. ring. -Qed. -Hint Resolve Ropp_0_le_ge_contravar: creal. - -Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r. -Proof. - intros; setoid_replace 0 with (-0); auto with creal. ring. -Qed. -Hint Resolve Ropp_0_ge_le_contravar: creal. - -(** *** Cancellation *) - -Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2. -Proof. - intros. intro abs. apply Ropp_lt_gt_contravar in abs. contradiction. -Qed. -Hint Immediate Ropp_le_cancel: creal. - -Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2. -Proof. - intros. apply Ropp_le_cancel. apply H. -Qed. - -(*********************************************************) -(** ** Order and multiplication *) -(*********************************************************) - -(** Remark: [Rmult_lt_compat_l] is an axiom *) - -(** *** Covariant compatibility *) - -Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r. -Proof. - intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with creal. -Qed. -Hint Resolve Rmult_lt_compat_r : core. - -Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r. -Proof. - intros. apply Rmult_lt_compat_r; assumption. -Qed. - -Lemma Rmult_gt_compat_l : forall r r1 r2, r > 0 -> r1 > r2 -> r * r1 > r * r2. -Proof. - intros. apply Rmult_lt_compat_l; assumption. -Qed. - -Lemma Rmult_gt_0_lt_compat : - forall r1 r2 r3 r4, - r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. -Proof. - intros; apply Rlt_trans with (r2 * r3); auto with creal. -Qed. - -(*********) -Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2. -Proof. - intros; setoid_replace 0 with (0 * r2); auto with creal. - rewrite Rmult_0_l. reflexivity. -Qed. - -Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0. -Proof. - apply Rmult_lt_0_compat. -Qed. - -(** *** Contravariant compatibility *) - -Lemma Rmult_lt_gt_compat_neg_l : - forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2. -Proof. - intros; setoid_replace r with (- - r); auto with creal. - rewrite (Ropp_mult_distr_l_reverse (- r)); - rewrite (Ropp_mult_distr_l_reverse (- r)). - apply Ropp_lt_gt_contravar; auto with creal. - rewrite Ropp_involutive. reflexivity. -Qed. - -(** *** Cancellation *) - -Lemma Rinv_0_lt_compat : forall r (rpos : 0 < r), 0 < (/ r) (inr rpos). -Proof. - intros. apply CRinv_0_lt_compat. exact rpos. -Qed. - -Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. -Proof. - intros z x y H H0. - apply (Rmult_lt_compat_l ((/z) (inr H))) in H0. - repeat rewrite <- Rmult_assoc in H0. rewrite Rinv_l in H0. - repeat rewrite Rmult_1_l in H0. apply H0. - apply Rinv_0_lt_compat. -Qed. - -Lemma Rmult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2. -Proof. - intros. - apply Rmult_lt_reg_l with r. - exact H. - now rewrite 2!(Rmult_comm r). -Qed. - -Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. -Proof. - intros. apply Rmult_lt_reg_l in H0; assumption. -Qed. - -Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2. -Proof. - intros. intro abs. apply (Rmult_lt_compat_l r) in abs. - contradiction. apply H. -Qed. - -Lemma Rmult_le_reg_r : forall r r1 r2, 0 < r -> r1 * r <= r2 * r -> r1 <= r2. -Proof. - intros. - apply Rmult_le_reg_l with r. - exact H. - now rewrite 2!(Rmult_comm r). -Qed. - -(*********************************************************) -(** ** Order and substraction *) -(*********************************************************) - -Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0. -Proof. - intros; apply (Rplus_lt_reg_l r2). - setoid_replace (r2 + (r1 - r2)) with r1 by ring. - now rewrite Rplus_0_r. -Qed. -Hint Resolve Rlt_minus: creal. - -Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0. -Proof. - intros; apply (Rplus_lt_reg_l r2). - setoid_replace (r2 + (r1 - r2)) with r1 by ring. - now rewrite Rplus_0_r. -Qed. - -Lemma Rlt_Rminus : forall a b, a < b -> 0 < b - a. -Proof. - intros a b; apply Rgt_minus. -Qed. - -(**********) -Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0. -Proof. - intros. intro abs. apply (Rplus_lt_compat_l r2) in abs. - unfold Rminus in abs. - rewrite Rplus_0_r, Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r in abs. - contradiction. -Qed. - -Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0. -Proof. - intros. intro abs. apply (Rplus_lt_compat_l r2) in abs. - unfold Rminus in abs. - rewrite Rplus_0_r, Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r in abs. - contradiction. -Qed. - -(**********) -Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2. -Proof. - intros. rewrite <- (Rplus_opp_r r2) in H. - apply Rplus_lt_reg_r in H. exact H. -Qed. - -Lemma Rminus_gt : forall r1 r2, r1 - r2 > 0 -> r1 > r2. -Proof. - intros. rewrite <- (Rplus_opp_r r2) in H. - apply Rplus_lt_reg_r in H. exact H. -Qed. - -Lemma Rminus_gt_0_lt : forall a b, 0 < b - a -> a < b. -Proof. intro; intro; apply Rminus_gt. Qed. - -(**********) -Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2. -Proof. - intros. rewrite <- (Rplus_opp_r r2) in H. - apply Rplus_le_reg_r in H. exact H. -Qed. - -Lemma Rminus_ge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2. -Proof. - intros. rewrite <- (Rplus_opp_r r2) in H. - apply Rplus_le_reg_r in H. exact H. -Qed. - -(**********) -Lemma tech_Rplus : forall r s, 0 <= r -> 0 < s -> r + s <> 0. -Proof. - intros; apply not_eq_sym; apply Rlt_not_eq. - rewrite Rplus_comm; setoid_replace 0 with (0 + 0); auto with creal. ring. -Qed. -Hint Immediate tech_Rplus: creal. - -(*********************************************************) -(** ** Zero is less than one *) -(*********************************************************) - -Lemma Rle_0_1 : 0 <= 1. -Proof. - intro abs. apply (Rlt_asym 0 1). - apply Rlt_0_1. apply abs. -Qed. - - -(*********************************************************) -(** ** Inverse *) -(*********************************************************) - -Lemma Rinv_1 : forall nz : 1 # 0, (/ 1) nz == 1. -Proof. - intros. rewrite <- (Rmult_1_l ((/1) nz)). rewrite Rinv_r. - reflexivity. right. apply Rlt_0_1. -Qed. -Hint Resolve Rinv_1: creal. - -(*********) -Lemma Ropp_inv_permute : forall r (rnz : r # 0) (ronz : (-r) # 0), - - (/ r) rnz == (/ - r) ronz. -Proof. - intros. - apply (Rmult_eq_reg_l (-r)). rewrite Rinv_r. - rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r. - rewrite Ropp_involutive. rewrite Rinv_r. reflexivity. - exact rnz. exact ronz. exact ronz. -Qed. - -(*********) -Lemma Rinv_neq_0_compat : forall r (rnz : r # 0), ((/ r) rnz) # 0. -Proof. - intros. destruct rnz. left. - assert (0 < (/-r) (inr (Ropp_0_gt_lt_contravar _ c))). - { apply Rinv_0_lt_compat. } - rewrite <- (Ropp_inv_permute _ (inl c)) in H. - apply Ropp_lt_cancel. rewrite Ropp_0. exact H. - right. apply Rinv_0_lt_compat. -Qed. -Hint Resolve Rinv_neq_0_compat: creal. - -(*********) -Lemma Rinv_involutive : forall r (rnz : r # 0) (rinz : ((/ r) rnz) # 0), - (/ ((/ r) rnz)) rinz == r. -Proof. - intros. apply (Rmult_eq_reg_l ((/r) rnz)). rewrite Rinv_r. - rewrite Rinv_l. reflexivity. exact rinz. exact rinz. -Qed. -Hint Resolve Rinv_involutive: creal. - -(*********) -Lemma Rinv_mult_distr : - forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1*r2) # 0), - (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz. -Proof. - intros. apply (Rmult_eq_reg_l r1). 2: exact r1nz. - rewrite <- Rmult_assoc. rewrite Rinv_r. rewrite Rmult_1_l. - apply (Rmult_eq_reg_l r2). 2: exact r2nz. - rewrite Rinv_r. rewrite <- Rmult_assoc. - rewrite (Rmult_comm r2 r1). rewrite Rinv_r. - reflexivity. exact rmnz. exact r2nz. exact r1nz. -Qed. - -Lemma Rinv_r_simpl_r : forall r1 r2 (rnz : r1 # 0), r1 * (/ r1) rnz * r2 == r2. -Proof. - intros; transitivity (1 * r2); auto with creal. - rewrite Rinv_r; auto with creal. rewrite Rmult_1_l. reflexivity. -Qed. - -Lemma Rinv_r_simpl_l : forall r1 r2 (rnz : r1 # 0), - r2 * r1 * (/ r1) rnz == r2. -Proof. - intros. rewrite Rmult_assoc. rewrite Rinv_r, Rmult_1_r. - reflexivity. exact rnz. -Qed. - -Lemma Rinv_r_simpl_m : forall r1 r2 (rnz : r1 # 0), - r1 * r2 * (/ r1) rnz == r2. -Proof. - intros. rewrite Rmult_comm, <- Rmult_assoc, Rinv_l, Rmult_1_l. - reflexivity. -Qed. -Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: creal. - -(*********) -Lemma Rinv_mult_simpl : - forall r1 r2 r3 (r1nz : r1 # 0) (r2nz : r2 # 0), - r1 * (/ r2) r2nz * (r3 * (/ r1) r1nz) == r3 * (/ r2) r2nz. -Proof. - intros a b c; intros. - transitivity (a * (/ a) r1nz * (c * (/ b) r2nz)); auto with creal. - ring. -Qed. - -Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0), - x == y - -> (/ x) rxnz == (/ y) rynz. -Proof. - intros. apply (Rmult_eq_reg_l x). rewrite Rinv_r. - rewrite H. rewrite Rinv_r. reflexivity. - exact rynz. exact rxnz. exact rxnz. -Qed. - - -(*********************************************************) -(** ** Order and inverse *) -(*********************************************************) - -Lemma Rinv_lt_0_compat : forall r (rneg : r < 0), (/ r) (inl rneg) < 0. -Proof. - intros. assert (0 < (/-r) (inr (Ropp_0_gt_lt_contravar r rneg))). - { apply Rinv_0_lt_compat. } - rewrite <- Ropp_inv_permute in H. rewrite <- Ropp_0 in H. - apply Ropp_lt_cancel in H. apply H. -Qed. -Hint Resolve Rinv_lt_0_compat: creal. - - - -(*********************************************************) -(** ** Miscellaneous *) -(*********************************************************) - -(**********) -Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1. -Proof. - intros. apply (Rle_lt_trans _ (r+0)). rewrite Rplus_0_r. - exact H. apply Rplus_lt_compat_l. apply Rlt_0_1. -Qed. -Hint Resolve Rle_lt_0_plus_1: creal. - -(**********) -Lemma Rlt_plus_1 : forall r, r < r + 1. -Proof. - intro r. rewrite <- Rplus_0_r. rewrite Rplus_assoc. - apply Rplus_lt_compat_l. rewrite Rplus_0_l. exact Rlt_0_1. -Qed. -Hint Resolve Rlt_plus_1: creal. - -(**********) -Lemma tech_Rgt_minus : forall r1 r2, 0 < r2 -> r1 > r1 - r2. -Proof. - intros. apply (Rplus_lt_reg_r r2). - unfold Rminus, CRminus; rewrite Rplus_assoc, Rplus_opp_l. - apply Rplus_lt_compat_l. exact H. -Qed. - -(*********************************************************) -(** ** Injection from [N] to [R] *) -(*********************************************************) - -(**********) -Lemma S_INR : forall n:nat, INR (S n) == INR n + 1. -Proof. - intro; destruct n. rewrite Rplus_0_l. reflexivity. reflexivity. -Qed. - -(**********) -Lemma IZN : forall n:Z, (0 <= n)%Z -> { m : nat | n = Z.of_nat m }. -Proof. - intros. exists (Z.to_nat n). rewrite Z2Nat.id. reflexivity. assumption. -Qed. - -Lemma le_succ_r_T : forall n m : nat, (n <= S m)%nat -> {(n <= m)%nat} + {n = S m}. -Proof. - intros. destruct (le_lt_dec n m). left. exact l. - right. apply Nat.le_succ_r in H. destruct H. - exfalso. apply (le_not_lt n m); assumption. exact H. -Qed. - -Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m. -Proof. - induction m. - - intros. exfalso. inversion H. - - intros. unfold lt in H. apply le_S_n in H. destruct m. - assert (n = 0)%nat. - { inversion H. reflexivity. } - subst n. apply Rlt_0_1. apply le_succ_r_T in H. destruct H. - rewrite S_INR. apply (Rlt_trans _ (INR (S m) + 0)). - rewrite Rplus_comm, Rplus_0_l. apply IHm. - apply le_n_S. exact l. - apply Rplus_lt_compat_l. exact Rlt_0_1. - subst n. rewrite (S_INR (S m)). rewrite <- (Rplus_0_l). - rewrite (Rplus_comm 0), Rplus_assoc. - apply Rplus_lt_compat_l. rewrite Rplus_0_l. - exact Rlt_0_1. -Qed. - -(**********) -Lemma S_O_plus_INR : forall n:nat, INR (1 + n) == INR 1 + INR n. -Proof. - intros; destruct n. - - rewrite Rplus_comm, Rplus_0_l. reflexivity. - - rewrite Rplus_comm. reflexivity. -Qed. - -(**********) -Lemma plus_INR : forall n m:nat, INR (n + m) == INR n + INR m. -Proof. - intros n m; induction n as [| n Hrecn]. - - rewrite Rplus_0_l. reflexivity. - - replace (S n + m)%nat with (S (n + m)); auto with arith. - repeat rewrite S_INR. - rewrite Hrecn; ring. -Qed. - -(**********) -Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) == INR n - INR m. -Proof. - intros n m le; pattern m, n; apply le_elim_rel. - intros. rewrite <- minus_n_O. simpl. - unfold Rminus, CRminus. rewrite Ropp_0, Rplus_0_r. reflexivity. - intros; repeat rewrite S_INR; simpl. - rewrite H0. unfold Rminus. ring. exact le. -Qed. - -(*********) -Lemma mult_INR : forall n m:nat, INR (n * m) == INR n * INR m. -Proof. - intros n m; induction n as [| n Hrecn]. - - rewrite Rmult_0_l. reflexivity. - - intros; repeat rewrite S_INR; simpl. - rewrite plus_INR. rewrite Hrecn; ring. -Qed. - -Lemma INR_IPR : forall p, INR (Pos.to_nat p) == IPR p. -Proof. - assert (H: forall p, 2 * INR (Pos.to_nat p) == IPR_2 p). - { induction p as [p|p|]. - - unfold IPR_2; rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp. - rewrite Rplus_comm. reflexivity. - - unfold IPR_2; now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp. - - apply Rmult_1_r. } - intros [p|p|] ; unfold IPR. - rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H. - apply Rplus_comm. - now rewrite Pos2Nat.inj_xO, mult_INR, <- H. - easy. -Qed. - -Fixpoint pow (r:R) (n:nat) : R := - match n with - | O => 1 - | S n => r * (pow r n) - end. - -Lemma Rpow_eq_compat : forall (x y : R) (n : nat), - x == y -> pow x n == pow y n. -Proof. - intro x. induction n. - - reflexivity. - - intros. simpl. rewrite IHn, H. reflexivity. exact H. -Qed. - -Lemma pow_INR (m n: nat) : INR (m ^ n) == pow (INR m) n. -Proof. now induction n as [|n IHn];[ | simpl; rewrite mult_INR, IHn]. Qed. - -(*********) -Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n. -Proof. - intros. apply (lt_INR 0). exact H. -Qed. -Hint Resolve lt_0_INR: creal. - -Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n. -Proof. - apply lt_INR. -Qed. -Hint Resolve lt_1_INR: creal. - -(**********) -Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (Pos.to_nat p). -Proof. - intro; apply lt_0_INR. - simpl; auto with creal. - apply Pos2Nat.is_pos. -Qed. -Hint Resolve pos_INR_nat_of_P: creal. - -(**********) -Lemma pos_INR : forall n:nat, 0 <= INR n. -Proof. - intro n; case n. - simpl; auto with creal. - auto with arith creal. -Qed. -Hint Resolve pos_INR: creal. - -Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat. -Proof. - intros n m. revert n. - induction m ; intros n H. - - elim (Rlt_irrefl 0). - apply Rle_lt_trans with (2 := H). - apply pos_INR. - - destruct n as [|n]. - apply Nat.lt_0_succ. - apply lt_n_S, IHm. - rewrite 2!S_INR in H. - apply Rplus_lt_reg_r with (1 := H). -Qed. -Hint Resolve INR_lt: creal. - -(*********) -Lemma le_INR : forall n m:nat, (n <= m)%nat -> INR n <= INR m. -Proof. - simple induction 1; intros; auto with creal. - rewrite S_INR. - apply Rle_trans with (INR m0); auto with creal. -Qed. -Hint Resolve le_INR: creal. - -(**********) -Lemma INR_not_0 : forall n:nat, INR n <> 0 -> n <> 0%nat. -Proof. - red; intros n H H1. - apply H. - rewrite H1; trivial. -Qed. -Hint Immediate INR_not_0: creal. - -(**********) -Lemma not_0_INR : forall n:nat, n <> 0%nat -> 0 < INR n. -Proof. - intro n; case n. - intro; absurd (0%nat = 0%nat); trivial. - intros; rewrite S_INR. - apply (Rlt_le_trans _ (0 + 1)). rewrite Rplus_0_l. apply Rlt_0_1. - apply Rplus_le_compat_r. apply pos_INR. -Qed. -Hint Resolve not_0_INR: creal. - -Lemma not_INR : forall n m:nat, n <> m -> INR n # INR m. -Proof. - intros n m H; case (le_lt_dec n m); intros H1. - left. apply lt_INR. - case (le_lt_or_eq _ _ H1); intros H2. - exact H2. contradiction. - right. apply lt_INR. exact H1. -Qed. -Hint Resolve not_INR: creal. - -Lemma INR_eq : forall n m:nat, INR n == INR m -> n = m. -Proof. - intros n m HR. - destruct (dec_eq_nat n m) as [H|H]. - exact H. exfalso. - apply not_INR in H. destruct HR,H; contradiction. -Qed. -Hint Resolve INR_eq: creal. - -Lemma INR_le : forall n m:nat, INR n <= INR m -> (n <= m)%nat. -Proof. - intros n m. revert n. - induction m ; intros n H. - - destruct n. apply le_refl. exfalso. - rewrite S_INR in H. - assert (0 + 1 <= 0). apply (Rle_trans _ (INR n + 1)). - apply Rplus_le_compat_r. apply pos_INR. apply H. - rewrite Rplus_0_l in H0. apply H0. apply Rlt_0_1. - - destruct n as [|n]. apply le_0_n. - apply le_n_S, IHm. - rewrite 2!S_INR in H. - apply Rplus_le_reg_r in H. apply H. -Qed. -Hint Resolve INR_le: creal. - -Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n # 1. -Proof. - intros n. - apply not_INR. -Qed. -Hint Resolve not_1_INR: creal. - -(*********************************************************) -(** ** Injection from [Z] to [R] *) -(*********************************************************) - -Lemma IPR_pos : forall p:positive, 0 < IPR p. -Proof. - intro p. rewrite <- INR_IPR. apply (lt_INR 0), Pos2Nat.is_pos. -Qed. - -Lemma IPR_double : forall p:positive, IPR (2*p) == 2 * IPR p. -Proof. - intro p. destruct p; try reflexivity. - rewrite Rmult_1_r. reflexivity. -Qed. - -Lemma INR_IZR_INZ : forall n:nat, INR n == IZR (Z.of_nat n). -Proof. - intros [|n]. - easy. - simpl Z.of_nat. unfold IZR. - now rewrite <- INR_IPR, SuccNat2Pos.id_succ. -Qed. - -Lemma plus_IZR_NEG_POS : - forall p q:positive, IZR (Zpos p + Zneg q) == IZR (Zpos p) + IZR (Zneg q). -Proof. - intros p q; simpl. rewrite Z.pos_sub_spec. - case Pos.compare_spec; intros H; unfold IZR. - subst. ring. - rewrite <- 3!INR_IPR, Pos2Nat.inj_sub. - rewrite minus_INR. - 2: (now apply lt_le_weak, Pos2Nat.inj_lt). - ring. - trivial. - rewrite <- 3!INR_IPR, Pos2Nat.inj_sub. - rewrite minus_INR. - 2: (now apply lt_le_weak, Pos2Nat.inj_lt). - unfold Rminus. ring. trivial. -Qed. - -Lemma plus_IPR : forall n m:positive, IPR (n + m) == IPR n + IPR m. -Proof. - intros. repeat rewrite <- INR_IPR. - rewrite Pos2Nat.inj_add. apply plus_INR. -Qed. - -(**********) -Lemma plus_IZR : forall n m:Z, IZR (n + m) == IZR n + IZR m. -Proof. - intro z; destruct z; intro t; destruct t; intros. - - rewrite Rplus_0_l. reflexivity. - - rewrite Rplus_0_l. rewrite Z.add_0_l. reflexivity. - - rewrite Rplus_0_l. reflexivity. - - rewrite Rplus_comm,Rplus_0_l. reflexivity. - - rewrite <- Pos2Z.inj_add. unfold IZR. apply plus_IPR. - - apply plus_IZR_NEG_POS. - - rewrite Rplus_comm,Rplus_0_l, Z.add_0_r. reflexivity. - - rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS. - - simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add, plus_INR. - ring. -Qed. - -Lemma mult_IPR : forall n m:positive, IPR (n * m) == IPR n * IPR m. -Proof. - intros. repeat rewrite <- INR_IPR. - rewrite Pos2Nat.inj_mul. apply mult_INR. -Qed. - -(**********) -Lemma mult_IZR : forall n m:Z, IZR (n * m) == IZR n * IZR m. -Proof. - intros n m. destruct n. - - rewrite Rmult_0_l. rewrite Z.mul_0_l. reflexivity. - - destruct m. rewrite Z.mul_0_r, Rmult_0_r. reflexivity. - simpl; unfold IZR. apply mult_IPR. - simpl. unfold IZR. rewrite mult_IPR. ring. - - destruct m. rewrite Z.mul_0_r, Rmult_0_r. reflexivity. - simpl. unfold IZR. rewrite mult_IPR. ring. - simpl. unfold IZR. rewrite mult_IPR. ring. -Qed. - -Lemma pow_IZR : forall z n, pow (IZR z) n == IZR (Z.pow z (Z.of_nat n)). -Proof. - intros z [|n];simpl; trivial. reflexivity. - rewrite Zpower_pos_nat. - rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl. - rewrite mult_IZR. - induction n;simpl;trivial. reflexivity. - rewrite mult_IZR;ring[IHn]. -Qed. - -(**********) -Lemma succ_IZR : forall n:Z, IZR (Z.succ n) == IZR n + 1. -Proof. - intro; unfold Z.succ; apply plus_IZR. -Qed. - -(**********) -Lemma opp_IZR : forall n:Z, IZR (- n) == - IZR n. -Proof. - intros [|z|z]; unfold IZR; simpl; auto with creal. - ring. - reflexivity. rewrite Ropp_involutive. reflexivity. -Qed. - -Definition Ropp_Ropp_IZR := opp_IZR. - -Lemma minus_IZR : forall n m:Z, IZR (n - m) == IZR n - IZR m. -Proof. - intros; unfold Z.sub, Rminus,CRminus. - rewrite <- opp_IZR. - apply plus_IZR. -Qed. - -(**********) -Lemma Z_R_minus : forall n m:Z, IZR n - IZR m == IZR (n - m). -Proof. - intros z1 z2; unfold Rminus,CRminus; unfold Z.sub. - rewrite <- (Ropp_Ropp_IZR z2); symmetry; apply plus_IZR. -Qed. - -(**********) -Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z. -Proof. - intro z; case z; simpl; intros. - elim (Rlt_irrefl _ H). - easy. - elim (Rlt_not_le _ _ H). - unfold IZR. - rewrite <- INR_IPR. - auto with creal. -Qed. - -(**********) -Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z. -Proof. - intros z1 z2 H; apply Z.lt_0_sub. - apply lt_0_IZR. - rewrite <- Z_R_minus. - exact (Rgt_minus (IZR z2) (IZR z1) H). -Qed. - -(**********) -Lemma eq_IZR_R0 : forall n:Z, IZR n == 0 -> n = 0%Z. -Proof. - intro z; destruct z; simpl; intros; auto with zarith. - unfold IZR in H. rewrite <- INR_IPR in H. - apply (INR_eq _ 0) in H. - exfalso. pose proof (Pos2Nat.is_pos p). - rewrite H in H0. inversion H0. - unfold IZR in H. rewrite <- INR_IPR in H. - apply (Rplus_eq_compat_r (INR (Pos.to_nat p))) in H. - rewrite Rplus_opp_l, Rplus_0_l in H. symmetry in H. - apply (INR_eq _ 0) in H. - exfalso. pose proof (Pos2Nat.is_pos p). - rewrite H in H0. inversion H0. -Qed. - -(**********) -Lemma eq_IZR : forall n m:Z, IZR n == IZR m -> n = m. -Proof. - intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H); - rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0); - intro; omega. -Qed. - -Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m. -Proof. - assert (forall n:Z, Z.lt 0 n -> 0 < IZR n) as posCase. - { intros. destruct (IZN n). apply Z.lt_le_incl. apply H. - subst n. rewrite <- INR_IZR_INZ. apply (lt_INR 0). - apply Nat2Z.inj_lt. apply H. } - intros. apply (Rplus_lt_reg_r (-(IZR n))). - pose proof minus_IZR. unfold Rminus,CRminus in H0. - repeat rewrite <- H0. unfold Zminus. - rewrite Z.add_opp_diag_r. apply posCase. - rewrite (Z.add_lt_mono_l _ _ n). ring_simplify. apply H. -Qed. - -(**********) -Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n # 0. -Proof. - intros. destruct n. exfalso. apply H. reflexivity. - right. apply (IZR_lt 0). reflexivity. - left. apply (IZR_lt _ 0). reflexivity. -Qed. - -(*********) -Lemma le_0_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z. -Proof. - intros. destruct n. discriminate. discriminate. - exfalso. rewrite <- Ropp_0 in H. unfold IZR in H. apply H. - apply Ropp_gt_lt_contravar. rewrite <- INR_IPR. - apply (lt_INR 0). apply Pos2Nat.is_pos. -Qed. - -(**********) -Lemma le_IZR : forall n m:Z, IZR n <= IZR m -> (n <= m)%Z. -Proof. - intros. apply (Rplus_le_compat_r (-(IZR n))) in H. - pose proof minus_IZR. unfold Rminus,CRminus in H0. - repeat rewrite <- H0 in H. unfold Zminus in H. - rewrite Z.add_opp_diag_r in H. - apply (Z.add_le_mono_l _ _ (-n)). ring_simplify. - rewrite Z.add_comm. apply le_0_IZR. apply H. -Qed. - -(**********) -Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z. -Proof. - intros. apply (le_IZR n 1). apply H. -Qed. - -(**********) -Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m. -Proof. - intros m n H; apply Rnot_lt_ge. intro abs. - apply lt_IZR in abs. omega. -Qed. - -Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m. -Proof. - intros m n H; apply Rnot_lt_ge. intro abs. - apply lt_IZR in abs. omega. -Qed. - -Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 # IZR z2. -Proof. - intros. destruct (not_0_IZR (z1-z2)). - intro abs. apply H. rewrite <- (Z.add_cancel_r _ _ (-z2)). - ring_simplify. exact abs. - left. apply IZR_lt. apply (lt_IZR _ 0) in c. - rewrite (Z.add_lt_mono_r _ _ (-z2)). - ring_simplify. exact c. - right. apply IZR_lt. apply (lt_IZR 0) in c. - rewrite (Z.add_lt_mono_l _ _ (-z2)). - ring_simplify. rewrite Z.add_comm. exact c. -Qed. - -Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : creal. -Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : creal. -Hint Extern 0 (IZR _ < IZR _) => apply IZR_lt, eq_refl : creal. -Hint Extern 0 (IZR _ > IZR _) => apply IZR_lt, eq_refl : creal. -Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : creal. - -Lemma one_IZR_lt1 : forall n:Z, -(1) < IZR n < 1 -> n = 0%Z. -Proof. - intros z [H1 H2]. - apply Z.le_antisymm. - apply Z.lt_succ_r; apply lt_IZR; trivial. - change 0%Z with (Z.succ (-1)). - apply Z.le_succ_l; apply lt_IZR; trivial. -Qed. - -Lemma one_IZR_r_R1 : - forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m. -Proof. - intros r z x [H1 H2] [H3 H4]. - cut ((z - x)%Z = 0%Z); auto with zarith. - apply one_IZR_lt1. - split; rewrite <- Z_R_minus. - setoid_replace (-(1)) with (r - (r + 1)). - unfold CReal_minus; apply Rplus_lt_le_compat; auto with creal. - ring. - setoid_replace 1 with (r + 1 - r). - unfold CReal_minus; apply Rplus_le_lt_compat; auto with creal. - ring. -Qed. - - -(**********) -Lemma single_z_r_R1 : - forall r (n m:Z), - r < IZR n -> IZR n <= r + 1 -> r < IZR m -> IZR m <= r + 1 -> n = m. -Proof. - intros; apply one_IZR_r_R1 with r; auto. -Qed. - -(**********) -Lemma tech_single_z_r_R1 : - forall r (n:Z), - r < IZR n -> - IZR n <= r + 1 -> - { s : Z & prod (s <> n) (r < IZR s <= r + 1) } -> False. -Proof. - intros r z H1 H2 [s [H3 [H4 H5]]]. - apply H3; apply single_z_r_R1 with r; trivial. -Qed. - - -Lemma Rmult_le_compat_l_half : forall r r1 r2, - 0 < r -> r1 <= r2 -> r * r1 <= r * r2. -Proof. - intros. intro abs. apply (Rmult_lt_reg_l) in abs. - contradiction. apply H. -Qed. - -Lemma INR_CR_of_Q : forall (n : nat), - CR_of_Q CR (Z.of_nat n # 1) == INR n. -Proof. - induction n. - - apply CR_of_Q_zero. - - transitivity (CR_of_Q CR (1 + (Z.of_nat n # 1))). - replace (S n) with (1 + n)%nat. 2: reflexivity. - rewrite (Nat2Z.inj_add 1 n). - apply CR_of_Q_proper. - rewrite <- (Qinv_plus_distr (Z.of_nat 1) (Z.of_nat n) 1). reflexivity. - rewrite CR_of_Q_plus. rewrite IHn. clear IHn. - setoid_replace (INR (S n)) with (1 + INR n). - rewrite CR_of_Q_one. reflexivity. - simpl. destruct n. rewrite Rplus_0_r. reflexivity. - rewrite Rplus_comm. reflexivity. -Qed. - -Definition Rup_nat (x : R) - : { n : nat & x < INR n }. -Proof. - intros. destruct (CR_archimedean CR x) as [p maj]. - exists (Pos.to_nat p). - rewrite <- INR_CR_of_Q, positive_nat_Z. exact maj. -Qed. - -Fixpoint Rarchimedean_ind (x:R) (n : Z) (p:nat) { struct p } - : (x < IZR n < x + 2 + (INR p)) - -> { n:Z & x < IZR n < x+2 }. -Proof. - destruct p. - - exists n. destruct H. split. exact r. rewrite Rplus_0_r in r0; exact r0. - - intros. destruct (linear_order_T (x+1+INR p) (IZR n) (x+2+INR p)). - do 2 rewrite Rplus_assoc. apply Rplus_lt_compat_l, Rplus_lt_compat_r. - rewrite <- (Rplus_0_r 1). apply Rplus_lt_compat_l. apply Rlt_0_1. - + apply (Rarchimedean_ind x (n-1)%Z p). unfold Zminus. - split; rewrite plus_IZR, opp_IZR. - setoid_replace (IZR 1) with 1. 2: reflexivity. - apply (Rplus_lt_reg_l 1). ring_simplify. - apply (Rle_lt_trans _ (x + 1 + INR p)). 2: exact r. - rewrite Rplus_assoc. apply Rplus_le_compat_l. - rewrite <- (Rplus_0_r 1), Rplus_assoc. apply Rplus_le_compat_l. - rewrite Rplus_0_l. apply (le_INR 0), le_0_n. - setoid_replace (IZR 1) with 1. 2: reflexivity. - apply (Rplus_lt_reg_l 1). ring_simplify. - setoid_replace (x + 2 + INR p + 1) with (x + 2 + INR (S p)). - apply H. rewrite S_INR. ring. - + apply (Rarchimedean_ind x n p). split. apply H. exact r. -Qed. - -Lemma Rarchimedean (x:R) : { n : Z & x < IZR n < x + 2 }. -Proof. - destruct (Rup_nat x) as [n nmaj]. - destruct (Rup_nat (INR n + - (x + 2))) as [p pmaj]. - apply (Rplus_lt_compat_r (x+2)) in pmaj. - rewrite Rplus_assoc, Rplus_opp_l, Rplus_0_r in pmaj. - apply (Rarchimedean_ind x (Z.of_nat n) p). - split; rewrite <- INR_IZR_INZ. exact nmaj. - rewrite Rplus_comm in pmaj. exact pmaj. -Qed. - -Lemma Rmult_le_0_compat : forall a b, - 0 <= a -> 0 <= b -> 0 <= a * b. -Proof. - (* Limit of (a + 1/n)*b when n -> infty. *) - intros. intro abs. - assert (0 < -(a*b)) as epsPos. - { rewrite <- Ropp_0. apply Ropp_gt_lt_contravar. apply abs. } - pose proof (Rup_nat (b * (/ (-(a*b))) (inr (Ropp_0_gt_lt_contravar _ abs)))) - as [n maj]. - destruct n as [|n]. - - simpl in maj. apply (Rmult_lt_compat_r (-(a*b))) in maj. - rewrite Rmult_0_l in maj. - rewrite Rmult_assoc in maj. rewrite Rinv_l in maj. - rewrite Rmult_1_r in maj. contradiction. - apply epsPos. - - (* n > 0 *) - assert (0 < INR (S n)) as nPos. - { apply (lt_INR 0). apply le_n_S, le_0_n. } - assert (b * (/ (INR (S n))) (inr nPos) < -(a*b)). - { apply (Rmult_lt_reg_r (INR (S n))). apply nPos. - rewrite Rmult_assoc. rewrite Rinv_l. - rewrite Rmult_1_r. apply (Rmult_lt_compat_r (-(a*b))) in maj. - rewrite Rmult_assoc in maj. rewrite Rinv_l in maj. - rewrite Rmult_1_r in maj. rewrite Rmult_comm. - apply maj. exact epsPos. } - pose proof (Rmult_le_compat_l_half (a + (/ (INR (S n))) (inr nPos)) - 0 b). - assert (a + (/ (INR (S n))) (inr nPos) > 0 + 0). - apply Rplus_le_lt_compat. apply H. apply Rinv_0_lt_compat. - rewrite Rplus_0_l in H3. specialize (H2 H3 H0). - clear H3. rewrite Rmult_0_r in H2. - apply H2. clear H2. rewrite Rmult_plus_distr_r. - apply (Rplus_lt_compat_l (a*b)) in H1. - rewrite Rplus_opp_r in H1. - rewrite (Rmult_comm ((/ (INR (S n))) (inr nPos))). - apply H1. -Qed. - -Lemma Rmult_le_compat_l : forall r r1 r2, - 0 <= r -> r1 <= r2 -> r * r1 <= r * r2. -Proof. - intros. apply Rminus_ge. apply Rge_minus in H0. - unfold Rminus,CRminus. rewrite Ropp_mult_distr_r. - rewrite <- Rmult_plus_distr_l. - apply Rmult_le_0_compat; assumption. -Qed. -Hint Resolve Rmult_le_compat_l: creal. - -Lemma Rmult_le_compat_r : forall r r1 r2, - 0 <= r -> r1 <= r2 -> r1 * r <= r2 * r. -Proof. - intros. rewrite <- (Rmult_comm r). rewrite <- (Rmult_comm r). - apply Rmult_le_compat_l; assumption. -Qed. -Hint Resolve Rmult_le_compat_r: creal. - -(*********) -Lemma Rmult_le_0_lt_compat : - forall r1 r2 r3 r4, - 0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. -Proof. - intros. apply (Rle_lt_trans _ (r2 * r3)). - apply Rmult_le_compat_r. apply H0. intro abs. apply (Rlt_asym r1 r2 H1). - apply abs. apply Rmult_lt_compat_l. exact (Rle_lt_trans 0 r1 r2 H H1). - exact H2. -Qed. - -Lemma Rmult_le_compat_neg_l : - forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1. -Proof. - intros. apply Ropp_le_cancel. - do 2 rewrite Ropp_mult_distr_l. apply Rmult_le_compat_l. - 2: exact H0. apply Ropp_0_ge_le_contravar. exact H. -Qed. -Hint Resolve Rmult_le_compat_neg_l: creal. - -Lemma Rmult_le_ge_compat_neg_l : - forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r1 >= r * r2. -Proof. - intros; apply Rle_ge; auto with creal. -Qed. -Hint Resolve Rmult_le_ge_compat_neg_l: creal. - - -(**********) -Lemma Rmult_ge_compat_l : - forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2. -Proof. - intros. apply Rmult_le_compat_l; assumption. -Qed. - -Lemma Rmult_ge_compat_r : - forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r. -Proof. - intros. apply Rmult_le_compat_r; assumption. -Qed. - - -(**********) -Lemma Rmult_le_compat : - forall r1 r2 r3 r4, - 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. -Proof. - intros x y z t H' H'0 H'1 H'2. - apply Rle_trans with (r2 := x * t); auto with creal. - repeat rewrite (fun x => Rmult_comm x t). - apply Rmult_le_compat_l; auto. - apply Rle_trans with z; auto. -Qed. -Hint Resolve Rmult_le_compat: creal. - -Lemma Rmult_ge_compat : - forall r1 r2 r3 r4, - r2 >= 0 -> r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4. -Proof. auto with creal rorders. Qed. - -Lemma mult_IPR_IZR : forall (n:positive) (m:Z), IZR (Z.pos n * m) == IPR n * IZR m. -Proof. - intros. rewrite mult_IZR. apply Rmult_eq_compat_r. reflexivity. -Qed. - -Definition IQR (q:Q) : R := - match q with - | Qmake a b => IZR a * (/ (IPR b)) (inr (IPR_pos b)) - end. -Arguments IQR q%Q : simpl never. - -Lemma plus_IQR : forall n m:Q, IQR (n + m) == IQR n + IQR m. -Proof. - intros. destruct n,m; unfold Qplus,IQR; simpl. - rewrite plus_IZR. repeat rewrite mult_IZR. - setoid_replace ((/ IPR (Qden * Qden0)) (inr (IPR_pos (Qden * Qden0)))) - with ((/ IPR Qden) (inr (IPR_pos Qden)) - * (/ IPR Qden0) (inr (IPR_pos Qden0))). - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. rewrite <- (Rmult_assoc (IZR (Z.pos Qden))). - rewrite Rinv_r. rewrite Rmult_1_l. - rewrite (Rmult_comm ((/IPR Qden) (inr (IPR_pos Qden)))). - rewrite <- (Rmult_assoc (IZR (Z.pos Qden0))). - rewrite Rinv_r. rewrite Rmult_1_l. reflexivity. unfold IZR. - right. apply IPR_pos. - right. apply IPR_pos. - rewrite <- (Rinv_mult_distr - _ _ _ _ (inr (Rmult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))). - apply Rinv_eq_compat. apply mult_IPR. -Qed. - -Lemma IQR_pos : forall q:Q, Qlt 0 q -> 0 < IQR q. -Proof. - intros. destruct q; unfold IQR. - apply Rmult_lt_0_compat. apply (IZR_lt 0). - unfold Qlt in H; simpl in H. - rewrite Z.mul_1_r in H. apply H. - apply Rinv_0_lt_compat. -Qed. - -Lemma opp_IQR : forall q:Q, IQR (- q) == - IQR q. -Proof. - intros [a b]; unfold IQR; simpl. - rewrite Ropp_mult_distr_l. - rewrite opp_IZR. reflexivity. -Qed. - -Lemma lt_IQR : forall n m:Q, IQR n < IQR m -> (n < m)%Q. -Proof. - intros. destruct n,m; unfold IQR in H. - unfold Qlt; simpl. apply (Rmult_lt_compat_r (IPR Qden)) in H. - rewrite Rmult_assoc in H. rewrite Rinv_l in H. - rewrite Rmult_1_r in H. rewrite (Rmult_comm (IZR Qnum0)) in H. - apply (Rmult_lt_compat_l (IPR Qden0)) in H. - do 2 rewrite <- Rmult_assoc in H. rewrite Rinv_r in H. - rewrite Rmult_1_l in H. - rewrite (Rmult_comm (IZR Qnum0)) in H. - do 2 rewrite <- mult_IPR_IZR in H. apply lt_IZR in H. - rewrite Z.mul_comm. rewrite (Z.mul_comm Qnum0). - apply H. - right. rewrite <- INR_IPR. apply (lt_INR 0). apply Pos2Nat.is_pos. - rewrite <- INR_IPR. apply (lt_INR 0). apply Pos2Nat.is_pos. - apply IPR_pos. -Qed. - -Lemma IQR_lt : forall n m:Q, Qlt n m -> IQR n < IQR m. -Proof. - intros. apply (Rplus_lt_reg_r (-IQR n)). - rewrite Rplus_opp_r. rewrite <- opp_IQR. rewrite <- plus_IQR. - apply IQR_pos. apply (Qplus_lt_l _ _ n). - ring_simplify. apply H. -Qed. - -Lemma IQR_nonneg : forall q:Q, Qle 0 q -> 0 <= (IQR q). -Proof. - intros [a b] H. unfold IQR;simpl. - apply (Rle_trans _ (IZR a * 0)). rewrite Rmult_0_r. apply Rle_refl. - apply Rmult_le_compat_l. - apply (IZR_le 0 a). unfold Qle in H; simpl in H. - rewrite Z.mul_1_r in H. apply H. - unfold Rle. apply Rlt_asym. apply Rinv_0_lt_compat. -Qed. - -Lemma IQR_le : forall n m:Q, Qle n m -> IQR n <= IQR m. -Proof. - intros. apply (Rplus_le_reg_r (-IQR n)). - rewrite Rplus_opp_r. rewrite <- opp_IQR. rewrite <- plus_IQR. - apply IQR_nonneg. apply (Qplus_le_l _ _ n). - ring_simplify. apply H. -Qed. - -Add Parametric Morphism : IQR - with signature Qeq ==> Req - as IQR_morph. -Proof. - intros. destruct x,y; unfold IQR; simpl. - unfold Qeq in H; simpl in H. - apply (Rmult_eq_reg_r (IZR (Z.pos Qden))). - rewrite Rmult_assoc. rewrite Rinv_l. rewrite Rmult_1_r. - rewrite (Rmult_comm (IZR Qnum0)). - apply (Rmult_eq_reg_l (IZR (Z.pos Qden0))). - rewrite <- Rmult_assoc. rewrite <- Rmult_assoc. rewrite Rinv_r. - rewrite Rmult_1_l. - repeat rewrite <- mult_IZR. - rewrite <- H. rewrite Zmult_comm. reflexivity. - right. apply IPR_pos. - right. apply (IZR_lt 0). apply Pos2Z.is_pos. - right. apply IPR_pos. -Qed. - -Instance IQR_morph_T - : CMorphisms.Proper - (CMorphisms.respectful Qeq Req) IQR. -Proof. - intros x y H. destruct x,y; unfold IQR. - unfold Qeq in H; simpl in H. - apply (Rmult_eq_reg_r (IZR (Z.pos Qden))). - 2: right; apply IPR_pos. - rewrite Rmult_assoc, Rinv_l, Rmult_1_r. - rewrite (Rmult_comm (IZR Qnum0)). - apply (Rmult_eq_reg_l (IZR (Z.pos Qden0))). - 2: right; apply IPR_pos. - rewrite <- Rmult_assoc, <- Rmult_assoc, Rinv_r. - rewrite Rmult_1_l. - repeat rewrite <- mult_IZR. - rewrite <- H. rewrite Zmult_comm. reflexivity. - right; apply IPR_pos. -Qed. - -Fixpoint Rfloor_pos (a : R) (n : nat) { struct n } - : 0 < a - -> a < INR n - -> { p : nat & INR p < a < INR p + 2 }. -Proof. - (* Decreasing loop on n, until it is the first integer above a. *) - intros H H0. destruct n. - - exfalso. apply (Rlt_asym 0 a); assumption. - - destruct n as [|p] eqn:des. - + (* n = 1 *) exists O. split. - apply H. rewrite Rplus_0_l. apply (Rlt_trans a (1+0)). - rewrite Rplus_comm, Rplus_0_l. apply H0. - apply Rplus_le_lt_compat. - apply Rle_refl. apply Rlt_0_1. - + (* n > 1 *) - destruct (linear_order_T (INR p) a (INR (S p))). - * rewrite <- Rplus_0_l, S_INR, Rplus_comm. apply Rplus_lt_compat_l. - apply Rlt_0_1. - * exists p. split. exact r. - rewrite S_INR, S_INR, Rplus_assoc in H0. exact H0. - * apply (Rfloor_pos a n H). rewrite des. apply r. -Qed. - -Definition Rfloor (a : R) - : { p : Z & IZR p < a < IZR p + 2 }. -Proof. - destruct (linear_order_T 0 a 1 Rlt_0_1). - - destruct (Rup_nat a). destruct (Rfloor_pos a x r r0). - exists (Z.of_nat x0). split; rewrite <- INR_IZR_INZ; apply p. - - apply (Rplus_lt_compat_l (-a)) in r. - rewrite Rplus_comm, Rplus_opp_r, Rplus_comm in r. - destruct (Rup_nat (1-a)). - destruct (Rfloor_pos (1-a) x r r0). - exists (-(Z.of_nat x0 + 1))%Z. split; rewrite opp_IZR, plus_IZR. - + rewrite <- (Ropp_involutive a). apply Ropp_gt_lt_contravar. - destruct p as [_ a0]. apply (Rplus_lt_reg_r 1). - rewrite Rplus_comm, Rplus_assoc. rewrite <- INR_IZR_INZ. apply a0. - + destruct p as [a0 _]. apply (Rplus_lt_compat_l a) in a0. - unfold Rminus in a0. - rewrite <- (Rplus_comm (1+-a)), Rplus_assoc, Rplus_opp_l, Rplus_0_r in a0. - rewrite <- INR_IZR_INZ. - apply (Rplus_lt_reg_r (INR x0)). unfold IZR, IPR, IPR_2. - ring_simplify. exact a0. -Qed. - -(* A point in an archimedean field is the limit of a - sequence of rational numbers (n maps to the q between - a and a+1/n). This is how real numbers compute, - and they are measured by exact rational numbers. *) -Definition RQ_dense (a b : R) - : a < b -> { q : Q & a < IQR q < b }. -Proof. - intros H0. - assert (0 < b - a) as epsPos. - { apply (Rplus_lt_compat_r (-a)) in H0. - rewrite Rplus_opp_r in H0. apply H0. } - pose proof (Rup_nat ((/(b-a)) (inr epsPos))) - as [n maj]. - destruct n as [|k]. - - exfalso. - apply (Rmult_lt_compat_l (b-a)) in maj. 2: apply epsPos. - rewrite Rmult_0_r in maj. rewrite Rinv_r in maj. - apply (Rlt_asym 0 1). apply Rlt_0_1. apply maj. - right. apply epsPos. - - (* 0 < n *) - pose (Pos.of_nat (S k)) as n. - destruct (Rfloor (IZR (2 * Z.pos n) * b)) as [p maj2]. - exists (p # (2*n))%Q. split. - + apply (Rlt_trans a (b - IQR (1 # n))). - apply (Rplus_lt_reg_r (IQR (1#n))). - unfold Rminus,CRminus. rewrite Rplus_assoc. rewrite Rplus_opp_l. - rewrite Rplus_0_r. apply (Rplus_lt_reg_l (-a)). - rewrite <- Rplus_assoc, Rplus_opp_l, Rplus_0_l. - rewrite Rplus_comm. unfold IQR. - rewrite Rmult_1_l. apply (Rmult_lt_reg_l (IPR n)). - apply IPR_pos. rewrite Rinv_r. - apply (Rmult_lt_compat_l (b-a)) in maj. - rewrite Rinv_r, Rmult_comm in maj. - rewrite <- INR_IPR. unfold n. rewrite Nat2Pos.id. - apply maj. discriminate. right. exact epsPos. exact epsPos. - right. apply IPR_pos. - apply (Rplus_lt_reg_r (IQR (1 # n))). - unfold Rminus,CRminus. rewrite Rplus_assoc, Rplus_opp_l. - rewrite Rplus_0_r. rewrite <- plus_IQR. - destruct maj2 as [_ maj2]. - setoid_replace ((p # 2 * n) + (1 # n))%Q - with ((p + 2 # 2 * n))%Q. unfold IQR. - apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))). - apply (IZR_lt 0). reflexivity. rewrite Rmult_assoc. - rewrite Rinv_l. rewrite Rmult_1_r. rewrite Rmult_comm. - rewrite plus_IZR. apply maj2. - setoid_replace (1#n)%Q with (2#2*n)%Q. 2: reflexivity. - apply Qinv_plus_distr. - + destruct maj2 as [maj2 _]. unfold IQR. - apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))). - apply (IZR_lt 0). apply Pos2Z.is_pos. rewrite Rmult_assoc, Rinv_l. - rewrite Rmult_1_r, Rmult_comm. apply maj2. -Qed. - -Definition RQ_limit : forall (x : R) (n:nat), - { q:Q & x < IQR q < x + IQR (1 # Pos.of_nat n) }. -Proof. - intros x n. apply (RQ_dense x (x + IQR (1 # Pos.of_nat n))). - rewrite <- (Rplus_0_r x). rewrite Rplus_assoc. - apply Rplus_lt_compat_l. rewrite Rplus_0_l. apply IQR_pos. - reflexivity. -Qed. - -(* Rlt is decided by the LPO in Type, - which is a non-constructive oracle. *) -Lemma Rlt_lpo_dec : forall x y : R, - (forall (P : nat -> Prop), (forall n, {P n} + {~P n}) - -> {n | ~P n} + {forall n, P n}) - -> (x < y) + (y <= x). -Proof. - intros x y lpo. - pose (fun n => let (l,_) := RQ_limit x n in l) as xn. - pose (fun n => let (l,_) := RQ_limit y n in l) as yn. - destruct (lpo (fun n:nat => Qle (yn n - xn n) (1 # Pos.of_nat n))). - - intro n. destruct (Qlt_le_dec (1 # Pos.of_nat n) (yn n - xn n)). - right. apply Qlt_not_le. exact q. left. exact q. - - left. destruct s as [n nmaj]. unfold xn,yn in nmaj. - destruct (RQ_limit x n), (RQ_limit y n); unfold proj1_sig in nmaj. - apply Qnot_le_lt in nmaj. - apply (Rlt_le_trans x (IQR x0)). apply p. - apply (Rle_trans _ (IQR (x1 - (1# Pos.of_nat n)))). - apply IQR_le. apply (Qplus_le_l _ _ ((1#Pos.of_nat n) - x0)). - ring_simplify. ring_simplify in nmaj. rewrite Qplus_comm. - apply Qlt_le_weak. exact nmaj. - unfold Qminus. rewrite plus_IQR,opp_IQR. - apply (Rplus_le_reg_r (IQR (1#Pos.of_nat n))). - ring_simplify. unfold Rle. apply Rlt_asym. rewrite Rplus_comm. apply p0. - - right. intro abs. - pose ((y - x) * IQR (1#2)) as eps. - assert (0 < eps) as epsPos. - { apply Rmult_lt_0_compat. apply Rgt_minus. exact abs. - apply IQR_pos. reflexivity. } - destruct (Rup_nat ((/eps) (inr epsPos))) as [n nmaj]. - specialize (q (S n)). unfold xn, yn in q. - destruct (RQ_limit x (S n)) as [a amaj], (RQ_limit y (S n)) as [b bmaj]; - unfold proj1_sig in q. - assert (IQR (1 # Pos.of_nat (S n)) < eps). - { unfold IQR. rewrite Rmult_1_l. - apply (Rmult_lt_reg_l (IPR (Pos.of_nat (S n)))). apply IPR_pos. - rewrite Rinv_r, <- INR_IPR, Nat2Pos.id. 2: discriminate. - apply (Rlt_trans _ _ (INR (S n))) in nmaj. - apply (Rmult_lt_compat_l eps) in nmaj. - rewrite Rinv_r, Rmult_comm in nmaj. exact nmaj. - right. exact epsPos. exact epsPos. apply lt_INR. apply le_n_S, le_refl. - right. apply IPR_pos. } - unfold eps in H. apply (Rlt_asym y (IQR b)). - + apply bmaj. - + apply (Rlt_le_trans _ (IQR a + (y - x) * IQR (1 # 2))). - apply IQR_le in q. - apply (Rle_lt_trans _ _ _ q) in H. - apply (Rplus_lt_reg_l (-IQR a)). - rewrite <- Rplus_assoc, Rplus_opp_l, Rplus_0_l, Rplus_comm, - <- opp_IQR, <- plus_IQR. exact H. - apply (Rplus_lt_compat_l x) in H. - destruct amaj. apply (Rlt_trans _ _ _ r0) in H. - apply (Rplus_lt_compat_r ((y - x) * IQR (1 # 2))) in H. - unfold Rle. apply Rlt_asym. - setoid_replace (x + (y - x) * IQR (1 # 2) + (y - x) * IQR (1 # 2)) with y in H. - exact H. - rewrite Rplus_assoc, <- Rmult_plus_distr_r. - setoid_replace (y - x + (y - x)) with ((y-x)*2). - unfold IQR. rewrite Rmult_1_l, Rmult_assoc, Rinv_r. ring. - right. apply (IZR_lt 0). reflexivity. - unfold IZR, IPR, IPR_2. ring. -Qed. - -Lemma Rlt_lpo_floor : forall x : R, - (forall (P : nat -> Prop), (forall n, {P n} + {~P n}) - -> {n | ~P n} + {forall n, P n}) - -> { p : Z & IZR p <= x < IZR p + 1 }. -Proof. - intros x lpo. destruct (Rfloor x) as [n [H H0]]. - destruct (Rlt_lpo_dec x (IZR n + 1) lpo). - - exists n. split. unfold Rle. apply Rlt_asym. exact H. exact r. - - exists (n+1)%Z. split. rewrite plus_IZR. exact r. - rewrite plus_IZR, Rplus_assoc. exact H0. -Qed. - - -(*********) -Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2. -Proof. - intros x y H H0; rewrite <- (Rmult_0_l x); rewrite <- (Rmult_comm x); - apply (Rmult_le_compat_l x 0 y H H0). -Qed. - -Lemma Rinv_le_contravar : - forall x y (xpos : 0 < x) (ynz : y # 0), - x <= y -> (/ y) ynz <= (/ x) (inr xpos). -Proof. - intros. intro abs. apply (Rmult_lt_compat_l x) in abs. - 2: apply xpos. rewrite Rinv_r in abs. - apply (Rmult_lt_compat_r y) in abs. - rewrite Rmult_assoc in abs. rewrite Rinv_l in abs. - rewrite Rmult_1_r in abs. rewrite Rmult_1_l in abs. contradiction. - exact (Rlt_le_trans _ x _ xpos H). - right. exact xpos. -Qed. - -Lemma Rle_Rinv : forall x y (xpos : 0 < x) (ypos : 0 < y), - x <= y -> (/ y) (inr ypos) <= (/ x) (inr xpos). -Proof. - intros. - apply Rinv_le_contravar with (1 := H). -Qed. - -Lemma Ropp_div : forall x y (ynz : y # 0), - -x * (/y) ynz == - (x * (/ y) ynz). -Proof. - intros; ring. -Qed. - -Lemma double : forall r1, 2 * r1 == r1 + r1. -Proof. - intros. rewrite (Rmult_plus_distr_r 1 1 r1), Rmult_1_l. reflexivity. -Qed. - -Lemma Rlt_0_2 : 0 < 2. -Proof. - apply (Rlt_trans 0 (0+1)). rewrite Rplus_0_l. exact Rlt_0_1. - apply Rplus_lt_le_compat. exact Rlt_0_1. apply Rle_refl. -Qed. - -Lemma double_var : forall r1, r1 == r1 * (/ 2) (inr Rlt_0_2) - + r1 * (/ 2) (inr Rlt_0_2). -Proof. - intro; rewrite <- double; rewrite <- Rmult_assoc; - symmetry ; apply Rinv_r_simpl_m. -Qed. - -(* IZR : Z -> R is a ring morphism *) -Lemma R_rm : ring_morph - 0 1 Rplus Rmult Rminus Ropp Req - 0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR. -Proof. -constructor ; try easy. -exact plus_IZR. -exact minus_IZR. -exact mult_IZR. -exact opp_IZR. -intros x y H. -replace y with x. reflexivity. -now apply Zeq_bool_eq. -Qed. - -Lemma Zeq_bool_IZR x y : - IZR x == IZR y -> Zeq_bool x y = true. -Proof. -intros H. -apply Zeq_is_eq_bool. -now apply eq_IZR. -Qed. - - -(*********************************************************) -(** ** Other rules about < and <= *) -(*********************************************************) - -Lemma Rmult_ge_0_gt_0_lt_compat : - forall r1 r2 r3 r4, - r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. -Proof. - intros. apply (Rle_lt_trans _ (r2 * r3)). - apply Rmult_le_compat_r. apply H. unfold Rle. apply Rlt_asym. apply H1. - apply Rmult_lt_compat_l. apply H0. apply H2. -Qed. - -Lemma le_epsilon : - forall r1 r2, (forall eps, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2. -Proof. - intros x y H. intro abs. - assert (0 < (x - y) * (/ 2) (inr Rlt_0_2)). - { apply (Rplus_lt_compat_r (-y)) in abs. rewrite Rplus_opp_r in abs. - apply Rmult_lt_0_compat. exact abs. - apply Rinv_0_lt_compat. } - specialize (H ((x - y) * (/ 2) (inr Rlt_0_2)) H0). - apply (Rmult_le_compat_l 2) in H. - rewrite Rmult_plus_distr_l in H. - apply (Rplus_le_compat_l (-x)) in H. - rewrite (Rmult_comm (x-y)), <- Rmult_assoc, Rinv_r, Rmult_1_l, - (Rmult_plus_distr_r 1 1), (Rmult_plus_distr_r 1 1) - in H. - ring_simplify in H; contradiction. - right. apply Rlt_0_2. unfold Rle. apply Rlt_asym. apply Rlt_0_2. -Qed. - -(**********) -Lemma Rdiv_lt_0_compat : forall a b (bpos : 0 < b), - 0 < a -> 0 < a * (/b) (inr bpos). -Proof. -intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption. -Qed. - -Lemma Rdiv_plus_distr : forall a b c (cnz : c # 0), - (a + b)* (/c) cnz == a* (/c) cnz + b* (/c) cnz. -Proof. - intros. apply Rmult_plus_distr_r. -Qed. - -Lemma Rdiv_minus_distr : forall a b c (cnz : c # 0), - (a - b)* (/c) cnz == a* (/c) cnz - b* (/c) cnz. -Proof. - intros; unfold Rminus,CRminus; rewrite Rmult_plus_distr_r. - apply Rplus_morph. reflexivity. - rewrite Ropp_mult_distr_l. reflexivity. -Qed. - - -(*********************************************************) -(** * Definitions of new types *) -(*********************************************************) - -Record nonnegreal : Type := mknonnegreal - {nonneg :> R; cond_nonneg : 0 <= nonneg}. - -Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}. - -Record nonposreal : Type := mknonposreal - {nonpos :> R; cond_nonpos : nonpos <= 0}. - -Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}. - -Record nonzeroreal : Type := mknonzeroreal - {nonzero :> R; cond_nonzero : nonzero <> 0}. diff --git a/theories/Reals/ConstructiveRcomplete.v b/theories/Reals/ConstructiveRcomplete.v index 0a515672f2..b575c17961 100644 --- a/theories/Reals/ConstructiveRcomplete.v +++ b/theories/Reals/ConstructiveRcomplete.v @@ -11,6 +11,7 @@ Require Import QArith_base. Require Import Qabs. +Require Import ConstructiveReals. Require Import ConstructiveCauchyRealsMult. Require Import Logic.ConstructiveEpsilon. @@ -347,3 +348,35 @@ Proof. apply Qplus_le_r. discriminate. rewrite Qinv_plus_distr. reflexivity. Qed. + +Definition CRealImplem : ConstructiveReals. +Proof. + assert (isLinearOrder CReal CRealLt) as lin. + { repeat split. exact CRealLt_asym. + exact CReal_lt_trans. + intros. destruct (CRealLt_dec x z y H). + left. exact c. right. exact c. } + apply (Build_ConstructiveReals + CReal CRealLt lin CRealLtProp + CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon + (inject_Q 0) (inject_Q 1) + CReal_plus CReal_opp CReal_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). + - intros. destruct (Rcauchy_complete xn) as [l cv]. + intro n. destruct (H n). exists x. intros. + specialize (a i j H0 H1) as [a b]. split. 2: exact b. + rewrite <- opp_inject_Q. + setoid_replace (-(1#n))%Q with (-1#n)%Q. exact a. reflexivity. + exists l. intros p. destruct (cv p). + exists x. intros. specialize (a i H0). split. 2: apply a. + unfold orderLe. + intro abs. setoid_replace (-1#p)%Q with (-(1#p))%Q in abs. + rewrite opp_inject_Q in abs. destruct a. contradiction. + reflexivity. +Defined. diff --git a/theories/Reals/ConstructiveRealsMorphisms.v b/theories/Reals/ConstructiveRealsMorphisms.v index 0d3027d475..7954e9a96c 100644 --- a/theories/Reals/ConstructiveRealsMorphisms.v +++ b/theories/Reals/ConstructiveRealsMorphisms.v @@ -29,7 +29,7 @@ Require Import QArith. Require Import Qabs. Require Import ConstructiveReals. Require Import ConstructiveCauchyRealsMult. -Require Import ConstructiveRIneq. +Require Import ConstructiveRcomplete. Record ConstructiveRealsMorphism (R1 R2 : ConstructiveReals) : Set := diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 3b108b485a..7813c7b975 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -13,7 +13,8 @@ (** * Basic lemmas for the classical real numbers *) (*********************************************************) -Require Import ConstructiveRIneq. +Require Import ConstructiveCauchyReals. +Require Import ConstructiveCauchyRealsMult. Require Export Raxioms. Require Import Rpow_def. Require Import Zpower. @@ -457,11 +458,13 @@ Qed. Lemma Rplus_eq_0_l : forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0. Proof. - intros. apply Rquot1. rewrite Rrepr_0. - apply (Rplus_eq_0_l (Rrepr r1) (Rrepr r2)). - rewrite Rrepr_le, Rrepr_0 in H. exact H. - rewrite Rrepr_le, Rrepr_0 in H0. exact H0. - rewrite <- Rrepr_plus, H1, Rrepr_0. reflexivity. + intros a b H [H0| H0] H1; auto with real. + absurd (0 < a + b). + rewrite H1; auto with real. + apply Rle_lt_trans with (a + 0). + rewrite Rplus_0_r; assumption. + auto using Rplus_lt_compat_l with real. + rewrite <- H0, Rplus_0_r in H1; assumption. Qed. Lemma Rplus_eq_R0 : @@ -541,9 +544,10 @@ Qed. (**********) Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2. Proof. - intros. apply Rquot1. apply (Rmult_eq_reg_l (Rrepr r)). - rewrite <- Rrepr_mult, <- Rrepr_mult, H. reflexivity. + intros. apply Rquot1. apply (CReal_mult_eq_reg_l (Rrepr r)). apply Rrepr_appart in H0. rewrite Rrepr_0 in H0. exact H0. + apply Rrepr_appart in H0. + rewrite <- Rrepr_mult, <- Rrepr_mult, H. reflexivity. Qed. Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r = r2 * r -> r <> 0 -> r1 = r2. @@ -996,16 +1000,16 @@ Qed. Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. Proof. - intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_l (Rrepr r)). + intros. rewrite Rlt_def. apply CRealLtForget. apply (CReal_plus_lt_reg_l (Rrepr r)). rewrite <- Rrepr_plus, <- Rrepr_plus. - rewrite Rlt_def in H. apply Rlt_epsilon. exact H. + rewrite Rlt_def in H. apply CRealLtEpsilon. exact H. Qed. Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2. Proof. - intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_r (Rrepr r)). + intros. rewrite Rlt_def. apply CRealLtForget. apply (CReal_plus_lt_reg_r (Rrepr r)). rewrite <- Rrepr_plus, <- Rrepr_plus. rewrite Rlt_def in H. - apply Rlt_epsilon. exact H. + apply CRealLtEpsilon. exact H. Qed. Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. @@ -1076,18 +1080,18 @@ Qed. Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2. Proof. intros. rewrite Rlt_def. rewrite Rrepr_opp, Rrepr_opp. - apply Rlt_forget. - apply Ropp_gt_lt_contravar. unfold Rgt in H. - rewrite Rlt_def in H. apply Rlt_epsilon. exact H. + apply CRealLtForget. + apply CReal_opp_gt_lt_contravar. unfold Rgt in H. + rewrite Rlt_def in H. apply CRealLtEpsilon. exact H. Qed. Hint Resolve Ropp_gt_lt_contravar : core. Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2. Proof. intros. unfold Rgt. rewrite Rlt_def. rewrite Rrepr_opp, Rrepr_opp. - apply Rlt_forget. - apply Ropp_lt_gt_contravar. rewrite Rlt_def in H. - apply Rlt_epsilon. exact H. + apply CRealLtForget. + apply CReal_opp_gt_lt_contravar. rewrite Rlt_def in H. + apply CRealLtEpsilon. exact H. Qed. Hint Resolve Ropp_lt_gt_contravar: real. @@ -1239,10 +1243,11 @@ Lemma Rmult_le_compat : forall r1 r2 r3 r4, 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. Proof. - intros. rewrite Rrepr_le, Rrepr_mult, Rrepr_mult. - apply Rmult_le_compat. rewrite <- Rrepr_0, <- Rrepr_le. exact H. - rewrite <- Rrepr_0, <- Rrepr_le. exact H0. - rewrite <- Rrepr_le. exact H1. rewrite <- Rrepr_le. exact H2. + intros x y z t H' H'0 H'1 H'2. + apply Rle_trans with (r2 := x * t); auto with real. + repeat rewrite (fun x => Rmult_comm x t). + apply Rmult_le_compat_l; auto. + apply Rle_trans with z; auto. Qed. Hint Resolve Rmult_le_compat: real. @@ -1307,18 +1312,20 @@ Qed. Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. Proof. - intros. rewrite Rlt_def in H,H0. rewrite Rlt_def. apply Rlt_forget. - apply (Rmult_lt_reg_l (Rrepr r)). - rewrite <- Rrepr_0. apply Rlt_epsilon. exact H. - rewrite <- Rrepr_mult, <- Rrepr_mult. apply Rlt_epsilon. exact H0. + intros z x y H H0. + case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0. + rewrite Eq0 in H0; exfalso; apply (Rlt_irrefl (z * y)); auto. + generalize (Rmult_lt_compat_l z y x H Eq0); intro; exfalso; + generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); + intro; apply (Rlt_irrefl (z * x)); auto. Qed. Lemma Rmult_lt_reg_r : forall r r1 r2 : R, 0 < r -> r1 * r < r2 * r -> r1 < r2. Proof. - intros. rewrite Rlt_def. rewrite Rlt_def in H, H0. - apply Rlt_forget. apply (Rmult_lt_reg_r (Rrepr r)). - rewrite <- Rrepr_0. apply Rlt_epsilon. exact H. - rewrite <- Rrepr_mult, <- Rrepr_mult. apply Rlt_epsilon. exact H0. + intros. + apply Rmult_lt_reg_l with r. + exact H. + now rewrite 2!(Rmult_comm r). Qed. Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. @@ -1326,10 +1333,14 @@ Proof. eauto using Rmult_lt_reg_l with rorders. Qed. Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2. Proof. - intros. rewrite Rrepr_le. rewrite Rlt_def in H. apply (Rmult_le_reg_l (Rrepr r)). - rewrite <- Rrepr_0. apply Rlt_epsilon. exact H. - rewrite <- Rrepr_mult, <- Rrepr_mult. - rewrite <- Rrepr_le. exact H0. + intros z x y H H0; case H0; auto with real. + intros H1; apply Rlt_le. + apply Rmult_lt_reg_l with (r := z); auto. + intros H1; replace x with (/ z * (z * x)); auto with real. + replace y with (/ z * (z * y)). + rewrite H1; auto with real. + rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. + rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. Qed. Lemma Rmult_le_reg_r : forall r r1 r2, 0 < r -> r1 * r <= r2 * r -> r1 <= r2. @@ -1574,9 +1585,11 @@ Qed. (**********) Lemma plus_INR : forall n m:nat, INR (n + m) = INR n + INR m. Proof. - intros. apply Rquot1. - rewrite Rrepr_INR, Rrepr_plus, plus_INR, - <- Rrepr_INR, <- Rrepr_INR. reflexivity. + intros n m; induction n as [| n Hrecn]. + simpl; auto with real. + replace (S n + m)%nat with (S (n + m)); auto with arith. + repeat rewrite S_INR. + rewrite Hrecn; ring. Qed. Hint Resolve plus_INR: real. @@ -1645,8 +1658,16 @@ Hint Resolve pos_INR: real. Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat. Proof. - intros. apply INR_lt. rewrite Rlt_def in H. - rewrite Rrepr_INR, Rrepr_INR in H. apply Rlt_epsilon. exact H. + intros n m. revert n. + induction m ; intros n H. + - elim (Rlt_irrefl 0). + apply Rle_lt_trans with (2 := H). + apply pos_INR. + - destruct n as [|n]. + apply Nat.lt_0_succ. + apply lt_n_S, IHm. + rewrite 2!S_INR in H. + apply Rplus_lt_reg_r with (1 := H). Qed. Hint Resolve INR_lt: real. @@ -1680,8 +1701,11 @@ Hint Resolve not_0_INR: real. Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m. Proof. - intros. apply Rappart_repr. rewrite Rrepr_INR, Rrepr_INR. - apply not_INR. exact H. + intros n m H; case (le_or_lt n m); intros H1. + case (le_lt_or_eq _ _ H1); intros H2. + apply Rlt_dichotomy_converse; auto with real. + exfalso; auto. + apply not_eq_sym; apply Rlt_dichotomy_converse; auto with real. Qed. Hint Resolve not_INR: real. @@ -1721,8 +1745,17 @@ Qed. Lemma INR_IPR : forall p, INR (Pos.to_nat p) = IPR p. Proof. - intros. apply Rquot1. rewrite Rrepr_INR, Rrepr_IPR. - apply INR_IPR. + assert (H: forall p, 2 * INR (Pos.to_nat p) = IPR_2 p). + induction p as [p|p|] ; simpl IPR_2. + rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp. + now rewrite (Rplus_comm (2 * _)). + now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp. + apply Rmult_1_r. + intros [p|p|] ; unfold IPR. + rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H. + apply Rplus_comm. + now rewrite Pos2Nat.inj_xO, mult_INR, <- H. + easy. Qed. (**********) @@ -1737,15 +1770,26 @@ Qed. Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q). Proof. - intros. apply Rquot1. rewrite Rrepr_plus. - do 3 rewrite Rrepr_IZR. apply plus_IZR_NEG_POS. + intros p q; simpl. rewrite Z.pos_sub_spec. + case Pos.compare_spec; intros H; unfold IZR. + subst. ring. + rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial. + rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt). + ring. + rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial. + rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt). + ring. Qed. (**********) Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m. Proof. - intros. apply Rquot1. - rewrite Rrepr_plus. do 3 rewrite Rrepr_IZR. apply plus_IZR. + intro z; destruct z; intro t; destruct t; intros; auto with real. + simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add. apply plus_INR. + apply plus_IZR_NEG_POS. + rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS. + simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add, plus_INR. + apply Ropp_plus_distr. Qed. (**********) @@ -1755,21 +1799,14 @@ Proof. unfold IZR; intros m n; rewrite <- 3!INR_IPR, Pos2Nat.inj_mul, mult_INR; ring. Qed. -Lemma Rrepr_pow : forall (x : R) (n : nat), - (ConstructiveRIneq.Req (Rrepr (pow x n)) - (ConstructiveRIneq.pow (Rrepr x) n)). -Proof. - intro x. induction n. - - apply Rrepr_1. - - simpl. rewrite Rrepr_mult, <- IHn. reflexivity. -Qed. - Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Z.pow z (Z.of_nat n)). Proof. - intros. apply Rquot1. - rewrite Rrepr_IZR, Rrepr_pow. - rewrite (Rpow_eq_compat _ _ n (Rrepr_IZR z)). - apply pow_IZR. + intros z [|n];simpl;trivial. + rewrite Zpower_pos_nat. + rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl. + rewrite mult_IZR. + induction n;simpl;trivial. + rewrite mult_IZR;ring[IHn]. Qed. (**********) @@ -1803,23 +1840,34 @@ Qed. (**********) Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z. Proof. - intros. apply lt_0_IZR. rewrite <- Rrepr_0, <- Rrepr_IZR. - rewrite Rlt_def in H. apply Rlt_epsilon. exact H. + intro z; case z; simpl; intros. + elim (Rlt_irrefl _ H). + easy. + elim (Rlt_not_le _ _ H). + unfold IZR. + rewrite <- INR_IPR. + auto with real. Qed. (**********) Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z. Proof. - intros. apply lt_IZR. - rewrite <- Rrepr_IZR, <- Rrepr_IZR. rewrite Rlt_def in H. - apply Rlt_epsilon. exact H. + intros z1 z2 H; apply Z.lt_0_sub. + apply lt_0_IZR. + rewrite <- Z_R_minus. + exact (Rgt_minus (IZR z2) (IZR z1) H). Qed. (**********) Lemma eq_IZR_R0 : forall n:Z, IZR n = 0 -> n = 0%Z. Proof. - intros. apply eq_IZR_R0. - rewrite <- Rrepr_0, <- Rrepr_IZR, H. reflexivity. + intro z; destruct z; simpl; intros; auto with zarith. + elim Rgt_not_eq with (2 := H). + unfold IZR. rewrite <- INR_IPR. + apply lt_0_INR, Pos2Nat.is_pos. + elim Rlt_not_eq with (2 := H). + unfold IZR. rewrite <- INR_IPR. + apply Ropp_lt_gt_0_contravar, lt_0_INR, Pos2Nat.is_pos. Qed. (**********) @@ -1895,21 +1943,26 @@ Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : real. Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z. Proof. - intros. apply one_IZR_lt1. do 2 rewrite Rlt_def in H. split. - rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_opp. - apply Rlt_epsilon. apply H. - rewrite <- Rrepr_IZR, <- Rrepr_1. apply Rlt_epsilon. apply H. + intros z [H1 H2]. + apply Z.le_antisymm. + apply Z.lt_succ_r; apply lt_IZR; trivial. + change 0%Z with (Z.succ (-1)). + apply Z.le_succ_l; apply lt_IZR; trivial. Qed. Lemma one_IZR_r_R1 : forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m. Proof. - intros. rewrite Rlt_def in H, H0. apply (one_IZR_r_R1 (Rrepr r)); split. - rewrite <- Rrepr_IZR. apply Rlt_epsilon. apply H. - rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le. - apply H. rewrite <- Rrepr_IZR. apply Rlt_epsilon. apply H0. - rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le. - apply H0. + intros r z x [H1 H2] [H3 H4]. + cut ((z - x)%Z = 0%Z); auto with zarith. + apply one_IZR_lt1. + rewrite <- Z_R_minus; split. + replace (-1) with (r - (r + 1)). + unfold Rminus; apply Rplus_lt_le_compat; auto with real. + ring. + replace 1 with (r + 1 - r). + unfold Rminus; apply Rplus_le_lt_compat; auto with real. + ring. Qed. @@ -1942,13 +1995,13 @@ Qed. Lemma Rinv_le_contravar : forall x y, 0 < x -> x <= y -> / y <= / x. Proof. - intros. apply Rrepr_le. assert (y <> 0). - intro abs. subst y. apply (Rlt_irrefl 0). exact (Rlt_le_trans 0 x 0 H H0). - apply Rrepr_appart in H1. - rewrite Rrepr_0 in H1. rewrite Rlt_def in H. rewrite Rrepr_0 in H. - apply Rlt_epsilon in H. - rewrite (Rrepr_inv y H1), (Rrepr_inv x (inr H)). - apply Rinv_le_contravar. rewrite <- Rrepr_le. exact H0. + intros x y H1 [H2|H2]. + apply Rlt_le. + apply Rinv_lt_contravar with (2 := H2). + apply Rmult_lt_0_compat with (1 := H1). + now apply Rlt_trans with x. + rewrite H2. + apply Rle_refl. Qed. Lemma Rle_Rinv : forall x y:R, 0 < x -> 0 < y -> x <= y -> / y <= / x. @@ -2012,10 +2065,18 @@ Qed. Lemma le_epsilon : forall r1 r2, (forall eps:R, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2. Proof. - intros. rewrite Rrepr_le. apply le_epsilon. - intros. rewrite <- (Rquot2 eps), <- Rrepr_plus. - rewrite <- Rrepr_le. apply H. rewrite Rlt_def. - rewrite Rquot2, Rrepr_0. apply Rlt_forget. exact H0. + intros x y H. + destruct (Rle_or_lt x y) as [H1|H1]. + exact H1. + apply Rplus_le_reg_r with x. + replace (y + x) with (2 * (y + (x - y) * / 2)) by field. + replace (x + x) with (2 * x) by ring. + apply Rmult_le_compat_l. + now apply (IZR_le 0 2). + apply H. + apply Rmult_lt_0_compat. + now apply Rgt_minus. + apply Rinv_0_lt_compat, Rlt_0_2. Qed. (**********) diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index d856d1c7fe..be283fb7cf 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -20,10 +20,12 @@ (*********************************************************) Require Export ZArith_base. -Require Import ConstructiveRIneq. +Require Import ClassicalDedekindReals. +Require Import ConstructiveCauchyReals. +Require Import ConstructiveCauchyRealsMult. +Require Import ConstructiveRcomplete. Require Import ConstructiveRealsLUB. Require Export Rdefinitions. -Declare Scope R_scope. Local Open Scope R_scope. (*********************************************************) @@ -34,7 +36,7 @@ Local Open Scope R_scope. (** ** Addition *) (*********************************************************) -Open Scope R_scope_constr. +Open Scope CReal_scope. Lemma Rrepr_0 : Rrepr 0 == 0. Proof. @@ -58,7 +60,7 @@ Qed. Lemma Rrepr_minus : forall x y:R, Rrepr (x - y) == Rrepr x - Rrepr y. Proof. - intros. unfold Rminus, CRminus. + intros. unfold Rminus, CReal_minus. rewrite Rrepr_plus, Rrepr_opp. reflexivity. Qed. @@ -72,10 +74,10 @@ Lemma Rrepr_inv : forall (x:R) (xnz : Rrepr x # 0), Proof. intros. rewrite RinvImpl.Rinv_def. destruct (Req_appart_dec x R0). - exfalso. subst x. destruct xnz. - rewrite Rrepr_0 in c. exact (Rlt_irrefl 0 c). - rewrite Rrepr_0 in c. exact (Rlt_irrefl 0 c). - - rewrite Rquot2. apply (Rmult_eq_reg_l (Rrepr x)). 2: exact xnz. - rewrite Rmult_comm, (Rmult_comm (Rrepr x)), Rinv_l, Rinv_l. + rewrite Rrepr_0 in c. exact (CRealLt_irrefl 0 c). + rewrite Rrepr_0 in c. exact (CRealLt_irrefl 0 c). + - rewrite Rquot2. apply (CReal_mult_eq_reg_l (Rrepr x)). exact xnz. + rewrite CReal_mult_comm, (CReal_mult_comm (Rrepr x)), CReal_inv_l, CReal_inv_l. reflexivity. Qed. @@ -83,12 +85,12 @@ Lemma Rrepr_le : forall x y:R, (x <= y)%R <-> Rrepr x <= Rrepr y. Proof. split. - intros [H|H] abs. rewrite RbaseSymbolsImpl.Rlt_def in H. - apply Rlt_epsilon in H. - exact (Rlt_asym (Rrepr x) (Rrepr y) H abs). - destruct H. exact (Rlt_asym (Rrepr x) (Rrepr x) abs abs). + apply CRealLtEpsilon in H. + exact (CRealLt_asym (Rrepr x) (Rrepr y) H abs). + destruct H. exact (CRealLt_asym (Rrepr x) (Rrepr x) abs abs). - intros. destruct (total_order_T x y). destruct s. left. exact r. right. exact e. - rewrite RbaseSymbolsImpl.Rlt_def in r. apply Rlt_epsilon in r. contradiction. + rewrite RbaseSymbolsImpl.Rlt_def in r. apply CRealLtEpsilon in r. contradiction. Qed. Lemma Rrepr_appart : forall x y:R, @@ -96,26 +98,26 @@ Lemma Rrepr_appart : forall x y:R, Proof. intros. destruct (total_order_T x y). destruct s. left. rewrite RbaseSymbolsImpl.Rlt_def in r. - apply Rlt_epsilon. exact r. contradiction. + apply CRealLtEpsilon. exact r. contradiction. right. rewrite RbaseSymbolsImpl.Rlt_def in r. - apply Rlt_epsilon. exact r. + apply CRealLtEpsilon. exact r. Qed. Lemma Rappart_repr : forall x y:R, Rrepr x # Rrepr y -> (x <> y)%R. Proof. intros x y [H|H] abs. - destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H). - destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H). + destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H). + destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H). Qed. -Close Scope R_scope_constr. +Close Scope CReal_scope. (**********) Lemma Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1. Proof. - intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply Rplus_comm. + intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply CReal_plus_comm. Qed. Hint Resolve Rplus_comm: real. @@ -123,7 +125,7 @@ Hint Resolve Rplus_comm: real. Lemma Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3). Proof. intros. apply Rquot1. repeat rewrite Rrepr_plus. - apply Rplus_assoc. + apply CReal_plus_assoc. Qed. Hint Resolve Rplus_assoc: real. @@ -131,7 +133,7 @@ Hint Resolve Rplus_assoc: real. Lemma Rplus_opp_r : forall r:R, r + - r = 0. Proof. intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_opp, Rrepr_0. - apply Rplus_opp_r. + apply CReal_plus_opp_r. Qed. Hint Resolve Rplus_opp_r: real. @@ -139,7 +141,7 @@ Hint Resolve Rplus_opp_r: real. Lemma Rplus_0_l : forall r:R, 0 + r = r. Proof. intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_0. - apply Rplus_0_l. + apply CReal_plus_0_l. Qed. Hint Resolve Rplus_0_l: real. @@ -150,7 +152,7 @@ Hint Resolve Rplus_0_l: real. (**********) Lemma Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1. Proof. - intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply Rmult_comm. + intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply CReal_mult_comm. Qed. Hint Resolve Rmult_comm: real. @@ -158,7 +160,7 @@ Hint Resolve Rmult_comm: real. Lemma Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3). Proof. intros. apply Rquot1. repeat rewrite Rrepr_mult. - apply Rmult_assoc. + apply CReal_mult_assoc. Qed. Hint Resolve Rmult_assoc: real. @@ -167,7 +169,7 @@ Lemma Rinv_l : forall r:R, r <> 0 -> / r * r = 1. Proof. intros. rewrite RinvImpl.Rinv_def; destruct (Req_appart_dec r R0). - contradiction. - - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply Rinv_l. + - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply CReal_inv_l. Qed. Hint Resolve Rinv_l: real. @@ -175,7 +177,7 @@ Hint Resolve Rinv_l: real. Lemma Rmult_1_l : forall r:R, 1 * r = r. Proof. intros. apply Rquot1. rewrite Rrepr_mult, Rrepr_1. - apply Rmult_1_l. + apply CReal_mult_1_l. Qed. Hint Resolve Rmult_1_l: real. @@ -183,17 +185,17 @@ Hint Resolve Rmult_1_l: real. Lemma R1_neq_R0 : 1 <> 0. Proof. intro abs. - assert (Req (CRone CR) (CRzero CR)). + assert (CRealEq 1%CReal 0%CReal). { transitivity (Rrepr 1). symmetry. - replace 1%R with (Rabst (CRone CR)). + replace 1%R with (Rabst 1%CReal). 2: unfold IZR,IPR; rewrite RbaseSymbolsImpl.R1_def; reflexivity. rewrite Rquot2. reflexivity. transitivity (Rrepr 0). rewrite abs. reflexivity. - replace 0%R with (Rabst (CRzero CR)). + replace 0%R with (Rabst 0%CReal). 2: unfold IZR; rewrite RbaseSymbolsImpl.R0_def; reflexivity. rewrite Rquot2. reflexivity. } - pose proof (Rlt_morph (CRzero CR) (CRzero CR) (Req_refl _) (CRone CR) (CRzero CR) H). - apply (Rlt_irrefl (CRzero CR)). apply H0. apply Rlt_0_1. + pose proof (CRealLt_morph 0%CReal 0%CReal (CRealEq_refl _) 1%CReal 0%CReal H). + apply (CRealLt_irrefl 0%CReal). apply H0. apply CRealLt_0_1. Qed. Hint Resolve R1_neq_R0: real. @@ -207,7 +209,7 @@ Lemma Proof. intros. apply Rquot1. rewrite Rrepr_mult, Rrepr_plus, Rrepr_plus, Rrepr_mult, Rrepr_mult. - apply Rmult_plus_distr_l. + apply CReal_mult_plus_distr_l. Qed. Hint Resolve Rmult_plus_distr_l: real. @@ -223,35 +225,35 @@ Hint Resolve Rmult_plus_distr_l: real. Lemma Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1. Proof. intros. intro abs. rewrite RbaseSymbolsImpl.Rlt_def in H, abs. - apply Rlt_epsilon in H. apply Rlt_epsilon in abs. - apply (Rlt_asym (Rrepr r1) (Rrepr r2)); assumption. + apply CRealLtEpsilon in H. apply CRealLtEpsilon in abs. + apply (CRealLt_asym (Rrepr r1) (Rrepr r2)); assumption. Qed. (**********) Lemma Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3. Proof. intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H, H0. - apply Rlt_epsilon in H. apply Rlt_epsilon in H0. - apply Rlt_forget. - apply (Rlt_trans (Rrepr r1) (Rrepr r2) (Rrepr r3)); assumption. + apply CRealLtEpsilon in H. apply CRealLtEpsilon in H0. + apply CRealLtForget. + apply (CReal_lt_trans (Rrepr r1) (Rrepr r2) (Rrepr r3)); assumption. Qed. (**********) Lemma Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2. Proof. intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H. - do 2 rewrite Rrepr_plus. apply Rlt_forget. - apply Rplus_lt_compat_l. apply Rlt_epsilon. exact H. + do 2 rewrite Rrepr_plus. apply CRealLtForget. + apply CReal_plus_lt_compat_l. apply CRealLtEpsilon. exact H. Qed. (**********) Lemma Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2. Proof. intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H. - do 2 rewrite Rrepr_mult. apply Rlt_forget. apply Rmult_lt_compat_l. - rewrite <- (Rquot2 (CRzero CR)). unfold IZR in H. - rewrite RbaseSymbolsImpl.R0_def in H. apply Rlt_epsilon. exact H. - rewrite RbaseSymbolsImpl.Rlt_def in H0. apply Rlt_epsilon. exact H0. + do 2 rewrite Rrepr_mult. apply CRealLtForget. apply CReal_mult_lt_compat_l. + rewrite <- (Rquot2 0%CReal). unfold IZR in H. + rewrite RbaseSymbolsImpl.R0_def in H. apply CRealLtEpsilon. exact H. + rewrite RbaseSymbolsImpl.Rlt_def in H0. apply CRealLtEpsilon. exact H0. Qed. Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. @@ -274,119 +276,133 @@ Arguments INR n%nat. (**********************************************************) Lemma Rrepr_INR : forall n : nat, - Req (Rrepr (INR n)) (ConstructiveRIneq.INR n). + CRealEq (Rrepr (INR n)) (inject_Z (Z.of_nat n)). Proof. induction n. - apply Rrepr_0. - - simpl. destruct n. apply Rrepr_1. - rewrite Rrepr_plus, <- IHn, Rrepr_1. reflexivity. + - replace (Z.of_nat (S n)) with (Z.of_nat n + 1)%Z. + simpl. destruct n. apply Rrepr_1. + rewrite Rrepr_plus,inject_Z_plus, <- IHn, Rrepr_1. reflexivity. + replace 1%Z with (Z.of_nat 1). rewrite <- (Nat2Z.inj_add n 1). + apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity. Qed. Lemma Rrepr_IPR2 : forall n : positive, - Req (Rrepr (IPR_2 n)) (ConstructiveRIneq.IPR_2 n). + CRealEq (Rrepr (IPR_2 n)) (inject_Z (Z.pos (n~0))). Proof. induction n. - - unfold IPR_2, ConstructiveRIneq.IPR_2. - rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, Rrepr_plus, Rrepr_plus, <- IHn. - unfold IPR_2. - rewrite Rquot2. rewrite RbaseSymbolsImpl.R1_def. reflexivity. - - unfold IPR_2, ConstructiveRIneq.IPR_2. - rewrite Rrepr_mult, Rrepr_plus, <- IHn. - rewrite RbaseSymbolsImpl.R1_def. rewrite Rquot2. - unfold IPR_2. rewrite RbaseSymbolsImpl.R1_def. reflexivity. - - unfold IPR_2, ConstructiveRIneq.IPR_2. - rewrite RbaseSymbolsImpl.R1_def. - rewrite Rrepr_plus, Rquot2. reflexivity. + - simpl. replace (Z.pos n~1~0) with ((Z.pos n~0 + 1) + (Z.pos n~0 + 1))%Z. + rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, inject_Z_plus, inject_Z_plus. + rewrite Rrepr_plus, Rrepr_plus, <- IHn. + rewrite Rquot2, CReal_mult_plus_distr_r, CReal_mult_1_l. + rewrite (CReal_plus_comm 1%CReal). repeat rewrite CReal_plus_assoc. + apply CReal_plus_morph. reflexivity. + reflexivity. + repeat rewrite <- Pos2Z.inj_add. apply f_equal. + rewrite Pos.add_diag. apply f_equal. + rewrite Pos.add_1_r. reflexivity. + - simpl. replace (Z.pos n~0~0) with ((Z.pos n~0) + (Z.pos n~0))%Z. + rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, inject_Z_plus. + rewrite Rrepr_plus, <- IHn. + rewrite Rquot2, CReal_mult_plus_distr_r, CReal_mult_1_l. reflexivity. + rewrite <- Pos2Z.inj_add. apply f_equal. + rewrite Pos.add_diag. reflexivity. + - simpl. rewrite Rrepr_plus, RbaseSymbolsImpl.R1_def, Rquot2. + replace 2%Z with (1 + 1)%Z. rewrite inject_Z_plus. reflexivity. + reflexivity. Qed. Lemma Rrepr_IPR : forall n : positive, - Req (Rrepr (IPR n)) (ConstructiveRIneq.IPR n). + CRealEq (Rrepr (IPR n)) (inject_Z (Z.pos n)). Proof. intro n. destruct n. - - unfold IPR, ConstructiveRIneq.IPR. - rewrite Rrepr_plus, <- Rrepr_IPR2. - rewrite RbaseSymbolsImpl.R1_def. rewrite Rquot2. reflexivity. - - unfold IPR, ConstructiveRIneq.IPR. - apply Rrepr_IPR2. + - unfold IPR. rewrite Rrepr_plus. + replace (n~1)%positive with (n~0 + 1)%positive. + rewrite Pos2Z.inj_add, inject_Z_plus, <- Rrepr_IPR2, CReal_plus_comm. + rewrite RbaseSymbolsImpl.R1_def, Rquot2. reflexivity. + rewrite Pos.add_1_r. reflexivity. + - apply Rrepr_IPR2. - unfold IPR. rewrite RbaseSymbolsImpl.R1_def. apply Rquot2. Qed. Lemma Rrepr_IZR : forall n : Z, - Req (Rrepr (IZR n)) (ConstructiveRIneq.IZR n). + CRealEq (Rrepr (IZR n)) (inject_Z n). Proof. intros [|p|n]. - unfold IZR. rewrite RbaseSymbolsImpl.R0_def. apply Rquot2. - apply Rrepr_IPR. - - unfold IZR, ConstructiveRIneq.IZR. - rewrite <- Rrepr_IPR, Rrepr_opp. reflexivity. + - unfold IZR. rewrite Rrepr_opp, Rrepr_IPR. rewrite <- opp_inject_Z. + replace (- Z.pos n)%Z with (Z.neg n). reflexivity. reflexivity. Qed. (**********) Lemma archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1. Proof. intro r. unfold up. - destruct (Rarchimedean (Rrepr r)) as [n nmaj], (total_order_T (IZR n - r) R1). + destruct (CRealArchimedean (Rrepr r)) as [n nmaj], (total_order_T (IZR n - r) R1). destruct s. - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR. - apply Rlt_forget. apply nmaj. + apply CRealLtForget. apply nmaj. unfold Rle. left. exact r0. - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. - rewrite Rrepr_IZR. apply Rlt_forget. apply nmaj. right. exact e. + rewrite Rrepr_IZR. apply CRealLtForget. apply nmaj. right. exact e. - split. + unfold Rgt, Z.pred. rewrite RbaseSymbolsImpl.Rlt_def. - rewrite Rrepr_IZR, plus_IZR. + rewrite Rrepr_IZR, inject_Z_plus. rewrite RbaseSymbolsImpl.Rlt_def in r0. rewrite Rrepr_minus in r0. rewrite <- (Rrepr_IZR n). - unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR. - apply Rlt_forget. apply Rlt_epsilon in r0. - unfold ConstructiveRIneq.Rminus in r0. - apply (ConstructiveRIneq.Rplus_lt_compat_l - (ConstructiveRIneq.Rplus (Rrepr r) (ConstructiveRIneq.Ropp (Rrepr R1)))) + apply CRealLtForget. apply CRealLtEpsilon in r0. + unfold CReal_minus in r0. + apply (CReal_plus_lt_compat_l + (CReal_plus (Rrepr r) (CReal_opp (Rrepr R1)))) in r0. - rewrite ConstructiveRIneq.Rplus_assoc, - ConstructiveRIneq.Rplus_opp_l, - ConstructiveRIneq.Rplus_0_r, + rewrite CReal_plus_assoc, + CReal_plus_opp_l, + CReal_plus_0_r, RbaseSymbolsImpl.R1_def, Rquot2, - ConstructiveRIneq.Rplus_comm, - ConstructiveRIneq.Rplus_assoc, - <- (ConstructiveRIneq.Rplus_assoc (ConstructiveRIneq.Ropp (Rrepr r))), - ConstructiveRIneq.Rplus_opp_l, - ConstructiveRIneq.Rplus_0_l + CReal_plus_comm, + CReal_plus_assoc, + <- (CReal_plus_assoc (CReal_opp (Rrepr r))), + CReal_plus_opp_l, + CReal_plus_0_l in r0. - exact r0. + rewrite (opp_inject_Z 1). exact r0. + destruct (total_order_T (IZR (Z.pred n) - r) 1). destruct s. left. exact r1. right. exact e. - exfalso. destruct nmaj as [_ nmaj]. rewrite <- Rrepr_IZR in nmaj. + exfalso. destruct nmaj as [_ nmaj]. + pose proof Rrepr_IZR as iz. unfold inject_Z in iz. + rewrite <- iz in nmaj. apply (Rlt_asym (IZR n) (r + 2)). rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_plus. rewrite (Rrepr_plus 1 1). - apply Rlt_forget. - apply (ConstructiveRIneq.Rlt_le_trans - _ (ConstructiveRIneq.Rplus (Rrepr r) (ConstructiveRIneq.IZR 2))). - apply nmaj. - unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, Rquot2. apply Rle_refl. + apply CRealLtForget. + apply (CReal_lt_le_trans _ _ _ nmaj). + unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, Rquot2. + rewrite <- (inject_Z_plus 1 1). apply CRealLe_refl. clear nmaj. unfold Z.pred in r1. rewrite RbaseSymbolsImpl.Rlt_def in r1. - rewrite Rrepr_minus, (Rrepr_IZR (n + -1)), plus_IZR, - <- (Rrepr_IZR n) - in r1. - unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR in r1. + rewrite Rrepr_minus, (Rrepr_IZR (n + -1)) in r1. + rewrite inject_Z_plus, <- (Rrepr_IZR n) in r1. rewrite RbaseSymbolsImpl.Rlt_def, Rrepr_plus. - apply Rlt_epsilon in r1. - apply (ConstructiveRIneq.Rplus_lt_compat_l - (ConstructiveRIneq.Rplus (Rrepr r) (CRone CR))) in r1. - apply Rlt_forget. - apply (ConstructiveRIneq.Rle_lt_trans - _ (ConstructiveRIneq.Rplus (ConstructiveRIneq.Rplus (Rrepr r) (Rrepr 1)) (CRone CR))). + apply CRealLtEpsilon in r1. + apply (CReal_plus_lt_compat_l + (CReal_plus (Rrepr r) 1%CReal)) in r1. + apply CRealLtForget. + apply (CReal_le_lt_trans + _ (CReal_plus (CReal_plus (Rrepr r) (Rrepr 1)) 1%CReal)). rewrite (Rrepr_plus 1 1). unfold IZR, IPR. - rewrite RbaseSymbolsImpl.R1_def, (Rquot2 (CRone CR)), <- ConstructiveRIneq.Rplus_assoc. - apply Rle_refl. - rewrite <- (ConstructiveRIneq.Rplus_comm (Rrepr 1)), - <- ConstructiveRIneq.Rplus_assoc, - (ConstructiveRIneq.Rplus_comm (Rrepr 1)) + rewrite RbaseSymbolsImpl.R1_def, (Rquot2 1%CReal), <- CReal_plus_assoc. + apply CRealLe_refl. + rewrite <- (CReal_plus_comm (Rrepr 1)), + <- CReal_plus_assoc, + (CReal_plus_comm (Rrepr 1)) in r1. - apply (ConstructiveRIneq.Rlt_le_trans _ _ _ r1). - unfold ConstructiveRIneq.Rminus. - ring_simplify. apply ConstructiveRIneq.Rle_refl. + apply (CReal_lt_le_trans _ _ _ r1). + unfold CReal_minus. rewrite (opp_inject_Z 1). + rewrite (CReal_plus_comm (Rrepr (IZR n))), CReal_plus_assoc, + <- (CReal_plus_assoc 1), <- (CReal_plus_assoc 1), CReal_plus_opp_r. + rewrite CReal_plus_0_l, CReal_plus_comm, CReal_plus_assoc, + CReal_plus_opp_l, CReal_plus_0_r. + apply CRealLe_refl. Qed. (**********************************************************) @@ -408,29 +424,29 @@ Lemma completeness : forall E:R -> Prop, bound E -> (exists x : R, E x) -> { m:R | is_lub E m }. Proof. - intros. pose (fun x:ConstructiveRIneq.R => E (Rabst x)) as Er. - assert (forall x y : CRcarrier CR, orderEq (CRcarrier CR) (CRlt CR) x y -> Er x <-> Er y) + intros. pose (fun x:CReal => E (Rabst x)) as Er. + assert (forall x y : CReal, CRealEq x y -> Er x <-> Er y) as Erproper. { intros. unfold Er. replace (Rabst x) with (Rabst y). reflexivity. apply Rquot1. do 2 rewrite Rquot2. split; apply H1. } - assert (exists x : ConstructiveRIneq.R, Er x) as Einhab. + assert (exists x : CReal, Er x) as Einhab. { destruct H0. exists (Rrepr x). unfold Er. replace (Rabst (Rrepr x)) with x. exact H0. apply Rquot1. rewrite Rquot2. reflexivity. } - assert (exists x : ConstructiveRIneq.R, - (forall y:ConstructiveRIneq.R, Er y -> ConstructiveRIneq.Rle y x)) + assert (exists x : CReal, + (forall y:CReal, Er y -> CRealLe y x)) as Ebound. { destruct H. exists (Rrepr x). intros y Ey. rewrite <- (Rquot2 y). apply Rrepr_le. apply H. exact Ey. } - destruct (CR_sig_lub CR + destruct (CR_sig_lub CRealImplem Er Erproper sig_forall_dec sig_not_dec Einhab Ebound). exists (Rabst x). split. intros y Ey. apply Rrepr_le. rewrite Rquot2. - unfold ConstructiveRIneq.Rle. apply a. + unfold CRealLe. apply a. unfold Er. replace (Rabst (Rrepr y)) with y. exact Ey. apply Rquot1. rewrite Rquot2. reflexivity. intros. destruct a. apply Rrepr_le. rewrite Rquot2. - unfold ConstructiveRIneq.Rle. apply H3. intros y Ey. + unfold CRealLe. apply H3. intros y Ey. intros. rewrite <- (Rquot2 y) in H4. apply Rrepr_le in H4. exact H4. apply H1, Ey. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index b1ce8109ca..35025ba9bc 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -8,17 +8,18 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(* Classical quotient of the constructive Cauchy real numbers. - This file contains the definition of the classical real numbers - type R, its algebraic operations, its order and the proof that - it is total, and the proof that R is archimedean (up). - It also defines IZR, the ring morphism from Z to R. *) +(* Abstraction of classical Dedekind reals behind an opaque module, + for backward compatibility. + + This file also contains the proof that classical reals are a + quotient of constructive Cauchy reals. *) Require Export ZArith_base. Require Import QArith_base. -Require Import ConstructiveRIneq. +Require Import ConstructiveCauchyReals. +Require Import ConstructiveCauchyRealsMult. +Require Import ClassicalDedekindReals. -Parameter R : Set. (* Declare primitive numeral notations for Scope R_scope *) Declare Scope R_scope. @@ -27,26 +28,18 @@ Declare ML Module "r_syntax_plugin". (* Declare Scope R_scope with Key R *) Delimit Scope R_scope with R. -(* Automatically open scope R_scope for arguments of type R *) -Bind Scope R_scope with R. - Local Open Scope R_scope. -(* The limited principle of omniscience *) -Axiom sig_forall_dec - : forall (P : nat -> Prop), - (forall n, {P n} + {~P n}) - -> {n | ~P n} + {forall n, P n}. - -Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }. - -Axiom Rabst : ConstructiveRIneq.R -> R. -Axiom Rrepr : R -> ConstructiveRIneq.R. -Axiom Rquot1 : forall x y:R, Req (Rrepr x) (Rrepr y) -> x = y. -Axiom Rquot2 : forall x:ConstructiveRIneq.R, Req (Rrepr (Rabst x)) x. (* Those symbols must be kept opaque, for backward compatibility. *) Module Type RbaseSymbolsSig. + Parameter R : Set. + Bind Scope R_scope with R. + Axiom Rabst : CReal -> R. + Axiom Rrepr : R -> CReal. + Axiom Rquot1 : forall x y:R, CRealEq (Rrepr x) (Rrepr y) -> x = y. + Axiom Rquot2 : forall x:CReal, CRealEq (Rrepr (Rabst x)) x. + Parameter R0 : R. Parameter R1 : R. Parameter Rplus : R -> R -> R. @@ -54,29 +47,34 @@ Module Type RbaseSymbolsSig. Parameter Ropp : R -> R. Parameter Rlt : R -> R -> Prop. - Parameter R0_def : R0 = Rabst (CRzero CR). - Parameter R1_def : R1 = Rabst (CRone CR). + Parameter R0_def : R0 = Rabst (inject_Q 0). + Parameter R1_def : R1 = Rabst (inject_Q 1). Parameter Rplus_def : forall x y : R, - Rplus x y = Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)). + Rplus x y = Rabst (CReal_plus (Rrepr x) (Rrepr y)). Parameter Rmult_def : forall x y : R, - Rmult x y = Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)). + Rmult x y = Rabst (CReal_mult (Rrepr x) (Rrepr y)). Parameter Ropp_def : forall x : R, - Ropp x = Rabst (ConstructiveRIneq.Ropp (Rrepr x)). + Ropp x = Rabst (CReal_opp (Rrepr x)). Parameter Rlt_def : forall x y : R, - Rlt x y = ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y). + Rlt x y = CRealLtProp (Rrepr x) (Rrepr y). End RbaseSymbolsSig. Module RbaseSymbolsImpl : RbaseSymbolsSig. - Definition R0 : R := Rabst (CRzero CR). - Definition R1 : R := Rabst (CRone CR). + Definition R := DReal. + Definition Rabst := DRealAbstr. + Definition Rrepr := DRealRepr. + Definition Rquot1 := DRealQuot1. + Definition Rquot2 := DRealQuot2. + Definition R0 : R := Rabst (inject_Q 0). + Definition R1 : R := Rabst (inject_Q 1). Definition Rplus : R -> R -> R - := fun x y : R => Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)). + := fun x y : R => Rabst (CReal_plus (Rrepr x) (Rrepr y)). Definition Rmult : R -> R -> R - := fun x y : R => Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)). + := fun x y : R => Rabst (CReal_mult (Rrepr x) (Rrepr y)). Definition Ropp : R -> R - := fun x : R => Rabst (ConstructiveRIneq.Ropp (Rrepr x)). + := fun x : R => Rabst (CReal_opp (Rrepr x)). Definition Rlt : R -> R -> Prop - := fun x y : R => ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y). + := fun x y : R => CRealLtProp (Rrepr x) (Rrepr y). Definition R0_def := eq_refl R0. Definition R1_def := eq_refl R1. @@ -88,6 +86,7 @@ End RbaseSymbolsImpl. Export RbaseSymbolsImpl. (* Keep the same names as before *) +Notation R := RbaseSymbolsImpl.R (only parsing). Notation R0 := RbaseSymbolsImpl.R0 (only parsing). Notation R1 := RbaseSymbolsImpl.R1 (only parsing). Notation Rplus := RbaseSymbolsImpl.Rplus (only parsing). @@ -95,6 +94,9 @@ Notation Rmult := RbaseSymbolsImpl.Rmult (only parsing). Notation Ropp := RbaseSymbolsImpl.Ropp (only parsing). Notation Rlt := RbaseSymbolsImpl.Rlt (only parsing). +(* Automatically open scope R_scope for arguments of type R *) +Bind Scope R_scope with R. + Infix "+" := Rplus : R_scope. Infix "*" := Rmult : R_scope. Notation "- x" := (Ropp x) : R_scope. @@ -160,11 +162,11 @@ Arguments IZR z%Z : simpl never. Lemma total_order_T : forall r1 r2:R, {Rlt r1 r2} + {r1 = r2} + {Rlt r2 r1}. Proof. - intros. destruct (Rlt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec). + intros. destruct (CRealLt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec). - left. left. rewrite RbaseSymbolsImpl.Rlt_def. - apply Rlt_forget. exact r. - - destruct (Rlt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec). - + right. rewrite RbaseSymbolsImpl.Rlt_def. apply Rlt_forget. exact r0. + apply CRealLtForget. exact c. + - destruct (CRealLt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec). + + right. rewrite RbaseSymbolsImpl.Rlt_def. apply CRealLtForget. exact c. + left. right. apply Rquot1. split; assumption. Qed. @@ -178,9 +180,9 @@ Proof. Qed. Lemma Rrepr_appart_0 : forall x:R, - (x < R0 \/ R0 < x) -> Rappart (Rrepr x) (CRzero CR). + (x < R0 \/ R0 < x) -> CReal_appart (Rrepr x) (inject_Q 0). Proof. - intros. apply CRltDisjunctEpsilon. destruct H. + intros. apply CRealLtDisjunctEpsilon. destruct H. left. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. exact H. right. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. @@ -192,7 +194,7 @@ Module Type RinvSig. Parameter Rinv_def : forall x : R, Rinv x = match Req_appart_dec x R0 with | left _ => R0 (* / 0 is undefined, we take 0 arbitrarily *) - | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r))) + | right r => Rabst ((CReal_inv (Rrepr x) (Rrepr_appart_0 x r))) end. End RinvSig. @@ -200,7 +202,7 @@ Module RinvImpl : RinvSig. Definition Rinv : R -> R := fun x => match Req_appart_dec x R0 with | left _ => R0 (* / 0 is undefined, we take 0 arbitrarily *) - | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r))) + | right r => Rabst ((CReal_inv (Rrepr x) (Rrepr_appart_0 x r))) end. Definition Rinv_def := fun x => eq_refl (Rinv x). End RinvImpl. @@ -215,7 +217,7 @@ Infix "/" := Rdiv : R_scope. (* First integer strictly above x *) Definition up (x : R) : Z. Proof. - destruct (Rarchimedean (Rrepr x)) as [n nmaj], (total_order_T (IZR n - x) R1). + destruct (CRealArchimedean (Rrepr x)) as [n nmaj], (total_order_T (IZR n - x) R1). destruct s. - exact n. - (* x = n-1 *) exact n. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 08253e5a8f..626ac0fe67 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -226,7 +226,7 @@ COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop) # We here define a bunch of variables about the files being part of the # Coq project in order to ease the writing of build target and build rules -VDFILE := .coqdeps +VDFILE := @DEP_FILE@ ALLSRCFILES := \ $(MLGFILES) \ @@ -312,7 +312,7 @@ else DO_NATDYNLINK = endif -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE)) +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) # Compilation targets ######################################################### @@ -732,7 +732,7 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack # projects. Note that extra options might be on the command line. VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) -$(VDFILE).d: $(VFILES) +$(VDFILE): $(VFILES) $(SHOW)'COQDEP VFILES' $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 1bd52d5bf1..b091ff3b4e 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -122,7 +122,7 @@ let read_whole_file s = let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s -let generate_makefile oc conf_file local_file args project = +let generate_makefile oc conf_file local_file dep_file args project = let coqlib = Envars.coqlib () in let makefile_template = let template = Filename.concat "tools" "CoqMakefile.in" in @@ -133,6 +133,7 @@ let generate_makefile oc conf_file local_file args project = (fun s (k,v) -> Str.global_substitute (Str.regexp_string k) (fun _ -> v) s) s [ "@CONF_FILE@", conf_file; "@LOCAL_FILE@", local_file; + "@DEP_FILE@", dep_file; "@COQ_VERSION@", Coq_config.version; "@PROJECT_FILE@", (Option.default "" project.project_file); "@COQ_MAKEFILE_INVOCATION@",String.concat " " (List.map quote args); @@ -412,6 +413,7 @@ let _ = let conf_file = Option.default "CoqMakefile" project.makefile ^ ".conf" in let local_file = Option.default "CoqMakefile" project.makefile ^ ".local" in + let dep_file = "." ^ Option.default "CoqMakefile" project.makefile ^ ".d" in if project.extra_targets <> [] then begin eprintf "Warning: -extra and -extra-phony are deprecated.\n"; @@ -434,7 +436,7 @@ let _ = Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1); let ocm = Option.cata open_out stdout project.makefile in - generate_makefile ocm conf_file local_file (prog :: args) project; + generate_makefile ocm conf_file local_file dep_file (prog :: args) project; close_out ocm; let occ = open_out conf_file in generate_conf occ project (prog :: args); diff --git a/vernac/classes.ml b/vernac/classes.ml index 0a8c4e6b0f..09866a75c9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -210,7 +210,7 @@ let discharge_class (_,cl) = in grs', discharge_rel_context subst 1 ctx @ ctx' in try let info = abs_context cl in - let ctx = info.Lib.abstr_ctx in + let ctx = info.Section.abstr_ctx in let ctx, subst = rel_of_variable_context ctx in let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in @@ -325,7 +325,7 @@ let declare_instance_constant info global imps ?hook name decl poly sigma term t let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in Declare.definition_message name; - Declare.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); + DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); instance_hook info global imps ?hook (GlobRef.ConstRef kn) let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name = @@ -338,7 +338,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst nam let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in - Declare.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); + DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); instance_hook pri global imps (GlobRef.ConstRef cst) let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index f9b73a59eb..e5db6146ca 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -69,7 +69,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name let kn = Declare.declare_constant ~name ~local ~kind decl in let gr = GlobRef.ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in + let () = DeclareUniv.declare_univ_binders gr pl in let () = Declare.assumption_message name in let env = Global.env () in let sigma = Evd.from_env env in @@ -217,7 +217,7 @@ let context_insection sigma ~poly ctx = in let entry = Declare.definition_entry ~univs ~types:t b in let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.Definition UnivNames.empty_binders entry [] + ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry [] in () in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 9745358ba2..5b3f15a08c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -104,4 +104,5 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o let ce = check_definition ~program_mode def in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + let kind = Decls.IsDefinition kind in ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 98b869d72e..cee5b7c1f4 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -15,18 +15,15 @@ open Util open Constr open Context open Environ -open Declare open Names open Libnames open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Impargs open Reductionops open Type_errors open Pretyping -open Indschemes open Context.Rel.Declaration open Entries @@ -80,12 +77,6 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } -let minductive_message = function - | [] -> user_err Pp.(str "No inductive definition.") - | [x] -> (Id.print x ++ str " is defined") - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are defined") - let check_all_names_different indl = let ind_names = List.map (fun ind -> ind.ind_name) indl in let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in @@ -541,62 +532,6 @@ let extract_mutual_inductive_declaration_components indl = let indl = extract_inductive indl in (params,indl), coes, List.flatten ntnl -let is_recursive mie = - let rec is_recursive_constructor lift typ = - match Constr.kind typ with - | Prod (_,arg,rest) -> - not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || - is_recursive_constructor (lift+1) rest - | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest - | _ -> false - in - match mie.mind_entry_inds with - | [ind] -> - let nparams = List.length mie.mind_entry_params in - List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc - | _ -> false - -let warn_non_primitive_record = - CWarnings.create ~name:"non-primitive-record" ~category:"record" - (fun indsp -> - (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++ - strbrk" could not be defined as a primitive record"))) - -let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls = - (* spiwack: raises an error if the structure is supposed to be non-recursive, - but isn't *) - begin match mie.mind_entry_finite with - | Declarations.BiFinite when is_recursive mie -> - if Option.has_some mie.mind_entry_record then - user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") - else - user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) - | _ -> () - end; - let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_, kn), prim = declare_mind mie in - let mind = Global.mind_of_delta_kn kn in - if primitive_expected && not prim then warn_non_primitive_record (mind,0); - Declare.declare_univ_binders (GlobRef.IndRef (mind,0)) pl; - List.iteri (fun i (indimpls, constrimpls) -> - let ind = (mind,i) in - let gr = GlobRef.IndRef ind in - maybe_declare_manual_implicits false gr indimpls; - List.iteri - (fun j impls -> - maybe_declare_manual_implicits false - (GlobRef.ConstructRef (ind, succ j)) impls) - constrimpls) - impls; - Flags.if_verbose Feedback.msg_info (minductive_message names); - if mie.mind_entry_private == None - then declare_default_schemes mind; - mind - -type one_inductive_impls = - Impargs.manual_implicits (* for inds *) * - Impargs.manual_implicits list (* for constrs *) - type uniform_inductive_flag = | UniformParameters | NonUniformParameters @@ -607,7 +542,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in (* Declare the mutual inductive block with its associated schemes *) - ignore (declare_mutual_inductive_with_eliminations mie pl impls); + ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) @@ -652,3 +587,5 @@ let make_cases ind = let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) mip.mind_nf_lc [] + +let declare_mutual_inductive_with_eliminations = DeclareInd.declare_mutual_inductive_with_eliminations diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7587bd165f..067fb3d2ca 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Entries open Vernacexpr open Constrexpr @@ -42,22 +41,18 @@ val do_mutual_inductive val make_cases : Names.inductive -> string list list +val declare_mutual_inductive_with_eliminations + : ?primitive_expected:bool + -> Entries.mutual_inductive_entry + -> UnivNames.universe_binders + -> DeclareInd.one_inductive_impls list + -> Names.MutInd.t + [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] + (************************************************************************) (** Internal API, exported for Record *) (************************************************************************) -(** Registering a mutual inductive definition together with its - associated schemes *) - -type one_inductive_impls = - Impargs.manual_implicits (* for inds *) * - Impargs.manual_implicits list (* for constrs *) - -val declare_mutual_inductive_with_eliminations : - ?primitive_expected:bool -> - mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> - MutInd.t - val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the @@ -72,7 +67,3 @@ val template_polymorphism_candidate : can be made parametric in its conclusion sort, if one is given. If the [Template Check] flag is false we just check that the conclusion sort is not small. *) - -val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t -(** [sign_level env sigma ctx] computes the universe level of the context [ctx] - as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 1926faaf0e..f044c025d8 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -48,13 +48,13 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let gr = match scope with | Discharge -> let () = - declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce) + declare_variable ~name ~kind (SectionLocalDef ce) in Names.GlobRef.VarRef name | Global local -> - let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in + let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in let gr = Names.GlobRef.ConstRef kn in - let () = Declare.declare_univ_binders gr udecl in + let () = DeclareUniv.declare_univ_binders gr udecl in gr in let () = maybe_declare_manual_implicits false gr imps in @@ -69,6 +69,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in + let kind = Decls.IsDefinition kind in declare_definition ~name ~scope ~kind ?hook_data udecl ce imps let check_definition_evars ~allow_evars sigma = diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 54a0c9a7e8..d6001f5970 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -42,7 +42,7 @@ end val declare_definition : name:Id.t -> scope:locality - -> kind:Decls.definition_object_kind + -> kind:Decls.logical_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> UnivNames.universe_binders -> Evd.side_effects Declare.proof_entry diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml new file mode 100644 index 0000000000..2375028541 --- /dev/null +++ b/vernac/declareInd.ml @@ -0,0 +1,214 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Entries + +(** Declaration of inductive blocks *) +let declare_inductive_argument_scopes kn mie = + List.iteri (fun i {mind_entry_consnames=lc} -> + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.IndRef (kn,i)); + for j=1 to List.length lc do + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j)); + done) mie.mind_entry_inds + +type inductive_obj = { + ind_names : (Id.t * Id.t list) list + (* For each block, name of the type + name of constructors *) +} + +let inductive_names sp kn obj = + let (dp,_) = Libnames.repr_path sp in + let kn = Global.mind_of_delta_kn kn in + let names, _ = + List.fold_left + (fun (names, n) (typename, consnames) -> + let ind_p = (kn,n) in + let names, _ = + List.fold_left + (fun (names, p) l -> + let sp = + Libnames.make_path dp l + in + ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1)) + (names, 1) consnames in + let sp = Libnames.make_path dp typename + in + ((sp, GlobRef.IndRef ind_p) :: names, n+1)) + ([], 0) obj.ind_names + in names + +let load_inductive i ((sp, kn), names) = + let names = inductive_names sp kn names in + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names + +let open_inductive i ((sp, kn), names) = + let names = inductive_names sp kn names in + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names + +let cache_inductive ((sp, kn), names) = + let names = inductive_names sp kn names in + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names + +let discharge_inductive ((sp, kn), names) = + Some names + +let inInductive : inductive_obj -> Libobject.obj = + let open Libobject in + declare_object {(default_object "INDUCTIVE") with + cache_function = cache_inductive; + load_function = load_inductive; + open_function = open_inductive; + classify_function = (fun a -> Substitute a); + subst_function = ident_subst_function; + discharge_function = discharge_inductive; + } + + +let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c + +let load_prim _ p = cache_prim p + +let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c + +let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) + +let inPrim : (Projection.Repr.t * Constant.t) -> Libobject.obj = + let open Libobject in + declare_object { + (default_object "PRIMPROJS") with + cache_function = cache_prim ; + load_function = load_prim; + subst_function = subst_prim; + classify_function = (fun x -> Substitute x); + discharge_function = discharge_prim } + +let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) + +let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = + let name = Label.to_id label in + let univs, u = match univs with + | Monomorphic_entry _ -> + (* Global constraints already defined through the inductive *) + Monomorphic_entry Univ.ContextSet.empty, Univ.Instance.empty + | Polymorphic_entry (nas, ctx) -> + Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx + in + let term = Vars.subst_instance_constr u term in + let types = Vars.subst_instance_constr u types in + let entry = Declare.definition_entry ~types ~univs term in + let cst = Declare.declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (Declare.DefinitionEntry entry) in + let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in + declare_primitive_projection p cst + +let declare_projections univs mind = + let env = Global.env () in + let mib = Environ.lookup_mind mind env in + let open Declarations in + match mib.mind_record with + | PrimRecord info -> + let iter_ind i (_, labs, _, _) = + let ind = (mind, i) in + let projs = Inductiveops.compute_projections env ind in + CArray.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs + in + let () = Array.iteri iter_ind info in + true + | FakeRecord -> false + | NotRecord -> false + +let feedback_axiom () = Feedback.(feedback AddedAxiom) + +let is_unsafe_typing_flags () = + let open Declarations in + let flags = Environ.typing_flags (Global.env()) in + not (flags.check_universes && flags.check_guarded && flags.check_positive) + +(* for initial declaration *) +let declare_mind mie = + let id = match mie.mind_entry_inds with + | ind::_ -> ind.mind_entry_typename + | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in + let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in + let names = List.map map_names mie.mind_entry_inds in + List.iter (fun (typ, cons) -> + Declare.check_exists typ; + List.iter Declare.check_exists cons) names; + let _kn' = Global.add_mind id mie in + let (sp,kn as oname) = Lib.add_leaf id (inInductive { ind_names = names }) in + if is_unsafe_typing_flags() then feedback_axiom (); + let mind = Global.mind_of_delta_kn kn in + let isprim = declare_projections mie.mind_entry_universes mind in + Impargs.declare_mib_implicits mind; + declare_inductive_argument_scopes mind mie; + oname, isprim + +let is_recursive mie = + let open Constr in + let rec is_recursive_constructor lift typ = + match Constr.kind typ with + | Prod (_,arg,rest) -> + not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || + is_recursive_constructor (lift+1) rest + | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest + | _ -> false + in + match mie.mind_entry_inds with + | [ind] -> + let nparams = List.length mie.mind_entry_params in + List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc + | _ -> false + +let warn_non_primitive_record = + CWarnings.create ~name:"non-primitive-record" ~category:"record" + (fun indsp -> + Pp.(hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++ + strbrk" could not be defined as a primitive record"))) + +let minductive_message = function + | [] -> CErrors.user_err Pp.(str "No inductive definition.") + | [x] -> Pp.(Id.print x ++ str " is defined") + | l -> Pp.(hov 0 (prlist_with_sep pr_comma Id.print l ++ + spc () ++ str "are defined")) + +type one_inductive_impls = + Impargs.manual_implicits (* for inds *) * + Impargs.manual_implicits list (* for constrs *) + +let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls = + (* spiwack: raises an error if the structure is supposed to be non-recursive, + but isn't *) + begin match mie.mind_entry_finite with + | Declarations.BiFinite when is_recursive mie -> + if Option.has_some mie.mind_entry_record then + CErrors.user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") + else + CErrors.user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) + | _ -> () + end; + let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in + let (_, kn), prim = declare_mind mie in + let mind = Global.mind_of_delta_kn kn in + if primitive_expected && not prim then warn_non_primitive_record (mind,0); + DeclareUniv.declare_univ_binders (GlobRef.IndRef (mind,0)) pl; + List.iteri (fun i (indimpls, constrimpls) -> + let ind = (mind,i) in + let gr = GlobRef.IndRef ind in + Impargs.maybe_declare_manual_implicits false gr indimpls; + List.iteri + (fun j impls -> + Impargs.maybe_declare_manual_implicits false + (GlobRef.ConstructRef (ind, succ j)) impls) + constrimpls) + impls; + Flags.if_verbose Feedback.msg_info (minductive_message names); + if mie.mind_entry_private == None + then Indschemes.declare_default_schemes mind; + mind diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli new file mode 100644 index 0000000000..df8895a999 --- /dev/null +++ b/vernac/declareInd.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Registering a mutual inductive definition together with its + associated schemes *) + +type one_inductive_impls = + Impargs.manual_implicits (* for inds *) * + Impargs.manual_implicits list (* for constrs *) + +val declare_mutual_inductive_with_eliminations + : ?primitive_expected:bool + -> Entries.mutual_inductive_entry + -> UnivNames.universe_binders + -> one_inductive_impls list + -> Names.MutInd.t diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 8fd6bc7eab..2c56f707f1 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -351,7 +351,8 @@ let declare_definition prg = let ubinders = UState.universe_binders uctx in let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in DeclareDef.declare_definition - ~name:prg.prg_name ~scope:prg.prg_scope ubinders ~kind:prg.prg_kind ce + ~name:prg.prg_name ~scope:prg.prg_scope ubinders + ~kind:Decls.(IsDefinition prg.prg_kind) ce prg.prg_implicits ?hook_data let rec lam_index n t acc = diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml new file mode 100644 index 0000000000..69ba9d76ec --- /dev/null +++ b/vernac/declareUniv.ml @@ -0,0 +1,110 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +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 *) + | UnqualifiedUniv (* other global universe *) + +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)) + else () + +let qualify_univ i dp src id = + match src with + | BoundUniv | UnqualifiedUniv -> + i, Libnames.make_path dp id + | QualifiedUniv l -> + let dp = DirPath.repr dp in + Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id + +let do_univ_name ~check i dp src (id,univ) = + let i, sp = qualify_univ i dp src id in + if check then check_exists_universe sp; + Nametab.push_universe i sp univ + +let cache_univ_names ((sp, _), (src, univs)) = + let depth = Lib.sections_depth () in + let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in + List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs + +let load_univ_names i ((sp, _), (src, univs)) = + List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs + +let open_univ_names i ((sp, _), (src, univs)) = + List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs + +let discharge_univ_names = function + | _, (BoundUniv, _) -> None + | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x + +let input_univ_names : universe_name_decl -> Libobject.obj = + let open Libobject in + declare_object + { (default_object "Global universe name state") with + cache_function = cache_univ_names; + load_function = load_univ_names; + open_function = open_univ_names; + discharge_function = discharge_univ_names; + subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); + classify_function = (fun a -> Substitute a) } + +let declare_univ_binders gr pl = + if Global.is_polymorphic gr then + () + else + let l = let open GlobRef in match gr with + | ConstRef c -> Label.to_id @@ Constant.label c + | IndRef (c, _) -> Label.to_id @@ MutInd.label c + | VarRef id -> + CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") + | ConstructRef _ -> + CErrors.anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on an constructor reference") + in + let univs = Id.Map.fold (fun id univ univs -> + match Univ.Level.name univ with + | None -> assert false (* having Prop/Set/Var as binders is nonsense *) + | Some univ -> (id,univ)::univs) pl [] + in + Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) + +let do_universe ~poly l = + let in_section = Global.sections_are_opened () in + let () = + if poly && not in_section then + CErrors.user_err ~hdr:"Constraint" + (Pp.str"Cannot declare polymorphic universes outside sections") + in + let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in + let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) + Univ.LSet.empty l, Univ.Constraint.empty + in + let src = if poly then BoundUniv else UnqualifiedUniv in + let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in + Declare.declare_universe_context ~poly ctx + +let do_constraint ~poly l = + let open Univ in + let u_of_id x = + Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x + in + let constraints = List.fold_left (fun acc (l, d, r) -> + let lu = u_of_id l and ru = u_of_id r in + Constraint.add (lu, d, ru) acc) + Constraint.empty l + in + let uctx = ContextSet.add_constraints constraints ContextSet.empty in + Declare.declare_universe_context ~poly uctx diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli new file mode 100644 index 0000000000..ce2a6e225c --- /dev/null +++ b/vernac/declareUniv.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +(** Global universe contexts, names and constraints *) +val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit + +val do_universe : poly:bool -> lident list -> unit +val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index e49277c51b..5ace8b917c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -335,7 +335,7 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe in let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in let () = Declare.assumption_message name in - Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx); + DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx); (* This takes care of the implicits and hook for the current constant*) process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms @@ -425,7 +425,7 @@ let finish_proved env sigma idopt po info = then Proof_using.suggest_constant (Global.env ()) kn in let gr = GlobRef.ConstRef kn in - Declare.declare_univ_binders gr (UState.universe_binders universes); + DeclareUniv.declare_univ_binders gr (UState.universe_binders universes); gr in Declare.definition_message name; diff --git a/vernac/record.ml b/vernac/record.ml index 831fb53549..b60bfdfa22 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -466,7 +466,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa in let mie = InferCumulativity.infer_inductive (Global.env ()) mie in let impls = List.map (fun _ -> paramimpls, []) record_data in - let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls + let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag in let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) = diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index afc701edbc..956b56e256 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -13,6 +13,7 @@ Ppvernac Proof_using Egramcoq Metasyntax +DeclareUniv DeclareDef DeclareObl Canonical @@ -28,6 +29,7 @@ ComDefinition Classes ComPrimitive ComAssumption +DeclareInd ComInductive ComFixpoint ComProgramFixpoint diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 430cee62c2..4ecd815dd2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -814,14 +814,14 @@ let vernac_universe ~poly l = user_err ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); - Declare.do_universe ~poly l + DeclareUniv.do_universe ~poly l let vernac_constraint ~poly l = if poly && not (Global.sections_are_opened ()) then user_err ~hdr:"vernac_constraint" (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); - Declare.do_constraint ~poly l + DeclareUniv.do_constraint ~poly l (**********************) (* Modules *) |