From 805ea901e6adf4439d4e0597df581058c91effe4 Mon Sep 17 00:00:00 2001 From: Julien Puydt Date: Tue, 13 Sep 2022 15:22:54 +0200 Subject: [PATCH 1/4] Adapt to hornerE respecting exponents - MC PR #923 --- theories/abel.v | 6 +++--- theories/xmathcomp/various.v | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/abel.v b/theories/abel.v index 8ce6a48..b1203e0 100644 --- a/theories/abel.v +++ b/theories/abel.v @@ -416,7 +416,7 @@ move=> n_gt0; have [->|xN0] := eqVneq x 0. rewrite [LHS](@all_roots_prod_XsubC _ _ ws). - by rewrite (monicP _) ?monic_XnsubC// scale1r big_map big_enum. - by rewrite size_XnsubC// size_map size_enum_ord. -- rewrite all_map; apply/allP => i _ /=; rewrite /root !hornerE hornerXn. +- rewrite all_map; apply/allP => i _ /=; rewrite /root !hornerE ?hornerXn. by rewrite exprMn exprAC [w ^+ _]prim_expr_order// expr1n mulr1 subrr. - by rewrite uniq_rootsE uniq_roots_Xn_sub_xn. Qed. @@ -433,7 +433,7 @@ Lemma dvdp_minpoly_Xn_subn E : (x ^+ p)%R \in E -> minPoly E x %| ('X^p - (x ^+ p)%:P). Proof using. move=> xpE; have [->|p_gt0] := posnP p; first by rewrite !expr0 subrr dvdp0. -by rewrite minPoly_dvdp /root ?poly_XnsubC_over// !hornerE hornerXn subrr. +by rewrite minPoly_dvdp /root ?poly_XnsubC_over// !hornerE ?hornerXn subrr. Qed. Lemma galois_cyclo_radical E : (p > 0)%N -> x ^+ p \in E -> @@ -1505,7 +1505,7 @@ have Cchar := Cchar => p_neq0; split. move=> /radicalP[]; case: i => // i in epw * => _ uik. pose v := i.+1.-root (iota (u ^+ i.+1)). have : ('X ^+ i.+1 - (v ^+ i.+1)%:P).[iota u] == 0. - by rewrite !hornerE hornerXn rootCK// rmorphX subrr. + by rewrite !hornerE ?hornerXn rootCK// rmorphX subrr. have /Xn_sub_xnE->// := prim1rootP (isT : 0 < i.+1)%N. rewrite horner_prod prodf_seq_eq0/= => /hasP[/= l _]. rewrite hornerXsubC subr_eq0 => /eqP u_eq. diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index 3138b31..9e4cfab 100644 --- a/theories/xmathcomp/various.v +++ b/theories/xmathcomp/various.v @@ -432,7 +432,7 @@ have Xxn0 : ('X - y%:P) ^+ n != 0 by rewrite ?expf_neq0 ?polyXsubC_eq0. apply/eqP; rewrite eqn_leq mup_leq ?mup_geq//. have [->|Nxy] := eqVneq x y. by rewrite /= dvdpp ?dvdp_Pexp2l ?size_XsubC ?ltnn. -by rewrite dvd1p dvdp_XsubCl /root horner_exp !hornerE expf_neq0// subr_eq0. +by rewrite dvd1p dvdp_XsubCl /root !hornerE ?horner_exp expf_neq0// subr_eq0. Qed. Lemma mupNroot (x : L) q : ~~ root q x -> mup x q = 0%N. From 7b015e2b1801434f429a931f411e034bc44037e3 Mon Sep 17 00:00:00 2001 From: Julien Puydt Date: Wed, 14 Sep 2022 09:13:16 +0200 Subject: [PATCH 2/4] Ensure compatibility with old & new hornerE version --- theories/xmathcomp/various.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index 9e4cfab..34163b4 100644 --- a/theories/xmathcomp/various.v +++ b/theories/xmathcomp/various.v @@ -432,7 +432,7 @@ have Xxn0 : ('X - y%:P) ^+ n != 0 by rewrite ?expf_neq0 ?polyXsubC_eq0. apply/eqP; rewrite eqn_leq mup_leq ?mup_geq//. have [->|Nxy] := eqVneq x y. by rewrite /= dvdpp ?dvdp_Pexp2l ?size_XsubC ?ltnn. -by rewrite dvd1p dvdp_XsubCl /root !hornerE ?horner_exp expf_neq0// subr_eq0. +by rewrite dvd1p dvdp_XsubCl /root !hornerE ?horner_exp !hornerE expf_neq0// subr_eq0. Qed. Lemma mupNroot (x : L) q : ~~ root q x -> mup x q = 0%N. From c84a5491f5f083bbf3456611a5836cce3e24497d Mon Sep 17 00:00:00 2001 From: Julien Puydt Date: Wed, 14 Sep 2022 09:53:54 +0200 Subject: [PATCH 3/4] Fix the previous change: it worked with old hornerE and not the new anymore --- theories/xmathcomp/various.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index 34163b4..b082ce2 100644 --- a/theories/xmathcomp/various.v +++ b/theories/xmathcomp/various.v @@ -432,7 +432,7 @@ have Xxn0 : ('X - y%:P) ^+ n != 0 by rewrite ?expf_neq0 ?polyXsubC_eq0. apply/eqP; rewrite eqn_leq mup_leq ?mup_geq//. have [->|Nxy] := eqVneq x y. by rewrite /= dvdpp ?dvdp_Pexp2l ?size_XsubC ?ltnn. -by rewrite dvd1p dvdp_XsubCl /root !hornerE ?horner_exp !hornerE expf_neq0// subr_eq0. +by rewrite dvd1p dvdp_XsubCl /root !hornerE ?horner_exp ?hornerE expf_neq0// subr_eq0. Qed. Lemma mupNroot (x : L) q : ~~ root q x -> mup x q = 0%N. From f7181aad1b751c0c951ad1e81fe45eb42a93ac8c Mon Sep 17 00:00:00 2001 From: Julien Puydt Date: Wed, 14 Sep 2022 17:09:31 +0200 Subject: [PATCH 4/4] Document how to simplify proofs when requiring MC >= 1.16.0 --- theories/abel.v | 3 +++ theories/xmathcomp/various.v | 1 + 2 files changed, 4 insertions(+) diff --git a/theories/abel.v b/theories/abel.v index b1203e0..b7525f7 100644 --- a/theories/abel.v +++ b/theories/abel.v @@ -417,6 +417,7 @@ rewrite [LHS](@all_roots_prod_XsubC _ _ ws). - by rewrite (monicP _) ?monic_XnsubC// scale1r big_map big_enum. - by rewrite size_XnsubC// size_map size_enum_ord. - rewrite all_map; apply/allP => i _ /=; rewrite /root !hornerE ?hornerXn. + (* FIXME: remove ?hornerXn when requiring MC >= 1.16.0 *) by rewrite exprMn exprAC [w ^+ _]prim_expr_order// expr1n mulr1 subrr. - by rewrite uniq_rootsE uniq_roots_Xn_sub_xn. Qed. @@ -434,6 +435,7 @@ Lemma dvdp_minpoly_Xn_subn E : Proof using. move=> xpE; have [->|p_gt0] := posnP p; first by rewrite !expr0 subrr dvdp0. by rewrite minPoly_dvdp /root ?poly_XnsubC_over// !hornerE ?hornerXn subrr. +(* FIXME: remove ?hornerXn when requiring MC >= 1.16.0 *) Qed. Lemma galois_cyclo_radical E : (p > 0)%N -> x ^+ p \in E -> @@ -1506,6 +1508,7 @@ have Cchar := Cchar => p_neq0; split. pose v := i.+1.-root (iota (u ^+ i.+1)). have : ('X ^+ i.+1 - (v ^+ i.+1)%:P).[iota u] == 0. by rewrite !hornerE ?hornerXn rootCK// rmorphX subrr. + (* FIXME: remove ?hornerXn when requiring MC >= 1.16.0 *) have /Xn_sub_xnE->// := prim1rootP (isT : 0 < i.+1)%N. rewrite horner_prod prodf_seq_eq0/= => /hasP[/= l _]. rewrite hornerXsubC subr_eq0 => /eqP u_eq. diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index b082ce2..d4057eb 100644 --- a/theories/xmathcomp/various.v +++ b/theories/xmathcomp/various.v @@ -433,6 +433,7 @@ apply/eqP; rewrite eqn_leq mup_leq ?mup_geq//. have [->|Nxy] := eqVneq x y. by rewrite /= dvdpp ?dvdp_Pexp2l ?size_XsubC ?ltnn. by rewrite dvd1p dvdp_XsubCl /root !hornerE ?horner_exp ?hornerE expf_neq0// subr_eq0. +(* FIXME: remove ?horner_exp ?hornerE when requiring MC >= 1.16.0 *) Qed. Lemma mupNroot (x : L) q : ~~ root q x -> mup x q = 0%N.