diff --git a/.nix/coq-overlays/mathcomp-analysis/default.nix b/.nix/coq-overlays/mathcomp-analysis/default.nix new file mode 100644 index 0000000000..97f2add33a --- /dev/null +++ b/.nix/coq-overlays/mathcomp-analysis/default.nix @@ -0,0 +1,123 @@ +{ lib, + mkCoqDerivation, + mathcomp, mathcomp-finmap, mathcomp-bigenough, + hierarchy-builder, + single ? false, + coqPackages, coq, version ? null }@args: + +let + repo = "analysis"; + owner = "math-comp"; + + release."1.5.0".sha256 = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88="; + release."1.4.0".sha256 = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg="; + release."1.2.0".sha256 = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo="; + release."1.1.0".sha256 = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o="; + release."1.0.0".sha256 = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4="; + release."0.7.0".sha256 = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60="; + release."0.6.7".sha256 = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA="; + release."0.6.6".sha256 = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y="; + release."0.6.5".sha256 = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E="; + release."0.6.1".sha256 = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0="; + release."0.6.0".sha256 = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg="; + release."0.5.3".sha256 = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k="; + release."0.5.2".sha256 = "0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw"; + release."0.5.1".sha256 = "1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68"; + release."0.3.13".sha256 = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg="; + release."0.3.10".sha256 = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI="; + release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4="; + release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5"; + release."0.3.4".sha256 = "18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c"; + release."0.3.3".sha256 = "1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867"; + release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; + release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; + + defaultVersion = let inherit (lib.versions) range; in + lib.switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.19" "8.20") (range "2.1.0" "2.2.0") ]; out = "1.5.0"; } + { cases = [ (range "8.17" "8.20") (range "2.0.0" "2.2.0") ]; out = "1.1.0"; } + { cases = [ (range "8.17" "8.19") (range "1.17.0" "1.19.0") ]; out = "0.7.0"; } + { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.7"; } + { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.6"; } + { cases = [ (range "8.14" "8.18") (range "1.15.0" "1.17.0") ]; out = "0.6.5"; } + { cases = [ (range "8.14" "8.18") (range "1.13.0" "1.16.0") ]; out = "0.6.1"; } + { cases = [ (range "8.14" "8.18") (range "1.13" "1.15") ]; out = "0.5.2"; } + { cases = [ (range "8.13" "8.15") (range "1.13" "1.14") ]; out = "0.5.1"; } + { cases = [ (range "8.13" "8.15") (range "1.12" "1.14") ]; out = "0.3.13"; } + { cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ]; out = "0.3.10"; } + { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "0.3.3"; } + { cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; } + { cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; } + ] null; + + # list of analysis packages sorted by dependency order + packages = { + "classical" = []; + "reals" = [ "classical" ]; + "altreals" = [ "reals" ]; + "analysis" = [ "reals" ]; + "reals-stdlib" = [ "reals" ]; + "analysis-stdlib" = [ "analysis" "reals-stdlib" ]; + }; + + mathcomp_ = package: let + classical-deps = [ mathcomp.algebra mathcomp-finmap ]; + analysis-deps = [ mathcomp.field mathcomp-bigenough ]; + intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package}); + pkgpath = lib.switch package [ + { case = "single"; out = "."; } + { case = "analysis"; out = "theories"; } + { case = "reals-stdlib"; out = "reals_stdlib"; } + { case = "analysis-stdlib"; out = "analysis_stdlib"; } + ] package; + pname = if package == "single" then "mathcomp-analysis-single" + else "mathcomp-${package}"; + derivation = mkCoqDerivation ({ + inherit version pname defaultVersion release repo owner; + + namePrefix = [ "coq" "mathcomp" ]; + + propagatedBuildInputs = + intra-deps + ++ lib.optionals (lib.elem package [ "classical" "single" ]) classical-deps + ++ lib.optionals (lib.elem package [ "analysis" "single" ]) analysis-deps; + + preBuild = '' + cd ${pkgpath} + ''; + + meta = { + description = "Analysis library compatible with Mathematical Components"; + maintainers = [ lib.maintainers.cohencyril ]; + license = lib.licenses.cecill-c; + }; + + passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages; + }); + # split packages didn't exist before 0.6, so bulding nothing in that case + patched-derivation1 = derivation.overrideAttrs (o: + lib.optionalAttrs (o.pname != null && o.pname != "mathcomp-analysis" && + o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version) + { preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; } + ); + patched-derivation2 = patched-derivation1.overrideAttrs (o: + lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" && + o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version) + { preBuild = ""; } + ); + # only packages classical and analysis existed before 1.7, so bulding nothing in that case + patched-derivation3 = patched-derivation2.overrideAttrs (o: + lib.optionalAttrs (o.pname != null && o.pname != "mathcomp-classical" && o.pname != "mathcomp-analysis" && + o.version != null && o.version != "dev" && lib.versions.isLt "1.7" o.version) + { preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; } + ); + patched-derivation = patched-derivation3.overrideAttrs (o: + lib.optionalAttrs (o.version != null + && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version)) + { + propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; + } + ); + in patched-derivation; +in +mathcomp_ (if single then "single" else "analysis") diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 893b808432..03c90f7b0c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,6 +4,39 @@ ### Added +- file `Rstruct_topology.v` + +- package `coq-mathcomp-reals` depending on `coq-mathcomp-classical` + with files + + `constructive_ereal.v` + + `reals.v` + + `real_interval.v` + + `signed.v` + + `itv.v` + + `prodnormedzmodule.v` + + `nsatz_realtype.v` + + `all_reals.v` + +- in file `separation_axioms.v`, + + new lemmas `compact_normal_local`, and `compact_normal`. + +- package `coq-mathcomp-altreals` depending on `coq-mathcomp-reals` + with files + + `xfinmap.v` + + `discrete.v` + + `realseq.v` + + `realsum.v` + + `distr.v` + +- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals` + with file + + `Rstruct.v` + +- package `coq-mathcomp-analysis-stdlib` depending on + `coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files + + `Rstruct_topology.v` + + `showcase/uniform_bigO.v` + - in file `separation_axioms.v`, + new lemmas `compact_normal_local`, and `compact_normal`. @@ -31,6 +64,16 @@ which removes the dependency on `R`. The old formulation can be recovered easily with `uniform_separatorP`. +- moved from `Rstruct.v` to `Rstruct_topology.v` + + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, + `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs` + and `nbhs_pt_comp` + +- moved from `real_interval.v` to `normedtype.v` + + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`, + `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`, + `disj_itv_Rhull` + ### Renamed ### Generalized diff --git a/_CoqProject b/_CoqProject index 4b266b2265..0c3ff3b819 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,5 +1,9 @@ -Q classical mathcomp.classical +-Q reals mathcomp.reals +-Q reals_stdlib mathcomp.reals_stdlib +-Q altreals mathcomp.altreals -Q theories mathcomp.analysis +-Q analysis_stdlib mathcomp.analysis_stdlib -arg -w -arg -parsing -arg -w -arg +undeclared-scope @@ -20,11 +24,22 @@ classical/fsbigop.v classical/set_interval.v classical/classical_orders.v classical/filter.v +reals/constructive_ereal.v +reals/reals.v +reals/real_interval.v +reals/signed.v +reals/itv.v +reals/prodnormedzmodule.v +reals/nsatz_realtype.v +reals/all_reals.v +altreals/xfinmap.v +altreals/discrete.v +altreals/realseq.v +altreals/realsum.v +altreals/distr.v +reals_stdlib/Rstruct.v theories/all_analysis.v -theories/constructive_ereal.v -theories/reals.v theories/landau.v -theories/Rstruct.v theories/topology_theory/topology.v theories/topology_theory/bool_topology.v @@ -48,15 +63,12 @@ theories/separation_axioms.v theories/function_spaces.v theories/ereal.v theories/cantor.v -theories/prodnormedzmodule.v theories/normedtype.v theories/realfun.v theories/sequences.v theories/exp.v theories/trigo.v -theories/nsatz_realtype.v theories/esum.v -theories/real_interval.v theories/lebesgue_measure.v theories/lebesgue_stieltjes_measure.v theories/forms.v @@ -67,15 +79,9 @@ theories/lebesgue_integral.v theories/ftc.v theories/hoelder.v theories/probability.v -theories/signed.v -theories/itv.v theories/convex.v theories/charge.v theories/kernel.v -theories/showcase/uniform_bigO.v theories/showcase/summability.v -theories/altreals/xfinmap.v -theories/altreals/discrete.v -theories/altreals/realseq.v -theories/altreals/realsum.v -theories/altreals/distr.v +analysis_stdlib/Rstruct_topology.v +analysis_stdlib/showcase/uniform_bigO.v diff --git a/theories/altreals/LICENSE b/altreals/LICENSE similarity index 100% rename from theories/altreals/LICENSE rename to altreals/LICENSE diff --git a/altreals/Make b/altreals/Make new file mode 100644 index 0000000000..85e6747e84 --- /dev/null +++ b/altreals/Make @@ -0,0 +1,14 @@ +-Q . mathcomp.altreals + +-arg -w -arg -parsing +-arg -w -arg +undeclared-scope +-arg -w -arg +non-primitive-record +-arg -w -arg -ambiguous-paths +-arg -w -arg -redundant-canonical-projection +-arg -w -arg -projection-no-head-constant + +xfinmap.v +discrete.v +realseq.v +realsum.v +distr.v diff --git a/altreals/Makefile b/altreals/Makefile new file mode 100644 index 0000000000..103b008b60 --- /dev/null +++ b/altreals/Makefile @@ -0,0 +1,7 @@ +# -*- Makefile -*- + +# setting variables +COQPROJECT?=Make + +# Main Makefile +include ../Makefile.common diff --git a/theories/altreals/dedekind.v b/altreals/dedekind.v similarity index 100% rename from theories/altreals/dedekind.v rename to altreals/dedekind.v diff --git a/theories/altreals/discrete.v b/altreals/discrete.v similarity index 100% rename from theories/altreals/discrete.v rename to altreals/discrete.v diff --git a/theories/altreals/distr.v b/altreals/distr.v similarity index 100% rename from theories/altreals/distr.v rename to altreals/distr.v diff --git a/theories/altreals/realseq.v b/altreals/realseq.v similarity index 100% rename from theories/altreals/realseq.v rename to altreals/realseq.v diff --git a/theories/altreals/realsum.v b/altreals/realsum.v similarity index 100% rename from theories/altreals/realsum.v rename to altreals/realsum.v diff --git a/theories/altreals/xfinmap.v b/altreals/xfinmap.v similarity index 100% rename from theories/altreals/xfinmap.v rename to altreals/xfinmap.v diff --git a/analysis_stdlib/Make b/analysis_stdlib/Make new file mode 100644 index 0000000000..c34e45fe9b --- /dev/null +++ b/analysis_stdlib/Make @@ -0,0 +1,11 @@ +-Q . mathcomp.analysis_stdlib + +-arg -w -arg -parsing +-arg -w -arg +undeclared-scope +-arg -w -arg +non-primitive-record +-arg -w -arg -ambiguous-paths +-arg -w -arg -redundant-canonical-projection +-arg -w -arg -projection-no-head-constant + +Rstruct_topology.v +showcase/uniform_bigO.v diff --git a/analysis_stdlib/Makefile b/analysis_stdlib/Makefile new file mode 100644 index 0000000000..103b008b60 --- /dev/null +++ b/analysis_stdlib/Makefile @@ -0,0 +1,7 @@ +# -*- Makefile -*- + +# setting variables +COQPROJECT?=Make + +# Main Makefile +include ../Makefile.common diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v new file mode 100644 index 0000000000..1d8e3f65a5 --- /dev/null +++ b/analysis_stdlib/Rstruct_topology.v @@ -0,0 +1,89 @@ +(**md**************************************************************************) +(* # Compatibility with the real numbers of Coq *) +(* *) +(* Lemmas about continuity *) +(******************************************************************************) + +Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf. +Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. +Require Import Rtrigo1 Reals. +From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum. +From mathcomp Require Import archimedean. +From HB Require Import structures. +From mathcomp Require Import mathcomp_extra. +From mathcomp Require Import boolp classical_sets. +From mathcomp Require Import reals signed. +From mathcomp Require Import topology. +From mathcomp Require Export Rstruct. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Theory. + +Local Open Scope R_scope. +Local Open Scope ring_scope. + +Section analysis_struct. + +HB.instance Definition _ := PseudoMetric.copy R R^o. +HB.instance Definition _ := Pointed.copy R R^o. + +(* TODO: express using ball?*) +Lemma continuity_pt_nbhs (f : R -> R) x : + continuity_pt f x <-> + forall eps : {posnum R}, nbhs x (fun u => `|f u - f x| < eps%:num). +Proof. +split=> [fcont e|fcont _/RltP/posnumP[e]]; last first. + have [_/posnumP[d] xd_fxe] := fcont e. + exists d%:num; split; first by apply/RltP; have := [gt0 of d%:num]. + by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /= distrC. +have /RltP egt0 := [gt0 of e%:num]. +have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0. +exists d%:num => //= y xyd; case: (eqVneq x y) => [->|xney]. + by rewrite subrr normr0. +apply/RltP/dx_fxe; split; first by split=> //; apply/eqP. +by have /RltP := xyd; rewrite distrC. +Qed. + +Lemma continuity_pt_cvg (f : R -> R) (x : R) : + continuity_pt f x <-> {for x, continuous f}. +Proof. +eapply iff_trans; first exact: continuity_pt_nbhs. +apply iff_sym. +have FF : Filter (f @ x)%classic. + by typeclasses eauto. + (*by apply fmap_filter; apply: @filter_filter' (locally_filter _).*) +case: (@fcvg_ballP _ _ (f @ x)%classic FF (f x)) => {FF}H1 H2. +(* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *) +split => [{H2} - /H1 {}H1 eps|{H1} H]. +- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num. + exists x0%:num => //= Hx0' /Hx0 /=. + by rewrite /= distrC; apply. +- apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0]. + exists x0%:num => //= y /Hx0 /= {}Hx0. + by rewrite /ball /= distrC. +Qed. + +Lemma continuity_ptE (f : R -> R) (x : R) : + continuity_pt f x <-> {for x, continuous f}. +Proof. exact: continuity_pt_cvg. Qed. + +Local Open Scope classical_set_scope. + +Lemma continuity_pt_cvg' f x : + continuity_pt f x <-> f @ x^' --> f x. +Proof. by rewrite continuity_ptE continuous_withinNx. Qed. + +Lemma continuity_pt_dnbhs f x : + continuity_pt f x <-> + forall eps, 0 < eps -> x^' (fun u => `|f x - f u| < eps). +Proof. +by rewrite continuity_pt_cvg' -filter_fromP cvg_ballP -filter_fromP. +Qed. + +Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) : + nbhs (f x) P -> continuity_pt f x -> \near x, P (f x). +Proof. by move=> Lf /continuity_pt_cvg; apply. Qed. + +End analysis_struct. diff --git a/theories/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v similarity index 98% rename from theories/showcase/uniform_bigO.v rename to analysis_stdlib/showcase/uniform_bigO.v index 5cf1f1180d..58e6e9c5b9 100644 --- a/theories/showcase/uniform_bigO.v +++ b/analysis_stdlib/showcase/uniform_bigO.v @@ -2,7 +2,7 @@ From Coq Require Import Reals. From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum. -From mathcomp Require Import boolp reals Rstruct ereal. +From mathcomp Require Import boolp reals Rstruct_topology ereal. From mathcomp Require Import classical_sets signed topology normedtype landau. Set Implicit Arguments. diff --git a/coq-mathcomp-altreals.opam b/coq-mathcomp-altreals.opam new file mode 100644 index 0000000000..e4088ca37c --- /dev/null +++ b/coq-mathcomp-altreals.opam @@ -0,0 +1,43 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. + +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library for alternative real numbers for mathematical components" +description: """ +This repository contains a library for alternative real numbers for +the Coq proof-assistant and using the Mathematical Components library.""" + +build: [make "-C" "altreals" "-j%{jobs}%"] +install: [make "-C" "altreals" "install"] +depends: [ + "coq-mathcomp-reals" { = version} +] + +tags: [ + "category:Mathematics/Real Numbers" + "keyword:real numbers" + "keyword:reals" + "logpath:mathcomp.altreals" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] diff --git a/coq-mathcomp-analysis-stdlib.opam b/coq-mathcomp-analysis-stdlib.opam new file mode 100644 index 0000000000..a6669caccf --- /dev/null +++ b/coq-mathcomp-analysis-stdlib.opam @@ -0,0 +1,44 @@ +*# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. + +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library to link real numbers from mathematical components and Stdlib" +description: """ +This repository contains a library to link real numbers for +the Coq proof-assistant using the Mathematical Components library and Stdlib.""" + +build: [make "-C" "analysis_stdlib" "-j%{jobs}%"] +install: [make "-C" "analysis_stdlib" "install"] +depends: [ + "coq-mathcomp-analysis" { = version} + "coq-mathcomp-reals-stdlib" +] + +tags: [ + "category:Mathematics/Real Numbers" + "keyword:real numbers" + "keyword:reals" + "logpath:mathcomp.reals_stdlib" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index 5ba3149457..a58028fede 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -18,9 +18,8 @@ the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-C" "theories" "-j%{jobs}%"] install: [make "-C" "theories" "install"] depends: [ - "coq" { (>= "8.19" & < "8.21~") | (= "dev") } "coq-mathcomp-classical" { = version} - "coq-mathcomp-solvable" { (>= "2.0.0") | (= "dev") } + "coq-mathcomp-solvable" "coq-mathcomp-field" "coq-mathcomp-bigenough" { (>= "1.0.0") } ] diff --git a/coq-mathcomp-reals-stdlib.opam b/coq-mathcomp-reals-stdlib.opam new file mode 100644 index 0000000000..c3a6649367 --- /dev/null +++ b/coq-mathcomp-reals-stdlib.opam @@ -0,0 +1,43 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. + +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library to link real numbers from mathematical components and Stdlib" +description: """ +This repository contains a library to link real numbers for +the Coq proof-assistant using the Mathematical Components library and Stdlib.""" + +build: [make "-C" "reals_stdlib" "-j%{jobs}%"] +install: [make "-C" "reals_stdlib" "install"] +depends: [ + "coq-mathcomp-reals" { = version} +] + +tags: [ + "category:Mathematics/Real Numbers" + "keyword:real numbers" + "keyword:reals" + "logpath:mathcomp.reals_stdlib" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] diff --git a/coq-mathcomp-reals.opam b/coq-mathcomp-reals.opam new file mode 100644 index 0000000000..ade61342df --- /dev/null +++ b/coq-mathcomp-reals.opam @@ -0,0 +1,43 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. + +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library for real numbers for mathematical components" +description: """ +This repository contains a library for real numbers for +the Coq proof-assistant and using the Mathematical Components library.""" + +build: [make "-C" "reals" "-j%{jobs}%"] +install: [make "-C" "reals" "install"] +depends: [ + "coq-mathcomp-classical" { = version} +] + +tags: [ + "category:Mathematics/Real Numbers" + "keyword:real numbers" + "keyword:reals" + "logpath:mathcomp.reals" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] diff --git a/etc/packager b/etc/packager new file mode 100755 index 0000000000..f7a736bc6b --- /dev/null +++ b/etc/packager @@ -0,0 +1,86 @@ +#!/bin/bash +set -e +set -x + +if [ -z $1 ] || [ $1 == "--help" ] || [ $1 == "-h" ] +then cat < $pkgdir/opam + sed -r "/^version/d" -i $pkgdir/opam + fi + echo "" >> $pkgdir/opam + echo "url {" >> $pkgdir/opam + echo $URLLINE >> $pkgdir/opam + if [ $VERSION != "dev" ] + then echo $CHECKSUMLINE >> $pkgdir/opam + fi + echo "}" >> $pkgdir/opam +done + +# finally test the existence of the archive +wget --spider $ARCHIVEURL diff --git a/reals/Make b/reals/Make new file mode 100644 index 0000000000..427b997d1c --- /dev/null +++ b/reals/Make @@ -0,0 +1,17 @@ +-Q . mathcomp.reals + +-arg -w -arg -parsing +-arg -w -arg +undeclared-scope +-arg -w -arg +non-primitive-record +-arg -w -arg -ambiguous-paths +-arg -w -arg -redundant-canonical-projection +-arg -w -arg -projection-no-head-constant + +constructive_ereal.v +reals.v +real_interval.v +signed.v +itv.v +prodnormedzmodule.v +nsatz_realtype.v +all_reals.v diff --git a/reals/Makefile b/reals/Makefile new file mode 100644 index 0000000000..103b008b60 --- /dev/null +++ b/reals/Makefile @@ -0,0 +1,7 @@ +# -*- Makefile -*- + +# setting variables +COQPROJECT?=Make + +# Main Makefile +include ../Makefile.common diff --git a/reals/all_reals.v b/reals/all_reals.v new file mode 100644 index 0000000000..1f7707f6c8 --- /dev/null +++ b/reals/all_reals.v @@ -0,0 +1,7 @@ +From mathcomp Require Export signed. +From mathcomp Require Export itv. +From mathcomp Require Export constructive_ereal. +From mathcomp Require Export reals. +From mathcomp Require Export real_interval. +From mathcomp Require Export prodnormedzmodule. +From mathcomp Require Export nsatz_realtype. diff --git a/theories/constructive_ereal.v b/reals/constructive_ereal.v similarity index 100% rename from theories/constructive_ereal.v rename to reals/constructive_ereal.v diff --git a/theories/itv.v b/reals/itv.v similarity index 100% rename from theories/itv.v rename to reals/itv.v diff --git a/theories/nsatz_realtype.v b/reals/nsatz_realtype.v similarity index 97% rename from theories/nsatz_realtype.v rename to reals/nsatz_realtype.v index a25a4c0f9f..13ac17f8ab 100644 --- a/theories/nsatz_realtype.v +++ b/reals/nsatz_realtype.v @@ -1,6 +1,6 @@ From Coq Require Import Nsatz. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum. -From mathcomp Require Import boolp reals ereal. +From mathcomp Require Import boolp reals constructive_ereal. (**md**************************************************************************) (* # nsatz for realType *) diff --git a/theories/prodnormedzmodule.v b/reals/prodnormedzmodule.v similarity index 100% rename from theories/prodnormedzmodule.v rename to reals/prodnormedzmodule.v diff --git a/theories/real_interval.v b/reals/real_interval.v similarity index 73% rename from theories/real_interval.v rename to reals/real_interval.v index 0e80b3a3de..15db5ad76f 100644 --- a/theories/real_interval.v +++ b/reals/real_interval.v @@ -4,7 +4,7 @@ From mathcomp Require Import fingroup perm rat archimedean finmap. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Export set_interval. From HB Require Import structures. -From mathcomp Require Import reals ereal signed topology normedtype sequences. +From mathcomp Require Import reals constructive_ereal signed. (**md**************************************************************************) (* # Sets and intervals on $\overline{\mathbb{R}}$ *) @@ -133,30 +133,6 @@ Section set_itv_realType. Variable R : realType. Implicit Types x : R. -Lemma set_itvK : {in neitv, cancel pred_set (@Rhull R)}. -Proof. -move=> [[[] x|[]] [[] y|[]]] /neitvP //; - rewrite /Rhull /= !(in_itv, inE)/= ?bnd_simp => xy. -- rewrite asboolT// inf_itv// lexx/= xy asboolT// asboolT//=. - by rewrite asboolF//= sup_itv//= ltxx ?andbF. -- by rewrite asboolT// inf_itv// ?asboolT// ?sup_itv// ?lexx ?xy. -- by rewrite asboolT//= inf_itv// lexx asboolT// asboolF. -- rewrite asboolT// inf_itv//= ltxx asboolF// asboolT//. - by rewrite sup_itv// ltxx andbF asboolF. - rewrite asboolT // inf_itv // ltxx asboolF // asboolT //. - by rewrite sup_itv // xy lexx asboolT. -- by rewrite asboolT // inf_itv// ltxx asboolF // asboolF. -- by rewrite asboolF // asboolT // sup_itv// ltxx asboolF. -- by rewrite asboolF // asboolT // sup_itv// lexx asboolT. -- by rewrite asboolF // asboolF. -Qed. - -Lemma RhullT : Rhull setT = `]-oo, +oo[%R :> interval R. -Proof. by rewrite /Rhull -set_itv_infty_infty asboolF// asboolF. Qed. - -Lemma RhullK : {in (@is_interval _ : set (set R)), cancel (@Rhull R) pred_set}. -Proof. by move=> X /asboolP iX; apply/esym/is_intervalP. Qed. - Lemma itv_c_inftyEbigcap x : `[x, +oo[%classic = \bigcap_k `]x - k.+1%:R^-1, +oo[%classic. Proof. @@ -191,85 +167,8 @@ rewrite in_itv /= andbT => xny. by rewrite in_itv /= andbT (lt_le_trans _ xny) // ltrDl invr_gt0. Qed. -Lemma set_itv_setT (i : interval R) : [set` i] = setT -> i = `]-oo, +oo[. -Proof. -have [i0 /(congr1 (@Rhull _))|] := boolP (neitv i). - by rewrite set_itvK// => ->; exact: RhullT. -by rewrite negbK => /eqP ->; rewrite predeqE => /(_ 0)[_]/(_ Logic.I). -Qed. - End set_itv_realType. -Section Rhull_lemmas. -Variable R : realType. -Implicit Types (a b t r : R) (A : set R). - -Lemma Rhull_smallest A : [set` Rhull A] = smallest (@is_interval R) A. -Proof. -apply/seteqP; split; last first. - by apply: smallest_sub; [apply: interval_is_interval | apply: sub_Rhull]. -move=> x /= + I [Iitv AI]; rewrite /Rhull. -have [|] := asboolP (has_lbound A) => lA; last first. - have /forallNP/(_ x)/existsNP[a] := lA. - move=> /existsNP[Aa /negP]; rewrite -ltNge => ax. - have [|]:= asboolP (has_ubound A) => uA; last first. - move=> ?; have /forallNP/(_ x)/existsNP[b] := uA. - move=> /existsNP[Ab /negP]; rewrite -ltNge => xb. - have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. - by rewrite ax xb. - have [As|NAs]/= := asboolP (A _) => xA. - by apply: (Iitv a (sup A)); by [apply: AI | rewrite ltW ?ax]. - have [||b Ab xb] := @sup_gt _ A x; do ?by [exists a | rewrite (itvP xA)]. - have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. - by rewrite ax xb. -have [|]:= asboolP (has_ubound A) => uA; last first. - have /forallNP/(_ x)/existsNP[b] := uA. - move=> /existsNP[Ab /negP]; rewrite -ltNge => xb. - have [Ai|NAi]/= := asboolP (A _) => xA. - by apply: (Iitv (inf A) b); by [apply: AI | rewrite (ltW xb)]. - have [||a Aa ax] := @inf_lt _ A x; do ?by [exists b | rewrite (itvP xA)]. - have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. - by rewrite ax xb. -have [Ai|NAi]/= := asboolP (A _); have [As|NAs]/= := asboolP (A _). -- by apply: Iitv; apply: AI. -- move=> xA. - have [||b Ab xb] := @sup_gt _ A x; do ?by [exists (inf A) | rewrite (itvP xA)]. - have /(_ (inf A) b) := Iitv; apply; do ?by apply: AI. - by rewrite (itvP xA) (ltW xb). -- move=> xA. - have [||a Aa ax] := @inf_lt _ A x; do ?by [exists (sup A) | rewrite (itvP xA)]. - have /(_ a (sup A)) := Iitv; apply; do ?by apply: AI. - by rewrite (itvP xA) (ltW ax). -have [->|/set0P AN0] := eqVneq A set0. - by rewrite inf0 sup0 itv_ge//= ltBSide/= ltxx. -move=> xA. -have [||a Aa ax] := @inf_lt _ A x; do ?by [|rewrite (itvP xA)]. -have [||b Ab xb] := @sup_gt _ A x; do ?by [|rewrite (itvP xA)]. -have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. -by rewrite ax xb. -Qed. - -Lemma le_Rhull : {homo (@Rhull R) : A B / (A `<=` B) >-> {subset A <= B}}. -Proof. -move=> A B AB; suff: [set` Rhull A] `<=` [set` Rhull B] by []. -rewrite Rhull_smallest; apply: smallest_sub; first exact: interval_is_interval. -by rewrite Rhull_smallest; apply: sub_smallest. -Qed. - -Lemma neitv_Rhull A : ~~ neitv (Rhull A) -> A = set0. -Proof. -move/negPn/eqP => A0; rewrite predeqE => r; split => // /sub_Rhull. -by rewrite A0. -Qed. - -Lemma Rhull_involutive A : Rhull [set` Rhull A] = Rhull A. -Proof. -have [A0|/neitv_Rhull] := boolP (neitv (Rhull A)); first by rewrite set_itvK. -by move=> ->; rewrite ?Rhull0 set_itvE Rhull0. -Qed. - -End Rhull_lemmas. - Coercion ereal_of_itv_bound T (b : itv_bound T) : \bar T := match b with BSide _ y => y%:E | +oo%O => +oo%E | -oo%O => -oo%E end. Arguments ereal_of_itv_bound T !b. @@ -351,12 +250,6 @@ Qed. End set_ereal. -Lemma disj_itv_Rhull {R : realType} (A B : set R) : A `&` B = set0 -> - is_interval A -> is_interval B -> disjoint_itv (Rhull A) (Rhull B). -Proof. -by move=> AB0 iA iB; rewrite /disjoint_itv RhullK ?inE// RhullK ?inE. -Qed. - Lemma set1_bigcap_oc (R : realType) (r : R) : [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic. Proof. diff --git a/theories/reals.v b/reals/reals.v similarity index 100% rename from theories/reals.v rename to reals/reals.v diff --git a/theories/signed.v b/reals/signed.v similarity index 100% rename from theories/signed.v rename to reals/signed.v diff --git a/reals_stdlib/Make b/reals_stdlib/Make new file mode 100644 index 0000000000..c5c217ea2a --- /dev/null +++ b/reals_stdlib/Make @@ -0,0 +1,10 @@ +-Q . mathcomp.reals_stdlib + +-arg -w -arg -parsing +-arg -w -arg +undeclared-scope +-arg -w -arg +non-primitive-record +-arg -w -arg -ambiguous-paths +-arg -w -arg -redundant-canonical-projection +-arg -w -arg -projection-no-head-constant + +Rstruct.v diff --git a/reals_stdlib/Makefile b/reals_stdlib/Makefile new file mode 100644 index 0000000000..103b008b60 --- /dev/null +++ b/reals_stdlib/Makefile @@ -0,0 +1,7 @@ +# -*- Makefile -*- + +# setting variables +COQPROJECT?=Make + +# Main Makefile +include ../Makefile.common diff --git a/theories/Rstruct.v b/reals_stdlib/Rstruct.v similarity index 91% rename from theories/Rstruct.v rename to reals_stdlib/Rstruct.v index ed64108796..4dbe8f0bf5 100644 --- a/theories/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -696,69 +696,3 @@ Qed. End bigmaxr. End ssreal_struct_contd. - -From mathcomp Require Import signed topology. - -Section analysis_struct. - -HB.instance Definition _ := PseudoMetric.copy R R^o. -HB.instance Definition _ := Pointed.copy R R^o. - -(* TODO: express using ball?*) -Lemma continuity_pt_nbhs (f : R -> R) x : - continuity_pt f x <-> - forall eps : {posnum R}, nbhs x (fun u => `|f u - f x| < eps%:num). -Proof. -split=> [fcont e|fcont _/RltP/posnumP[e]]; last first. - have [_/posnumP[d] xd_fxe] := fcont e. - exists d%:num; split; first by apply/RltP; have := [gt0 of d%:num]. - by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /= distrC. -have /RltP egt0 := [gt0 of e%:num]. -have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0. -exists d%:num => //= y xyd; case: (eqVneq x y) => [->|xney]. - by rewrite subrr normr0. -apply/RltP/dx_fxe; split; first by split=> //; apply/eqP. -by have /RltP := xyd; rewrite distrC. -Qed. - -Lemma continuity_pt_cvg (f : R -> R) (x : R) : - continuity_pt f x <-> {for x, continuous f}. -Proof. -eapply iff_trans; first exact: continuity_pt_nbhs. -apply iff_sym. -have FF : Filter (f @ x)%classic. - by typeclasses eauto. - (*by apply fmap_filter; apply: @filter_filter' (locally_filter _).*) -case: (@fcvg_ballP _ _ (f @ x)%classic FF (f x)) => {FF}H1 H2. -(* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *) -split => [{H2} - /H1 {}H1 eps|{H1} H]. -- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num. - exists x0%:num => //= Hx0' /Hx0 /=. - by rewrite /= distrC; apply. -- apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0]. - exists x0%:num => //= y /Hx0 /= {}Hx0. - by rewrite /ball /= distrC. -Qed. - -Lemma continuity_ptE (f : R -> R) (x : R) : - continuity_pt f x <-> {for x, continuous f}. -Proof. exact: continuity_pt_cvg. Qed. - -Local Open Scope classical_set_scope. - -Lemma continuity_pt_cvg' f x : - continuity_pt f x <-> f @ x^' --> f x. -Proof. by rewrite continuity_ptE continuous_withinNx. Qed. - -Lemma continuity_pt_dnbhs f x : - continuity_pt f x <-> - forall eps, 0 < eps -> x^' (fun u => `|f x - f u| < eps). -Proof. -by rewrite continuity_pt_cvg' -filter_fromP cvg_ballP -filter_fromP. -Qed. - -Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) : - nbhs (f x) P -> continuity_pt f x -> \near x, P (f x). -Proof. by move=> Lf /continuity_pt_cvg; apply. Qed. - -End analysis_struct. diff --git a/theories/Make b/theories/Make index 06da64bdef..95312be86f 100644 --- a/theories/Make +++ b/theories/Make @@ -7,11 +7,8 @@ -arg -w -arg -redundant-canonical-projection -arg -w -arg -projection-no-head-constant -constructive_ereal.v -reals.v +ereal.v landau.v -Rstruct.v - topology_theory/topology.v topology_theory/bool_topology.v topology_theory/compact.v @@ -29,20 +26,15 @@ topology_theory/weak_topology.v topology_theory/num_topology.v topology_theory/quotient_topology.v topology_theory/one_point_compactification.v - -ereal.v separation_axioms.v function_spaces.v cantor.v -prodnormedzmodule.v normedtype.v realfun.v sequences.v exp.v trigo.v -nsatz_realtype.v esum.v -real_interval.v lebesgue_measure.v forms.v derive.v @@ -53,16 +45,8 @@ ftc.v hoelder.v probability.v lebesgue_stieltjes_measure.v -signed.v -itv.v convex.v charge.v kernel.v all_analysis.v -showcase/uniform_bigO.v showcase/summability.v -altreals/xfinmap.v -altreals/discrete.v -altreals/realseq.v -altreals/realsum.v -altreals/distr.v diff --git a/theories/all_analysis.v b/theories/all_analysis.v index 6a3e1bc010..99bdb7e9d6 100644 --- a/theories/all_analysis.v +++ b/theories/all_analysis.v @@ -1,8 +1,5 @@ -From mathcomp Require Export constructive_ereal. From mathcomp Require Export ereal. -From mathcomp Require Export reals. From mathcomp Require Export landau. -From mathcomp Require Export Rstruct. From mathcomp Require Export topology. From mathcomp Require Export function_spaces. From mathcomp Require Export cantor. @@ -12,9 +9,7 @@ From mathcomp Require Export realfun. From mathcomp Require Export sequences. From mathcomp Require Export exp. From mathcomp Require Export trigo. -From mathcomp Require Export nsatz_realtype. From mathcomp Require Export esum. -From mathcomp Require Export real_interval. From mathcomp Require Export lebesgue_measure. From mathcomp Require Export forms. From mathcomp Require Export derive. @@ -25,8 +20,6 @@ From mathcomp Require Export ftc. From mathcomp Require Export hoelder. From mathcomp Require Export probability. From mathcomp Require Export lebesgue_stieltjes_measure. -From mathcomp Require Export signed. -From mathcomp Require Export itv. From mathcomp Require Export convex. From mathcomp Require Export charge. From mathcomp Require Export kernel. diff --git a/theories/normedtype.v b/theories/normedtype.v index 6068c10017..debaf7d26c 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -6,7 +6,7 @@ From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import archimedean. From mathcomp Require Import cardinality set_interval ereal reals. From mathcomp Require Import signed topology prodnormedzmodule function_spaces. -From mathcomp Require Export separation_axioms. +From mathcomp Require Export real_interval separation_axioms. (**md**************************************************************************) (* # Norm-related Notions *) @@ -6049,3 +6049,116 @@ by have [j [Dj BiBj ij]] := maxD i Vi; move/(_ _ cBix) => ?; exists j. Qed. End vitali_lemma_infinite. + +Section set_itv_realType. +Variable R : realType. +Implicit Types x : R. + +Lemma set_itvK : {in neitv, cancel pred_set (@Rhull R)}. +Proof. +move=> [[[] x|[]] [[] y|[]]] /neitvP //; + rewrite /Rhull /= !(in_itv, inE)/= ?bnd_simp => xy. +- rewrite asboolT// inf_itv// lexx/= xy asboolT// asboolT//=. + by rewrite asboolF//= sup_itv//= ltxx ?andbF. +- by rewrite asboolT// inf_itv// ?asboolT// ?sup_itv// ?lexx ?xy. +- by rewrite asboolT//= inf_itv// lexx asboolT// asboolF. +- rewrite asboolT// inf_itv//= ltxx asboolF// asboolT//. + by rewrite sup_itv// ltxx andbF asboolF. + rewrite asboolT // inf_itv // ltxx asboolF // asboolT //. + by rewrite sup_itv // xy lexx asboolT. +- by rewrite asboolT // inf_itv// ltxx asboolF // asboolF. +- by rewrite asboolF // asboolT // sup_itv// ltxx asboolF. +- by rewrite asboolF // asboolT // sup_itv// lexx asboolT. +- by rewrite asboolF // asboolF. +Qed. + +Lemma RhullT : Rhull setT = `]-oo, +oo[%R :> interval R. +Proof. by rewrite /Rhull -set_itv_infty_infty asboolF// asboolF. Qed. + +Lemma RhullK : {in (@is_interval _ : set (set R)), cancel (@Rhull R) pred_set}. +Proof. by move=> X /asboolP iX; apply/esym/is_intervalP. Qed. + +Lemma set_itv_setT (i : interval R) : [set` i] = setT -> i = `]-oo, +oo[. +Proof. +have [i0 /(congr1 (@Rhull _))|] := boolP (neitv i). + by rewrite set_itvK// => ->; exact: RhullT. +by rewrite negbK => /eqP ->; rewrite predeqE => /(_ 0)[_]/(_ Logic.I). +Qed. + +End set_itv_realType. + +Section Rhull_lemmas. +Variable R : realType. +Implicit Types (a b t r : R) (A : set R). + +Lemma Rhull_smallest A : [set` Rhull A] = smallest (@is_interval R) A. +Proof. +apply/seteqP; split; last first. + by apply: smallest_sub; [apply: interval_is_interval | apply: sub_Rhull]. +move=> x /= + I [Iitv AI]; rewrite /Rhull. +have [|] := asboolP (has_lbound A) => lA; last first. + have /forallNP/(_ x)/existsNP[a] := lA. + move=> /existsNP[Aa /negP]; rewrite -ltNge => ax. + have [|]:= asboolP (has_ubound A) => uA; last first. + move=> ?; have /forallNP/(_ x)/existsNP[b] := uA. + move=> /existsNP[Ab /negP]; rewrite -ltNge => xb. + have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. + by rewrite ax xb. + have [As|NAs]/= := asboolP (A _) => xA. + by apply: (Iitv a (sup A)); by [apply: AI | rewrite ltW ?ax]. + have [||b Ab xb] := @sup_gt _ A x; do ?by [exists a | rewrite (itvP xA)]. + have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. + by rewrite ax xb. +have [|]:= asboolP (has_ubound A) => uA; last first. + have /forallNP/(_ x)/existsNP[b] := uA. + move=> /existsNP[Ab /negP]; rewrite -ltNge => xb. + have [Ai|NAi]/= := asboolP (A _) => xA. + by apply: (Iitv (inf A) b); by [apply: AI | rewrite (ltW xb)]. + have [||a Aa ax] := @inf_lt _ A x; do ?by [exists b | rewrite (itvP xA)]. + have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. + by rewrite ax xb. +have [Ai|NAi]/= := asboolP (A _); have [As|NAs]/= := asboolP (A _). +- by apply: Iitv; apply: AI. +- move=> xA. + have [||b Ab xb] := @sup_gt _ A x; do ?by [exists (inf A) | rewrite (itvP xA)]. + have /(_ (inf A) b) := Iitv; apply; do ?by apply: AI. + by rewrite (itvP xA) (ltW xb). +- move=> xA. + have [||a Aa ax] := @inf_lt _ A x; do ?by [exists (sup A) | rewrite (itvP xA)]. + have /(_ a (sup A)) := Iitv; apply; do ?by apply: AI. + by rewrite (itvP xA) (ltW ax). +have [->|/set0P AN0] := eqVneq A set0. + by rewrite inf0 sup0 itv_ge//= ltBSide/= ltxx. +move=> xA. +have [||a Aa ax] := @inf_lt _ A x; do ?by [|rewrite (itvP xA)]. +have [||b Ab xb] := @sup_gt _ A x; do ?by [|rewrite (itvP xA)]. +have /is_intervalPlt/(_ a b) := Iitv; apply; do ?by apply: AI. +by rewrite ax xb. +Qed. + +Lemma le_Rhull : {homo (@Rhull R) : A B / (A `<=` B) >-> {subset A <= B}}. +Proof. +move=> A B AB; suff: [set` Rhull A] `<=` [set` Rhull B] by []. +rewrite Rhull_smallest; apply: smallest_sub; first exact: interval_is_interval. +by rewrite Rhull_smallest; apply: sub_smallest. +Qed. + +Lemma neitv_Rhull A : ~~ neitv (Rhull A) -> A = set0. +Proof. +move/negPn/eqP => A0; rewrite predeqE => r; split => // /sub_Rhull. +by rewrite A0. +Qed. + +Lemma Rhull_involutive A : Rhull [set` Rhull A] = Rhull A. +Proof. +have [A0|/neitv_Rhull] := boolP (neitv (Rhull A)); first by rewrite set_itvK. +by move=> ->; rewrite ?Rhull0 set_itvE Rhull0. +Qed. + +End Rhull_lemmas. + +Lemma disj_itv_Rhull {R : realType} (A B : set R) : A `&` B = set0 -> + is_interval A -> is_interval B -> disjoint_itv (Rhull A) (Rhull B). +Proof. +by move=> AB0 iA iB; rewrite /disjoint_itv RhullK ?inE// RhullK ?inE. +Qed. diff --git a/theories/showcase/summability.v b/theories/showcase/summability.v index 9892dd9c9e..dae60a5b90 100644 --- a/theories/showcase/summability.v +++ b/theories/showcase/summability.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From Coq Require Reals. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. From mathcomp Require Import interval zmodp. From mathcomp Require Import boolp classical_sets. -From mathcomp Require Import ereal reals Rstruct signed topology normedtype. +From mathcomp Require Import ereal reals signed topology normedtype. (**md**************************************************************************) (* This file proposes a replacement for the definition `summable` (file *)