Port to MathComp 2

.github/workflows/docker-action.yml

@@ -17,10 +17,13 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
+          - 'mathcomp/mathcomp-dev:coq-8.16'
+          - 'mathcomp/mathcomp-dev:coq-8.17'
+          - 'mathcomp/mathcomp-dev:coq-8.18'
+          - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

README.md

@@ -41,16 +41,16 @@ remains the sole trusted code base.
   - Assia Mahboubi ([**@amahboubi**](https://github.com/amahboubi))
   - Kazuhiko Sakaguchi ([**@pi8027**](https://github.com/pi8027))
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: 8.15 or later
+- Compatible Coq versions: 8.16 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp field](https://math-comp.github.io)
-  - [CoqEAL 1.1.3 or later](https://github.com/coq-community/coqeal)
-  - [MathComp real closed fields 1.1.4 or later](https://github.com/math-comp/real-closed)
+  - [CoqEAL 2.0.0 or later](https://github.com/coq-community/coqeal)
+  - [MathComp real closed fields 2.0.0 or later](https://github.com/math-comp/real-closed)
   - [MathComp bigenough 1.0.1 or later](https://github.com/math-comp/bigenough)
-  - [Mczify](https://github.com/math-comp/mczify) 1.3.0 or later
-  - [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.0.0 or later
+  - [Mczify](https://github.com/math-comp/mczify) 1.5.0 or later
+  - [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.2.0 or later
 - Coq namespace: `mathcomp.apery`
 - Related publication(s):
   - [A Formal Proof of the Irrationality of ζ(3)](https://arxiv.org/abs/1912.06611) 

coq-mathcomp-apery.opam

@@ -23,15 +23,15 @@ remains the sole trusted code base."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.15" & < "8.19~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {>= "1.17" & < "1.18~"}
+  "coq" {(>= "8.16" & < "8.19~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.1~") | (= "dev")}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field" 
-  "coq-coqeal" {>= "1.1.3" & < "2~"}
-  "coq-mathcomp-real-closed" {>= "1.1.4" & < "2~"}
+  "coq-coqeal" {>= "2.0.0"}
+  "coq-mathcomp-real-closed" {>= "2.0.0"}
   "coq-mathcomp-bigenough" {>= "1.0.1"}
-  "coq-mathcomp-zify" {>= "1.3.0" & < "1.14~"}
-  "coq-mathcomp-algebra-tactics" {>= "1.0.0" & < "1.2~"}
+  "coq-mathcomp-zify" {>= "1.5.0"}
+  "coq-mathcomp-algebra-tactics" {>= "1.2.0"}
 ]
 
 tags: [

meta.yml

@@ -51,25 +51,31 @@ license:
   identifier: CECILL-C
 
 supported_coq_versions:
-  text: 8.15 or later
-  opam: '{(>= "8.15" & < "8.19~") | (= "dev")}'
+  text: 8.16 or later
+  opam: '{(>= "8.16" & < "8.19~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: '1.17.0-coq-8.15'
+- version: '2.0.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.16'
+- version: '2.0.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.18'
+- version: '2.0.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
+- version: 'coq-8.16'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.17'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.18'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-dev'
+  repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.17" & < "1.18~"}'
+    version: '{(>= "2.0" & < "2.1~") | (= "dev")}'
   description: |-
-    [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-
@@ -80,29 +86,29 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-coqeal
-    version: '{>= "1.1.3" & < "2~"}'
+    version: '{>= "2.0.0"}'
   description: |-
-    [CoqEAL 1.1.3 or later](https://github.com/coq-community/coqeal)
+    [CoqEAL 2.0.0 or later](https://github.com/coq-community/coqeal)
 - opam:
     name: coq-mathcomp-real-closed
-    version: '{>= "1.1.4" & < "2~"}'
+    version: '{>= "2.0.0"}'
   description: |-
-    [MathComp real closed fields 1.1.4 or later](https://github.com/math-comp/real-closed)
+    [MathComp real closed fields 2.0.0 or later](https://github.com/math-comp/real-closed)
 - opam:
     name: coq-mathcomp-bigenough
     version: '{>= "1.0.1"}'
   description: |-
     [MathComp bigenough 1.0.1 or later](https://github.com/math-comp/bigenough)
 - opam:
     name: coq-mathcomp-zify
-    version: '{>= "1.3.0" & < "1.14~"}'
+    version: '{>= "1.5.0"}'
   description: |-
-    [Mczify](https://github.com/math-comp/mczify) 1.3.0 or later
+    [Mczify](https://github.com/math-comp/mczify) 1.5.0 or later
 - opam:
     name: coq-mathcomp-algebra-tactics
-    version: '{>= "1.0.0" & < "1.2~"}'
+    version: '{>= "1.2.0"}'
   description: |-
-    [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.0.0 or later
+    [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.2.0 or later
 
 namespace: mathcomp.apery
 

theories/floor.v

@@ -59,8 +59,7 @@ Proof.
 apply/floorQ_unique; move: (floorQ_spec q) (floorQ_spec (q / m.+1%:Q)).
 rewrite !ler_pdivlMr ?ltr_pdivrMr ?ltr0z // intrD -intrM ler_int.
 move=> /andP[_ Hq] /andP[Hdiv /le_lt_trans ->] //.
-rewrite -ltzD1 -(ltr_int [numDomainType of rat]) intrD.
-by rewrite (le_lt_trans Hdiv).
+by rewrite -ltzD1 -(ltr_int rat) intrD (le_lt_trans Hdiv).
 Qed.
 
 (* Lemma floorQ_div_pos (q : rat) (m : nat) :  *)

theories/hanson.v

@@ -540,7 +540,7 @@ suff [K [Kpos KP]] : exists K : rat,
   suff: (C n m.+1)%:R <= (k%:Q + 1) * 3%:R ^ n.
     by rewrite -[_ + 1%:R]natrD -[_ ^ n]natrX -natrM ler_nat addn1.
   exact/le_trans/ler_wpM2r/ltW/leKSn/exprz_ge0.
-move mE: 10%:Q => m.
+move mE: 10%N%:Q => m. (* FIXME *)
 have lt0m : 0 < m by rewrite -mE.
 have le0m : 0 <= m by exact: ltW.
 have lt1m : 1 < m by rewrite -mE.

theories/rat_of_Z.v

@@ -1,3 +1,4 @@
+From HB Require Import structures.
 Require Import ZArith.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.zify Require Export ssrZ.
@@ -45,12 +46,14 @@
 Fact rat_of_Z_is_additive : additive rat_of_Z.
 Proof. by move=> m n; rewrite rat_of_ZEdef !raddfB. Qed.
 
-Canonical rat_of_Z_additive := Additive rat_of_Z_is_additive.
+HB.instance Definition _ :=
+  GRing.isAdditive.Build Z rat rat_of_Z rat_of_Z_is_additive.
 
 Fact rat_of_Z_is_multiplicative : multiplicative rat_of_Z.
-Proof. by rewrite rat_of_ZEdef; exact: rmorphismMP [rmorphism of _ \o _]. Qed.
+Proof. by rewrite rat_of_ZEdef; exact: rmorphismMP (_ \o _). Qed.
 
-Canonical rat_of_Z_rmorphism := AddRMorphism rat_of_Z_is_multiplicative.
+HB.instance Definition _ :=
+  GRing.isMultiplicative.Build Z rat rat_of_Z rat_of_Z_is_multiplicative.
 
 Lemma zify_rat_of_Z_subproof n : rat_of_Z n = (int_of_Z n)%:~R.
 Proof. by rewrite rat_of_ZEdef. Qed.

theories/tactics.v

@@ -83,8 +83,8 @@ Proof. by rewrite 2!zifyRingE ltr_int. Qed.
 
 End Internals.
 
-Lemma rpred_zify (R : ringType) (S : {pred R}) (ringS : subringPred S)
-                 (kS : keyed_pred ringS) (e : zifyRing R) : rval e \in kS.
+Lemma rpred_zify (R : ringType) (S : subringClosed R) (e : zifyRing R) :
+  rval e \in S.
 Proof. by rewrite zifyRingE rpred_int. Qed.
 
 Canonical zify_zero.

theories/z3irrational.v

@@ -76,7 +76,7 @@ Qed.
 
 (* Actual definition of \zeta(3) as a Cauchy real, i.e. the equivalence class *)
 (* of the sequence z3seq for Cauchy equivalence. *)
-Definition z3 : creal rat_realFieldType := CReal creal_z3seq.
+Definition z3 : creal rat := CReal creal_z3seq.
 
 (* We prove that the sequences z3seq and b / a are asymptotically close. *)
 Lemma z3seq_b_over_a_asympt : {asympt e : i / `|z3seq i - b_over_a_seq i| < e}.
@@ -267,8 +267,7 @@ pose_big_enough M.
     - apply/lt_creal_cst; apply: mulr_gt0; first exact: lt_0_Kdelta.
       apply: divr_gt0; last by apply: exprn_gt0; rewrite ltr0n.
       rewrite invr_gt0; exact: lt_0_Ka.
-    - apply/lt_creal_cst; rewrite ltrXn2r //; first exact: ltW.
-      apply: hanson; raise_big_enough.
+    - by apply/lt_creal_cst/ltrXn2r/hanson => //; raise_big_enough.
     - apply: lecr_lt_trans (NdeltaP _) _; first by raise_big_enough.
       apply/lt_creal_cst; rewrite ltr_pM2l; last exact: lt_0_Kdelta.
       apply: a_asympt; raise_big_enough.