From 1499da1063b72f689dcc6b974cac26cb88129c0e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 5 May 2022 15:22:27 +0200 Subject: [PATCH] Port to MathComp 2.0 --- .github/workflows/docker-action.yml | 22 +------ README.md | 4 +- coq-mathcomp-zify.opam | 4 +- meta.yml | 48 ++------------ theories/ssrZ.v | 99 +++++++++++------------------ theories/zify_algebra.v | 7 +- theories/zify_ssreflect.v | 2 +- 7 files changed, 53 insertions(+), 133 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 78597c9..f5a14b3 100644 --- a/.github/workflows/docker-action.yml +++ b/.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' diff --git a/README.md b/README.md index 342b9c5..ca1f6ab 100644 --- a/README.md +++ b/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 diff --git a/coq-mathcomp-zify.opam b/coq-mathcomp-zify.opam index 90e2371..e46251a 100644 --- a/coq-mathcomp-zify.opam +++ b/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" ] diff --git a/meta.yml b/meta.yml index cf78ccd..e5eebbf 100644 --- a/meta.yml +++ b/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: |- diff --git a/theories/ssrZ.v b/theories/ssrZ.v index 38d30ee..d14c6b5 100644 --- a/theories/ssrZ.v +++ b/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. diff --git a/theories/zify_algebra.v b/theories/zify_algebra.v index 20f3b4f..6aad53f 100644 --- a/theories/zify_algebra.v +++ b/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. diff --git a/theories/zify_ssreflect.v b/theories/zify_ssreflect.v index 9db8601..de0bbdd 100644 --- a/theories/zify_ssreflect.v +++ b/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.