math-comp · CohenCyril · Oct 3, 2023
diff --git a/.nix/coq-overlays/mathcomp-analysis/default.nix b/.nix/coq-overlays/mathcomp-analysis/default.nix
@@ -0,0 +1,90 @@
+{ lib,
+  mkCoqDerivation, recurseIntoAttrs,
+  mathcomp, mathcomp-finmap, mathcomp-bigenough,
+  hierarchy-builder, mathcomp-real-closed,
+  single ? false,
+  coqPackages, coq, version ? null }@args:
+with builtins // lib;
+let
+  repo  = "analysis";
+  owner = "math-comp";
+
+  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 = with versions; lib.switch [ coq.version mathcomp.version ]  [
+      { cases = [ (isGe "8.14") (isGe "1.13.0") ];               out = "0.6.1"; }
+      { cases = [ (isGe "8.14") (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" "analysis" ];
+
+  mathcomp_ = package: let
+      classical-deps = [ mathcomp.algebra mathcomp-finmap ];
+      analysis-deps = [ mathcomp.field mathcomp-bigenough mathcomp-real-closed ];
+      intra-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages)));
+      pkgpath = if package == "single" then "."
+        else if package == "analysis" then "theories" else "${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
+          ++ optionals (elem package [ "classical" "single" ]) classical-deps
+          ++ optionals (elem package [ "analysis" "single" ]) analysis-deps;
+
+        preBuild = ''
+          cd ${pkgpath}
+        '';
+
+        meta = {
+          description = "Analysis library compatible with Mathematical Components";
+          maintainers = [ maintainers.cohencyril ];
+          license     = licenses.cecill-c;
+        };
+
+        passthru = genAttrs packages mathcomp_;
+      });
+    # split packages didn't exist before 0.6, so bulding nothing in that case
+    patched-derivation1 = derivation.overrideAttrs (o:
+      optionalAttrs (o.pname != null && o.pname != "mathcomp-analysis" &&
+         o.version != null && o.version != "dev" && versions.isLt "0.6" o.version)
+      { preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; }
+    );
+    patched-derivation2 = patched-derivation1.overrideAttrs (o:
+      optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" &&
+         o.version != null && o.version != "dev" && versions.isLt "0.6" o.version)
+      { preBuild = ""; }
+    );
+    patched-derivation = patched-derivation2.overrideAttrs (o:
+      optionalAttrs (o.version != null
+        && (o.version == "dev" || 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/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam
@@ -22,6 +22,7 @@ depends: [
   "coq-mathcomp-solvable" { (>= "1.15.0" & < "1.18~") | (= "dev") }
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
+  "coq-mathcomp-real-closed" { (>= "1.4.0") }
 ]
 
 tags: [

diff --git a/theories/misc/ereal_num_nbhs_nbhs.v b/theories/misc/ereal_num_nbhs_nbhs.v
@@ -0,0 +1,55 @@
+Require Import Reals.
+From mathcomp Require Import all_ssreflect all_algebra finmap.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import fsbigop cardinality set_interval.
+From mathcomp Require Import Rstruct complex.
+Require Import constructive_ereal reals signed topology normedtype ereal.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import Order.TTheory GRing.Theory Num.Theory.
+Import numFieldTopology.Exports.
+
+Local Open Scope ring_scope.
+Local Open Scope ereal_scope.
+Local Open Scope classical_set_scope.
+
+Lemma ereal_nbhs_pinftyE (R : numFieldType) (A : set (\bar R)) :
+   (\forall k \near +oo%E, A k) = (A +oo%E /\ \forall k \near +oo%R, A k%:E).
+Proof.
+apply/propeqP; split; last first.
+  by move=> [Ay [M [Mreal AM]]]; exists M; split=> // -[r | |]//; apply: AM.
+move=> [M [Mreal AM]]; split; first exact: AM.
+by exists M; split=> // y My; apply: AM.
+Qed.
+
+Definition C := R[i].
+
+Lemma ereal_nbhs_nbhs :
+  ereal_nbhs +oo (`](0 : \bar C), +oo]%classic) /\
+  ~ ereal_nbhs +oo (ereal_nbhs^~ `](0 : \bar C), +oo]%classic).
+Proof.
+have [i Ni_eq1 iNreal] : (exists2 i : C, (`|i| = 1)%R & i \isn't Num.real).
+  by exists 'i; rewrite ?normCi// nonRealCi.
+have NiV2_lt1 : (`|i / 2| < 1)%R.
+  by rewrite normf_div Ni_eq1 gtr0_norm// mul1r invf_lt1// ltr_addl.
+rewrite ![ereal_nbhs _ _]ereal_nbhs_pinftyE.
+split.
+  split=> //=; first by rewrite in_itv/= lt0y lexx.
+  exists 0%R; split=> // x x_gt0; rewrite in_itv//= lte_fin x_gt0//=.
+  by rewrite real_leey/= gtr0_real.
+move=> [_ [M [Mreal]]]/(_ (M + 1)%R _)[]; first by rewrite ltr_addl.
+move=> x /= x_gt0/=.
+have x_neq0 : x != 0%R by rewrite gt_eqF.
+have x_real: x \is Num.real by rewrite gtr0_real.
+move=> /(_ (M + 1 + x * (i / 2))%R) /=.
+rewrite opprD addNKr normrN normrM gtr0_norm//.
+rewrite -ltr_pdivl_mull// mulVf ?gt_eqF// => /(_ NiV2_lt1).
+suff: (M + 1 + x * (i / 2))%R \isn't Num.real.
+  apply: contraNnot; move: (_ + _)%R => y.
+  by rewrite in_itv/= => /andP[/gtr0_real].
+rewrite rpredDl/=; last by rewrite rpredD// rpred1.
+by rewrite fpredMl//= fpred_divr// rpred_nat.
+Qed.