From 4c7f27095f401893bf1b091ed39ffaf6fd299044 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sun, 3 Oct 2021 20:03:21 +0900 Subject: [PATCH 1/2] Simplify non-zero conditions of the field tactic --- examples/field_examples.v | 8 ++--- theories/ring.v | 63 +++++++++++++++++++++++++++++++-------- 2 files changed, 55 insertions(+), 16 deletions(-) diff --git a/examples/field_examples.v b/examples/field_examples.v index 1c42c49..a8708c7 100644 --- a/examples/field_examples.v +++ b/examples/field_examples.v @@ -14,14 +14,14 @@ Local Open Scope ring_scope. (abstract) field. *) Goal forall (F : fieldType) (x : F), x != 0 -> (1 - 1 / x) * x - x + 1 = 0. -Proof. by move=> F x x_neq0; field; exact/eqP. Qed. +Proof. by move=> F x x_neq0; field. Qed. Goal forall (F F' : fieldType) (f : {rmorphism F -> F'}) (x : F), f x != 0 -> f ((1 - 1 / x) * x - x + 1) = 0. -Proof. by move=> F F' f x x_neq0; field; exact/eqP. Qed. +Proof. by move=> F F' f x x_neq0; field. Qed. Goal forall (F : fieldType) (x y : F), y != 0 -> y = x -> x / y = 1. -Proof. by move=> F x y y_neq0; field; exact/eqP. Qed. +Proof. by move=> F x y y_neq0; field. Qed. Goal forall (F : fieldType) (x y : F), y != 0 -> y = 1 -> x = 1 -> x / y = 1. -Proof. by move=> F x y y_neq0; field; exact/eqP. Qed. +Proof. by move=> F x y y_neq0; field. Qed. diff --git a/theories/ring.v b/theories/ring.v index 0f96eb8..4d3b380 100644 --- a/theories/ring.v +++ b/theories/ring.v @@ -267,6 +267,57 @@ move: F f; elim e using (@RingExpr_ind' P P0); rewrite {R e}/P {}/P0 //=. - by move=> V V' g e1 IHe1 F f; rewrite -IHe1. Qed. +Lemma lock_PCond (F : fieldType) (l : seq F) (le : seq (PExpr Z)) : + (forall zero one add mul sub opp Feq R_of_int exp, + zero = 0 -> one = 1 -> add = +%R -> mul = *%R -> sub = (fun x y => x - y) -> + opp = -%R -> Feq = eq -> R_of_int = intmul 1 -> exp = @GRing.exp F -> + Field_theory.PCond + zero one add mul sub opp Feq + (fun n : Z => R_of_int (int_of_Z n)) N.to_nat exp l le) -> + Field_theory.PCond + 0 1 +%R *%R (fun x y => x - y) -%R eq + (fun n : Z => (int_of_Z n)%:~R) N.to_nat (@GRing.exp F) l le. +Proof. exact. Qed. + +Ltac ring_reflection RMcorrect1 RMcorrect2 Rcorrect := + apply: (eq_trans RMcorrect1); + apply: (eq_trans _ (esym RMcorrect2)); + apply: Rcorrect; + [vm_compute; reflexivity]. + +Ltac simpl_PCond := + let zero := fresh "zero" in + let one := fresh "one" in + let add := fresh "add" in + let mul := fresh "mul" in + let sub := fresh "sub" in + let opp := fresh "opp" in + let Feq := fresh "Feq" in + let R_of_int := fresh "R_of_int" in + let exp := fresh "exp" in + let zeroE := fresh "zeroE" in + let oneE := fresh "oneE" in + let addE := fresh "addE" in + let mulE := fresh "mulE" in + let subE := fresh "subE" in + let oppE := fresh "oppE" in + let FeqE := fresh "FeqE" in + let R_of_intE := fresh "R_of_intE" in + let expE := fresh "expE" in + apply: Internals.lock_PCond; + move=> zero one add mul sub opp Feq R_of_int exp; + move=> zeroE oneE addE mulE subE oppE FeqE R_of_intE expE; + vm_compute; + rewrite ?{zero}zeroE ?{one}oneE ?{add}addE ?{mul}mulE ?{sub}subE ?{opp}oppE; + rewrite ?{Feq}FeqE ?{R_of_int}R_of_intE ?{exp}expE; + do ?split; apply/eqP. + +Ltac field_reflection FMcorrect1 FMcorrect2 Fcorrect := + apply: (eq_trans FMcorrect1); + apply: (eq_trans _ (esym FMcorrect2)); + apply: Fcorrect; [reflexivity | reflexivity | reflexivity | + vm_compute; reflexivity | simpl_PCond]. + End Internals. Register Coq.Init.Logic.eq as ring.eq. @@ -279,12 +330,6 @@ Elpi Accumulate File "theories/quote.elpi". Elpi Accumulate File "theories/ring.elpi". Elpi Typecheck. -Ltac ring_reflection RMcorrect1 RMcorrect2 Rcorrect := - apply: (eq_trans RMcorrect1); - apply: (eq_trans _ (esym RMcorrect2)); - apply: Rcorrect; - [vm_compute; reflexivity]. - Tactic Notation "ring" := elpi ring. Tactic Notation "ring" ":" ne_constr_list(L) := elpi ring ltac_term_list:(L). @@ -293,11 +338,5 @@ Elpi Accumulate File "theories/quote.elpi". Elpi Accumulate File "theories/field.elpi". Elpi Typecheck. -Ltac field_reflection FMcorrect1 FMcorrect2 Fcorrect := - apply: (eq_trans FMcorrect1); - apply: (eq_trans _ (esym FMcorrect2)); - apply: Fcorrect; [reflexivity | reflexivity | reflexivity | - vm_compute; reflexivity | simpl]. - Tactic Notation "field" := elpi field. Tactic Notation "field" ":" ne_constr_list(L) := elpi field ltac_term_list:(L). From 5c1a241b239c07c47cc28193bbb9a9ec7dc5c9cf Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sun, 3 Oct 2021 20:21:32 +0900 Subject: [PATCH 2/2] Update doc --- README.md | 16 ++++++++-------- coq-mathcomp-algebra-tactics.opam | 14 +++++++------- meta.yml | 18 +++++++++--------- 3 files changed, 24 insertions(+), 24 deletions(-) diff --git a/README.md b/README.md index 25fde42..abb3c5c 100644 --- a/README.md +++ b/README.md @@ -13,12 +13,12 @@ Follow the instructions on https://github.com/coq-community/templates to regener 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. +that work with any `comRingType` and `fieldType` instances, 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 and additive functions to leaves of +ring/field expressions before normalization to the Horner form. ## Meta @@ -54,7 +54,7 @@ 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 +The way we adapt the 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 b88830c..0dc3e50 100644 --- a/coq-mathcomp-algebra-tactics.opam +++ b/coq-mathcomp-algebra-tactics.opam @@ -10,15 +10,15 @@ 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: "Reflexive ring and field tactics for Mathematical Components" +synopsis: "Ring and field tactics for Mathematical Components" description: """ 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.""" +that work with any `comRingType` and `fieldType` instances, 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 and additive functions to leaves of +ring/field expressions before normalization to the Horner form.""" build: [make "-j%{jobs}%" ] install: [make "install"] diff --git a/meta.yml b/meta.yml index 6dd6d49..5be3f9d 100644 --- a/meta.yml +++ b/meta.yml @@ -6,16 +6,16 @@ organization: math-comp action: true synopsis: >- - Reflexive ring and field tactics for Mathematical Components + Ring and field tactics for Mathematical Components description: |- 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. + that work with any `comRingType` and `fieldType` instances, 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 and additive functions to leaves of + ring/field expressions before normalization to the Horner form. authors: - name: Kazuhiko Sakaguchi @@ -65,8 +65,8 @@ 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 + The way we adapt the 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.