Port to MathComp 2.0

.github/workflows/docker-action.yml

@@ -17,26 +17,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
-          - 'mathcomp/mathcomp-dev:coq-8.13'
-          - 'mathcomp/mathcomp-dev:coq-8.14'
-          - 'mathcomp/mathcomp-dev:coq-8.15'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-8.16'
           - 'mathcomp/mathcomp-dev:coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-dev'

README.md

@@ -21,9 +21,9 @@ by extending the zify tactic.
 - Author(s):
   - Kazuhiko Sakaguchi (initial)
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
-- Compatible Coq versions: 8.13 or later
+- Compatible Coq versions: 8.16 or later
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) ssreflect 1.12 or later
+  - [MathComp](https://math-comp.github.io) ssreflect 2.0 or later
   - [MathComp](https://math-comp.github.io) algebra
 - Coq namespace: `mathcomp.zify`
 - Related publication(s): none

coq-mathcomp-zify.opam

@@ -19,8 +19,8 @@ by extending the zify tactic."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.13"}
-  "coq-mathcomp-ssreflect" {>= "1.12"}
+  "coq" {>= "8.16"}
+  "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-mathcomp-algebra" 
 ]
 

meta.yml

@@ -25,52 +25,16 @@ license:
   file: CeCILL-B
 
 supported_coq_versions:
-  text: 8.13 or later
-  opam: '{>= "8.13"}'
+  text: 8.16 or later
+  opam: '{>= "8.16"}'
 
 tested_coq_nix_versions:
 
 tested_coq_opam_versions:
-- version: '1.12.0-coq-8.13'
+- version: '2.0.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.14'
+- version: '2.0.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: 'coq-8.13'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.14'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.15'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.16'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.17'
@@ -81,9 +45,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.12"}'
+    version: '{>= "2.0"}'
   description: |-
