mathcomp 2.1

.github/workflows/docker-action.yml

@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

README.md

@@ -11,8 +11,6 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 
 
-
-
 A proof of Fermat's theorem on sum of two squares.
 It is the proof that uses gaussian integers. This is done in ssreflect.
 It contains two files :
@@ -43,11 +41,11 @@ reflect
 - Author(s):
   - Laurent Théry
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.17 or later
+- Compatible Coq versions: 8.18 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
-  - [MathComp algebra 1.17 or later](https://math-comp.github.io)
-  - [MathComp field 1.17 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.1 or later](https://math-comp.github.io)
+  - [MathComp field 2.1 or later](https://math-comp.github.io)
 - Coq namespace: `twoSquare`
 - Related publication(s): none
 

coq-twoSquare.opam

@@ -41,10 +41,10 @@ reflect
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.17")}
-  "coq-mathcomp-ssreflect" {(>= "1.17.0")}
-  "coq-mathcomp-algebra" {(>= "1.17.0")}
-  "coq-mathcomp-field" {(>= "1.17.0")}
+  "coq" {(>= "8.18")}
+  "coq-mathcomp-ssreflect" {(>= "2.1.0")}
+  "coq-mathcomp-algebra" {(>= "2.1.0")}
+  "coq-mathcomp-field" {(>= "2.1.0")}
 ]
 
 tags: [

fermat2.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra all_field.
+From mathcomp Require Import all_ssreflect all_algebra all_field archimedean.
 Require Import gauss_int.
 
 Set Implicit Arguments.
@@ -51,8 +51,8 @@ Proof.
 apply: (iffP idP) => [/sum2sP[m [n ->]]|[x1->]].
 exists (m%:R + iGI * n%:R)%R.
   by rewrite normGIE /= !algGI_nat Re_rect ?Im_rect 
-             ?CrealE ?conjC_nat ?natCK // !normr_nat !natCK.
-rewrite normGIE; set m := truncC _; set n := truncC _.
+             ?CrealE ?conjC_nat ?natrK // !normr_nat !natrK.
+rewrite normGIE; set m := Num.trunc _; set n := Num.trunc _.
 by apply/sum2sP; exists m; exists n.
 Qed.
 
@@ -84,7 +84,7 @@ have PGIp : primeGI (p%:R).
 pose z := (a%:R + iGI * b%:R)%R.
 have F : ('N z)%GI = a ^ 2 + b ^ 2.
   by rewrite normGIE /= !algGI_nat !(Re_rect, Im_rect)
-            ?Creal_Cnat // !normr_nat !natCK.
+            ?Rreal_nat // !normr_nat !natrK.
 have F1 : (p%:R %| z * conjGI z)%GI%R.
   rewrite conjGIM_norm F.
   case/dvdnP: pDab => q1 ->.
@@ -94,20 +94,20 @@ have []: ~ (p %| gcdn a b).
 rewrite dvdn_gcd.
 have [F2|] := boolP (p%:R %| z)%GI.
   have := dvdGI_nat_dvdz_Re F2.
-  rewrite Re_rect /= algGI_nat ?Creal_Cnat //=
-           (intCK (Posz a)) /= => ->.
+  rewrite Re_rect /= algGI_nat ?Rreal_nat //=
+           (intrKfloor (Posz a)) /= => ->.
   have := dvdGI_nat_dvdz_Im F2.
-  by rewrite Im_rect /= algGI_nat ?Creal_Cnat //=
-           (intCK (Posz b)).
+  by rewrite Im_rect /= algGI_nat ?Rreal_nat //=
+           (intrKfloor (Posz b)).
 rewrite -primeGI_coprime // => HH.
 have F2 : (p%:R %| conjGI z)%GI.
   by rewrite -(Gauss_dvdGIr _ HH).
 have := dvdGI_nat_dvdz_Re F2.
-rewrite Re_conj Re_rect /= algGI_nat ?Creal_Cnat //=
-           (intCK (Posz a)) => ->.
+rewrite Re_conj Re_rect /= algGI_nat ?Rreal_nat //=
+           (intrKfloor (Posz a)) => ->.
 have := dvdGI_nat_dvdz_Im F2.
-rewrite Im_conj Im_rect /= algGI_nat ?Creal_Cnat //=.
-by rewrite floorCN ?Cint_Cnat // abszN (intCK (Posz b)).
+rewrite Im_conj Im_rect /= algGI_nat ?Rreal_nat //=.
+by rewrite floorN ?intr_nat // abszN (intrKfloor (Posz b)).
 Qed.
 
 Lemma sum2sX x n :