Move basic definitions and lemmas about Z to mczify

README.md

@@ -2,7 +2,7 @@
 This file was generated from `meta.yml`, please do not edit manually.
 Follow the instructions on https://github.com/coq-community/templates to regenerate.
 --->
-# Algebra-tactics
+# Algebra Tactics
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
@@ -12,8 +12,13 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 
 
-This library provides experimental `ring` and `field` tactics for
-`comRingType` and `fieldType` instances of Mathematical Components.
+This library provides `ring` and `field` tactics for Mathematical Components,
+that work with any `comRingType`s and `fieldType`s, respectively. Their
+instance resolution is done through canonical structure inference. Therefore,
+they work with abstract rings and do not require `Add Ring` and `Add Field`
+commands. Another key feature of this library is that they automatically push
+down ring morphisms to leaves of ring and field expressions before
+normalization to the Horner form.
 
 ## Meta
 
@@ -23,14 +28,14 @@ This library provides experimental `ring` and `field` tactics for
 - Compatible Coq versions: 8.13 or later
 - Additional dependencies:
   - [MathComp](https://math-comp.github.io) 1.12.0 or later
-  - [Mczify](https://github.com/math-comp/mczify) 1.0.0 or later
+  - [Mczify](https://github.com/math-comp/mczify) 1.1.0 or later
   - [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.10.1 or later
 - Coq namespace: `mathcomp.algebra_tactics`
 - Related publication(s): none
 
 ## Building and installation instructions
 
-The easiest way to install the latest released version of Algebra-tactics
+The easiest way to install the latest released version of Algebra Tactics
 is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
@@ -48,4 +53,8 @@ make install
 ```
 
 
-
+## Credits
+The way we adapt internals of Coq's `ring` and `field` tactics to algebraic
+structures of the Mathematical Components library is inspired by the
+[elliptic-curves-ssr](https://github.com/strub/elliptic-curves-ssr) library by
+Evmorfia-Iro Bartzia and Pierre-Yves Strub.

coq-mathcomp-algebra-tactics.opam

@@ -10,17 +10,22 @@ dev-repo: "git+https://github.com/math-comp/algebra-tactics.git"
 bug-reports: "https://github.com/math-comp/algebra-tactics/issues"
 license: "CECILL-B"
 
-synopsis: "Experimental reflexive tactics for ring and field expressions"
+synopsis: "Reflexive ring and field tactics for Mathematical Components"
 description: """
-This library provides experimental `ring` and `field` tactics for
-`comRingType` and `fieldType` instances of Mathematical Components."""
+This library provides `ring` and `field` tactics for Mathematical Components,
+that work with any `comRingType`s and `fieldType`s, respectively. Their
+instance resolution is done through canonical structure inference. Therefore,
+they work with abstract rings and do not require `Add Ring` and `Add Field`
+commands. Another key feature of this library is that they automatically push
+down ring morphisms to leaves of ring and field expressions before
+normalization to the Horner form."""
 
 build: [make "-j%{jobs}%" ]
 install: [make "install"]
 depends: [
   "coq" {(>= "8.13" & < "8.15~") | (= "dev")}
   "coq-mathcomp-algebra" {(>= "1.12" & < "1.13~") | (= "dev")}
-  "coq-mathcomp-zify" {(>= "1.0.0") | (= "dev")}
+  "coq-mathcomp-zify" {(>= "1.1.0") | (= "dev")}
   "coq-elpi" {(>= "1.10.1") | (= "dev")}
 ]
 

meta.yml

@@ -1,16 +1,21 @@
 ---
-fullname: Algebra-tactics
+fullname: Algebra Tactics
 shortname: algebra-tactics
 opam_name: coq-mathcomp-algebra-tactics
 organization: math-comp
 action: true
 
 synopsis: >-
-  Experimental reflexive tactics for ring and field expressions
+  Reflexive ring and field tactics for Mathematical Components
 
 description: |-
-  This library provides experimental `ring` and `field` tactics for
-  `comRingType` and `fieldType` instances of Mathematical Components.
+  This library provides `ring` and `field` tactics for Mathematical Components,
+  that work with any `comRingType`s and `fieldType`s, respectively. Their
+  instance resolution is done through canonical structure inference. Therefore,
+  they work with abstract rings and do not require `Add Ring` and `Add Field`
+  commands. Another key feature of this library is that they automatically push
+  down ring morphisms to leaves of ring and field expressions before
+  normalization to the Horner form.
 
 authors:
 - name: Kazuhiko Sakaguchi
@@ -47,14 +52,22 @@ dependencies:
     [MathComp](https://math-comp.github.io) 1.12.0 or later
 - opam:
     name: coq-mathcomp-zify
-    version: '{(>= "1.0.0") | (= "dev")}'
+    version: '{(>= "1.1.0") | (= "dev")}'
   description: |-
-    [Mczify](https://github.com/math-comp/mczify) 1.0.0 or later
+    [Mczify](https://github.com/math-comp/mczify) 1.1.0 or later
 - opam:
     name: coq-elpi
     version: '{(>= "1.10.1") | (= "dev")}'
   description: |-
     [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.10.1 or later
 
 namespace: mathcomp.algebra_tactics
+
+documentation: |-
+  ## Credits
+  The way we adapt internals of Coq's `ring` and `field` tactics to algebraic
+  structures of the Mathematical Components library is inspired by the
+  [elliptic-curves-ssr](https://github.com/strub/elliptic-curves-ssr) library by
+  Evmorfia-Iro Bartzia and Pierre-Yves Strub.
+
 ---

theories/ring.v

@@ -2,7 +2,7 @@ From Coq Require Import ZArith ZifyClasses Ring Ring_polynom Field_theory.
 From elpi Require Export elpi.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint rat.
-From mathcomp Require Import zify.
+From mathcomp Require Import zify ssrZ.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -12,109 +12,48 @@ Import GRing.Theory.
 
 Local Open Scope ring_scope.
 
-Definition int_of_Z (n : Z) : int :=
-  match n with
-  | Z0 => Posz 0
-  | Zpos p => Posz (Pos.to_nat p)
-  | Zneg p => Negz (Pos.to_nat p).-1
-  end.
-
-Definition Z_of_int (n : int) : Z :=
-  match n with
-  | Posz n => Z.of_nat n
-  | Negz n' => Z.opp (Z.of_nat (n' + 1))
-  end.
-
-Lemma int_of_ZK : cancel int_of_Z Z_of_int.
-Proof. by case=> //= p; lia. Qed.
-
-Instance Op_int_of_Z : UnOp int_of_Z := { TUOp := id; TUOpInj := int_of_ZK }.
-Add Zify UnOp Op_int_of_Z.
-
-Instance Op_Z_of_int : UnOp Z_of_int := { TUOp := id; TUOpInj := fun => erefl }.
-Add Zify UnOp Op_Z_of_int.
-
-Lemma Z_of_intK : cancel Z_of_int int_of_Z.
-Proof. by move=> ?; lia. Qed.
-
-(* The following proofs are based on ones in elliptic-curves-ssr:             *)
-(* https://github.com/strub/elliptic-curves-ssr/blob/631af893e591466207929714c45b5f7476d579d0/common/ssrring.v *)
-
-Lemma Z_eqP : Equality.axiom Z.eqb.
-Proof. by move=> x y; apply: (iffP idP); lia. Qed.
-
-Canonical Z_eqType := EqType Z (EqMixin Z_eqP).
-Canonical Z_choiceType := ChoiceType Z (CanChoiceMixin int_of_ZK).
-Canonical Z_countType := CountType Z (CanCountMixin int_of_ZK).
-
-Definition Z_zmodMixin :=
-  ZmodMixin Zplus_assoc Zplus_comm Zplus_0_l Zplus_opp_l.
-Canonical Z_zmodType := ZmodType Z Z_zmodMixin.
-
-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.
-
-Module Import AuxLemmas.
+Module Import Internals.
 
 Implicit Types (R : ringType) (F : fieldType).
 
-Section Ring.
-
-Variable (R : ringType).
-
-Let R_of_Z (n : Z) : R := (int_of_Z n)%:~R.
-
-Lemma R_of_Z_is_additive : additive R_of_Z.
-Proof. by move=> x y; rewrite -mulrzBr /+%R /-%R /=; congr intmul; lia. Qed.
-
-Local Canonical R_of_Z_additive := Additive R_of_Z_is_additive.
-
-Lemma R_of_Z_is_multiplicative : multiplicative R_of_Z.
-Proof. by split=> //= x y; rewrite -intrM /*%R /=; congr intmul; lia. Qed.
-
-Local Canonical R_of_Z_rmorphism := AddRMorphism R_of_Z_is_multiplicative.
-
-Lemma RE : @ring_eq_ext R +%R *%R -%R eq.
+Lemma RE R : @ring_eq_ext R +%R *%R -%R eq.
 Proof. by split; do! move=> ? _ <-. Qed.
 
-Lemma RZ : ring_morph 0 1 +%R *%R (fun x y => x - y) -%R eq
-                      0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool R_of_Z.
+Lemma RZ R : ring_morph 0 1 +%R *%R (fun x y : R => x - y) -%R eq
+                        0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb
+                        (fun n => (int_of_Z n)%:~R).
 Proof.
-by split=> //=;
-  [ exact: rmorphD | exact: rmorphB | exact: rmorphM | exact: raddfN
-  | by move=> x y /Zeq_bool_eq -> ].
+split=> //= [x y | x y | x y | x | x y /Z.eqb_eq -> //].
+- by rewrite !rmorphD.
+- by rewrite !rmorphB.
+- by rewrite !rmorphM.
+- by rewrite !rmorphN.
 Qed.
 
-Lemma PN : @power_theory R 1 *%R eq nat nat_of_N (@GRing.exp R).
+Lemma PN R : @power_theory R 1 *%R eq nat nat_of_N (@GRing.exp R).
 Proof.
 by split=> r [] //=; elim=> //= p <-;
   rewrite (Pos2Nat.inj_xI, Pos2Nat.inj_xO) ?exprS -exprD addnn -mul2n.
 Qed.
 
-End Ring.
-
 Lemma RR (R : comRingType) :
   @ring_theory R 0 1 +%R *%R (fun x y => x - y) -%R eq.
 Proof.
 exact/mk_rt/subrr/(fun _ _ => erefl)/mulrDl/mulrA/mulrC/mul1r/addrA/addrC/add0r.
 Qed.
 
-Lemma RF (F : fieldType) :
-  @field_theory
-    F 0 1 +%R *%R (fun x y => x - y) -%R (fun x y => x / y) GRing.inv eq.
+Lemma RF F : @field_theory F 0 1 +%R *%R (fun x y => x - y) -%R
+                           (fun x y => x / y) GRing.inv eq.
 Proof.
-by split => //= [||x /eqP];
-  [exact: RR | apply/eqP; rewrite oner_eq0 | exact: mulVf].
+by split=> // [||x /eqP]; [exact: RR | exact/eqP/oner_neq0 | exact: mulVf].
 Qed.
 
 Definition Rcorrect (R : comRingType) :=
   ring_correct
     (Eqsth R) (RE R) (Rth_ARth (Eqsth R) (RE R) (RR R)) (RZ R) (PN R)
     (triv_div_th (Eqsth R) (RE R) (Rth_ARth (Eqsth R) (RE R) (RR R)) (RZ R)).
 
-Definition Fcorrect (F : fieldType) :=
+Definition Fcorrect F :=
   Field_correct
     (Eqsth F) (RE F) (congr1 GRing.inv)
     (F2AF (Eqsth F) (RE F) (RF F)) (RZ F) (PN F)
@@ -259,7 +198,7 @@ elim: {R} e F f => //=.
   by rewrite -[Negz _]intz rmorph_int /intmul mulrS NEeval_correct.
 Qed.
 
-End AuxLemmas.
+End Internals.
 
 Register Coq.Init.Logic.eq       as ring.eq.
 Register Coq.Init.Logic.eq_refl  as ring.erefl.