Skip to content

Adapt to hornerE respecting exponents - math-comp's PR #923 #81

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Sep 20, 2022
Merged

Adapt to hornerE respecting exponents - math-comp's PR #923 #81

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
805ea90
Adapt to hornerE respecting exponents - MC PR #923
Sep 13, 2022
7b015e2
Ensure compatibility with old & new hornerE version
Sep 14, 2022
c84a549
Fix the previous change: it worked with old hornerE and not the new a…
Sep 14, 2022
f7181aa
Document how to simplify proofs when requiring MC >= 1.16.0
Sep 14, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions theories/abel.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -416,7 +416,8 @@ 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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
- rewrite all_map; apply/allP => i _ /=; rewrite /root !hornerE ?hornerXn.
- rewrite all_map; apply/allP => i _ /=; rewrite /root !hornerE ?hornerXn.
(* FIXME: remove ?hornerXn above once requiring MathComp >= 1.16.0 *)

(* 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.
Expand All @@ -433,7 +434,8 @@ 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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
by rewrite minPoly_dvdp /root ?poly_XnsubC_over// !hornerE ?hornerXn subrr.
by rewrite minPoly_dvdp /root ?poly_XnsubC_over// !hornerE ?hornerXn subrr.
(* FIXME: remove ?hornerXn above once requiring MathComp >= 1.16.0 *)

(* FIXME: remove ?hornerXn when requiring MC >= 1.16.0 *)
Qed.

Lemma galois_cyclo_radical E : (p > 0)%N -> x ^+ p \in E ->
Expand Down Expand Up @@ -1505,7 +1507,8 @@ 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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
by rewrite !hornerE ?hornerXn rootCK// rmorphX subrr.
by rewrite !hornerE ?hornerXn rootCK// rmorphX subrr.
(* FIXME: remove ?hornerXn above once requiring MathComp >= 1.16.0 *)

(* 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.
Expand Down
3 changes: 2 additions & 1 deletion theories/xmathcomp/various.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -432,7 +432,8 @@ 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 ?hornerE expf_neq0// subr_eq0.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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.
(* FIXME: remove ?horner_exp ?hornerE above once requiring MathComp >= 1.16.0 *)

(* 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.
Expand Down