mathcomp 2.1

.github/workflows/docker-action.yml

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

README.md

@@ -64,15 +64,15 @@ A note about sorting network is available [here](https://hal.inria.fr/hal-035856
 - 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:
   - [ Hierarchy Builder 1.6.0 or later](https://github.com/math-comp/hierarchy-builder)
-  - [MathComp ssreflect 2.0.0 or later](https://math-comp.github.io)
-  - [MathComp fingroup 2.0.0 or later](https://math-comp.github.io)
-  - [MathComp algebra 2.0.0 or later](https://math-comp.github.io)
-  - [MathComp field 2.0.0 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io)
+  - [MathComp fingroup 2.1.0 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.1.0 or later](https://math-comp.github.io)
+  - [MathComp field 2.1.0 or later](https://math-comp.github.io)
   - [MathComp zify 1.5.0+2.0+8.16 or later](https://github.com/math-comp/mczify)
-  - [MathComp Algebra Tactics 1.2.1 or later](https://github.com/math-comp/algebra-tactics)
+  - [MathComp Algebra Tactics 1.2.2 or later](https://github.com/math-comp/algebra-tactics)
 - Coq namespace: `mathcomp-extra`
 - Related publication(s): none
 

_CoqProject

@@ -9,8 +9,6 @@ matroid.v
 rsa.v
 aks_algo.v
 aks.v
-qpoly.v
-qfpoly.v
 more_thm.v
 rootn.v
 bgcdn.v

aks.v

@@ -1,7 +1,7 @@
 From mathcomp Require Import all_ssreflect all_fingroup all_field.
-From mathcomp Require Import ssralg finalg poly polydiv zmodp vector.
+From mathcomp Require Import ssralg finalg poly polydiv zmodp vector qpoly.
 From mathcomp Require cyclic.
-Require Import more_thm rootn qpoly qfpoly lcm_lbound.
+Require Import more_thm rootn lcm_lbound.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -60,16 +60,16 @@ have XmD1 : 'X^m.+1 != 1 :> {poly R}.
 case: k => [|k mIp nIp].
   rewrite /introspective !subrr !rmodp0 exprM => /eqP->.
   rewrite comp_poly_exp => /eqP->.
-  by rewrite -comp_polyA comp_polyXn -exprM.
+  by rewrite -comp_polyA comp_Xn_poly -exprM.
 have XM : ('X^k.+1 - 1 : {poly R}) \is monic.
   rewrite qualifE /= lead_coefDl ?lead_coefXn ?unitr1 //.
   by rewrite size_polyXn size_opp size_polyC oner_neq0.
 rewrite /introspective exprM -rmodpX // (eqP mIp) rmodpX //.
-rewrite exprM -['X^m.+1 ^+_]comp_polyXn comp_poly_exp comp_polyA.
+rewrite exprM -['X^m.+1 ^+_]comp_Xn_poly comp_poly_exp comp_polyA.
 rewrite -subr_eq0 -rmodpB // -comp_polyB.
 apply: rdvdp_trans (_ : rdvdp (('X^k.+1 -1) \Po 'X^m.+1) _) => //.
 - by apply: monic_comp_poly => //; rewrite qualifE /= lead_coefXn.
-- rewrite comp_polyB comp_polyXn comp_polyC -exprM mulnC exprM.
+- rewrite comp_polyB comp_Xn_poly comp_polyC -exprM mulnC exprM.
   by apply: dvdp_geom.
 apply: rdvdp_comp_poly => //; first by rewrite qualifE /= lead_coefXn.
 by rewrite /rdvdp rmodpB // subr_eq0.
@@ -109,13 +109,13 @@ have kNZ : k%:R != 0 :> F.
 have pCF : [char {poly F}].-nat p.
   rewrite /pnat prime_gt0 //=; apply/allP => q.
   rewrite primes_prime //= inE => /eqP->.
-  rewrite inE pP -poly_natmul polyC_eq0 /=.
+  rewrite inE pP -polyC_natr polyC_eq0 /=.
   by case/andP : pC.
 rewrite -subr_eq0 -modpN -modpD -[_ == 0]/(_ %| _).
 rewrite -(separable_exp _ (separable_polyXnsub1 _) (prime_gt0 pP)) //.
 rewrite exprDn_char // exprNn_char // -exprM divnK //.
 rewrite comp_polyD comp_polyC [_ ^+ p]exprDn_char //.
-rewrite comp_poly_exp comp_polyXn -exprM divnK //.
+rewrite comp_poly_exp comp_Xn_poly -exprM divnK //.
 rewrite -polyC_exp fin_little_fermat //.
 rewrite /dvdp modpD modpN subr_eq0 //.
 move: nIkX.
@@ -654,7 +654,7 @@ apply/val_inj; rewrite /= /mk_monic !hMI //= -[RHS](rmod0p h).
 pose z : {poly F}:= 'X^k - 1.
 have zM : z \is monic by apply: monic_Xn_sub_1.
 apply: rmodn_trans hDxk1 _; rewrite ?hMI -/z // rmod0p.
-rewrite comp_polyB !comp_polyXn rmodpB //.
+rewrite comp_polyB !comp_Xn_poly rmodpB //.
 apply/eqP; rewrite subr_eq0; apply/eqP.
 have F0 : rmodp 'X^k z = 1.
   rewrite -['X^k](subrK 1) rmodpD // rmodpp // add0r rmodp_small //.
@@ -1469,7 +1469,7 @@ congr (_ + _).
 rewrite -mulr_algr -Zp_nat scaler_nat.
 rewrite rmodp_small // size_Xn_sub_1 //.
 apply: leq_trans (size_mul_leq _ _) _.
-rewrite -poly_natmul size_polyC.
+rewrite -polyC_natr size_polyC.
 apply: leq_trans (size_PolyZ n k v1).
 case: eqP=> _; first by rewrite addn0 leq_pred.
 by rewrite addn1.
@@ -1504,7 +1504,7 @@ Lemma poly_modnp_pow n k p v : 0 < k -> 1 < n ->
     rmodp (PolyZ n k v ^+ Pos.to_nat p) ('X^k - 1).
 Proof.
 move=> k_gt0 n_gt1 sv2E.
-have xnM := monic_Xn_sub_1 [ringType of 'Z_n] k_gt0.
+have xnM := monic_Xn_sub_1 (GRing.Ring.clone _ 'Z_n) k_gt0.
 elim: p => [p1 IH|p1 IH|] /=; last first.
 - by rewrite expr1 rmodp_small // size_Xn_sub_1 // ltnS size_PolyZ.
 - rewrite poly_modnp_mul ?size_modnp_pow //= IH.

batcher.v

@@ -95,7 +95,7 @@ Lemma sorted_nfun_batcher_merge_rec m (t : (`2^ m.+1).-tuple bool) :
 Proof.
 elim: m t => [t tS dS|m IH t tS dS /=].
   rewrite [batcher_merge_rec_aux 0]/= tsorted2 /=.
-  by rewrite cswapE_min // cswapE_max // le_minl le_maxr lexx.
+  by rewrite cswapE_min // cswapE_max // ge_min le_max lexx.
 rewrite nfun_rcons nfun_eodup.
 set n1 := nfun _ _; set n2 := nfun _ _.
 have n1P : perm_eq n1 (tetake t) by apply: perm_nfun.

coq-mathcomp-extra.opam

@@ -62,14 +62,14 @@ A note about sorting network is available [here](https://hal.inria.fr/hal-035856
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.17")}
+  "coq" {(>= "8.18")}
   "coq-hierarchy-builder" {(>= "1.6.0")}
-  "coq-mathcomp-ssreflect" {(>= "2.0.0")}
-  "coq-mathcomp-fingroup" {(>= "2.0.0")}
-  "coq-mathcomp-algebra" {(>= "2.0.0")}
-  "coq-mathcomp-field" {(>= "2.0.0")}
+  "coq-mathcomp-ssreflect" {(>= "2.1.0")}
+  "coq-mathcomp-fingroup" {(>= "2.1.0")}
+  "coq-mathcomp-algebra" {(>= "2.1.0")}
+  "coq-mathcomp-field" {(>= "2.1.0")}
   "coq-mathcomp-zify" {(>= "1.5.0+2.0+8.16")}
-  "coq-mathcomp-algebra-tactics" {(>= "1.2.1")}
+  "coq-mathcomp-algebra-tactics" {(>= "1.2.2")}
 ]
 
 tags: [

elliptic.v

@@ -1071,7 +1071,7 @@ Qed.
 (******************************************************************************)
 
 Definition elt_enum := 
-  pmap (elt_g A B) (enum [finType of option (K * K)%type]).
+  pmap (elt_g A B) (enum (Finite.clone _ (option (K * K)%type))).
 
 Lemma elt_enum_uniq : uniq elt_enum.
 Proof.
@@ -1094,7 +1094,7 @@ HB.instance Definition _ := Countable.copy (elt A B)
 HB.instance Definition _ := isFinite.Build (elt A B)
   (Finite.uniq_enumP elt_enum_uniq mem_elt_enum).
 
-Lemma card_elt : (#|[finType of elt A B]| <= #|K|.*2.+1)%N.
+Lemma card_elt : (#|(Finite.clone _ (elt A B))| <= #|K|.*2.+1)%N.
 Proof.
 rewrite !cardT.
 pose ff b x := if Kroot (x ^+ 3 +  A * x + B) is Some y 

fft.v

@@ -26,11 +26,11 @@ Unset Printing Implicit Defensive.
 
 Import GRing.Theory Num.Theory Order.POrderTheory Num.ExtraDef Num.
 
-
 Section FFT.
 
 Local Open Scope ring_scope.
 
+Notation nat := Datatypes.nat.
 (* Arbitary idomain                                                           *)
 (* In fact  it works for an arbitray ring. We ask for idomain in order to use *)
 (* primitive-root and sqr_eqf1                                                *)

iterative.v

@@ -17,6 +17,8 @@ Variable R : ringType.
 
 Implicit Type p : {poly R}.
 
+Local Notation nat := Datatypes.nat.
+
 Variable left : nat -> {poly R} -> {poly R}.
 Variable right : nat -> {poly R} -> {poly R}.
 Variable merge : nat -> {poly R} -> {poly R} -> {poly R}.

meta.yml

@@ -70,8 +70,8 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: '8.17 or later'
-  opam: '{(>= "8.17")}'
+  text: '8.18 or later'
+  opam: '{(>= "8.18")}'
 
 dependencies:
 - opam:
@@ -81,37 +81,37 @@ dependencies:
     [ Hierarchy Builder 1.6.0 or later](https://github.com/math-comp/hierarchy-builder)
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.0.0")}'
+    version: '{(>= "2.1.0")}'
   description: |-
-    [MathComp ssreflect 2.0.0 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{(>= "2.0.0")}'
+    version: '{(>= "2.1.0")}'
   description: |-
-    [MathComp fingroup 2.0.0 or later](https://math-comp.github.io)
+    [MathComp fingroup 2.1.0 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{(>= "2.0.0")}'
+    version: '{(>= "2.1.0")}'
   description: |-
-    [MathComp algebra 2.0.0 or later](https://math-comp.github.io)
+    [MathComp algebra 2.1.0 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{(>= "2.0.0")}'
+    version: '{(>= "2.1.0")}'
   description: |-
-    [MathComp field 2.0.0 or later](https://math-comp.github.io)
+    [MathComp field 2.1.0 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-zify
     version: '{(>= "1.5.0+2.0+8.16")}'
   description: |-
     [MathComp zify 1.5.0+2.0+8.16 or later](https://github.com/math-comp/mczify)
 - opam:
     name: coq-mathcomp-algebra-tactics
-    version: '{(>= "1.2.1")}'
+    version: '{(>= "1.2.2")}'
   description: |-
-    [MathComp Algebra Tactics 1.2.1 or later](https://github.com/math-comp/algebra-tactics)
+    [MathComp Algebra Tactics 1.2.2 or later](https://github.com/math-comp/algebra-tactics)
 
 tested_coq_opam_versions:
-- version: '2.0.0-coq-8.18'
+- version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 
 namespace: mathcomp-extra