-    [MathComp](https://math-comp.github.io) ssreflect 1.12 or later
+    [MathComp](https://math-comp.github.io) ssreflect 2.0 or later
 - opam:
     name: coq-mathcomp-algebra
   description: |-

theories/ssrZ.v

@@ -1,5 +1,6 @@
 From Coq Require Import ZArith.
 
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype tuple finfun bigop finset prime.
 From mathcomp Require Import order binomial ssralg countalg ssrnum ssrint.
@@ -41,19 +42,19 @@ Implicit Types (m n : Z).
 Fact eqZP : Equality.axiom Z.eqb.
 Proof. by move=> x y; apply: (iffP idP); lia. Qed.
 
-Canonical Z_eqType := EqType Z (EqMixin eqZP).
-Canonical Z_choiceType := ChoiceType Z (CanChoiceMixin int_of_ZK).
-Canonical Z_countType := CountType Z (CanCountMixin int_of_ZK).
+#[export]
+HB.instance Definition _ := hasDecEq.Build Z eqZP.
 
-Definition Z_zmodMixin :=
-  ZmodMixin Zplus_assoc Zplus_comm Zplus_0_l Zplus_opp_l.
-Canonical Z_zmodType := ZmodType Z Z_zmodMixin.
+#[export]
+HB.instance Definition _ := Countable.copy Z (can_type int_of_ZK).
 
-Definition Z_ringMixin :=
-  RingMixin
-    Zmult_assoc Zmult_1_l Zmult_1_r Zmult_plus_distr_l Zmult_plus_distr_r isT.
-Canonical Z_ringType := RingType Z Z_ringMixin.
-Canonical Z_comRingType := ComRingType Z Zmult_comm.
+#[export]
+HB.instance Definition _ := GRing.isZmodule.Build Z
+  Zplus_assoc Zplus_comm Zplus_0_l Zplus_opp_l.
+
+#[export]
+HB.instance Definition _ := GRing.Zmodule_isComRing.Build Z
+  Zmult_assoc Zmult_comm Zmult_1_l Zmult_plus_distr_l isT.
 
 Definition unitZ := [qualify a n : Z | (n == Z.pos xH) || (n == Z.neg xH)].
 Definition invZ n := n.
@@ -67,20 +68,15 @@ Proof. case: m n => [|[m|m|]|[m|m|]] [|n|n] //= []; lia. Qed.
 Fact invZ_out : {in [predC unitZ], invZ =1 id}.
 Proof. exact. Qed.
 
+#[export]
+HB.instance Definition _ := GRing.ComRing_hasMulInverse.Build Z
+  mulVZ unitZPl invZ_out.
+
 Fact idomain_axiomZ m n : (m * n = 0)%R -> (m == 0%R) || (n == 0%R).
 Proof. by case: m n => [|m|m] []. Qed.
 
-Canonical Z_unitRingType :=
-  UnitRingType Z (ComUnitRingMixin mulVZ unitZPl invZ_out).
-Canonical Z_comUnitRing := [comUnitRingType of Z].
-Canonical Z_idomainType := IdomainType Z idomain_axiomZ.
-
-Canonical Z_countZmodType := [countZmodType of Z].
-Canonical Z_countRingType := [countRingType of Z].
-Canonical Z_countComRingType := [countComRingType of Z].
-Canonical Z_countUnitRingType := [countUnitRingType of Z].
-Canonical Z_countComUnitRingType := [countComUnitRingType of Z].
-Canonical Z_countIdomainType := [countIdomainType of Z].
+#[export]
+HB.instance Definition _ := GRing.ComUnitRing_isIntegral.Build Z idomain_axiomZ.
 
 Fact leZ_add m n : Z.leb 0 m -> Z.leb 0 n -> Z.leb 0 (m + n). Proof. lia. Qed.
 Fact leZ_mul m n : Z.leb 0 m -> Z.leb 0 n -> Z.leb 0 (m * n). Proof. lia. Qed.
@@ -98,17 +94,9 @@ Fact geZ0_norm m : Z.leb 0 m -> Z.abs m = m. Proof. lia. Qed.
 Fact ltZ_def m n : (Z.ltb m n) = (n != m) && (Z.leb m n).
 Proof. by rewrite eqE /=; lia. Qed.
 
-Definition Mixin : realLeMixin [idomainType of Z] :=
-  RealLeMixin
-    leZ_add leZ_mul leZ_anti subZ_ge0 (leZ_total 0) normZN geZ0_norm ltZ_def.
-
-Canonical Z_porderType := POrderType ring_display Z Mixin.
-Canonical Z_latticeType := LatticeType Z Mixin.
-Canonical Z_distrLatticeType := DistrLatticeType Z Mixin.
-Canonical Z_orderType := OrderType Z leZ_total.
-Canonical Z_numDomainType := NumDomainType Z Mixin.
-Canonical Z_normedZmodType := NormedZmodType Z Z Mixin.
-Canonical Z_realDomainType := [realDomainType of Z].
+#[export]
+HB.instance Definition _ := Num.IntegralDomain_isLeReal.Build Z
+  leZ_add leZ_mul leZ_anti subZ_ge0 (leZ_total 0) normZN geZ0_norm ltZ_def.
 
 Fact Z_of_intE (n : int) : Z_of_int n = (n%:~R)%R.
 Proof.
@@ -121,48 +109,33 @@ Qed.
 Fact Z_of_int_is_additive : additive Z_of_int.
 Proof. by move=> m n; rewrite !Z_of_intE raddfB. Qed.
 
-Canonical Z_of_int_additive := Additive Z_of_int_is_additive.
+#[export]
+HB.instance Definition _ := GRing.isAdditive.Build int Z Z_of_int
+  Z_of_int_is_additive.
 
 Fact int_of_Z_is_additive : additive int_of_Z.
 Proof. exact: can2_additive Z_of_intK int_of_ZK. Qed.
 
-Canonical int_of_Z_additive := Additive int_of_Z_is_additive.
+#[export]
+HB.instance Definition _ := GRing.isAdditive.Build Z int int_of_Z
+  int_of_Z_is_additive.
 
 Fact Z_of_int_is_multiplicative : multiplicative Z_of_int.
 Proof. by split => // n m; rewrite !Z_of_intE rmorphM. Qed.
 
-Canonical Z_of_int_rmorphism := AddRMorphism Z_of_int_is_multiplicative.
+#[export]
+HB.instance Definition _ := GRing.isMultiplicative.Build int Z Z_of_int
+  Z_of_int_is_multiplicative.
 
 Fact int_of_Z_is_multiplicative : multiplicative int_of_Z.
 Proof. exact: can2_rmorphism Z_of_intK int_of_ZK. Qed.
 
-Canonical int_of_Z_rmorphism := AddRMorphism int_of_Z_is_multiplicative.
+#[export]
+HB.instance Definition _ := GRing.isMultiplicative.Build Z int int_of_Z
+  int_of_Z_is_multiplicative.
+
+Module Exports. HB.reexport. End Exports.
 
 End ZInstances.
 
-Canonical ZInstances.Z_eqType.
-Canonical ZInstances.Z_choiceType.
-Canonical ZInstances.Z_countType.
-Canonical ZInstances.Z_zmodType.
-Canonical ZInstances.Z_ringType.
-Canonical ZInstances.Z_comRingType.
-Canonical ZInstances.Z_unitRingType.
-Canonical ZInstances.Z_comUnitRing.
-Canonical ZInstances.Z_idomainType.
-Canonical ZInstances.Z_countZmodType.
-Canonical ZInstances.Z_countRingType.
-Canonical ZInstances.Z_countComRingType.
-Canonical ZInstances.Z_countUnitRingType.
-Canonical ZInstances.Z_countComUnitRingType.
-Canonical ZInstances.Z_countIdomainType.
-Canonical ZInstances.Z_porderType.
-Canonical ZInstances.Z_latticeType.
-Canonical ZInstances.Z_distrLatticeType.
-Canonical ZInstances.Z_orderType.
-Canonical ZInstances.Z_numDomainType.
-Canonical ZInstances.Z_normedZmodType.
-Canonical ZInstances.Z_realDomainType.
-Canonical ZInstances.Z_of_int_additive.
-Canonical ZInstances.int_of_Z_additive.
-Canonical ZInstances.Z_of_int_rmorphism.
-Canonical ZInstances.int_of_Z_rmorphism.
+Export ZInstances.Exports.

theories/zify_algebra.v

@@ -49,7 +49,7 @@ Instance Op_int_eq : BinRel (@eq int) :=
 Add Zify BinRel Op_int_eq.
 
 #[global]
-Instance Op_int_eq_op : BinOp (@eq_op int_eqType : int -> int -> bool) :=
+Instance Op_int_eq_op : BinOp (@eq_op int : int -> int -> bool) :=
   { TBOp := Z.eqb;
     TBOpInj := ltac:(move=> [] ? [] ?; do 2 rewrite eqE /=; lia) }.
 Add Zify BinOp Op_int_eq_op.
@@ -98,7 +98,7 @@ Instance Op_int_intmul : BinOp ( *~%R%R : int -> int -> int) :=
 Add Zify BinOp Op_int_intmul.
 
 #[global]
-Instance Op_int_scale : BinOp (@GRing.scale _ [lmodType int of int^o]) :=
+Instance Op_int_scale : BinOp (@GRing.scale _ int^o) :=
   Op_mulz.
 Add Zify BinOp Op_int_scale.
 
@@ -274,7 +274,8 @@ Instance Op_Z_intmul : BinOp ( *~%R%R : Z -> int -> Z) :=
 Add Zify BinOp Op_Z_intmul.
 
 #[global]
-Instance Op_Z_scale : BinOp (@GRing.scale _ [lmodType Z of Z^o]) := Op_Z_mulr.
+Instance Op_Z_scale : BinOp (@GRing.scale _ Z^o) :=
+  Op_Z_mulr.
 Add Zify BinOp Op_Z_scale.
 
 Fact Op_Z_exp_subproof n m : (n ^+ m)%R = (n ^ Z.of_nat m)%Z.

theories/zify_ssreflect.v

@@ -133,7 +133,7 @@ Instance Op_bool_top' : CstOp (Order.bottom : bool^d) := Op_true.
 Add Zify CstOp Op_bool_top'.
 
 #[global]
-Instance Op_bool_sub : BinOp (Order.sub : bool -> bool -> bool) :=
+Instance Op_bool_sub : BinOp (Order.diff : bool -> bool -> bool) :=
   { TBOp x y := x && ~~ y; TBOpInj := ltac:(by case=> [][]) }.
 Add Zify BinOp Op_bool_sub.