From f7181aad1b751c0c951ad1e81fe45eb42a93ac8c Mon Sep 17 00:00:00 2001 From: Julien Puydt Date: Wed, 14 Sep 2022 17:09:31 +0200 Subject: [PATCH] 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.