Merge pull request #1721 from proux01/mc1469

Adapt to math-comp/math-comp#1469

Author: proux01

.github/workflows/nix-action-8.20-2.3.0.yml

@@ -52,11 +52,6 @@ in {
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
 
-  bundles."8.20-2.3.0".coqPackages = common-bundle // {
-    coq.override.version = "8.20";
-    mathcomp.override.version = "2.3.0";
-  };
-
   bundles."8.20-2.4.0".coqPackages = common-bundle // {
     coq.override.version = "8.20";
     mathcomp.override.version = "2.4.0";

.nix/config.nix

@@ -80,6 +80,11 @@
 
 ### Removed
 
+- file `interval_inference.v` (now in MathComp)
+
+- in file `all_reals.v`
+  + export of `interval_inference` (now in mathcomp-algebra, but not automatically exported)
+
 ### Infrastructure
 
 ### Misc

CHANGELOG_UNRELEASED.md

@@ -3,7 +3,7 @@
 ## Requirements
 
 - [The Coq Proof Assistant version ≥ 8.20 / Rocq Prover version ≥ 9.0](https://rocq-prover.org)
-- [Mathematical Components version ≥ 2.3.0](https://github.com/math-comp/math-comp)
+- [Mathematical Components version ≥ 2.4.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 2.1.0](https://github.com/math-comp/finmap)
 - [Hierarchy builder version ≥ 1.8.0](https://github.com/math-comp/hierarchy-builder)
 - [bigenough ≥ 1.0.0](https://github.com/math-comp/bigenough)
@@ -73,7 +73,7 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
 
-With the example of Coq 8.20.1 and MathComp 2.3.0. For other versions, update the
+With the example of Coq 8.20.1 and MathComp 2.4.0. For other versions, update the
 version numbers accordingly.
 
 1. Install Coq 8.20.1
@@ -82,11 +82,11 @@ $ opam install coq.8.20.1
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.2.3.0
-$ opam install coq-mathcomp-fingroup.2.3.0
-$ opam install coq-mathcomp-algebra.2.3.0
-$ opam install coq-mathcomp-solvable.2.3.0
-$ opam install coq-mathcomp-field.2.3.0
+$ opam install coq-mathcomp-ssreflect.2.4.0
+$ opam install coq-mathcomp-fingroup.2.4.0
+$ opam install coq-mathcomp-algebra.2.4.0
+$ opam install coq-mathcomp-solvable.2.4.0
+$ opam install coq-mathcomp-field.2.4.0
 ```
 3. Install the Finite maps library
 ```

INSTALL.md

@@ -45,25 +45,6 @@ all: config build
 .PHONY: pre-makefile
 
 Makefile.coq: pre-makefile $(COQPROJECT) Makefile
-	(echo "From mathcomp.algebra Require Import interval_inference." > test_interval_inference.v \
-	 && ($(COQC) test_interval_inference.v > /dev/null 2>&1) \
-	 && test -f interval_inference.v -o -f reals/interval_inference.v \
-	 && touch rm_interval_inference) || true
-	$(RM) test_interval_inference.v
-	test -f rm_interval_inference \
-	  && sed -i.bak '/interval_inference/ d' $(COQPROJECT) \
-	  && $(RM) $(COQPROJECT).bak || true
-	test -f rm_interval_inference \
-	  && sed -i.bak '/interval_inference/ d' all_reals.v \
-	  && $(RM) all_reals.v.bak || true
-	test -f rm_interval_inference \
-	  && sed -i.bak '/interval_inference/ d' reals/all_reals.v \
-	  && $(RM) reals/all_reals.v.bak || true
-	test -f rm_interval_inference && $(RM) interval_inference.v || true
-	test -f rm_interval_inference && $(RM) reals/interval_inference.v || true
-	$(RM) rm_interval_inference
-	# Remove everything above when requiring mathcomp >= 2.4.0
-	# (also remove file reals/interval_inference.v and references to it)
 	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
 
 # Global config, build, clean and distclean --------------------------
@@ -142,6 +123,5 @@ html: build $(DOCDIR)/dependency_graph.dot
 	-hierarchy-graph $(DOCDIR)/hierarchy_graph.dot \
         -index-blacklist etc/rocqnavi_index-blacklist \
         -show-type-information-using-coqtop-process \
-	-external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect \
-	-external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra
-
+	-external https://math-comp.github.io/htmldoc_2_4_0/ mathcomp.ssreflect \
+	-external https://math-comp.github.io/htmldoc_2_4_0/ mathcomp.algebra

Makefile.common

@@ -26,11 +26,11 @@ In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the fol
 - License: [CeCILL-C](LICENSE)
 - Compatible Rocq versions: Coq 8.20, Rocq 9.0 (or dev)
 - Additional dependencies:
-  - [MathComp ssreflect 2.3.0 or later](https://math-comp.github.io)
-  - [MathComp fingroup 2.3.0 or later](https://math-comp.github.io)
-  - [MathComp algebra 2.3.0 or later](https://math-comp.github.io)
-  - [MathComp solvable 2.3.0 or later](https://math-comp.github.io)
-  - [MathComp field 2.3.0 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.4.0 or later](https://math-comp.github.io)
+  - [MathComp fingroup 2.4.0 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.4.0 or later](https://math-comp.github.io)
+  - [MathComp solvable 2.4.0 or later](https://math-comp.github.io)
+  - [MathComp field 2.4.0 or later](https://math-comp.github.io)
   - [MathComp finmap 2.1.0](https://github.com/math-comp/finmap)
   - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough)
   - [Hierarchy Builder 1.8.0 or later](https://github.com/math-comp/hierarchy-builder)

README.md

@@ -30,7 +30,6 @@ reals/constructive_ereal.v
 reals/reals.v
 reals/real_interval.v
 reals/signed.v
-reals/interval_inference.v
 reals/prodnormedzmodule.v
 reals/all_reals.v
 experimental_reals/xfinmap.v

_CoqProject

@@ -147,22 +147,22 @@ Context {R : archiDomainType}.
 Implicit Type x : R.
 
 Lemma ge_floor x : (Num.floor x)%:~R <= x.
-Proof. exact: Num.Theory.ge_floor. Qed.
+Proof. exact: Num.Theory.floor_le_tmp. Qed.
 
 #[deprecated(since="mathcomp 2.4.0", note="Use floor_ge_int_tmp instead.")]
 Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x).
-Proof. exact: Num.Theory.floor_ge_int. Qed.
+Proof. by rewrite floor_ge_int_tmp. Qed.
 
 Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
 Proof. exact: Num.Theory.lt_succ_floor. Qed.
 
 #[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.le_ceil` instead")]
 Lemma ceil_ge x : x <= (Num.ceil x)%:~R.
-Proof. exact: Num.Theory.le_ceil. Qed.
+Proof. exact: Num.Theory.ceil_ge. Qed.
 
 #[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.ceil_le_int`")]
 Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z).
-Proof. exact: Num.Theory.ceil_le_int. Qed.
+Proof. by rewrite Num.Theory.ceil_le_int_tmp. Qed.
 
 Lemma ceilN x : Num.ceil (- x) = - Num.floor x.
 Proof. by rewrite ?ceilNfloor /Num.ceil opprK. Qed.
@@ -331,7 +331,7 @@ by move=> ?; rewrite [RHS]real_ltNge ?realz -?real_floor_ge_int_tmp -?ltNge.
 Qed.
 
 Lemma le_floor : {homo (@Num.floor R) : x y / x <= y}.
-Proof. exact: floor_le. Qed.
+Proof. exact: le_floor. Qed.
 
 Lemma real_floor_eq x n : x \is Num.real ->
   (Num.floor x == n) = (n%:~R <= x < (n + 1)%:~R).
@@ -392,7 +392,7 @@ by move=> xr; apply/eqP/idP => [<-|]; [exact: real_ceil_itv|exact: ceil_def].
 Qed.
 
 Lemma le_ceil_tmp : {homo (@Num.ceil R) : x y / x <= y}.
-Proof. exact: ceil_le. Qed.
+Proof. exact: le_ceil_tmp. Qed.
 
 Lemma real_ceil_ge0 x : x \is Num.real -> (0 <= Num.ceil x) = (-1 < x).
 Proof.

classical/mathcomp_extra.v

@@ -363,7 +363,7 @@ Implicit Type x : R.
 Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R.
 Proof.
 rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x.
-  by rewrite !gtr0_norm ?ceil_gt0// (le_trans (Num.Theory.le_ceil _))// lerDl.
+  by rewrite !gtr0_norm ?ceil_gt0// (le_trans (Num.Theory.ceil_ge _))// lerDl.
 by rewrite !ler0_norm ?ceil_le0// ?ceilNfloor opprK intrD1 ltW// floorD1_gt.
 Qed.
 

classical/unstable.v

@@ -17,7 +17,7 @@ install: [make "-C" "classical" "install"]
 depends: [
   ("coq" {>= "8.20" & < "8.21~"}
   | "coq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
-  "coq-mathcomp-ssreflect" { (>= "2.3.0" & < "2.5~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
   "coq-mathcomp-finmap" { (>= "2.1.0") }