diff --git a/README.md b/README.md index f72652d..25fde42 100644 --- a/README.md +++ b/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. diff --git a/coq-mathcomp-algebra-tactics.opam b/coq-mathcomp-algebra-tactics.opam index c6d95dc..b88830c 100644 --- a/coq-mathcomp-algebra-tactics.opam +++ b/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")} ] diff --git a/meta.yml b/meta.yml index cf535b9..6dd6d49 100644 --- a/meta.yml +++ b/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,9 +52,9 @@ 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")}' @@ -57,4 +62,12 @@ dependencies: [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. + --- diff --git a/theories/ring.v b/theories/ring.v index c0f9126..4c573d7 100644 --- a/theories/ring.v +++ b/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,101 +12,40 @@ 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) := @@ -114,7 +53,7 @@ Definition Rcorrect (R : comRingType) := (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.