Merge pull request #81 from SnarkBoojum/adapt_MC_PR_923

Adapt to hornerE respecting exponents - math-comp's PR #923
math-comp · Sep 20, 2022 · 56cbd91 · 56cbd91
2 parents 1b5e247 + f7181aa
commit 56cbd91
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/theories/abel.v b/theories/abel.v
@@ -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.
+  (* 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.
@@ -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.
+(* FIXME: remove ?hornerXn when requiring MC >= 1.16.0 *)
 Qed.
 
 Lemma galois_cyclo_radical E : (p > 0)%N -> x ^+ p \in E ->
@@ -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.
+    (* 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
@@ -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.
+(* 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.