diff options
| author | Cyril Cohen | 2020-01-03 14:45:53 +0100 |
|---|---|---|
| committer | GitHub | 2020-01-03 14:45:53 +0100 |
| commit | c7fa2a1444d450bcebdeea47800fef1436690b6d (patch) | |
| tree | e0cf42c9b4b8ad39ddec274a368e1f6800b9cc49 /mathcomp/algebra/polydiv.v | |
| parent | a93a392121e8e02c6fdaa6c674dd90af8b12c28d (diff) | |
| parent | a06d61a8e226eeabc52f1a22e469dca1e6077065 (diff) | |
Merge pull request #443 from pi8027/eqVneq
Refactoring and linting proofs especially in polydiv.v
Diffstat (limited to 'mathcomp/algebra/polydiv.v')
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 1374 |
1 files changed, 582 insertions, 792 deletions
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 6b5d003..afd0c6c 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -115,7 +115,7 @@ Variable R : ringType. Implicit Types d p q r : {poly R}. (* Pseudo division, defined on an arbitrary ring *) -Definition redivp_rec (q : {poly R}) := +Definition redivp_rec (q : {poly R}) := let sq := size q in let cq := lead_coef q in fix loop (k : nat) (qq r : {poly R})(n : nat) {struct n} := @@ -146,54 +146,48 @@ rewrite /rdivp unlock; case: ifP => // Hp; rewrite /redivp_rec !size_poly0. by rewrite polySpred ?Hp. Qed. -Lemma rdivp0 p : rdivp p 0 = 0. -Proof. by rewrite /rdivp unlock eqxx. Qed. +Lemma rdivp0 p : rdivp p 0 = 0. Proof. by rewrite /rdivp unlock eqxx. Qed. Lemma rdivp_small p q : size p < size q -> rdivp p q = 0. Proof. rewrite /rdivp unlock; have [-> | _ ltpq] := eqP; first by rewrite size_poly0. -by case: (size p) => [|s]; rewrite /= ltpq. +by case: (size p) => [|s]; rewrite /= ltpq. Qed. Lemma leq_rdivp p q : size (rdivp p q) <= size p. Proof. have [/rdivp_small->|] := ltnP (size p) (size q); first by rewrite size_poly0. rewrite /rdivp /rmodp /rscalp unlock. -case q0: (q == 0) => /=; first by rewrite size_poly0. +have [->|q0] //= := eqVneq q 0. have: size (0 : {poly R}) <= size p by rewrite size_poly0. -move: (leqnn (size p)); move: {2 3 4 6}(size p) => A. +move: {2 3 4 6}(size p) (leqnn (size p)) => A. elim: (size p) 0%N (0 : {poly R}) {1 3 4}p (leqnn (size p)) => [|n ihn] k q1 r. - by move/size_poly_leq0P->; rewrite /= size_poly0 lt0n size_poly_eq0 q0. + by move/size_poly_leq0P->; rewrite /= size_poly0 size_poly_gt0 q0. move=> /= hrn hr hq1 hq; case: ltnP => //= hqr. -have sq: 0 < size q by rewrite size_poly_gt0 q0. +have sq: 0 < size q by rewrite size_poly_gt0. have sr: 0 < size r by apply: leq_trans sq hqr. apply: ihn => //. - apply/leq_sizeP => j hnj. rewrite coefB -scalerAl coefZ coefXnM ltn_subRL ltnNge. - have hj : (size r).-1 <= j. - by apply: leq_trans hnj; move: hrn; rewrite -{1}(prednK sr) ltnS. - rewrite polySpred -?size_poly_gt0 // (leq_ltn_trans hj) /=; last first. - by rewrite -{1}(add0n j) ltn_add2r. - move: (hj); rewrite leq_eqVlt; case/orP. - move/eqP<-; rewrite (@polySpred _ q) ?q0 // subSS coefMC. - rewrite subKn; first by rewrite lead_coefE subrr. - by rewrite -ltnS -!polySpred // ?q0 -?size_poly_gt0. - move=> {hj} hj; move: (hj); rewrite prednK // coefMC; move/leq_sizeP=> -> //. - suff: size q <= j - (size r - size q). - by rewrite mul0r sub0r; move/leq_sizeP=> -> //; rewrite mulr0 oppr0. - rewrite subnBA // addnC -(prednK sq) -(prednK sr) addSn subSS. - by rewrite -addnBA ?(ltnW hj) // -{1}[_.-1]addn0 ltn_add2l subn_gt0. + have hj : (size r).-1 <= j by apply: leq_trans hnj; rewrite -ltnS prednK. + rewrite [r in r <= _]polySpred -?size_poly_gt0 // coefMC. + rewrite (leq_ltn_trans hj) /=; last by rewrite -add1n leq_add2r. + move: hj; rewrite leq_eqVlt prednK // => /predU1P [<- | hj]. + by rewrite -subn1 subnAC subKn // !subn1 !lead_coefE subrr. + have/leq_sizeP-> //: size q <= j - (size r - size q). + by rewrite subnBA // leq_psubRL // leq_add2r. + by move/leq_sizeP: (hj) => -> //; rewrite mul0r mulr0 subr0. - apply: leq_trans (size_add _ _) _; rewrite geq_max; apply/andP; split. apply: leq_trans (size_mul_leq _ _) _. by rewrite size_polyC lead_coef_eq0 q0 /= addn1. rewrite size_opp; apply: leq_trans (size_mul_leq _ _) _. - apply: leq_trans hr; rewrite -subn1 leq_subLR -{2}(subnK hqr) addnA leq_add2r. - by rewrite add1n -(@size_polyXn R) size_scale_leq. + apply: leq_trans hr; rewrite -subn1 leq_subLR -[in (1 + _)%N](subnK hqr). + by rewrite addnA leq_add2r add1n -(@size_polyXn R) size_scale_leq. apply: leq_trans (size_add _ _) _; rewrite geq_max; apply/andP; split. apply: leq_trans (size_mul_leq _ _) _. by rewrite size_polyC lead_coef_eq0 q0 /= addnS addn0. -apply: leq_trans (size_scale_leq _ _) _; rewrite size_polyXn. -by rewrite -subSn // leq_subLR -add1n leq_add. +apply: leq_trans (size_scale_leq _ _) _. +by rewrite size_polyXn -subSn // leq_subLR -add1n leq_add. Qed. Lemma rmod0p p : rmodp 0 p = 0. @@ -202,43 +196,32 @@ rewrite /rmodp unlock; case: ifP => // Hp; rewrite /redivp_rec !size_poly0. by rewrite polySpred ?Hp. Qed. -Lemma rmodp0 p : rmodp p 0 = p. -Proof. by rewrite /rmodp unlock eqxx. Qed. +Lemma rmodp0 p : rmodp p 0 = p. Proof. by rewrite /rmodp unlock eqxx. Qed. Lemma rscalp_small p q : size p < size q -> rscalp p q = 0%N. Proof. -rewrite /rscalp unlock; case: eqP => Eq // spq. +rewrite /rscalp unlock; case: eqP => _ // spq. by case sp: (size p) => [| s] /=; rewrite spq. Qed. Lemma ltn_rmodp p q : (size (rmodp p q) < size q) = (q != 0). Proof. -rewrite /rdivp /rmodp /rscalp unlock; case q0 : (q == 0). - by rewrite (eqP q0) /= size_poly0 ltn0. +rewrite /rdivp /rmodp /rscalp unlock; have [->|q0] := eqVneq q 0. + by rewrite /= size_poly0 ltn0. elim: (size p) 0%N 0 {1 3}p (leqnn (size p)) => [|n ihn] k q1 r. - rewrite leqn0 size_poly_eq0; move/eqP->; rewrite /= size_poly0 /= lt0n. - by rewrite size_poly_eq0 q0 /= size_poly0 lt0n size_poly_eq0 q0. -move=> hr /=; case: (@ltnP (size r) _) => //= hsrq; rewrite ihn //. -apply/leq_sizeP => j hnj; rewrite coefB. -have sr: 0 < size r. - by apply: leq_trans hsrq; apply: neq0_lt0n; rewrite size_poly_eq0. -have sq: 0 < size q by rewrite size_poly_gt0 q0. -have hj : (size r).-1 <= j. - by apply: leq_trans hnj; move: hr; rewrite -{1}(prednK sr) ltnS. -rewrite -scalerAl !coefZ coefXnM ltn_subRL ltnNge; move: (sr). -move/prednK => {1}<-. -have -> /= : (size r).-1 < size q + j. - apply: (@leq_trans ((size q) + (size r).-1)); last by rewrite leq_add2l. - by rewrite -{1}[_.-1]add0n ltn_add2r. -move: (hj); rewrite leq_eqVlt; case/orP. - move/eqP<-; rewrite -{1}(prednK sq) -{3}(prednK sr) subSS. - rewrite subKn; first by rewrite coefMC !lead_coefE subrr. - by move: hsrq; rewrite -{1}(prednK sq) -{1}(prednK sr) ltnS. -move=> {hj} hj; move: (hj); rewrite prednK // coefMC; move/leq_sizeP=> -> //. -suff: size q <= j - (size r - size q). - by rewrite mul0r sub0r; move/leq_sizeP=> -> //; rewrite mulr0 oppr0. -rewrite subnBA // addnC -(prednK sq) -(prednK sr) addSn subSS. -by rewrite -addnBA ?(ltnW hj) // -{1}[_.-1]addn0 ltn_add2l subn_gt0. + move/size_poly_leq0P->. + by rewrite /= size_poly0 size_poly_gt0 q0 size_poly0 size_poly_gt0. +move=> hr /=; case: (ltnP (size r)) => // hsrq; apply/ihn/leq_sizeP => j hnj. +rewrite coefB -scalerAl !coefZ coefXnM coefMC ltn_subRL ltnNge. +have sq: 0 < size q by rewrite size_poly_gt0. +have sr: 0 < size r by apply: leq_trans hsrq. +have hj: (size r).-1 <= j by apply: leq_trans hnj; rewrite -ltnS prednK. +move: (leq_add sq hj); rewrite add1n prednK // => -> /=. +move: hj; rewrite leq_eqVlt prednK // => /predU1P [<- | hj]. + by rewrite -predn_sub subKn // !lead_coefE subrr. +have/leq_sizeP -> //: size q <= j - (size r - size q). + by rewrite subnBA // leq_subRL ?leq_add2r // (leq_trans hj) // leq_addr. +by move/leq_sizeP: hj => -> //; rewrite mul0r mulr0 subr0. Qed. Lemma ltn_rmodpN0 p q : q != 0 -> size (rmodp p q) < size q. @@ -246,69 +229,61 @@ Proof. by rewrite ltn_rmodp. Qed. Lemma rmodp1 p : rmodp p 1 = 0. Proof. -case p0: (p == 0); first by rewrite (eqP p0) rmod0p. -apply/eqP; rewrite -size_poly_eq0. -by have := (ltn_rmodp p 1); rewrite size_polyC !oner_neq0 ltnS leqn0. +apply/eqP; have := ltn_rmodp p 1. +by rewrite !oner_neq0 -size_poly_eq0 size_poly1 ltnS leqn0. Qed. Lemma rmodp_small p q : size p < size q -> rmodp p q = p. Proof. -rewrite /rmodp unlock; case: eqP => Eq; first by rewrite Eq size_poly0. +rewrite /rmodp unlock; have [->|_] := eqP; first by rewrite size_poly0. by case sp: (size p) => [| s] Hs /=; rewrite sp Hs /=. Qed. -Lemma leq_rmodp m d : size (rmodp m d) <= size m. +Lemma leq_rmodp m d : size (rmodp m d) <= size m. Proof. case: (ltnP (size m) (size d)) => [|h]; first by move/rmodp_small->. -case d0: (d == 0); first by rewrite (eqP d0) rmodp0. -by apply: leq_trans h; apply: ltnW; rewrite ltn_rmodp d0. +have [->|d0] := eqVneq d 0; first by rewrite rmodp0. +by apply: leq_trans h; apply: ltnW; rewrite ltn_rmodp. Qed. Lemma rmodpC p c : c != 0 -> rmodp p c%:P = 0. Proof. -move=> Hc; apply/eqP; rewrite -size_poly_eq0 -leqn0 -ltnS. +move=> Hc; apply/eqP; rewrite -size_poly_leq0 -ltnS. have -> : 1%N = nat_of_bool (c != 0) by rewrite Hc. by rewrite -size_polyC ltn_rmodp polyC_eq0. Qed. -Lemma rdvdp0 d : rdvdp d 0. -Proof. by rewrite /rdvdp rmod0p. Qed. +Lemma rdvdp0 d : rdvdp d 0. Proof. by rewrite /rdvdp rmod0p. Qed. -Lemma rdvd0p n : (rdvdp 0 n) = (n == 0). -Proof. by rewrite /rdvdp rmodp0. Qed. +Lemma rdvd0p n : rdvdp 0 n = (n == 0). Proof. by rewrite /rdvdp rmodp0. Qed. Lemma rdvd0pP n : reflect (n = 0) (rdvdp 0 n). -Proof. by apply: (iffP idP); rewrite rdvd0p; move/eqP. Qed. +Proof. by apply: (iffP idP); rewrite rdvd0p; move/eqP. Qed. Lemma rdvdpN0 p q : rdvdp p q -> q != 0 -> p != 0. -Proof. by move=> pq hq; apply: contraL pq => /eqP ->; rewrite rdvd0p. Qed. +Proof. by move=> pq hq; apply: contraTneq pq => ->; rewrite rdvd0p. Qed. -Lemma rdvdp1 d : (rdvdp d 1) = ((size d) == 1%N). +Lemma rdvdp1 d : rdvdp d 1 = (size d == 1%N). Proof. -rewrite /rdvdp; case d0: (d == 0). - by rewrite (eqP d0) rmodp0 size_poly0 (negPf (@oner_neq0 _)). -have:= (size_poly_eq0 d); rewrite d0; move/negbT; rewrite -lt0n. -rewrite leq_eqVlt; case/orP => hd; last first. - by rewrite rmodp_small ?size_poly1 // oner_eq0 -(subnKC hd). -rewrite eq_sym in hd; rewrite hd; have [c cn0 ->] := size_poly1P _ hd. +rewrite /rdvdp; have [->|] := eqVneq d 0. + by rewrite rmodp0 size_poly0 (negPf (oner_neq0 _)). +rewrite -size_poly_leq0 -ltnS; case: ltngtP => // [|/eqP] hd _. + by rewrite rmodp_small ?size_poly1 // oner_eq0. +have [c cn0 ->] := size_poly1P _ hd. rewrite /rmodp unlock -size_poly_eq0 size_poly1 /= size_poly1 size_polyC cn0 /=. by rewrite polyC_eq0 (negPf cn0) !lead_coefC !scale1r subrr !size_poly0. Qed. -Lemma rdvd1p m : rdvdp 1 m. -Proof. by rewrite /rdvdp rmodp1. Qed. +Lemma rdvd1p m : rdvdp 1 m. Proof. by rewrite /rdvdp rmodp1. Qed. Lemma Nrdvdp_small (n d : {poly R}) : - n != 0 -> size n < size d -> (rdvdp d n) = false. -Proof. -by move=> nn0 hs; rewrite /rdvdp; rewrite (rmodp_small hs); apply: negPf. -Qed. + n != 0 -> size n < size d -> rdvdp d n = false. +Proof. by move=> nn0 hs; rewrite /rdvdp (rmodp_small hs); apply: negPf. Qed. Lemma rmodp_eq0P p q : reflect (rmodp p q = 0) (rdvdp q p). Proof. exact: (iffP eqP). Qed. -Lemma rmodp_eq0 p q : rdvdp q p -> rmodp p q = 0. -Proof. by move/rmodp_eq0P. Qed. +Lemma rmodp_eq0 p q : rdvdp q p -> rmodp p q = 0. Proof. exact: rmodp_eq0P. Qed. Lemma rdvdp_leq p q : rdvdp p q -> q != 0 -> size p <= size q. Proof. by move=> dvd_pq; rewrite leqNgt; apply: contra => /rmodp_small <-. Qed. @@ -331,8 +306,8 @@ Qed. Lemma rgcdp0 : right_id 0 rgcdp. Proof. -move=> p; have:= rgcd0p p; rewrite /rgcdp size_poly0 size_poly_gt0 if_neg. -by case: ifP => /= p0; rewrite ?(eqxx, p0) // (eqP p0). +move=> p; have:= rgcd0p p; rewrite /rgcdp size_poly0 size_poly_gt0. +by case: eqVneq => p0; rewrite ?(eqxx, p0) //= eqxx. Qed. Lemma rgcdpE p q : @@ -346,38 +321,30 @@ pose rgcdp_rec := fix rgcdp_rec (n : nat) (pp qq : {poly R}) {struct n} := have Irec: forall m n p q, size q <= m -> size q <= n -> size q < size p -> rgcdp_rec m p q = rgcdp_rec n p q. + elim=> [|m Hrec] [|n] //= p1 q1. - - rewrite leqn0 size_poly_eq0; move/eqP=> -> _. - rewrite size_poly0 size_poly_gt0 rmodp0 => nzp. - by rewrite (negPf nzp); case: n => [|n] /=; rewrite rmod0p eqxx. - - rewrite leqn0 size_poly_eq0 => _; move/eqP=> ->. - rewrite size_poly0 size_poly_gt0 rmodp0 => nzp. - by rewrite (negPf nzp); case: m {Hrec} => [|m] /=; rewrite rmod0p eqxx. - case: ifP => Epq Sm Sn Sq //; rewrite ?Epq //. - case: (eqVneq q1 0) => [->|nzq]. + - move/size_poly_leq0P=> -> _; rewrite size_poly0 size_poly_gt0 rmodp0. + by move/negPf->; case: n => [|n] /=; rewrite rmod0p eqxx. + - move=> _ /size_poly_leq0P ->; rewrite size_poly0 size_poly_gt0 rmodp0. + by move/negPf->; case: m {Hrec} => [|m] /=; rewrite rmod0p eqxx. + case: eqVneq => Epq Sm Sn Sq //; have [->|nzq] := eqVneq q1 0. by case: n m {Sm Sn Hrec} => [|m] [|n] //=; rewrite rmod0p eqxx. apply: Hrec; last by rewrite ltn_rmodp. by rewrite -ltnS (leq_trans _ Sm) // ltn_rmodp. by rewrite -ltnS (leq_trans _ Sn) // ltn_rmodp. -case: (eqVneq p 0) => [-> | nzp]. +have [->|nzp] := eqVneq p 0. by rewrite rmod0p rmodp0 rgcd0p rgcdp0 if_same. -case: (eqVneq q 0) => [-> | nzq]. +have [->|nzq] := eqVneq q 0. by rewrite rmod0p rmodp0 rgcd0p rgcdp0 if_same. -rewrite /rgcdp -/rgcdp_rec. -case: ltnP; rewrite (negPf nzp, negPf nzq) //=. - move=> ltpq; rewrite ltn_rmodp (negPf nzp) //=. - rewrite -(ltn_predK ltpq) /=; case: eqP => [->|]. +rewrite /rgcdp -/rgcdp_rec !ltn_rmodp (negPf nzp) (negPf nzq) /=. +have [ltpq|leqp] := ltnP; rewrite !(negPf nzp, negPf nzq) //= polySpred //=. + have [->|nzqp] := eqVneq. by case: (size p) => [|[|s]]; rewrite /= rmodp0 (negPf nzp) // rmod0p eqxx. - move/eqP=> nzqp; rewrite (negPf nzp). apply: Irec => //; last by rewrite ltn_rmodp. - by rewrite -ltnS (ltn_predK ltpq) (leq_trans _ ltpq) ?leqW // ltn_rmodp. + by rewrite -ltnS -polySpred // (leq_trans _ ltpq) ?leqW // ltn_rmodp. by rewrite ltnW // ltn_rmodp. -move=> leqp; rewrite ltn_rmodp (negPf nzq) //=. -have p_gt0: size p > 0 by rewrite size_poly_gt0. -rewrite -(prednK p_gt0) /=; case: eqP => [->|]. +have [->|nzpq] := eqVneq. by case: (size q) => [|[|s]]; rewrite /= rmodp0 (negPf nzq) // rmod0p eqxx. -move/eqP=> nzpq; rewrite (negPf nzq). apply: Irec => //; last by rewrite ltn_rmodp. - by rewrite -ltnS (prednK p_gt0) (leq_trans _ leqp) // ltn_rmodp. + by rewrite -ltnS -polySpred // (leq_trans _ leqp) // ltn_rmodp. by rewrite ltnW // ltn_rmodp. Qed. @@ -388,38 +355,35 @@ Variant comm_redivp_spec m d : nat * {poly R} * {poly R} -> Type := Lemma comm_redivpP m d : comm_redivp_spec m d (redivp m d). Proof. -rewrite unlock; case: (altP (d =P 0))=> [->| Hd]. +rewrite unlock; have [->|Hd] := eqVneq d 0. by constructor; rewrite !(simp, eqxx). have: GRing.comm d (lead_coef d)%:P -> m * (lead_coef d ^+ 0)%:P = 0 * d + m. by rewrite !simp. -elim: (size m) 0%N 0 {1 4 6}m (leqnn (size m))=> - [|n IHn] k q r Hr /=. - have{Hr} ->: r = 0 by apply/eqP; rewrite -size_poly_eq0; move: Hr; case: size. +elim: (size m) 0%N 0 {1 4 6}m (leqnn (size m)) => [|n IHn] k q r Hr /=. + move/size_poly_leq0P: Hr ->. suff hsd: size (0: {poly R}) < size d by rewrite hsd => /= ?; constructor. - by rewrite size_polyC eqxx (polySpred Hd). -case: ltP=> Hlt Heq; first by constructor=> // _; apply/ltP. -apply: IHn=> [|Cda]; last first. + by rewrite size_poly0 size_poly_gt0. +case: ltnP => Hlt Heq; first by constructor. +apply/IHn=> [|Cda]; last first. rewrite mulrDl addrAC -addrA subrK exprSr polyC_mul mulrA Heq //. by rewrite mulrDl -mulrA Cda mulrA. -apply/leq_sizeP => j Hj. -rewrite coefD coefN coefMC -scalerAl coefZ coefXnM. -move/ltP: Hlt; rewrite -leqNgt=> Hlt. +apply/leq_sizeP => j Hj; rewrite coefB coefMC -scalerAl coefZ coefXnM. +rewrite ltn_subRL ltnNge (leq_trans Hr) /=; last first. + by apply: leq_ltn_trans Hj _; rewrite -add1n leq_add2r size_poly_gt0. move: Hj; rewrite leq_eqVlt; case/predU1P => [<-{j} | Hj]; last first. - rewrite nth_default ?(leq_trans Hqq) // ?simp; last by apply: (leq_trans Hr). - rewrite nth_default; first by rewrite if_same !simp oppr0. + rewrite !nth_default ?simp ?oppr0 ?(leq_trans Hr) //. by rewrite -{1}(subKn Hlt) leq_sub2r // (leq_trans Hr). move: Hr; rewrite leq_eqVlt ltnS; case/predU1P=> Hqq; last first. - rewrite !nth_default ?if_same ?simp ?oppr0 //. - by rewrite -{1}(subKn Hlt) leq_sub2r // (leq_trans Hqq). -rewrite {2}/lead_coef Hqq polySpred // subSS ltnNge leq_subr /=. -by rewrite subKn ?addrN // -subn1 leq_subLR add1n -Hqq. + by rewrite !nth_default ?simp ?oppr0 // -{1}(subKn Hlt) leq_sub2r. +rewrite /lead_coef Hqq polySpred // subSS subKn ?addrN //. +by rewrite -subn1 leq_subLR add1n -Hqq. Qed. Lemma rmodpp p : GRing.comm p (lead_coef p)%:P -> rmodp p p = 0. Proof. -move=> hC; rewrite /rmodp unlock; case: ifP => hp /=; first by rewrite (eqP hp). -move: (hp); rewrite -size_poly_eq0 /redivp_rec; case sp: (size p)=> [|n] // _. -rewrite mul0r sp ltnn add0r subnn expr0 hC alg_polyC subrr. +move=> hC; rewrite /rmodp unlock; have [-> //|] := eqVneq. +rewrite -size_poly_eq0 /redivp_rec; case sp: (size p)=> [|n] // _. +rewrite sp ltnn subnn expr0 hC alg_polyC !simp subrr. by case: n sp => [|n] sp; rewrite size_polyC /= eqxx. Qed. @@ -459,18 +423,17 @@ Lemma redivp_eq q r : let c := (lead_coef d ^+ k)%:P in redivp (q * d + r) d = (k, q * c, r * c). Proof. -move=> lt_rd; case: comm_redivpP=> k q1 r1; move/(_ Cdl)=> Heq. -have: d != 0 by case: (size d) lt_rd (size_poly_eq0 d) => // n _ <-. -move=> dn0; move/(_ dn0)=> Hs. +move=> lt_rd; case: comm_redivpP=> k q1 r1 /(_ Cdl) Heq. +have dn0: d != 0 by case: (size d) lt_rd (size_poly_eq0 d) => // n _ <-. +move=> /(_ dn0) Hs. have eC : q * d * (lead_coef d ^+ k)%:P = q * (lead_coef d ^+ k)%:P * d. - by rewrite -mulrA polyC_exp (GRing.commrX k Cdl) mulrA. + by rewrite -mulrA polyC_exp (commrX k Cdl) mulrA. suff e1 : q1 = q * (lead_coef d ^+ k)%:P. - congr (_, _, _) => //=; move/eqP: Heq; rewrite [_ + r1]addrC. - rewrite -subr_eq; move/eqP<-; rewrite e1 mulrDl addrAC -{2}(add0r (r * _)). - by rewrite eC subrr add0r. + congr (_, _, _) => //=; move/eqP: Heq. + by rewrite [_ + r1]addrC -subr_eq e1 mulrDl addrAC eC subrr add0r; move/eqP. have : (q1 - q * (lead_coef d ^+ k)%:P) * d = r * (lead_coef d ^+ k)%:P - r1. apply: (@addIr _ r1); rewrite subrK. - apply: (@addrI _ ((q * (lead_coef d ^+ k)%:P) * d)). + apply: (@addrI _ ((q * (lead_coef d ^+ k)%:P) * d)). by rewrite mulrDl mulNr !addrA [_ + (q1 * d)]addrC addrK -eC -mulrDl. move/eqP; rewrite -[_ == _ - _]subr_eq0 rreg_div0 //. by case/andP; rewrite subr_eq0; move/eqP. @@ -496,15 +459,14 @@ have Hnq0 := rreg_lead0 Rreg; set lq := lead_coef d. pose v := rscalp p d; pose m := maxn v k. rewrite /rdvdp -(rreg_polyMC_eq0 _ (@rregX _ _ (m - v) Rreg)). suff: - ((rdivp p d) * (lq ^+ (m - v))%:P - q1 * (lq ^+ (m - k))%:P) * d + - (rmodp p d) * (lq ^+ (m - v))%:P == 0. + ((rdivp p d) * (lq ^+ (m - v))%:P - q1 * (lq ^+ (m - k))%:P) * d + + (rmodp p d) * (lq ^+ (m - v))%:P == 0. rewrite rreg_div0 //; first by case/andP. - by rewrite rreg_size ?ltn_rmodp //; apply rregX. -rewrite mulrDl addrAC mulNr -!mulrA polyC_exp -(GRing.commrX (m-v) Cdl). + by rewrite rreg_size ?ltn_rmodp //; exact: rregX. +rewrite mulrDl addrAC mulNr -!mulrA polyC_exp -(commrX (m-v) Cdl). rewrite -polyC_exp mulrA -mulrDl -rdivp_eq // [(_ ^+ (m - k))%:P]polyC_exp. -rewrite -(GRing.commrX (m-k) Cdl) -polyC_exp mulrA -he -!mulrA -!polyC_mul. -rewrite -/v -!exprD addnC subnK ?leq_maxl //. -by rewrite addnC subnK ?subrr ?leq_maxr. +rewrite -(commrX (m-k) Cdl) -polyC_exp mulrA -he -!mulrA -!polyC_mul -/v. +by rewrite -!exprD addnC subnK ?leq_maxl // addnC subnK ?subrr ?leq_maxr. Qed. Variant rdvdp_spec p q : {poly R} -> bool -> Type := @@ -523,27 +485,23 @@ Qed. Lemma rdvdp_mull p : rdvdp d (p * d). Proof. by apply: (@eq_rdvdp 0%N p); rewrite expr0 mulr1. Qed. -Lemma rmodp_mull p : rmodp (p * d) d = 0. -Proof. -case: (d =P 0)=> Hd; first by rewrite Hd simp rmod0p. -by apply/eqP; apply: rdvdp_mull. -Qed. +Lemma rmodp_mull p : rmodp (p * d) d = 0. Proof. exact/eqP/rdvdp_mull. Qed. Lemma rmodpp : rmodp d d = 0. -Proof. by rewrite -{1}(mul1r d) rmodp_mull. Qed. +Proof. by rewrite -[d in rmodp d _]mul1r rmodp_mull. Qed. Lemma rdivpp : rdivp d d = (lead_coef d ^+ rscalp d d)%:P. +Proof. have dn0 : d != 0 by rewrite -lead_coef_eq0 rreg_neq0. move: (rdivp_eq d); rewrite rmodpp addr0. suff ->: GRing.comm d (lead_coef d ^+ rscalp d d)%:P by move/(rreg_lead Rreg)->. by rewrite polyC_exp; apply: commrX. Qed. -Lemma rdvdpp : rdvdp d d. -Proof. by apply/eqP; apply: rmodpp. Qed. +Lemma rdvdpp : rdvdp d d. Proof. exact/eqP/rmodpp. Qed. -Lemma rdivpK p : rdvdp d p -> - (rdivp p d) * d = p * (lead_coef d ^+ rscalp p d)%:P. +Lemma rdivpK p : rdvdp d p -> + rdivp p d * d = p * (lead_coef d ^+ rscalp p d)%:P. Proof. by rewrite rdivp_eq /rdvdp; move/eqP->; rewrite addr0. Qed. End ComRegDivisor. @@ -565,18 +523,17 @@ Implicit Types p q r : {poly R}. Variable d : {poly R}. Hypothesis mond : d \is monic. -Lemma redivp_eq q r : size r < size d -> +Lemma redivp_eq q r : size r < size d -> let k := (redivp (q * d + r) d).1.1 in redivp (q * d + r) d = (k, q, r). Proof. -case: (monic_comreg mond)=> Hc Hr; move/(redivp_eq Hc Hr q). +case: (monic_comreg mond)=> Hc Hr /(redivp_eq Hc Hr q). by rewrite (eqP mond) => -> /=; rewrite expr1n !mulr1. Qed. -Lemma rdivp_eq p : - p = (rdivp p d) * d + (rmodp p d). +Lemma rdivp_eq p : p = rdivp p d * d + rmodp p d. Proof. -rewrite -rdivp_eq; rewrite (eqP mond); last exact: commr1. +rewrite -rdivp_eq (eqP mond); last exact: commr1. by rewrite expr1n mulr1. Qed. @@ -585,31 +542,28 @@ Proof. by case: (monic_comreg mond) => hc hr; rewrite rdivpp // (eqP mond) expr1n. Qed. -Lemma rdivp_addl_mul_small q r : - size r < size d -> rdivp (q * d + r) d = q. +Lemma rdivp_addl_mul_small q r : size r < size d -> rdivp (q * d + r) d = q. Proof. by move=> Hd; case: (monic_comreg mond)=> Hc Hr; rewrite /rdivp redivp_eq. Qed. Lemma rdivp_addl_mul q r : rdivp (q * d + r) d = q + rdivp r d. Proof. -case: (monic_comreg mond)=> Hc Hr; rewrite {1}(rdivp_eq r) addrA. +case: (monic_comreg mond)=> Hc Hr; rewrite [r in _ * _ + r]rdivp_eq addrA. by rewrite -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0. Qed. -Lemma rdivp_addl q r : - rdvdp d q -> rdivp (q + r) d = rdivp q d + rdivp r d. +Lemma rdivp_addl q r : rdvdp d q -> rdivp (q + r) d = rdivp q d + rdivp r d. Proof. -case: (monic_comreg mond)=> Hc Hr; rewrite {1}(rdivp_eq r) addrA. -rewrite {2}(rdivp_eq q); move/rmodp_eq0P->; rewrite addr0. -by rewrite -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0. +case: (monic_comreg mond)=> Hc Hr; rewrite [r in q + r]rdivp_eq addrA. +rewrite [q in q + _ + _]rdivp_eq; move/rmodp_eq0P->. +by rewrite addr0 -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0. Qed. -Lemma rdivp_addr q r : - rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d. +Lemma rdivp_addr q r : rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d. Proof. by rewrite addrC; move/rdivp_addl->; rewrite addrC. Qed. -Lemma rdivp_mull p : rdivp (p * d) d = p. +Lemma rdivp_mull p : rdivp (p * d) d = p. Proof. by rewrite -[p * d]addr0 rdivp_addl_mul rdiv0p addr0. Qed. Lemma rmodp_mull p : rmodp (p * d) d = 0. @@ -622,26 +576,21 @@ Proof. by apply: rmodpp; rewrite (eqP mond); [apply: commr1 | apply: rreg1]. Qed. -Lemma rmodp_addl_mul_small q r : - size r < size d -> rmodp (q * d + r) d = r. +Lemma rmodp_addl_mul_small q r : size r < size d -> rmodp (q * d + r) d = r. Proof. by move=> Hd; case: (monic_comreg mond)=> Hc Hr; rewrite /rmodp redivp_eq. Qed. Lemma rmodp_add p q : rmodp (p + q) d = rmodp p d + rmodp q d. Proof. -rewrite {1}(rdivp_eq p) {1}(rdivp_eq q). -rewrite addrCA 2!addrA -mulrDl (addrC (rdivp q d)) -addrA. +rewrite [p in LHS]rdivp_eq [q in LHS]rdivp_eq addrACA -mulrDl. rewrite rmodp_addl_mul_small //; apply: (leq_ltn_trans (size_add _ _)). by rewrite gtn_max !ltn_rmodp // monic_neq0. Qed. Lemma rmodp_mulmr p q : rmodp (p * (rmodp q d)) d = rmodp (p * q) d. Proof. -have -> : rmodp q d = q - (rdivp q d) * d. - by rewrite {2}(rdivp_eq q) addrAC subrr add0r. -rewrite mulrDr rmodp_add -mulNr mulrA. -by rewrite -{2}[rmodp _ _]addr0; congr (_ + _); apply: rmodp_mull. +by rewrite [q in RHS]rdivp_eq mulrDr rmodp_add mulrA rmodp_mull add0r. Qed. Lemma rdvdpp : rdvdp d d. @@ -666,14 +615,12 @@ Qed. Lemma rdvdpP p : reflect (exists qq, p = qq * d) (rdvdp d p). Proof. -case: (monic_comreg mond)=> Hc Hr; apply: (iffP idP). - case: rdvdp_eqP=> // k qq; rewrite (eqP mond) expr1n mulr1 => -> _. - by exists qq. -by case=> [qq]; move/eq_rdvdp. +case: (monic_comreg mond)=> Hc Hr; apply: (iffP idP) => [|[qq] /eq_rdvdp //]. +by case: rdvdp_eqP=> // k qq; rewrite (eqP mond) expr1n mulr1 => ->; exists qq. Qed. Lemma rdivpK p : rdvdp d p -> (rdivp p d) * d = p. -Proof. by move=> dvddp; rewrite {2}[p]rdivp_eq rmodp_eq0 ?addr0. Qed. +Proof. by move=> dvddp; rewrite [RHS]rdivp_eq rmodp_eq0 ?addr0. Qed. End MonicDivisor. End RingMonic. @@ -690,21 +637,19 @@ Variable R : ringType. Implicit Types d p q r : {poly R}. Lemma rdivp1 p : rdivp p 1 = p. -Proof. by rewrite -{1}(mulr1 p) rdivp_mull // monic1. Qed. +Proof. by rewrite -[p in LHS]mulr1 rdivp_mull // monic1. Qed. Lemma rdvdp_XsubCl p x : rdvdp ('X - x%:P) p = root p x. Proof. -have [HcX Hr] := (monic_comreg (monicXsubC x)). -apply/rmodp_eq0P/factor_theorem; last first. - by case=> p1 ->; apply: rmodp_mull; apply: monicXsubC. +have [HcX Hr] := monic_comreg (monicXsubC x). +apply/rmodp_eq0P/factor_theorem => [|[p1 ->]]; last exact/rmodp_mull/monicXsubC. move=> e0; exists (rdivp p ('X - x%:P)). -by rewrite {1}(rdivp_eq (monicXsubC x) p) e0 addr0. +by rewrite [LHS](rdivp_eq (monicXsubC x)) e0 addr0. Qed. Lemma polyXsubCP p x : reflect (p.[x] = 0) (rdvdp ('X - x%:P) p). Proof. by apply: (iffP idP); rewrite rdvdp_XsubCl; move/rootP. Qed. - Lemma root_factor_theorem p x : root p x = (rdvdp ('X - x%:P) p). Proof. by rewrite rdvdp_XsubCl. Qed. @@ -729,7 +674,6 @@ Variant redivp_spec (m d : {poly R}) : nat * {poly R} * {poly R} -> Type := (lead_coef d ^+ k) *: m = q * d + r & (d != 0 -> size r < size d) : redivp_spec m d (k, q, r). - Lemma redivpP m d : redivp_spec m d (redivp m d). Proof. rewrite redivp_def; constructor; last by move=> dn0; rewrite ltn_rmodp. @@ -737,22 +681,23 @@ by rewrite -mul_polyC mulrC rdivp_eq //= /GRing.comm mulrC. Qed. Lemma rdivp_eq d p : - (lead_coef d ^+ (rscalp p d)) *: p = (rdivp p d) * d + (rmodp p d). + (lead_coef d ^+ rscalp p d) *: p = rdivp p d * d + rmodp p d. Proof. by rewrite /rdivp /rmodp /rscalp; case: redivpP=> k q1 r1 Hc _; apply: Hc. Qed. Lemma rdvdp_eqP d p : rdvdp_spec p d (rmodp p d) (rdvdp d p). Proof. -case hdvd: (rdvdp d p); last by apply: RdvdpN; move/rmodp_eq0P/eqP: hdvd. +case hdvd: (rdvdp d p); last by move/rmodp_eq0P/eqP/RdvdpN: hdvd. move/rmodp_eq0P: (hdvd)->; apply: (@Rdvdp _ _ _ (rscalp p d) (rdivp p d)). by rewrite mulrC mul_polyC rdivp_eq; move/rmodp_eq0P: (hdvd)->; rewrite addr0. Qed. Lemma rdvdp_eq q p : - (rdvdp q p) = ((lead_coef q) ^+ (rscalp p q) *: p == (rdivp p q) * q). -apply/rmodp_eq0P/eqP; rewrite rdivp_eq; first by move->; rewrite addr0. -by move/eqP; rewrite eq_sym addrC -subr_eq subrr; move/eqP->. + rdvdp q p = (lead_coef q ^+ rscalp p q *: p == rdivp p q * q). +Proof. +rewrite rdivp_eq; apply/rmodp_eq0P/eqP => [->|/eqP]; first by rewrite addr0. +by rewrite eq_sym addrC -subr_eq subrr; move/eqP<-. Qed. End CommutativeRingPseudoDivision. @@ -769,10 +714,9 @@ Variable R : unitRingType. Implicit Type p q r d : {poly R}. Lemma uniq_roots_rdvdp p rs : - all (root p) rs -> uniq_roots rs -> - rdvdp (\prod_(z <- rs) ('X - z%:P)) p. + all (root p) rs -> uniq_roots rs -> rdvdp (\prod_(z <- rs) ('X - z%:P)) p. Proof. -move=> rrs; case/(uniq_roots_prod_XsubC rrs)=> q ->. +move=> rrs /(uniq_roots_prod_XsubC rrs) [q ->]. exact/RingMonic.rdvdp_mull/monic_prod_XsubC. Qed. @@ -802,8 +746,7 @@ Definition divp p q := ((edivp p q).1).2. Definition modp p q := (edivp p q).2. Definition scalp p q := ((edivp p q).1).1. Definition dvdp p q := modp q p == 0. -Definition eqp p q := (dvdp p q) && (dvdp q p). - +Definition eqp p q := (dvdp p q) && (dvdp q p). End IDomainPseudoDivisionDefs. @@ -822,46 +765,39 @@ Section WeakTheoryForIDomainPseudoDivision. Variable R : idomainType. Implicit Type p q r d : {poly R}. - Lemma edivp_def p q : edivp p q = (scalp p q, divp p q, modp p q). Proof. by rewrite /scalp /divp /modp; case: (edivp p q) => [[]] /=. Qed. -Lemma edivp_redivp p q : (lead_coef q \in GRing.unit) = false -> +Lemma edivp_redivp p q : lead_coef q \in GRing.unit = false -> edivp p q = redivp p q. Proof. by move=> hu; rewrite unlock hu; case: (redivp p q) => [[? ?] ?]. Qed. Lemma divpE p q : p %/ q = if lead_coef q \in GRing.unit - then (lead_coef q)^-(rscalp p q) *: (rdivp p q) + then lead_coef q ^- rscalp p q *: rdivp p q else rdivp p q. -Proof. -by case ulcq: (lead_coef q \in GRing.unit); rewrite /divp unlock redivp_def ulcq. -Qed. +Proof. by case: ifP; rewrite /divp unlock redivp_def => ->. Qed. Lemma modpE p q : p %% q = if lead_coef q \in GRing.unit - then (lead_coef q)^-(rscalp p q) *: (rmodp p q) + then lead_coef q ^- rscalp p q *: (rmodp p q) else rmodp p q. -Proof. -by case ulcq: (lead_coef q \in GRing.unit); rewrite /modp unlock redivp_def ulcq. -Qed. +Proof. by case: ifP; rewrite /modp unlock redivp_def => ->. Qed. Lemma scalpE p q : scalp p q = if lead_coef q \in GRing.unit then 0%N else rscalp p q. -Proof. -by case h: (lead_coef q \in GRing.unit); rewrite /scalp unlock redivp_def h. -Qed. +Proof. by case: ifP; rewrite /scalp unlock redivp_def => ->. Qed. Lemma dvdpE p q : p %| q = rdvdp p q. Proof. rewrite /dvdp modpE /rdvdp; case ulcq: (lead_coef p \in GRing.unit)=> //. -rewrite -[_ *: _ == 0]size_poly_eq0 size_scale ?size_poly_eq0 //. +rewrite -[in LHS]size_poly_eq0 size_scale ?size_poly_eq0 //. by rewrite invr_eq0 expf_neq0 //; apply: contraTneq ulcq => ->; rewrite unitr0. Qed. Lemma lc_expn_scalp_neq0 p q : lead_coef q ^+ scalp p q != 0. Proof. -case: (eqVneq q 0) => [->|nzq]; last by rewrite expf_neq0 ?lead_coef_eq0. +have [->|nzq] := eqVneq q 0; last by rewrite expf_neq0 ?lead_coef_eq0. by rewrite /scalp 2!unlock /= eqxx lead_coef0 unitr0 /= oner_neq0. Qed. @@ -899,46 +835,33 @@ Lemma edivp_eq d q r : size r < size d -> lead_coef d \in GRing.unit -> Proof. have hC : GRing.comm d (lead_coef d)%:P by apply: mulrC. move=> hsrd hu; rewrite unlock hu; case et: (redivp _ _) => [[s qq] rr]. -have cdn0 : lead_coef d != 0. - by move: hu; case d0: (lead_coef d == 0) => //; rewrite (eqP d0) unitr0. -move: (et); rewrite RingComRreg.redivp_eq //; last by apply/rregP. -rewrite et /=; case=> e1 e2; rewrite -!mul_polyC -!exprVn !polyC_exp. -suff h x y: x * (lead_coef d ^+ s)%:P = y -> ((lead_coef d)^-1)%:P ^+ s * y = x. - by congr (_, _, _); apply: h. -have hn0 : (lead_coef d)%:P ^+ s != 0 by apply: expf_neq0; rewrite polyC_eq0. -move=> hh; apply: (mulfI hn0); rewrite mulrA -exprMn -polyC_mul divrr //. -by rewrite expr1n mul1r -polyC_exp mulrC; apply: sym_eq. +have cdn0 : lead_coef d != 0 by case: eqP hu => //= ->; rewrite unitr0. +move: (et); rewrite RingComRreg.redivp_eq //; last exact/rregP. +rewrite et /= mulrC (mulrC r) !mul_polyC; case=> <- <-. +by rewrite !scalerA mulVr ?scale1r // unitrX. Qed. -Lemma divp_eq p q : - (lead_coef q ^+ (scalp p q)) *: p = (p %/ q) * q + (p %% q). +Lemma divp_eq p q : (lead_coef q ^+ scalp p q) *: p = (p %/ q) * q + (p %% q). Proof. rewrite divpE modpE scalpE. case uq: (lead_coef q \in GRing.unit); last by rewrite rdivp_eq. -rewrite expr0 scale1r; case: (altP (q =P 0)) => [-> | qn0]. - rewrite mulr0 add0r lead_coef0 rmodp0 /rscalp unlock eqxx expr0 invr1. - by rewrite scale1r. -have hn0 : (lead_coef q ^+ rscalp p q)%:P != 0. - by rewrite polyC_eq0 expf_neq0 // lead_coef_eq0. -apply: (mulfI hn0). -rewrite -scalerAl -scalerDr !mul_polyC scalerA mulrV ?unitrX //. -by rewrite scale1r rdivp_eq. +rewrite expr0 scale1r; have [->|qn0] := eqVneq q 0. + by rewrite lead_coef0 expr0n /rscalp unlock eqxx invr1 !scale1r rmodp0 !simp. +by rewrite -scalerAl -scalerDr -rdivp_eq scalerA mulVr (scale1r, unitrX). Qed. - -Lemma dvdp_eq q p : - (q %| p) = ((lead_coef q) ^+ (scalp p q) *: p == (p %/ q) * q). +Lemma dvdp_eq q p : (q %| p) = (lead_coef q ^+ scalp p q *: p == (p %/ q) * q). Proof. rewrite dvdpE rdvdp_eq scalpE divpE; case: ifP => ulcq //. -rewrite expr0 scale1r; apply/eqP/eqP. - by rewrite -scalerAl; move<-; rewrite scalerA mulVr ?scale1r // unitrX. -by move=> {2}->; rewrite scalerAl scalerA mulrV ?scale1r // unitrX. +rewrite expr0 scale1r -scalerAl; apply/eqP/eqP => [<- | {2}->]. + by rewrite scalerA mulVr ?scale1r // unitrX. +by rewrite scalerA mulrV ?scale1r // unitrX. Qed. -Lemma divpK d p : d %| p -> p %/ d * d = ((lead_coef d) ^+ (scalp p d)) *: p. +Lemma divpK d p : d %| p -> p %/ d * d = (lead_coef d ^+ scalp p d) *: p. Proof. by rewrite dvdp_eq; move/eqP->. Qed. -Lemma divpKC d p : d %| p -> d * (p %/ d) = ((lead_coef d) ^+ (scalp p d)) *: p. +Lemma divpKC d p : d %| p -> d * (p %/ d) = (lead_coef d ^+ scalp p d) *: p. Proof. by move=> ?; rewrite mulrC divpK. Qed. Lemma dvdpP q p : @@ -948,37 +871,32 @@ rewrite dvdp_eq; apply: (iffP eqP) => [e | [[c qq] cn0 e]]. by exists (lead_coef q ^+ scalp p q, p %/ q) => //=. apply/eqP; rewrite -dvdp_eq dvdpE. have Ecc: c%:P != 0 by rewrite polyC_eq0. -case: (eqVneq p 0) => [->|nz_p]; first by rewrite rdvdp0. -pose p1 : {poly R} := lead_coef q ^+ rscalp p q *: qq - c *: (rdivp p q). -have E1: c *: (rmodp p q) = p1 * q. - rewrite mulrDl {1}mulNr -scalerAl -e scalerA mulrC -scalerA -scalerAl. +have [->|nz_p] := eqVneq p 0; first by rewrite rdvdp0. +pose p1 : {poly R} := lead_coef q ^+ rscalp p q *: qq - c *: (rdivp p q). +have E1: c *: rmodp p q = p1 * q. + rewrite mulrDl mulNr -scalerAl -e scalerA mulrC -scalerA -scalerAl. by rewrite -scalerBr rdivp_eq addrC addKr. -rewrite /dvdp; apply/idPn=> m_nz. -have: p1 * q != 0 by rewrite -E1 -mul_polyC mulf_neq0 // -/(dvdp q p) dvdpE. -rewrite mulf_eq0; case/norP=> p1_nz q_nz; have:= ltn_rmodp p q. -rewrite q_nz -(size_scale _ cn0) E1 size_mul //. -by rewrite polySpred // ltnNge leq_addl. +suff: p1 * q == 0 by rewrite -E1 -mul_polyC mulf_eq0 (negPf Ecc). +rewrite mulf_eq0; apply/norP; case=> p1_nz q_nz; have:= ltn_rmodp p q. +by rewrite q_nz -(size_scale _ cn0) E1 size_mul // polySpred // ltnNge leq_addl. Qed. -Lemma mulpK p q : q != 0 -> - p * q %/ q = lead_coef q ^+ scalp (p * q) q *: p. +Lemma mulpK p q : q != 0 -> p * q %/ q = lead_coef q ^+ scalp (p * q) q *: p. Proof. -move=> qn0; move/rregP: (qn0); apply; rewrite -scalerAl divp_eq. +move=> qn0; apply: (rregP qn0); rewrite -scalerAl divp_eq. suff -> : (p * q) %% q = 0 by rewrite addr0. rewrite modpE RingComRreg.rmodp_mull ?scaler0 ?if_same //. by red; rewrite mulrC. by apply/rregP; rewrite lead_coef_eq0. Qed. -Lemma mulKp p q : q != 0 -> - q * p %/ q = lead_coef q ^+ scalp (p * q) q *: p. +Lemma mulKp p q : q != 0 -> q * p %/ q = lead_coef q ^+ scalp (p * q) q *: p. Proof. by move=> nzq; rewrite mulrC; apply: mulpK. Qed. Lemma divpp p : p != 0 -> p %/ p = (lead_coef p ^+ scalp p p)%:P. Proof. -move=> np0; have := (divp_eq p p). -suff -> : p %% p = 0. - by rewrite addr0; move/eqP; rewrite -mul_polyC (inj_eq (mulIf np0)); move/eqP. +move=> np0; have := divp_eq p p. +suff -> : p %% p = 0 by rewrite addr0 -mul_polyC; move/(mulIf np0). rewrite modpE Ring.rmodpp; last by red; rewrite mulrC. by rewrite scaler0 if_same. Qed. @@ -1009,10 +927,9 @@ Qed. Lemma leq_divp p q : (size (p %/ q) <= size p). Proof. -rewrite /divp unlock redivp_def /=; case: ifP=> /=; rewrite ?leq_rdivp //. -move=> ulcq; rewrite size_scale ?leq_rdivp //. -rewrite -exprVn expf_neq0 // invr_eq0. -by move: ulcq; case lcq0: (lead_coef q == 0) => //; rewrite (eqP lcq0) unitr0. +rewrite /divp unlock redivp_def /=; case: ifP => ulcq; rewrite ?leq_rdivp //=. +rewrite size_scale ?leq_rdivp // -exprVn expf_neq0 // invr_eq0. +by case: eqP ulcq => // ->; rewrite unitr0. Qed. Lemma div0p p : 0 %/ p = 0. @@ -1062,42 +979,37 @@ Qed. Lemma modp_mull p q : (p * q) %% q = 0. Proof. -case: (altP (q =P 0)) => [-> | nq0]; first by rewrite modp0 mulr0. -have rlcq : (GRing.rreg (lead_coef q)) by apply/rregP; rewrite lead_coef_eq0. -have hC : GRing.comm q (lead_coef q)%:P by red; rewrite mulrC. +have [-> | nq0] := eqVneq q 0; first by rewrite modp0 mulr0. +have rlcq : GRing.rreg (lead_coef q) by apply/rregP; rewrite lead_coef_eq0. +have hC : GRing.comm q (lead_coef q)%:P by red; rewrite mulrC. by rewrite modpE; case: ifP => ulcq; rewrite RingComRreg.rmodp_mull // scaler0. Qed. -Lemma modp_mulr d p : (d * p) %% d = 0. -Proof. by rewrite mulrC modp_mull. Qed. +Lemma modp_mulr d p : (d * p) %% d = 0. Proof. by rewrite mulrC modp_mull. Qed. Lemma modpp d : d %% d = 0. -Proof. by rewrite -{1}(mul1r d) modp_mull. Qed. +Proof. by rewrite -[d in d %% _]mul1r modp_mull. Qed. Lemma ltn_modp p q : (size (p %% q) < size q) = (q != 0). Proof. -rewrite /modp unlock redivp_def /=; case: ifP=> /=; rewrite ?ltn_rmodp //. -move=> ulcq; rewrite size_scale ?ltn_rmodp //. -rewrite -exprVn expf_neq0 // invr_eq0. -by move: ulcq; case lcq0: (lead_coef q == 0) => //; rewrite (eqP lcq0) unitr0. +rewrite /modp unlock redivp_def /=; case: ifP=> ulcq; rewrite ?ltn_rmodp //=. +rewrite size_scale ?ltn_rmodp // -exprVn expf_neq0 // invr_eq0. +by case: eqP ulcq => // ->; rewrite unitr0. Qed. Lemma ltn_divpl d q p : d != 0 -> (size (q %/ d) < size p) = (size q < size (p * d)). Proof. -move=> dn0; have sd : size d > 0 by rewrite size_poly_gt0 dn0. +move=> dn0. have: (lead_coef d) ^+ (scalp q d) != 0 by apply: lc_expn_scalp_neq0. -move/size_scale; move/(_ q)<-; rewrite divp_eq; case quo0 : (q %/ d == 0). - rewrite (eqP quo0) mul0r add0r size_poly0. - case p0 : (p == 0); first by rewrite (eqP p0) mul0r size_poly0 ltnn ltn0. - have sp : size p > 0 by rewrite size_poly_gt0 p0. - rewrite /= size_mul ?p0 // sp; apply: sym_eq; move/prednK:(sp)<-. - by rewrite addSn /= ltn_addl // ltn_modp. +move/(size_scale q)<-; rewrite divp_eq; have [->|quo0] := eqVneq (q %/ d) 0. + rewrite mul0r add0r size_poly0 size_poly_gt0. + have [->|pn0] := eqVneq p 0; first by rewrite mul0r size_poly0 ltn0. + by rewrite size_mul // (polySpred pn0) addSn ltn_addl // ltn_modp. rewrite size_addl; last first. - rewrite size_mul ?quo0 //; move/negbT: quo0; rewrite -size_poly_gt0. - by move/prednK<-; rewrite addSn /= ltn_addl // ltn_modp. -case: (altP (p =P 0)) => [-> | pn0]; first by rewrite mul0r size_poly0 !ltn0. -by rewrite !size_mul ?quo0 //; move/prednK: sd<-; rewrite !addnS ltn_add2r. + by rewrite size_mul // (polySpred quo0) addSn /= ltn_addl // ltn_modp. +have [->|pn0] := eqVneq p 0; first by rewrite mul0r size_poly0 !ltn0. +by rewrite !size_mul ?quo0 // (polySpred dn0) !addnS ltn_add2r. Qed. Lemma leq_divpr d p q : d != 0 -> @@ -1106,33 +1018,26 @@ Proof. by move=> dn0; rewrite leqNgt ltn_divpl // -leqNgt. Qed. Lemma divpN0 d p : d != 0 -> (p %/ d != 0) = (size d <= size p). Proof. -move=> dn0; rewrite -{2}(mul1r d) -leq_divpr // size_polyC oner_eq0 /=. -by rewrite size_poly_gt0. +move=> dn0. +by rewrite -[d in RHS]mul1r -leq_divpr // size_polyC oner_eq0 size_poly_gt0. Qed. -Lemma size_divp p q : q != 0 -> size (p %/ q) = ((size p) - (size q).-1)%N. +Lemma size_divp p q : q != 0 -> size (p %/ q) = (size p - (size q).-1)%N. Proof. move=> nq0; case: (leqP (size q) (size p)) => sqp; last first. move: (sqp); rewrite -{1}(ltn_predK sqp) ltnS -subn_eq0 divp_small //. by move/eqP->; rewrite size_poly0. -move: (nq0); rewrite -size_poly_gt0 => lt0sq. -move: (sqp); move/(leq_trans lt0sq) => lt0sp. -move: (lt0sp); rewrite size_poly_gt0=> p0. -move: (divp_eq p q); move/(congr1 (size \o (@polyseq R)))=> /=. +have np0 : p != 0. + by rewrite -size_poly_gt0; apply: leq_trans sqp; rewrite size_poly_gt0. +have /= := congr1 (size \o @polyseq R) (divp_eq p q). rewrite size_scale; last by rewrite expf_eq0 lead_coef_eq0 (negPf nq0) andbF. -case: (eqVneq (p %/ q) 0) => [-> | qq0]. +have [->|qq0] := eqVneq (p %/ q) 0. by rewrite mul0r add0r=> es; move: nq0; rewrite -(ltn_modp p) -es ltnNge sqp. -move/negP:(qq0); move/negP; rewrite -size_poly_gt0 => lt0qq. rewrite size_addl. - rewrite size_mul ?qq0 // => ->. - apply/eqP; rewrite -(eqn_add2r ((size q).-1)). - rewrite subnK; first by rewrite -subn1 addnBA // subn1. - rewrite /leq -(subnDl 1%N) !add1n prednK // (@ltn_predK (size q)) //. - by rewrite addnC subnDA subnn sub0n. - by rewrite -[size q]add0n ltn_add2r. + by move->; apply/eqP; rewrite size_mul // (polySpred nq0) addnS /= addnK. rewrite size_mul ?qq0 //. -move: nq0; rewrite -(ltn_modp p); move/leq_trans; apply; move/prednK: lt0qq<-. -by rewrite addSn /= leq_addl. +move: nq0; rewrite -(ltn_modp p); move/leq_trans; apply. +by rewrite (polySpred qq0) addSn /= leq_addl. Qed. Lemma ltn_modpN0 p q : q != 0 -> size (p %% q) < size q. @@ -1140,39 +1045,36 @@ Proof. by rewrite ltn_modp. Qed. Lemma modp_mod p q : (p %% q) %% q = p %% q. Proof. -by case: (eqVneq q 0) => [-> | qn0]; rewrite ?modp0 // modp_small ?ltn_modp. +by have [->|qn0] := eqVneq q 0; rewrite ?modp0 // modp_small ?ltn_modp. Qed. -Lemma leq_modp m d : size (m %% d) <= size m. +Lemma leq_modp m d : size (m %% d) <= size m. Proof. rewrite /modp unlock redivp_def /=; case: ifP; rewrite ?leq_rmodp //. move=> ud; rewrite size_scale ?leq_rmodp // invr_eq0 expf_neq0 //. by apply: contraTneq ud => ->; rewrite unitr0. Qed. -Lemma dvdp0 d : d %| 0. -Proof. by rewrite /dvdp mod0p. Qed. +Lemma dvdp0 d : d %| 0. Proof. by rewrite /dvdp mod0p. Qed. Hint Resolve dvdp0 : core. -Lemma dvd0p p : (0 %| p) = (p == 0). -Proof. by rewrite /dvdp modp0. Qed. +Lemma dvd0p p : (0 %| p) = (p == 0). Proof. by rewrite /dvdp modp0. Qed. Lemma dvd0pP p : reflect (p = 0) (0 %| p). Proof. by apply: (iffP idP); rewrite dvd0p; move/eqP. Qed. Lemma dvdpN0 p q : p %| q -> q != 0 -> p != 0. -Proof. by move=> pq hq; apply: contraL pq=> /eqP ->; rewrite dvd0p. Qed. +Proof. by move=> pq hq; apply: contraTneq pq => ->; rewrite dvd0p. Qed. -Lemma dvdp1 d : (d %| 1) = ((size d) == 1%N). +Lemma dvdp1 d : (d %| 1) = (size d == 1%N). Proof. rewrite /dvdp modpE; case ud: (lead_coef d \in GRing.unit); last exact: rdvdp1. rewrite -size_poly_eq0 size_scale; first by rewrite size_poly_eq0 -rdvdp1. by rewrite invr_eq0 expf_neq0 //; apply: contraTneq ud => ->; rewrite unitr0. Qed. -Lemma dvd1p m : 1 %| m. -Proof. by rewrite /dvdp modp1. Qed. +Lemma dvd1p m : 1 %| m. Proof. by rewrite /dvdp modp1. Qed. Lemma gtNdvdp p q : p != 0 -> size p < size q -> (q %| p) = false. Proof. @@ -1182,57 +1084,52 @@ Qed. Lemma modp_eq0P p q : reflect (p %% q = 0) (q %| p). Proof. exact: (iffP eqP). Qed. -Lemma modp_eq0 p q : (q %| p) -> p %% q = 0. -Proof. by move/modp_eq0P. Qed. +Lemma modp_eq0 p q : (q %| p) -> p %% q = 0. Proof. exact: modp_eq0P. Qed. Lemma leq_divpl d p q : d %| p -> (size (p %/ d) <= size q) = (size p <= size (q * d)). Proof. -case: (eqVneq d 0) => [-> | nd0]. - by move/dvd0pP->; rewrite divp0 size_poly0 !leq0n. -move=> hd; rewrite leq_eqVlt ltn_divpl // (leq_eqVlt (size p)). +case: (eqVneq d 0) => [-> /dvd0pP -> | nd0 hd]. + by rewrite divp0 size_poly0 !leq0n. +rewrite leq_eqVlt ltn_divpl // (leq_eqVlt (size p)). case lhs: (size p < size (q * d)); rewrite ?orbT ?orbF //. have: (lead_coef d) ^+ (scalp p d) != 0 by rewrite expf_neq0 // lead_coef_eq0. -move/size_scale; move/(_ p)<-; rewrite divp_eq. -move/modp_eq0P: hd->; rewrite addr0; case: (altP (p %/ d =P 0))=> [-> | quon0]. - rewrite mul0r size_poly0 eq_sym (eq_sym 0%N) size_poly_eq0. - case: (altP (q =P 0)) => [-> | nq0]; first by rewrite mul0r size_poly0 eqxx. - by rewrite size_poly_eq0 mulf_eq0 (negPf nq0) (negPf nd0). -case: (altP (q =P 0)) => [-> | nq0]. +move/(size_scale p)<-; rewrite divp_eq; move/modp_eq0P: hd->; rewrite addr0. +have [-> | quon0] := eqVneq (p %/ d) 0. + rewrite mul0r size_poly0 2!(eq_sym 0%N) !size_poly_eq0. + by rewrite mulf_eq0 (negPf nd0) orbF. +have [-> | nq0] := eqVneq q 0. by rewrite mul0r size_poly0 !size_poly_eq0 mulf_eq0 (negPf nd0) orbF. -rewrite !size_mul //; move: nd0; rewrite -size_poly_gt0; move/prednK<-. -by rewrite !addnS /= eqn_add2r. +by rewrite !size_mul // (polySpred nd0) !addnS /= eqn_add2r. Qed. Lemma dvdp_leq p q : q != 0 -> p %| q -> size p <= size q. -move=> nq0 /modp_eq0P => rpq; case: (ltnP (size p) (size q)). - by move/ltnW->. -rewrite leq_eqVlt; case/orP; first by move/eqP->. -by move/modp_small; rewrite rpq => h; move: nq0; rewrite h eqxx. +Proof. +move=> nq0 /modp_eq0P. +by case: ltngtP => // /modp_small -> /eqP; rewrite (negPf nq0). Qed. Lemma eq_dvdp c quo q p : c != 0 -> c *: p = quo * q -> q %| p. Proof. move=> cn0; case: (eqVneq p 0) => [->|nz_quo def_quo] //. -pose p1 : {poly R} := lead_coef q ^+ scalp p q *: quo - c *: (p %/ q). +pose p1 : {poly R} := lead_coef q ^+ scalp p q *: quo - c *: (p %/ q). have E1: c *: (p %% q) = p1 * q. - rewrite mulrDl {1}mulNr-scalerAl -def_quo scalerA mulrC -scalerA. + rewrite mulrDl mulNr -scalerAl -def_quo scalerA mulrC -scalerA. by rewrite -scalerAl -scalerBr divp_eq addrAC subrr add0r. rewrite /dvdp; apply/idPn=> m_nz. have: p1 * q != 0 by rewrite -E1 -mul_polyC mulf_neq0 // polyC_eq0. rewrite mulf_eq0; case/norP=> p1_nz q_nz. -have := (ltn_modp p q); rewrite q_nz -(size_scale (p %% q) cn0) E1. +have := ltn_modp p q; rewrite q_nz -(size_scale (p %% q) cn0) E1. by rewrite size_mul // polySpred // ltnNge leq_addl. Qed. -Lemma dvdpp d : d %| d. -Proof. by rewrite /dvdp modpp. Qed. +Lemma dvdpp d : d %| d. Proof. by rewrite /dvdp modpp. Qed. Hint Resolve dvdpp : core. -Lemma divp_dvd p q : (p %| q) -> ((q %/ p) %| q). +Lemma divp_dvd p q : p %| q -> (q %/ p) %| q. Proof. -case: (eqVneq p 0) => [-> | np0]; first by rewrite divp0. +have [-> | np0] := eqVneq p 0; first by rewrite divp0. rewrite dvdp_eq => /eqP h. apply: (@eq_dvdp ((lead_coef p)^+ (scalp q p)) p); last by rewrite mulrC. by rewrite expf_neq0 // lead_coef_eq0. @@ -1240,7 +1137,7 @@ Qed. Lemma dvdp_mull m d n : d %| n -> d %| m * n. Proof. -case: (eqVneq d 0) => [-> |dn0]; first by move/dvd0pP->; rewrite mulr0 dvdpp. +case: (eqVneq d 0) => [-> /dvd0pP -> | dn0]; first by rewrite mulr0 dvdpp. rewrite dvdp_eq => /eqP e. apply: (@eq_dvdp (lead_coef d ^+ scalp n d) (m * (n %/ d))). by rewrite expf_neq0 // lead_coef_eq0. @@ -1254,8 +1151,8 @@ Hint Resolve dvdp_mull dvdp_mulr : core. Lemma dvdp_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2. Proof. -case: (eqVneq d1 0) => [-> |d1n0]; first by move/dvd0pP->; rewrite !mul0r dvdpp. -case: (eqVneq d2 0) => [-> |d2n0]; first by move=> _ /dvd0pP ->; rewrite !mulr0. +case: (eqVneq d1 0) => [-> /dvd0pP -> | d1n0]; first by rewrite !mul0r dvdpp. +case: (eqVneq d2 0) => [-> _ /dvd0pP -> | d2n0]; first by rewrite !mulr0. rewrite dvdp_eq; set c1 := _ ^+ _; set q1 := _ %/ _; move/eqP=> Hq1. rewrite dvdp_eq; set c2 := _ ^+ _; set q2 := _ %/ _; move/eqP=> Hq2. apply: (@eq_dvdp (c1 * c2) (q1 * q2)). @@ -1266,7 +1163,7 @@ Qed. Lemma dvdp_addr m d n : d %| m -> (d %| m + n) = (d %| n). Proof. -case: (altP (d =P 0)) => [-> | dn0]; first by move/dvd0pP->; rewrite add0r. +case: (eqVneq d 0) => [-> /dvd0pP -> | dn0]; first by rewrite add0r. rewrite dvdp_eq; set c1 := _ ^+ _; set q1 := _ %/ _; move/eqP=> Eq1. apply/idP/idP; rewrite dvdp_eq; set c2 := _ ^+ _; set q2 := _ %/ _. have sn0 : c1 * c2 != 0. @@ -1277,7 +1174,7 @@ apply/idP/idP; rewrite dvdp_eq; set c2 := _ ^+ _; set q2 := _ %/ _. have sn0 : c1 * c2 != 0. by rewrite !mulf_neq0 // expf_eq0 lead_coef_eq0 (negPf dn0) andbF. move/eqP=> Eq2; apply: (@eq_dvdp _ (c1 *: q2 + c2 *: q1) _ _ sn0). -by rewrite mulrDl -!scalerAl -Eq1 -Eq2 !scalerA mulrC addrC scalerDr. +by rewrite mulrDl -!scalerAl -Eq1 -Eq2 !scalerA mulrC addrC scalerDr. Qed. Lemma dvdp_addl n d m : d %| n -> (d %| m + n) = (d %| m). @@ -1286,27 +1183,27 @@ Proof. by rewrite addrC; apply: dvdp_addr. Qed. Lemma dvdp_add d m n : d %| m -> d %| n -> d %| m + n. Proof. by move/dvdp_addr->. Qed. -Lemma dvdp_add_eq d m n : d %| m + n -> (d %| m) = (d %| n). +Lemma dvdp_add_eq d m n : d %| m + n -> (d %| m) = (d %| n). Proof. by move=> ?; apply/idP/idP; [move/dvdp_addr <-| move/dvdp_addl <-]. Qed. Lemma dvdp_subr d m n : d %| m -> (d %| m - n) = (d %| n). -Proof. by move=> ?; apply dvdp_add_eq; rewrite -addrA addNr simp. Qed. +Proof. by move=> ?; apply: dvdp_add_eq; rewrite -addrA addNr simp. Qed. -Lemma dvdp_subl d m n : d %| n -> (d %| m - n) = (d %| m). +Lemma dvdp_subl d m n : d %| n -> (d %| m - n) = (d %| m). Proof. by move/dvdp_addl<-; rewrite subrK. Qed. -Lemma dvdp_sub d m n : d %| m -> d %| n -> d %| m - n. -Proof. by move=> *; rewrite dvdp_subl. Qed. +Lemma dvdp_sub d m n : d %| m -> d %| n -> d %| m - n. +Proof. by move=> *; rewrite dvdp_subl. Qed. Lemma dvdp_mod d n m : d %| n -> (d %| m) = (d %| m %% n). Proof. -case: (altP (n =P 0)) => [-> | nn0]; first by rewrite modp0. -case: (altP (d =P 0)) => [-> | dn0]; first by move/dvd0pP->; rewrite modp0. +have [-> | nn0] := eqVneq n 0; first by rewrite modp0. +case: (eqVneq d 0) => [-> /dvd0pP -> | dn0]; first by rewrite modp0. rewrite dvdp_eq; set c1 := _ ^+ _; set q1 := _ %/ _; move/eqP=> Eq1. apply/idP/idP; rewrite dvdp_eq; set c2 := _ ^+ _; set q2 := _ %/ _. have sn0 : c1 * c2 != 0. by rewrite !mulf_neq0 // expf_eq0 lead_coef_eq0 (negPf dn0) andbF. - pose quo := (c1 * lead_coef n ^+ scalp m n) *: q2 - c2 *: (m %/ n) * q1. + pose quo := (c1 * lead_coef n ^+ scalp m n) *: q2 - c2 *: (m %/ n) * q1. move/eqP=> Eq2; apply: (@eq_dvdp _ quo _ _ sn0). rewrite mulrDl mulNr -!scalerAl -!mulrA -Eq1 -Eq2 -scalerAr !scalerA. rewrite mulrC [_ * c2]mulrC mulrA -[((_ * _) * _) *: _]scalerA -scalerBr. @@ -1314,7 +1211,7 @@ apply/idP/idP; rewrite dvdp_eq; set c2 := _ ^+ _; set q2 := _ %/ _. have sn0 : c1 * c2 * lead_coef n ^+ scalp m n != 0. rewrite !mulf_neq0 // expf_eq0 lead_coef_eq0 ?(negPf dn0) ?andbF //. by rewrite (negPf nn0) andbF. -move/eqP=> Eq2; apply: (@eq_dvdp _ (c2 *: (m %/ n) * q1 + c1 *: q2) _ _ sn0). +move/eqP=> Eq2; apply: (@eq_dvdp _ (c2 *: (m %/ n) * q1 + c1 *: q2) _ _ sn0). rewrite -scalerA divp_eq scalerDr -!scalerA Eq2 scalerAl scalerAr Eq1. by rewrite scalerAl mulrDl mulrA. Qed. @@ -1322,35 +1219,32 @@ Qed. Lemma dvdp_trans : transitive (@dvdp R). Proof. move=> n d m. -case: (altP (d =P 0)) => [-> | dn0]; first by move/dvd0pP->. -case: (altP (n =P 0)) => [-> | nn0]; first by move=> _ /dvd0pP ->. +case: (eqVneq d 0) => [-> /dvd0pP -> // | dn0]. +case: (eqVneq n 0) => [-> _ /dvd0pP -> // | nn0]. rewrite dvdp_eq; set c1 := _ ^+ _; set q1 := _ %/ _; move/eqP=> Hq1. rewrite dvdp_eq; set c2 := _ ^+ _; set q2 := _ %/ _; move/eqP=> Hq2. have sn0 : c1 * c2 != 0 by rewrite mulf_neq0 // expf_neq0 // lead_coef_eq0. by apply: (@eq_dvdp _ (q2 * q1) _ _ sn0); rewrite -scalerA Hq2 scalerAr Hq1 mulrA. Qed. -Lemma dvdp_mulIl p q : p %| p * q. -Proof. by apply: dvdp_mulr; apply: dvdpp. Qed. +Lemma dvdp_mulIl p q : p %| p * q. Proof. exact/dvdp_mulr/dvdpp. Qed. -Lemma dvdp_mulIr p q : q %| p * q. -Proof. by apply: dvdp_mull; apply: dvdpp. Qed. +Lemma dvdp_mulIr p q : q %| p * q. Proof. exact/dvdp_mull/dvdpp. Qed. Lemma dvdp_mul2r r p q : r != 0 -> (p * r %| q * r) = (p %| q). Proof. move=> nzr. -case: (eqVneq p 0) => [-> | pn0]. +have [-> | pn0] := eqVneq p 0. by rewrite mul0r !dvd0p mulf_eq0 (negPf nzr) orbF. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite mul0r !dvdp0. +have [-> | qn0] := eqVneq q 0; first by rewrite mul0r !dvdp0. apply/idP/idP; last by move=> ?; rewrite dvdp_mul ?dvdpp. rewrite dvdp_eq; set c := _ ^+ _; set x := _ %/ _; move/eqP=> Hx. -apply: (@eq_dvdp c x). - by rewrite expf_neq0 // lead_coef_eq0 mulf_neq0. -by apply: (GRing.mulIf nzr); rewrite -GRing.mulrA -GRing.scalerAl. +apply: (@eq_dvdp c x); first by rewrite expf_neq0 // lead_coef_eq0 mulf_neq0. +by apply: (mulIf nzr); rewrite -mulrA -scalerAl. Qed. Lemma dvdp_mul2l r p q: r != 0 -> (r * p %| r * q) = (p %| q). -Proof. by rewrite ![r * _]GRing.mulrC; apply: dvdp_mul2r. Qed. +Proof. by rewrite ![r * _]mulrC; apply: dvdp_mul2r. Qed. Lemma ltn_divpr d p q : d %| q -> (size p < size (q %/ d)) = (size (p * d) < size q). @@ -1360,11 +1254,9 @@ Lemma dvdp_exp d k p : 0 < k -> d %| p -> d %| (p ^+ k). Proof. by case: k => // k _ d_dv_m; rewrite exprS dvdp_mulr. Qed. Lemma dvdp_exp2l d k l : k <= l -> d ^+ k %| d ^+ l. -Proof. -by move/subnK <-; rewrite exprD dvdp_mull // ?lead_coef_exp ?unitrX. -Qed. +Proof. by move/subnK <-; rewrite exprD dvdp_mull // ?lead_coef_exp ?unitrX. Qed. -Lemma dvdp_Pexp2l d k l : 1 < size d -> (d ^+ k %| d ^+ l) = (k <= l). +Lemma dvdp_Pexp2l d k l : 1 < size d -> (d ^+ k %| d ^+ l) = (k <= l). Proof. move=> sd; case: leqP => [|gt_n_m]; first exact: dvdp_exp2l. have dn0 : d != 0 by rewrite -size_poly_gt0; apply: ltn_trans sd. @@ -1375,7 +1267,7 @@ Qed. Lemma dvdp_exp2r p q k : p %| q -> p ^+ k %| q ^+ k. Proof. -case: (eqVneq p 0) => [-> | pn0]; first by move/dvd0pP->. +case: (eqVneq p 0) => [-> /dvd0pP -> // | pn0]. rewrite dvdp_eq; set c := _ ^+ _; set t := _ %/ _; move/eqP=> e. apply: (@eq_dvdp (c ^+ k) (t ^+ k)); first by rewrite !expf_neq0 ?lead_coef_eq0. by rewrite -exprMn -exprZn; congr (_ ^+ k). @@ -1384,17 +1276,10 @@ Qed. Lemma dvdp_exp_sub p q k l: p != 0 -> (p ^+ k %| q * p ^+ l) = (p ^+ (k - l) %| q). Proof. -move=> pn0; case: (leqP k l)=> hkl. +move=> pn0; case: (leqP k l)=> [|/ltnW] hkl. move: (hkl); rewrite -subn_eq0; move/eqP->; rewrite expr0 dvd1p. - apply: dvdp_mull; case: (ltnP 1%N (size p)) => sp. - by rewrite dvdp_Pexp2l. - move: sp; case esp: (size p) => [|sp]. - by move/eqP: esp; rewrite size_poly_eq0 (negPf pn0). - rewrite ltnS leqn0; move/eqP=> sp0; move/eqP: esp; rewrite sp0. - by case/size_poly1P => c cn0 ->; move/subnK: hkl<-; rewrite exprD dvdp_mulIr. -rewrite -{1}[k](@subnK l) 1?ltnW// exprD dvdp_mul2r//. -elim: l {hkl}=> [|l ihl]; first by rewrite expr0 oner_eq0. -by rewrite exprS mulf_neq0. + exact/dvdp_mull/dvdp_exp2l. +by rewrite -[in LHS](subnK hkl) exprD dvdp_mul2r // expf_eq0 (negPf pn0) andbF. Qed. Lemma dvdp_XsubCl p x : ('X - x%:P) %| p = root p x. @@ -1417,12 +1302,11 @@ move=> rrs; case/(uniq_roots_prod_XsubC rrs)=> q ->. by apply: dvdp_mull; rewrite // (eqP (monic_prod_XsubC _)) unitr1. Qed. - -Lemma root_bigmul : forall x (ps : seq {poly R}), +Lemma root_bigmul x (ps : seq {poly R}) : ~~root (\big[*%R/1]_(p <- ps) p) x = all (fun p => ~~ root p x) ps. Proof. -move=> x; elim; first by rewrite big_nil root1. -by move=> p ps ihp; rewrite big_cons /= rootM negb_or ihp. +elim: ps => [|p ps ihp]; first by rewrite big_nil root1. +by rewrite big_cons /= rootM negb_or ihp. Qed. Lemma eqpP m n : @@ -1432,11 +1316,11 @@ Proof. apply: (iffP idP) => [| [[c1 c2]/andP[nz_c1 nz_c2 eq_cmn]]]; last first. rewrite /eqp (@eq_dvdp c2 c1%:P) -?eq_cmn ?mul_polyC // (@eq_dvdp c1 c2%:P) //. by rewrite eq_cmn mul_polyC. -case: (eqVneq m 0) => [-> | m_nz]. - by case/andP => /dvd0pP -> _; exists (1, 1); rewrite ?scaler0 // oner_eq0. -case: (eqVneq n 0) => [-> | n_nz]. - by case/andP => _ /dvd0pP ->; exists (1, 1); rewrite ?scaler0 // oner_eq0. -case/andP; rewrite !dvdp_eq; set c1 := _ ^+ _; set c2 := _ ^+ _. +case: (eqVneq m 0) => [-> /andP [/dvd0pP -> _] | m_nz]. + by exists (1, 1); rewrite ?scaler0 // oner_eq0. +case: (eqVneq n 0) => [-> /andP [_ /dvd0pP ->] | n_nz /andP []]. + by exists (1, 1); rewrite ?scaler0 // oner_eq0. +rewrite !dvdp_eq; set c1 := _ ^+ _; set c2 := _ ^+ _. set q1 := _ %/ _; set q2 := _ %/ _; move/eqP => Hq1 /eqP Hq2; have Hc1 : c1 != 0 by rewrite expf_eq0 lead_coef_eq0 negb_and m_nz orbT. have Hc2 : c2 != 0 by rewrite expf_eq0 lead_coef_eq0 negb_and n_nz orbT. @@ -1448,7 +1332,7 @@ rewrite mulf_eq0; case/norP=> nz_q1 nz_q2. have: size q2 <= 1%N. have:= size_mul nz_q1 nz_q2; rewrite def_q12 size_polyC mulf_neq0 //=. by rewrite polySpred // => ->; rewrite leq_addl. -rewrite leq_eqVlt ltnS leqn0 size_poly_eq0 (negPf nz_q2) orbF. +rewrite leq_eqVlt ltnS size_poly_leq0 (negPf nz_q2) orbF. case/size_poly1P=> c cn0 cqe; exists (c2, c); first by rewrite Hc2. by rewrite Hq2 -mul_polyC -cqe. Qed. @@ -1458,12 +1342,10 @@ Proof. move=> /eqpP [[c1 c2] /= /andP [nz_c1 nz_c2]] eq. have/(congr1 lead_coef) := eq; rewrite !lead_coefZ. move=> eqC; apply/(@mulfI _ c2%:P); rewrite ?polyC_eq0 //. -rewrite !mul_polyC scalerA -eqC mulrC -scalerA eq. -by rewrite !scalerA mulrC. +by rewrite !mul_polyC scalerA -eqC mulrC -scalerA eq !scalerA mulrC. Qed. -Lemma eqpxx : reflexive (@eqp R). -Proof. by move=> p; rewrite /eqp dvdpp. Qed. +Lemma eqpxx : reflexive (@eqp R). Proof. by move=> p; rewrite /eqp dvdpp. Qed. Hint Resolve eqpxx : core. @@ -1478,23 +1360,22 @@ Qed. Lemma eqp_ltrans : left_transitive (@eqp R). Proof. -move=> p q r pq. -by apply/idP/idP=> e; apply: eqp_trans e; rewrite // eqp_sym. +by move=> p q r pq; apply/idP/idP; apply: eqp_trans; rewrite // eqp_sym. Qed. Lemma eqp_rtrans : right_transitive (@eqp R). Proof. by move=> x y xy z; rewrite eqp_sym (eqp_ltrans xy) eqp_sym. Qed. -Lemma eqp0 : forall p, (p %= 0) = (p == 0). +Lemma eqp0 p : (p %= 0) = (p == 0). Proof. -move=> p; case: eqP; move/eqP=> Ep; first by rewrite (eqP Ep) eqpxx. -by apply/negP; case/andP=> _; rewrite /dvdp modp0 (negPf Ep). +have [->|Ep] := eqVneq; first by rewrite ?eqpxx. +by apply/negP => /andP [_]; rewrite /dvdp modp0 (negPf Ep). Qed. Lemma eqp01 : 0 %= (1 : {poly R}) = false. Proof. -case abs : (0 %= 1) => //; case/eqpP: abs=> [[c1 c2]] /andP [c1n0 c2n0] /=. -by rewrite scaler0 alg_polyC; move/eqP; rewrite eq_sym polyC_eq0 (negbTE c2n0). +case: eqpP => // -[[c1 c2]] /andP [c1n0 c2n0] /= /esym /eqP. +by rewrite scaler0 alg_polyC polyC_eq0 (negPf c2n0). Qed. Lemma eqp_scale p c : c != 0 -> c *: p %= p. @@ -1505,9 +1386,8 @@ Qed. Lemma eqp_size p q : p %= q -> size p = size q. Proof. -case: (q =P 0); move/eqP => Eq; first by rewrite (eqP Eq) eqp0; move/eqP->. -rewrite eqp_sym; case: (p =P 0); move/eqP => Ep. - by rewrite (eqP Ep) eqp0; move/eqP->. +have [->|Eq] := eqVneq q 0; first by rewrite eqp0; move/eqP->. +rewrite eqp_sym; have [->|Ep] := eqVneq p 0; first by rewrite eqp0; move/eqP->. by case/andP => Dp Dq; apply: anti_leq; rewrite !dvdp_leq. Qed. @@ -1515,7 +1395,7 @@ Lemma size_poly_eq1 p : (size p == 1%N) = (p %= 1). Proof. apply/size_poly1P/idP=> [[c cn0 ep] |]. by apply/eqpP; exists (1, c); rewrite ?oner_eq0 // alg_polyC scale1r. -by move/eqp_size; rewrite size_poly1; move/eqP; move/size_poly1P. +by move/eqp_size; rewrite size_poly1; move/eqP/size_poly1P. Qed. Lemma polyXsubC_eqp1 (x : R) : ('X - x%:P %= 1) = false. @@ -1525,11 +1405,9 @@ Lemma dvdp_eqp1 p q : p %| q -> q %= 1 -> p %= 1. Proof. move=> dpq hq. have sizeq : size q == 1%N by rewrite size_poly_eq1. -have n0q : q != 0. - by case abs: (q == 0) => //; move: hq; rewrite (eqP abs) eqp01. -rewrite -size_poly_eq1 eqn_leq -{1}(eqP sizeq) dvdp_leq //=. -case p0 : (size p == 0%N); last by rewrite neq0_lt0n. -by move: dpq; rewrite size_poly_eq0 in p0; rewrite (eqP p0) dvd0p (negbTE n0q). +have n0q : q != 0 by case: eqP hq => // ->; rewrite eqp01. +rewrite -size_poly_eq1 eqn_leq -{1}(eqP sizeq) dvdp_leq //= size_poly_gt0. +by apply/eqP => p0; move: dpq n0q; rewrite p0 dvd0p => ->. Qed. Lemma eqp_dvdr q p d: p %= q -> d %| p = (d %| q). @@ -1546,10 +1424,10 @@ by rewrite /eqp; case/andP=> dd' d'd dp; apply: (dvdp_trans d'd). Qed. Lemma dvdp_scaler c m n : c != 0 -> m %| c *: n = (m %| n). -Proof. by move=> cn0; apply: eqp_dvdr; apply: eqp_scale. Qed. +Proof. by move=> cn0; exact/eqp_dvdr/eqp_scale. Qed. Lemma dvdp_scalel c m n : c != 0 -> (c *: m %| n) = (m %| n). -Proof. by move=> cn0; apply: eqp_dvdl; apply: eqp_scale. Qed. +Proof. by move=> cn0; exact/eqp_dvdl/eqp_scale. Qed. Lemma dvdp_opp d p : d %| (- p) = (d %| p). Proof. by apply: eqp_dvdr; rewrite -scaleN1r eqp_scale ?oppr_eq0 ?oner_eq0. Qed. @@ -1560,16 +1438,16 @@ Proof. by move=> nz_r; rewrite /eqp !dvdp_mul2r. Qed. Lemma eqp_mul2l r p q: r != 0 -> (r * p %= r * q) = (p %= q). Proof. by move=> nz_r; rewrite /eqp !dvdp_mul2l. Qed. -Lemma eqp_mull r p q: (q %= r) -> (p * q %= p * r). +Lemma eqp_mull r p q: q %= r -> p * q %= p * r. Proof. case/eqpP=> [[c d]] /andP [c0 d0 e]; apply/eqpP; exists (c, d); rewrite ?c0 //. by rewrite scalerAr e -scalerAr. Qed. -Lemma eqp_mulr q p r : (p %= q) -> (p * r %= q * r). +Lemma eqp_mulr q p r : p %= q -> p * r %= q * r. Proof. by move=> epq; rewrite ![_ * r]mulrC eqp_mull. Qed. -Lemma eqp_exp p q k : p %= q -> p ^+ k %= q ^+ k. +Lemma eqp_exp p q k : p %= q -> p ^+ k %= q ^+ k. Proof. move=> pq; elim: k=> [|k ihk]; first by rewrite !expr0 eqpxx. by rewrite !exprS (@eqp_trans (q * p ^+ k)) // (eqp_mulr, eqp_mull). @@ -1578,8 +1456,8 @@ Qed. Lemma polyC_eqp1 (c : R) : (c%:P %= 1) = (c != 0). Proof. apply/eqpP/idP => [[[x y]] |nc0] /=. - case c0: (c == 0); rewrite // alg_polyC (eqP c0) scaler0. - by case/andP=> _ /=; move/negbTE<-; move/eqP; rewrite eq_sym polyC_eq0. + case: (eqVneq c) => [->|] //= /andP [_] /negPf <- /eqP. + by rewrite alg_polyC scaler0 eq_sym polyC_eq0. exists (1, c); first by rewrite nc0 /= oner_neq0. by rewrite alg_polyC scale1r. Qed. @@ -1590,14 +1468,13 @@ Proof. by move/eqp_dvdl->; rewrite dvd1p. Qed. Lemma dvdp_size_eqp p q : p %| q -> size p == size q = (p %= q). Proof. move=> pq; apply/idP/idP; last by move/eqp_size->. -case (q =P 0)=> [->|]; [|move/eqP => Hq]. - by rewrite size_poly0 size_poly_eq0; move/eqP->; rewrite eqpxx. -case (p =P 0)=> [->|]; [|move/eqP => Hp]. - by rewrite size_poly0 eq_sym size_poly_eq0; move/eqP->; rewrite eqpxx. +have [->|Hq] := eqVneq q 0; first by rewrite size_poly0 size_poly_eq0 eqp0. +have [->|Hp] := eqVneq p 0. + by rewrite size_poly0 eq_sym size_poly_eq0 eqp_sym eqp0. move: pq; rewrite dvdp_eq; set c := _ ^+ _; set x := _ %/ _; move/eqP=> eqpq. -move: (eqpq); move/(congr1 (size \o (@polyseq R)))=> /=. -have cn0 : c != 0 by rewrite expf_neq0 // lead_coef_eq0. -rewrite (@eqp_size _ q); last by apply: eqp_scale. +have /= := congr1 (size \o @polyseq R) eqpq. +have cn0 : c != 0 by rewrite expf_neq0 // lead_coef_eq0. +rewrite (@eqp_size _ q); last exact: eqp_scale. rewrite size_mul ?p0 // => [-> HH|]; last first. apply/eqP=> HH; move: eqpq; rewrite HH mul0r. by move/eqP; rewrite scale_poly_eq0 (negPf Hq) (negPf cn0). @@ -1611,8 +1488,7 @@ Qed. Lemma eqp_root p q : p %= q -> root p =1 root q. Proof. move/eqpP=> [[c d]] /andP [c0 d0 e] x; move/negPf:c0=>c0; move/negPf:d0=>d0. -rewrite rootE -[_==_]orFb -c0 -mulf_eq0 -hornerZ e hornerZ. -by rewrite mulf_eq0 d0. +by rewrite rootE -[_==_]orFb -c0 -mulf_eq0 -hornerZ e hornerZ mulf_eq0 d0. Qed. Lemma eqp_rmod_mod p q : rmodp p q %= modp p q. @@ -1632,7 +1508,7 @@ Lemma dvd_eqp_divl d p q (dvd_dp : d %| q) (eq_pq : p %= q) : p %/ d %= q %/ d. Proof. case: (eqVneq q 0) eq_pq=> [->|q_neq0]; first by rewrite eqp0=> /eqP->. -have d_neq0: d != 0 by apply: contraL dvd_dp=> /eqP->; rewrite dvd0p. +have d_neq0: d != 0 by apply: contraTneq dvd_dp=> ->; rewrite dvd0p. move=> eq_pq; rewrite -(@eqp_mul2r d) // !divpK // ?(eqp_dvdr _ eq_pq) //. rewrite (eqp_ltrans (eqp_scale _ _)) ?lc_expn_scalp_neq0 //. by rewrite (eqp_rtrans (eqp_scale _ _)) ?lc_expn_scalp_neq0. @@ -1659,7 +1535,7 @@ Qed. Lemma gcdp0 : right_id 0 gcdp. Proof. move=> p; have:= gcd0p p; rewrite /gcdp /gcdp_rec size_poly0 size_poly_gt0. -by rewrite if_neg; case: ifP => /= p0; rewrite ?(eqxx, p0) // (eqP p0). +by case: eqVneq => //= ->; rewrite eqxx. Qed. Lemma gcdpE p q : @@ -1673,54 +1549,44 @@ pose gcdpE_rec := fix gcdpE_rec (n : nat) (pp qq : {poly R}) {struct n} := have Irec: forall k l p q, size q <= k -> size q <= l -> size q < size p -> gcdpE_rec k p q = gcdpE_rec l p q. + elim=> [|m Hrec] [|n] //= p1 q1. - - rewrite leqn0 size_poly_eq0; move/eqP=> -> _. - rewrite size_poly0 size_poly_gt0 modp0 => nzp. - by rewrite (negPf nzp); case: n => [|n] /=; rewrite mod0p eqxx. - - rewrite leqn0 size_poly_eq0 => _; move/eqP=> ->. - rewrite size_poly0 size_poly_gt0 modp0 => nzp. - by rewrite (negPf nzp); case: m {Hrec} => [|m] /=; rewrite mod0p eqxx. - case: ifP => Epq Sm Sn Sq //; rewrite ?Epq //. - case: (eqVneq q1 0) => [->|nzq]. + - move/size_poly_leq0P=> -> _; rewrite size_poly0 size_poly_gt0 modp0. + by move/negPf ->; case: n => [|n] /=; rewrite mod0p eqxx. + - move=> _ /size_poly_leq0P ->; rewrite size_poly0 size_poly_gt0 modp0. + by move/negPf ->; case: m {Hrec} => [|m] /=; rewrite mod0p eqxx. + case: eqP => Epq Sm Sn Sq //; have [->|nzq] := eqVneq q1 0. by case: n m {Sm Sn Hrec} => [|m] [|n] //=; rewrite mod0p eqxx. apply: Hrec; last by rewrite ltn_modp. by rewrite -ltnS (leq_trans _ Sm) // ltn_modp. by rewrite -ltnS (leq_trans _ Sn) // ltn_modp. -case: (eqVneq p 0) => [-> | nzp]. - by rewrite mod0p modp0 gcd0p gcdp0 if_same. -case: (eqVneq q 0) => [-> | nzq]. - by rewrite mod0p modp0 gcd0p gcdp0 if_same. -rewrite /gcdp /gcdp_rec. -case: ltnP; rewrite (negPf nzp, negPf nzq) //=. - move=> ltpq; rewrite ltn_modp (negPf nzp) //=. - rewrite -(ltn_predK ltpq) /=; case: eqP => [->|]. +have [->|nzp] := eqVneq p 0; first by rewrite mod0p modp0 gcd0p gcdp0 if_same. +have [->|nzq] := eqVneq q 0; first by rewrite mod0p modp0 gcd0p gcdp0 if_same. +rewrite /gcdp /gcdp_rec !ltn_modp !(negPf nzp, negPf nzq) /=. +have [ltpq|leqp] := ltnP; rewrite !(negPf nzp, negPf nzq) /= polySpred //. + have [->|nzqp] := eqVneq. by case: (size p) => [|[|s]]; rewrite /= modp0 (negPf nzp) // mod0p eqxx. - move/eqP=> nzqp; rewrite (negPf nzp). apply: Irec => //; last by rewrite ltn_modp. - by rewrite -ltnS (ltn_predK ltpq) (leq_trans _ ltpq) ?leqW // ltn_modp. + by rewrite -ltnS -polySpred // (leq_trans _ ltpq) ?leqW // ltn_modp. by rewrite ltnW // ltn_modp. -move=> leqp; rewrite ltn_modp (negPf nzq) //=. -have p_gt0: size p > 0 by rewrite size_poly_gt0. -rewrite -(prednK p_gt0) /=; case: eqP => [->|]. +case: eqVneq => [->|nzpq]. by case: (size q) => [|[|s]]; rewrite /= modp0 (negPf nzq) // mod0p eqxx. -move/eqP=> nzpq; rewrite (negPf nzq); apply: Irec => //; rewrite ?ltn_modp //. - by rewrite -ltnS (prednK p_gt0) (leq_trans _ leqp) // ltn_modp. +apply: Irec => //; rewrite ?ltn_modp //. + by rewrite -ltnS -polySpred // (leq_trans _ leqp) // ltn_modp. by rewrite ltnW // ltn_modp. Qed. Lemma size_gcd1p p : size (gcdp 1 p) = 1%N. Proof. -rewrite gcdpE size_polyC oner_eq0 /= modp1; case: ltnP. +rewrite gcdpE size_polyC oner_eq0 /= modp1; have [|/size1_polyC ->] := ltnP. by rewrite gcd0p size_polyC oner_eq0. -move/size1_polyC=> e; rewrite e. -case p00: (p`_0 == 0); first by rewrite (eqP p00) modp0 gcdp0 size_poly1. -by rewrite modpC ?p00 // gcd0p size_polyC p00. +have [->|p00] := eqVneq p`_0 0; first by rewrite modp0 gcdp0 size_poly1. +by rewrite modpC // gcd0p size_polyC p00. Qed. Lemma size_gcdp1 p : size (gcdp p 1) = 1%N. -rewrite gcdpE size_polyC oner_eq0 /= modp1; case: ltnP; last first. - by rewrite gcd0p size_polyC oner_eq0. -rewrite ltnS leqn0 size_poly_eq0; move/eqP->; rewrite gcdp0 modp0 size_polyC. -by rewrite oner_eq0. +Proof. +rewrite gcdpE size_polyC oner_eq0 /= modp1 ltnS; case: leqP. + by move/size_poly_leq0P->; rewrite gcdp0 modp0 size_polyC oner_eq0. +by rewrite gcd0p size_polyC oner_eq0. Qed. Lemma gcdpp : idempotent gcdp. @@ -1740,11 +1606,9 @@ suffices /IHr/andP[E1 E2]: minn (size q) (size (p %% q)) < r. by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp. Qed. -Lemma dvdp_gcdl p q : gcdp p q %| p. -Proof. by case/andP: (dvdp_gcdlr p q). Qed. +Lemma dvdp_gcdl p q : gcdp p q %| p. Proof. by case/andP: (dvdp_gcdlr p q). Qed. -Lemma dvdp_gcdr p q :gcdp p q %| q. -Proof. by case/andP: (dvdp_gcdlr p q). Qed. +Lemma dvdp_gcdr p q :gcdp p q %| q. Proof. by case/andP: (dvdp_gcdlr p q). Qed. Lemma leq_gcdpl p q : p != 0 -> size (gcdp p q) <= size p. Proof. by move=> pn0; move: (dvdp_gcdl p q); apply: dvdp_leq. Qed. @@ -1766,16 +1630,16 @@ apply: IHr => //; last by rewrite -(dvdp_mod _ dv_n). by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp. Qed. -Lemma gcdpC : forall p q, gcdp p q %= gcdp q p. -Proof. by move=> p q; rewrite /eqp !dvdp_gcd !dvdp_gcdl !dvdp_gcdr. Qed. +Lemma gcdpC p q : gcdp p q %= gcdp q p. +Proof. by rewrite /eqp !dvdp_gcd !dvdp_gcdl !dvdp_gcdr. Qed. Lemma gcd1p p : gcdp 1 p %= 1. Proof. rewrite -size_poly_eq1 gcdpE size_poly1; case: ltnP. by rewrite modp1 gcd0p size_poly1 eqxx. move/size1_polyC=> e; rewrite e. -case p00: (p`_0 == 0); first by rewrite (eqP p00) modp0 gcdp0 size_poly1. -by rewrite modpC ?p00 // gcd0p size_polyC p00. +have [->|p00] := eqVneq p`_0 0; first by rewrite modp0 gcdp0 size_poly1. +by rewrite modpC // gcd0p size_polyC p00. Qed. Lemma gcdp1 p : gcdp p 1 %= 1. @@ -1784,25 +1648,25 @@ Proof. by rewrite (eqp_ltrans (gcdpC _ _)) gcd1p. Qed. Lemma gcdp_addl_mul p q r: gcdp r (p * r + q) %= gcdp r q. Proof. suff h m n d : gcdp d n %| gcdp d (m * d + n). - apply/andP; split => //; rewrite {2}(_: q = (-p) * r + (p * r + q)) ?H //. - by rewrite GRing.mulNr GRing.addKr. + apply/andP; split => //. + by rewrite {2}(_: q = (-p) * r + (p * r + q)) ?H // mulNr addKr. by rewrite dvdp_gcd dvdp_gcdl /= dvdp_addr ?dvdp_gcdr ?dvdp_mull ?dvdp_gcdl. Qed. Lemma gcdp_addl m n : gcdp m (m + n) %= gcdp m n. -Proof. by rewrite -{2}(mul1r m) gcdp_addl_mul. Qed. +Proof. by rewrite -[m in m + _]mul1r gcdp_addl_mul. Qed. Lemma gcdp_addr m n : gcdp m (n + m) %= gcdp m n. Proof. by rewrite addrC gcdp_addl. Qed. Lemma gcdp_mull m n : gcdp n (m * n) %= n. Proof. -case: (eqVneq n 0) => [-> | nn0]; first by rewrite gcd0p mulr0 eqpxx. -case: (eqVneq m 0) => [-> | mn0]; first by rewrite mul0r gcdp0 eqpxx. -rewrite gcdpE modp_mull gcd0p size_mul //; case: ifP; first by rewrite eqpxx. -rewrite (polySpred mn0) addSn /= -{1}[size n]add0n ltn_add2r; move/negbT. -rewrite -ltnNge prednK ?size_poly_gt0 // leq_eqVlt ltnS leqn0 size_poly_eq0. -rewrite (negPf mn0) orbF; case/size_poly1P=> c cn0 -> {mn0 m}; rewrite mul_polyC. +have [-> | nn0] := eqVneq n 0; first by rewrite gcd0p mulr0 eqpxx. +have [-> | mn0] := eqVneq m 0; first by rewrite mul0r gcdp0 eqpxx. +rewrite gcdpE modp_mull gcd0p size_mul //; case: leqP; last by rewrite eqpxx. +rewrite (polySpred mn0) addSn /= -[n in _ <= n]add0n leq_add2r -ltnS. +rewrite -polySpred //= leq_eqVlt ltnS size_poly_leq0 (negPf mn0) orbF. +case/size_poly1P=> c cn0 -> {mn0 m}; rewrite mul_polyC. suff -> : n %% (c *: n) = 0 by rewrite gcd0p; apply: eqp_scale. by apply/modp_eq0P; rewrite dvdp_scalel. Qed. @@ -1826,21 +1690,21 @@ Qed. Lemma dvdp_gcd_idl m n : m %| n -> gcdp m n %= m. Proof. -case: (eqVneq m 0) => [-> | mn0]. +have [-> | mn0] := eqVneq m 0. by rewrite dvd0p => /eqP ->; rewrite gcdp0 eqpxx. -rewrite dvdp_eq; move/eqP; move/(f_equal (gcdp m)) => h. -apply: eqp_trans (gcdp_mull (n %/ m) _); rewrite -h eqp_sym gcdp_scaler //. -by rewrite expf_neq0 // lead_coef_eq0. +rewrite dvdp_eq; move/eqP/(f_equal (gcdp m)) => h. +apply: eqp_trans (gcdp_mull (n %/ m) _). +by rewrite -h eqp_sym gcdp_scaler // expf_neq0 // lead_coef_eq0. Qed. Lemma dvdp_gcd_idr m n : n %| m -> gcdp m n %= n. -Proof. by move/dvdp_gcd_idl => h; apply: eqp_trans h; apply: gcdpC. Qed. +Proof. by move/dvdp_gcd_idl; exact/eqp_trans/gcdpC. Qed. Lemma gcdp_exp p k l : gcdp (p ^+ k) (p ^+ l) %= p ^+ minn k l. Proof. wlog leqmn: k l / k <= l. move=> hwlog; case: (leqP k l); first exact: hwlog. - by move/ltnW; rewrite minnC; move/hwlog=> h; apply: eqp_trans h; apply: gcdpC. + by move/ltnW; rewrite minnC; move/hwlog; apply/eqp_trans/gcdpC. rewrite (minn_idPl leqmn); move/subnK: leqmn<-; rewrite exprD. by apply: eqp_trans (gcdp_mull _ _) _; apply: eqpxx. Qed. @@ -1859,7 +1723,8 @@ move=> eqr; rewrite /eqp !(dvdp_gcd, dvdp_gcdl, andbT) /=. by rewrite -(eqp_dvdr _ eqr) dvdp_gcdr (eqp_dvdr _ eqr) dvdp_gcdr. Qed. -Lemma eqp_gcdl r p q : p %= q -> gcdp p r %= gcdp q r. +Lemma eqp_gcdl r p q : p %= q -> gcdp p r %= gcdp q r. +Proof. move=> eqr; rewrite /eqp !(dvdp_gcd, dvdp_gcdr, andbT) /=. by rewrite -(eqp_dvdr _ eqr) dvdp_gcdl (eqp_dvdr _ eqr) dvdp_gcdl. Qed. @@ -1872,34 +1737,33 @@ Qed. Lemma eqp_rgcd_gcd p q : rgcdp p q %= gcdp p q. Proof. -move: (leqnn (minn (size p) (size q))); move: {2}(minn (size p) (size q)) => n. +move: {2}(minn (size p) (size q)) (leqnn (minn (size p) (size q))) => n. elim: n p q => [p q|n ihn p q hs]. rewrite leqn0 /minn; case: ltnP => _; rewrite size_poly_eq0; move/eqP->. by rewrite gcd0p rgcd0p eqpxx. by rewrite gcdp0 rgcdp0 eqpxx. -case: (eqVneq p 0) => [-> | pn0]; first by rewrite gcd0p rgcd0p eqpxx. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite gcdp0 rgcdp0 eqpxx. +have [-> | pn0] := eqVneq p 0; first by rewrite gcd0p rgcd0p eqpxx. +have [-> | qn0] := eqVneq q 0; first by rewrite gcdp0 rgcdp0 eqpxx. rewrite gcdpE rgcdpE; case: ltnP => sp. - have e := (eqp_rmod_mod q p); move: (e); move/(eqp_gcdl p) => h. - apply: eqp_trans h; apply: ihn; rewrite (eqp_size e) geq_min. - by rewrite -ltnS (leq_trans _ hs) // (minn_idPl (ltnW _)) ?ltn_modp. -have e := (eqp_rmod_mod p q); move: (e); move/(eqp_gcdl q) => h. -apply: eqp_trans h; apply: ihn; rewrite (eqp_size e) geq_min. -by rewrite -ltnS (leq_trans _ hs) // (minn_idPr _) ?ltn_modp. + have e := eqp_rmod_mod q p; apply/eqp_trans/ihn: (eqp_gcdl p e). + rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) //. + by rewrite (minn_idPl (ltnW _)) ?ltn_modp. +have e := eqp_rmod_mod p q; apply/eqp_trans/ihn: (eqp_gcdl q e). +rewrite (eqp_size e) geq_min -ltnS (leq_trans _ hs) //. +by rewrite (minn_idPr _) ?ltn_modp. Qed. Lemma gcdp_modr m n : gcdp m (n %% m) %= gcdp m n. Proof. -case: (eqVneq m 0) => [-> | mn0]; first by rewrite modp0 eqpxx. +have [-> | mn0] := eqVneq m 0; first by rewrite modp0 eqpxx. have : (lead_coef m) ^+ (scalp n m) != 0 by rewrite expf_neq0 // lead_coef_eq0. -move/gcdp_scaler; move/(_ m n) => h; apply: eqp_trans h; rewrite divp_eq. -by rewrite eqp_sym gcdp_addl_mul. +move/(gcdp_scaler m n); apply/eqp_trans. +by rewrite divp_eq eqp_sym gcdp_addl_mul. Qed. Lemma gcdp_modl m n : gcdp (m %% n) n %= gcdp m n. Proof. -apply: eqp_trans (gcdpC _ _) _; apply: eqp_trans (gcdp_modr _ _) _. -exact: gcdpC. +apply: eqp_trans (gcdpC _ _); apply: eqp_trans (gcdp_modr _ _); exact: gcdpC. Qed. Lemma gcdp_def d m n : @@ -1915,33 +1779,26 @@ Definition coprimep p q := size (gcdp p q) == 1%N. Lemma coprimep_size_gcd p q : coprimep p q -> size (gcdp p q) = 1%N. Proof. by rewrite /coprimep=> /eqP. Qed. -Lemma coprimep_def p q : (coprimep p q) = (size (gcdp p q) == 1%N). +Lemma coprimep_def p q : coprimep p q = (size (gcdp p q) == 1%N). Proof. done. Qed. -Lemma coprimep_scalel c m n : - c != 0 -> coprimep (c *: m) n = coprimep m n. +Lemma coprimep_scalel c m n : c != 0 -> coprimep (c *: m) n = coprimep m n. Proof. by move=> ?; rewrite !coprimep_def (eqp_size (gcdp_scalel _ _ _)). Qed. -Lemma coprimep_scaler c m n: - c != 0 -> coprimep m (c *: n) = coprimep m n. +Lemma coprimep_scaler c m n: c != 0 -> coprimep m (c *: n) = coprimep m n. Proof. by move=> ?; rewrite !coprimep_def (eqp_size (gcdp_scaler _ _ _)). Qed. Lemma coprimepp p : coprimep p p = (size p == 1%N). Proof. by rewrite coprimep_def gcdpp. Qed. -Lemma gcdp_eqp1 p q : gcdp p q %= 1 = (coprimep p q). +Lemma gcdp_eqp1 p q : gcdp p q %= 1 = coprimep p q. Proof. by rewrite coprimep_def size_poly_eq1. Qed. Lemma coprimep_sym p q : coprimep p q = coprimep q p. -Proof. -by rewrite -!gcdp_eqp1; apply: eqp_ltrans; rewrite gcdpC. -Qed. +Proof. by rewrite -!gcdp_eqp1; apply: eqp_ltrans; rewrite gcdpC. Qed. Lemma coprime1p p : coprimep 1 p. -Proof. -rewrite /coprimep -[1%N](size_poly1 R); apply/eqP; apply: eqp_size. -exact: gcd1p. -Qed. +Proof. by rewrite /coprimep -[1%N](size_poly1 R); exact/eqP/eqp_size/gcd1p. Qed. Lemma coprimep1 p : coprimep p 1. Proof. by rewrite coprimep_sym; apply: coprime1p. Qed. @@ -1956,12 +1813,10 @@ Proof. by rewrite coprimep_sym coprimep0. Qed. Lemma coprimepP p q : reflect (forall d, d %| p -> d %| q -> d %= 1) (coprimep p q). Proof. -apply: (iffP idP)=> [|h]. - rewrite /coprimep; move/eqP=> hs d dvddp dvddq. - have dvddg: d %| gcdp p q by rewrite dvdp_gcd dvddp dvddq. - by apply: (dvdp_eqp1 dvddg); rewrite -size_poly_eq1; apply/eqP. -case/andP: (dvdp_gcdlr p q)=> h1 h2. -by rewrite /coprimep size_poly_eq1; apply: h. +rewrite /coprimep; apply: (iffP idP) => [/eqP hs d dvddp dvddq | h]. + have/dvdp_eqp1: d %| gcdp p q by rewrite dvdp_gcd dvddp dvddq. + by rewrite -size_poly_eq1 hs; exact. +by rewrite size_poly_eq1; case/andP: (dvdp_gcdlr p q); apply: h. Qed. Lemma coprimepPn p q : p != 0 -> @@ -1969,43 +1824,35 @@ Lemma coprimepPn p q : p != 0 -> Proof. move=> p0; apply: (iffP idP). by rewrite -gcdp_eqp1=> ng1; exists (gcdp p q); rewrite dvdpp /=. -case=> d; case/andP=> dg; apply: contra; rewrite -gcdp_eqp1=> g1. +case=> d /andP [dg]; apply: contra; rewrite -gcdp_eqp1=> g1. by move: dg; rewrite (eqp_dvdr _ g1) dvdp1 size_poly_eq1. Qed. Lemma coprimep_dvdl q p r : r %| q -> coprimep p q -> coprimep p r. Proof. -move=> rq cpq; apply/coprimepP=> d dp dr; move/coprimepP:cpq=> cpq'. -by apply: cpq'; rewrite // (dvdp_trans dr). +move=> rp /coprimepP cpq'; apply/coprimepP => d dp dr. +exact/cpq'/(dvdp_trans dr). Qed. -Lemma coprimep_dvdr p q r : - r %| p -> coprimep p q -> coprimep r q. +Lemma coprimep_dvdr p q r : r %| p -> coprimep p q -> coprimep r q. Proof. -move=> rp; rewrite ![coprimep _ q]coprimep_sym. -by move/coprimep_dvdl; apply. +by move=> rp; rewrite ![coprimep _ q]coprimep_sym; apply/coprimep_dvdl. Qed. - Lemma coprimep_modl p q : coprimep (p %% q) q = coprimep p q. Proof. -symmetry; rewrite !coprimep_def. -case: (ltnP (size p) (size q))=> hpq; first by rewrite modp_small. -by rewrite gcdpE ltnNge hpq. +rewrite !coprimep_def [in RHS]gcdpE. +by case: ltnP => // hpq; rewrite modp_small // gcdpE hpq. Qed. Lemma coprimep_modr q p : coprimep q (p %% q) = coprimep q p. Proof. by rewrite ![coprimep q _]coprimep_sym coprimep_modl. Qed. -Lemma rcoprimep_coprimep q p : rcoprimep q p = coprimep q p. -Proof. -by rewrite /coprimep /rcoprimep; rewrite (eqp_size (eqp_rgcd_gcd _ _)). -Qed. +Lemma rcoprimep_coprimep q p : rcoprimep q p = coprimep q p. +Proof. by rewrite /coprimep /rcoprimep (eqp_size (eqp_rgcd_gcd _ _)). Qed. Lemma eqp_coprimepr p q r : q %= r -> coprimep p q = coprimep p r. -Proof. -by rewrite -!gcdp_eqp1; move/(eqp_gcdr p) => h1; apply: (eqp_ltrans h1). -Qed. +Proof. by rewrite -!gcdp_eqp1; move/(eqp_gcdr p)/eqp_ltrans. Qed. Lemma eqp_coprimepl p q r : q %= r -> coprimep q p = coprimep r p. Proof. by rewrite !(coprimep_sym _ p); apply: eqp_coprimepr. Qed. @@ -2023,17 +1870,16 @@ Definition egcdp p q := else let e := egcdp_rec q p (size p) in (e.2, e.1). (* No provable egcd0p *) -Lemma egcdp0 p : egcdp p 0 = (1, 0). -Proof. by rewrite /egcdp size_poly0. Qed. +Lemma egcdp0 p : egcdp p 0 = (1, 0). Proof. by rewrite /egcdp size_poly0. Qed. Lemma egcdp_recP : forall k p q, q != 0 -> size q <= k -> size q <= size p -> let e := (egcdp_rec p q k) in [/\ size e.1 <= size q, size e.2 <= size p & gcdp p q %= e.1 * p + e.2 * q]. Proof. -elim=> [|k ihk] p q /= qn0; first by rewrite leqn0 size_poly_eq0 (negPf qn0). +elim=> [|k ihk] p q /= qn0; first by rewrite size_poly_leq0 (negPf qn0). move=> sqSn qsp; rewrite (negPf qn0). have sp : size p > 0 by apply: leq_trans qsp; rewrite size_poly_gt0. -case: (eqVneq (p %% q) 0) => [r0 | rn0] /=. +have [r0 | rn0] /= := eqVneq (p %%q) 0. rewrite r0 /egcdp_rec; case: k ihk sqSn => [|n] ihn sqSn /=. rewrite !scaler0 !mul0r subr0 add0r mul1r size_poly0 size_poly1. by rewrite dvdp_gcd_idr /dvdp ?r0. @@ -2042,64 +1888,60 @@ case: (eqVneq (p %% q) 0) => [r0 | rn0] /=. have h1 : size (p %% q) <= k. by rewrite -ltnS; apply: leq_trans sqSn; rewrite ltn_modp. have h2 : size (p %% q) <= size q by rewrite ltnW // ltn_modp. -have := (ihk q (p %% q) rn0 h1 h2). +have := ihk q (p %% q) rn0 h1 h2. case: (egcdp_rec _ _)=> u v /= => [[ihn'1 ihn'2 ihn'3]]. rewrite gcdpE ltnNge qsp //= (eqp_ltrans (gcdpC _ _)); split; last first. - apply: (eqp_trans ihn'3). rewrite mulrBl addrCA -scalerAl scalerAr -mulrA -mulrBr. by rewrite divp_eq addrAC subrr add0r eqpxx. - apply: (leq_trans (size_add _ _)). - case: (eqVneq v 0)=> [-> | vn0]. + have [-> | vn0] := eqVneq v 0. rewrite mul0r size_opp size_poly0 maxn0; apply: leq_trans ihn'1 _. exact: leq_modp. - case: (eqVneq (p %/ q) 0)=> [-> | qqn0]. + have [-> | qqn0] := eqVneq (p %/ q) 0. rewrite mulr0 size_opp size_poly0 maxn0; apply: leq_trans ihn'1 _. exact: leq_modp. rewrite geq_max (leq_trans ihn'1) ?leq_modp //= size_opp size_mul //. - move: (ihn'2); rewrite -(leq_add2r (size (p %/ q))). - have : size v + size (p %/ q) > 0 by rewrite addn_gt0 size_poly_gt0 vn0. - have : size q + size (p %/ q) > 0 by rewrite addn_gt0 size_poly_gt0 qn0. - do 2!move/prednK=> {1}<-; rewrite ltnS => h; apply: leq_trans h _. - rewrite size_divp // addnBA; last by apply: leq_trans qsp; apply: leq_pred. - rewrite addnC -addnBA ?leq_pred //; move: qn0; rewrite -size_poly_eq0 -lt0n. - by move/prednK=> {1}<-; rewrite subSnn addn1. + move: (ihn'2); rewrite (polySpred vn0) (polySpred qn0). + rewrite -(ltn_add2r (size (p %/ q))) !addSn /= ltnS; move/leq_trans; apply. + rewrite size_divp // addnBA ?addKn //. + by apply: leq_trans qsp; apply: leq_pred. - by rewrite size_scale // lc_expn_scalp_neq0. Qed. -Lemma egcdpP p q : p != 0 -> q != 0 -> forall (e := egcdp p q), +Lemma egcdpP p q : p != 0 -> q != 0 -> forall (e := egcdp p q), [/\ size e.1 <= size q, size e.2 <= size p & gcdp p q %= e.1 * p + e.2 * q]. Proof. -move=> pn0 qn0; rewrite /egcdp; case: (leqP (size q) (size p)) => /= hp. - by apply: egcdp_recP. -move/ltnW: hp => hp; case: (egcdp_recP pn0 (leqnn (size p)) hp) => h1 h2 h3. -by split => //; rewrite (eqp_ltrans (gcdpC _ _)) addrC. +rewrite /egcdp => pn0 qn0; case: (leqP (size q) (size p)) => /= [|/ltnW] hp. + exact: egcdp_recP. +case: (egcdp_recP pn0 (leqnn (size p)) hp) => h1 h2 h3; split => //. +by rewrite (eqp_ltrans (gcdpC _ _)) addrC. Qed. Lemma egcdpE p q (e := egcdp p q) : gcdp p q %= e.1 * p + e.2 * q. Proof. rewrite {}/e; have [-> /= | qn0] := eqVneq q 0. by rewrite gcdp0 egcdp0 mul1r mulr0 addr0. -have [p0 | pn0] := eqVneq p 0; last by case: (egcdpP pn0 qn0). -rewrite p0 gcd0p mulr0 add0r /egcdp size_poly0 leqn0 size_poly_eq0 (negPf qn0). -by rewrite /= mul1r. +have [-> | pn0] := eqVneq p 0; last by case: (egcdpP pn0 qn0). +by rewrite gcd0p /egcdp size_poly0 size_poly_leq0 (negPf qn0) /= !simp. Qed. Lemma Bezoutp p q : exists u, u.1 * p + u.2 * q %= (gcdp p q). Proof. -case: (eqVneq p 0) => [-> | pn0]. +have [-> | pn0] := eqVneq p 0. by rewrite gcd0p; exists (0, 1); rewrite mul0r mul1r add0r. -case: (eqVneq q 0) => [-> | qn0]. +have [-> | qn0] := eqVneq q 0. by rewrite gcdp0; exists (1, 0); rewrite mul0r mul1r addr0. pose e := egcdp p q; exists e; rewrite eqp_sym. by case: (egcdpP pn0 qn0). Qed. -Lemma Bezout_coprimepP : forall p q, +Lemma Bezout_coprimepP p q : reflect (exists u, u.1 * p + u.2 * q %= 1) (coprimep p q). Proof. -move=> p q; rewrite -gcdp_eqp1; apply: (iffP idP)=> [g1|]. +rewrite -gcdp_eqp1; apply: (iffP idP)=> [g1|]. by case: (Bezoutp p q) => [[u v] Puv]; exists (u, v); apply: eqp_trans g1. -case=> [[u v]]; rewrite eqp_sym=> Puv; rewrite /eqp (eqp_dvdr _ Puv). +case=> [[u v]]; rewrite eqp_sym=> Puv; rewrite /eqp (eqp_dvdr _ Puv). by rewrite dvdp_addr dvdp_mull ?dvdp_gcdl ?dvdp_gcdr //= dvd1p. Qed. @@ -2109,15 +1951,15 @@ case/Bezout_coprimepP=> [[u v] euv] px0. move/eqpP: euv => [[c1 c2]] /andP /= [c1n0 c2n0 e]. suffices: c1 * (v.[x] * q.[x]) != 0. by rewrite !mulf_eq0 !negb_or c1n0 /=; case/andP. -move/(f_equal (fun t => horner t x)): e; rewrite /= !hornerZ hornerD. +have := f_equal (horner^~ x) e; rewrite /= !hornerZ hornerD. by rewrite !hornerM (eqP px0) mulr0 add0r hornerC mulr1; move->. Qed. Lemma Gauss_dvdpl p q d: coprimep d q -> (d %| p * q) = (d %| p). Proof. move/Bezout_coprimepP=>[[u v] Puv]; apply/idP/idP; last exact: dvdp_mulr. -move: Puv; move/(eqp_mull p); rewrite mulr1 mulrDr eqp_sym=> peq dpq. -rewrite (eqp_dvdr _ peq) dvdp_addr; first by rewrite mulrA mulrAC dvdp_mulr. +move/(eqp_mull p): Puv; rewrite mulr1 mulrDr eqp_sym=> peq dpq. +rewrite (eqp_dvdr _ peq) dvdp_addr; first by rewrite mulrA mulrAC dvdp_mulr. by rewrite mulrA dvdp_mull ?dvdpp. Qed. @@ -2127,17 +1969,17 @@ Proof. by rewrite mulrC; apply: Gauss_dvdpl. Qed. (* This could be simplified with the introduction of lcmp *) Lemma Gauss_dvdp m n p : coprimep m n -> (m * n %| p) = (m %| p) && (n %| p). Proof. -case: (eqVneq m 0) => [-> | mn0]. +have [-> | mn0] := eqVneq m 0. by rewrite coprime0p => /eqp_dvdl->; rewrite !mul0r dvd0p dvd1p andbT. -case: (eqVneq n 0) => [-> | nn0]. +have [-> | nn0] := eqVneq n 0. by rewrite coprimep0 => /eqp_dvdl->; rewrite !mulr0 dvd1p. -move=> hc; apply/idP/idP. - move/Gauss_dvdpl: hc => <- h; move/(dvdp_mull m): (h); rewrite dvdp_mul2l //. - move->; move/(dvdp_mulr n): (h); rewrite dvdp_mul2r // andbT. +move=> hc; apply/idP/idP => [mnmp | /andP [dmp dnp]]. + move/Gauss_dvdpl: hc => <-; move: (dvdp_mull m mnmp); rewrite dvdp_mul2l //. + move->; move: (dvdp_mulr n mnmp); rewrite dvdp_mul2r // andbT. exact: dvdp_mulr. -case/andP => dmp dnp; move: (dnp); rewrite dvdp_eq. +move: (dnp); rewrite dvdp_eq. set c2 := _ ^+ _; set q2 := _ %/ _; move/eqP=> e2. -have := (sym_eq (Gauss_dvdpl q2 hc)); rewrite -e2. +have/esym := Gauss_dvdpl q2 hc; rewrite -e2. have -> : m %| c2 *: p by rewrite -mul_polyC dvdp_mull. rewrite dvdp_eq; set c3 := _ ^+ _; set q3 := _ %/ _; move/eqP=> e3. apply: (@eq_dvdp (c3 * c2) q3). @@ -2195,7 +2037,7 @@ Proof. by rewrite !(coprimep_sym m); apply: coprimep_expl. Qed. Lemma gcdp_mul2l p q r : gcdp (p * q) (p * r) %= (p * gcdp q r). Proof. -case: (eqVneq p 0)=> [->|hp]; first by rewrite !mul0r gcdp0 eqpxx. +have [->|hp] := eqVneq p 0; first by rewrite !mul0r gcdp0 eqpxx. rewrite /eqp !dvdp_gcd !dvdp_mul2l // dvdp_gcdr dvdp_gcdl !andbT. move: (Bezoutp q r) => [[u v]] huv. rewrite eqp_sym in huv; rewrite (eqp_dvdr _ (eqp_mull _ huv)). @@ -2203,25 +2045,23 @@ rewrite mulrDr ![p * (_ * _)]mulrCA. by apply: dvdp_add; rewrite dvdp_mull// (dvdp_gcdr, dvdp_gcdl). Qed. -Lemma gcdp_mul2r q r p : gcdp (q * p) (r * p) %= (gcdp q r * p). -Proof. by rewrite ![_ * p]GRing.mulrC gcdp_mul2l. Qed. +Lemma gcdp_mul2r q r p : gcdp (q * p) (r * p) %= gcdp q r * p. +Proof. by rewrite ![_ * p]mulrC gcdp_mul2l. Qed. Lemma mulp_gcdr p q r : r * (gcdp p q) %= gcdp (r * p) (r * q). Proof. by rewrite eqp_sym gcdp_mul2l. Qed. Lemma mulp_gcdl p q r : (gcdp p q) * r %= gcdp (p * r) (q * r). -Proof. by rewrite eqp_sym gcdp_mul2r. Qed. +Proof. by rewrite eqp_sym gcdp_mul2r. Qed. Lemma coprimep_div_gcd p q : (p != 0) || (q != 0) -> coprimep (p %/ (gcdp p q)) (q %/ gcdp p q). Proof. -move=> hpq. -have gpq0: gcdp p q != 0 by rewrite gcdp_eq0 negb_and. -rewrite -gcdp_eqp1 -(@eqp_mul2r (gcdp p q)) // mul1r. +rewrite -negb_and -gcdp_eq0 -gcdp_eqp1 => gpq0. +rewrite -(@eqp_mul2r (gcdp p q)) // mul1r (eqp_ltrans (mulp_gcdl _ _ _)). have: gcdp p q %| p by rewrite dvdp_gcdl. have: gcdp p q %| q by rewrite dvdp_gcdr. -rewrite !dvdp_eq eq_sym; move/eqP=> hq; rewrite eq_sym; move/eqP=> hp. -rewrite (eqp_ltrans (mulp_gcdl _ _ _)) hq hp. +rewrite !dvdp_eq => /eqP <- /eqP <-. have lcn0 k : (lead_coef (gcdp p q)) ^+ k != 0. by rewrite expf_neq0 ?lead_coef_eq0. by apply: eqp_gcd; rewrite ?eqp_scale. @@ -2240,7 +2080,7 @@ Qed. Lemma dvdp_div_eq0 p q : q %| p -> (p %/ q == 0) = (p == 0). Proof. -move=> dvdp_qp; have [->|p_neq0] := altP (p =P 0); first by rewrite div0p eqxx. +move=> dvdp_qp; have [->|p_neq0] := eqVneq p 0; first by rewrite div0p eqxx. rewrite divp_eq0 ltnNge dvdp_leq // (negPf p_neq0) orbF /=. by apply: contraTF dvdp_qp=> /eqP ->; rewrite dvd0p. Qed. @@ -2250,6 +2090,7 @@ Lemma Bezout_coprimepPn p q : p != 0 -> q != 0 -> (0 < size uv.1 < size q) && (0 < size uv.2 < size p) & uv.1 * p = uv.2 * q) (~~ (coprimep p q)). +Proof. move=> pn0 qn0; apply: (iffP idP); last first. case=> [[u v] /= /andP [/andP [ps1 s1] /andP [ps2 s2]] e]. have: ~~(size (q * p) <= size (u * p)). @@ -2257,49 +2098,46 @@ move=> pn0 qn0; apply: (iffP idP); last first. by rewrite ltn_add2r. apply: contra => ?; apply: dvdp_leq; rewrite ?mulf_neq0 // -?size_poly_gt0 //. by rewrite mulrC Gauss_dvdp // dvdp_mull // e dvdp_mull. -rewrite coprimep_def neq_ltn. -case/orP; first by rewrite ltnS leqn0 size_poly_eq0 gcdp_eq0 -[p == 0]negbK pn0. +rewrite coprimep_def neq_ltn ltnS size_poly_leq0 gcdp_eq0. +rewrite (negPf pn0) (negPf qn0) /=. case sg: (size (gcdp p q)) => [|n] //; case: n sg=> [|n] // sg _. move: (dvdp_gcdl p q); rewrite dvdp_eq; set c1 := _ ^+ _; move/eqP=> hu1. move: (dvdp_gcdr p q); rewrite dvdp_eq; set c2 := _ ^+ _; move/eqP=> hv1. exists (c1 *: (q %/ gcdp p q), c2 *: (p %/ gcdp p q)); last first. - by rewrite -!{1}scalerAl !scalerAr hu1 hv1 mulrCA. -rewrite !{1}size_scale ?lc_expn_scalp_neq0 //= !size_poly_gt0 !divp_eq0. + by rewrite -!scalerAl !scalerAr hu1 hv1 mulrCA. +rewrite !size_scale ?lc_expn_scalp_neq0 //= !size_poly_gt0 !divp_eq0. rewrite gcdp_eq0 !(negPf pn0) !(negPf qn0) /= -!leqNgt leq_gcdpl //. rewrite leq_gcdpr //= !ltn_divpl -?size_poly_eq0 ?sg //. rewrite !size_mul // -?size_poly_eq0 ?sg // ![(_ + n.+2)%N]addnS /=. -by rewrite -{1}(addn0 (size p)) -{1}(addn0 (size q)) !ltn_add2l. +by rewrite -!(addn1 (size _)) !leq_add2l. Qed. Lemma dvdp_pexp2r m n k : k > 0 -> (m ^+ k %| n ^+ k) = (m %| n). Proof. move=> k_gt0; apply/idP/idP; last exact: dvdp_exp2r. -case: (eqVneq n 0) => [-> | nn0] //; case: (eqVneq m 0) => [-> | mn0]. +have [-> // | nn0] := eqVneq n 0; have [-> | mn0] := eqVneq m 0. move/prednK: k_gt0=> {1}<-; rewrite exprS mul0r //= !dvd0p expf_eq0. by case/andP=> _ ->. -set d := gcdp m n; have := (dvdp_gcdr m n); rewrite -/d dvdp_eq. +set d := gcdp m n; have := dvdp_gcdr m n; rewrite -/d dvdp_eq. set c1 := _ ^+ _; set n' := _ %/ _; move/eqP=> def_n. -have := (dvdp_gcdl m n); rewrite -/d dvdp_eq. +have := dvdp_gcdl m n; rewrite -/d dvdp_eq. set c2 := _ ^+ _; set m' := _ %/ _; move/eqP=> def_m. have dn0 : d != 0 by rewrite gcdp_eq0 negb_and nn0 orbT. have c1n0 : c1 != 0 by rewrite !expf_neq0 // lead_coef_eq0. have c2n0 : c2 != 0 by rewrite !expf_neq0 // lead_coef_eq0. -rewrite -(@dvdp_scaler (c1 ^+ k)) ?expf_neq0 ?lead_coef_eq0 //. have c2k_n0 : c2 ^+ k != 0 by rewrite !expf_neq0 // lead_coef_eq0. -rewrite -(@dvdp_scalel (c2 ^+k)) // -!exprZn def_m def_n !exprMn. +rewrite -(@dvdp_scaler (c1 ^+ k)) ?expf_neq0 ?lead_coef_eq0 //. +rewrite -(@dvdp_scalel (c2 ^+ k)) // -!exprZn def_m def_n !exprMn. rewrite dvdp_mul2r ?expf_neq0 //. have: coprimep (m' ^+ k) (n' ^+ k). - rewrite coprimep_pexpl // coprimep_pexpr //; apply: coprimep_div_gcd. - by rewrite nn0 orbT. + by rewrite coprimep_pexpl // coprimep_pexpr // coprimep_div_gcd ?mn0. move/coprimepP=> hc hd. have /size_poly1P [c cn0 em'] : size m' == 1%N. - case: (eqVneq m' 0) => [m'0 |m'_n0]. - move/eqP: def_m; rewrite m'0 mul0r scale_poly_eq0. - by rewrite (negPf mn0) (negPf c2n0). - have := (hc _ (dvdpp _) hd); rewrite -size_poly_eq1. + case: (eqVneq m' 0) def_m => [-> /eqP | m'_n0 def_m]. + by rewrite mul0r scale_poly_eq0 (negPf mn0) (negPf c2n0). + have := hc _ (dvdpp _) hd; rewrite -size_poly_eq1. rewrite polySpred; last by rewrite expf_eq0 negb_and m'_n0 orbT. - rewrite size_exp eqSS muln_eq0; move: k_gt0; rewrite lt0n; move/negPf->. - by rewrite orbF -{2}(@prednK (size m')) ?lt0n // size_poly_eq0. + by rewrite size_exp eqSS muln_eq0 orbC eqn0Ngt k_gt0 /= -eqSS -polySpred. rewrite -(@dvdp_scalel c2) // def_m em' mul_polyC dvdp_scalel //. by rewrite -(@dvdp_scaler c1) // def_n dvdp_mull. Qed. @@ -2308,15 +2146,15 @@ Lemma root_gcd p q x : root (gcdp p q) x = root p x && root q x. Proof. rewrite /= !root_factor_theorem; apply/idP/andP=> [dg| [dp dq]]. by split; apply: dvdp_trans dg _; rewrite ?(dvdp_gcdl, dvdp_gcdr). -have:= (Bezoutp p q)=> [[[u v]]]; rewrite eqp_sym=> e. +have:= Bezoutp p q => [[[u v]]]; rewrite eqp_sym=> e. by rewrite (eqp_dvdr _ e) dvdp_addl dvdp_mull. Qed. -Lemma root_biggcd : forall x (ps : seq {poly R}), +Lemma root_biggcd x (ps : seq {poly R}) : root (\big[gcdp/0]_(p <- ps) p) x = all (fun p => root p x) ps. Proof. -move=> x; elim; first by rewrite big_nil root0. -by move=> p ps ihp; rewrite big_cons /= root_gcd ihp. +elim: ps => [|p ps ihp]; first by rewrite big_nil root0. +by rewrite big_cons /= root_gcd ihp. Qed. (* "gdcop Q P" is the Greatest Divisor of P which is coprime to Q *) @@ -2331,23 +2169,22 @@ Definition gdcop q p := gdcop_rec q p (size p). Variant gdcop_spec q p : {poly R} -> Type := GdcopSpec r of (dvdp r p) & ((coprimep r q) || (p == 0)) - & (forall d, dvdp d p -> coprimep d q -> dvdp d r) + & (forall d, dvdp d p -> coprimep d q -> dvdp d r) : gdcop_spec q p r. Lemma gdcop0 q : gdcop q 0 = (q == 0)%:R. -Proof. by rewrite /gdcop size_poly0. Qed. +Proof. by rewrite /gdcop size_poly0. Qed. -Lemma gdcop_recP : forall q p k, - size p <= k -> gdcop_spec q p (gdcop_rec q p k). +Lemma gdcop_recP q p k : size p <= k -> gdcop_spec q p (gdcop_rec q p k). Proof. -move=> q p k; elim: k p => [p | k ihk p] /=. - rewrite leqn0 size_poly_eq0; move/eqP->. - case q0: (_ == _); split; rewrite ?coprime1p // ?eqxx ?orbT //. - by move=> d _; rewrite (eqP q0) coprimep0 dvdp1 size_poly_eq1. +elim: k p => [p | k ihk p] /=. + move/size_poly_leq0P->. + have [->|q0] := eqVneq; split; rewrite ?coprime1p // ?eqxx ?orbT //. + by move=> d _; rewrite coprimep0 dvdp1 size_poly_eq1. move=> hs; case cop : (coprimep _ _); first by split; rewrite ?dvdpp ?cop. -case (eqVneq p 0) => [-> | p0]. +have [-> | p0] := eqVneq p 0. by rewrite div0p; apply: ihk; rewrite size_poly0 leq0n. -case: (eqVneq q 0) => [-> | q0]. +have [-> | q0] := eqVneq q 0. rewrite gcdp0 divpp ?p0 //= => {hs ihk}; case: k=> /=. rewrite eqxx; split; rewrite ?dvd1p ?coprimep0 ?eqpxx //=. by move=> d _; rewrite coprimep0 dvdp1 size_poly_eq1. @@ -2359,26 +2196,24 @@ move: (dvdp_gcdl p q); rewrite dvdp_eq; move/eqP=> e. have sgp : size (gcdp p q) <= size p. by apply: dvdp_leq; rewrite ?gcdp_eq0 ?p0 ?q0 // dvdp_gcdl. have : p %/ gcdp p q != 0; last move/negPf=>p'n0. - move: (dvdp_mulIl (p %/ gcdp p q) (gcdp p q)); move/dvdpN0; apply; rewrite -e. - by rewrite scale_poly_eq0 negb_or lc_expn_scalp_neq0. + apply: dvdpN0 (dvdp_mulIl (p %/ gcdp p q) (gcdp p q)) _. + by rewrite -e scale_poly_eq0 negb_or lc_expn_scalp_neq0. have gn0 : gcdp p q != 0. - move: (dvdp_mulIr (p %/ gcdp p q) (gcdp p q)); move/dvdpN0; apply; rewrite -e. - by rewrite scale_poly_eq0 negb_or lc_expn_scalp_neq0. + apply: dvdpN0 (dvdp_mulIr (p %/ gcdp p q) (gcdp p q)) _. + by rewrite -e scale_poly_eq0 negb_or lc_expn_scalp_neq0. have sp' : size (p %/ (gcdp p q)) <= k. - rewrite size_divp ?sgp // leq_subLR (leq_trans hs)//. - rewrite -subn_gt0 addnK -subn1 ltn_subRL addn0 ltnNge leq_eqVlt. - by rewrite [_ == _]cop ltnS leqn0 size_poly_eq0 (negPf gn0). + rewrite size_divp ?sgp // leq_subLR (leq_trans hs) // -add1n leq_add2r -subn1. + by rewrite ltn_subRL add1n ltn_neqAle eq_sym [_ == _]cop size_poly_gt0 gn0. case (ihk _ sp')=> r' dr'p'; first rewrite p'n0 orbF=> cr'q maxr'. constructor=> //=; rewrite ?(negPf p0) ?orbF //. exact/(dvdp_trans dr'p')/divp_dvd/dvdp_gcdl. move=> d dp cdq; apply: maxr'; last by rewrite cdq. case dpq: (d %| gcdp p q). - move: (dpq); rewrite dvdp_gcd dp /= => dq; apply: dvdUp; move: cdq. - apply: contraLR=> nd1; apply/coprimepPn; last first. + move: (dpq); rewrite dvdp_gcd dp /= => dq; apply: dvdUp. + apply: contraLR cdq => nd1; apply/coprimepPn; last first. by exists d; rewrite dvdp_gcd dvdpp dq nd1. - move/negP: p0; move/negP; apply: contra=> d0; move: dp; rewrite (eqP d0). - by rewrite dvd0p. -move: (dp); apply: contraLR=> ndp'. + by apply: contraNneq p0 => d0; move: dp; rewrite d0 dvd0p. +apply: contraLR dp => ndp'. rewrite (@eqp_dvdr ((lead_coef (gcdp p q) ^+ scalp p (gcdp p q))*:p)). by rewrite e; rewrite Gauss_dvdpl //; apply: (coprimep_dvdl (dvdp_gcdr _ _)). by rewrite eqp_sym eqp_scale // lc_expn_scalp_neq0. @@ -2393,24 +2228,23 @@ Proof. by move=> q_neq0; case: gdcopP=> d; rewrite (negPf q_neq0) orbF. Qed. Lemma size2_dvdp_gdco p q d : p != 0 -> size d = 2%N -> (d %| (gdcop q p)) = (d %| p) && ~~(d %| q). Proof. -case: (eqVneq d 0) => [-> | dn0]; first by rewrite size_poly0. +have [-> | dn0] := eqVneq d 0; first by rewrite size_poly0. move=> p0 sd; apply/idP/idP. case: gdcopP=> r rp crq maxr dr; move/negPf: (p0)=> p0f. rewrite (dvdp_trans dr) //=. - move: crq; apply: contraL=> dq; rewrite p0f orbF; apply/coprimepPn. - by move: p0; apply: contra=> r0; move: rp; rewrite (eqP r0) dvd0p. + apply: contraL crq => dq; rewrite p0f orbF; apply/coprimepPn. + by apply: contraNneq p0 => r0; move: rp; rewrite r0 dvd0p. by exists d; rewrite dvdp_gcd dr dq -size_poly_eq1 sd. case/andP=> dp dq; case: gdcopP=> r rp crq maxr; apply: maxr=> //. apply/coprimepP=> x xd xq. move: (dvdp_leq dn0 xd); rewrite leq_eqVlt sd; case/orP; last first. - rewrite ltnS leq_eqVlt; case/orP; first by rewrite -size_poly_eq1. - rewrite ltnS leqn0 size_poly_eq0; move/eqP=> x0; move: xd; rewrite x0 dvd0p. - by rewrite (negPf dn0). + rewrite ltnS leq_eqVlt ltnS size_poly_leq0 orbC. + case/predU1P => [x0|]; last by rewrite -size_poly_eq1. + by move: xd; rewrite x0 dvd0p (negPf dn0). by rewrite -sd dvdp_size_eqp //; move/(eqp_dvdl q); rewrite xq (negPf dq). Qed. -Lemma dvdp_gdco p q : (gdcop p q) %| q. -Proof. by case: gdcopP. Qed. +Lemma dvdp_gdco p q : (gdcop p q) %| q. Proof. by case: gdcopP. Qed. Lemma root_gdco p q x : p != 0 -> root (gdcop q p) x = root p x && ~~(root q x). Proof. @@ -2421,14 +2255,14 @@ Qed. Lemma dvdp_comp_poly r p q : (p %| q) -> (p \Po r) %| (q \Po r). Proof. -case: (eqVneq p 0) => [-> | pn0]. +have [-> | pn0] := eqVneq p 0. by rewrite comp_poly0 !dvd0p; move/eqP->; rewrite comp_poly0. rewrite dvdp_eq; set c := _ ^+ _; set s := _ %/ _; move/eqP=> Hq. apply: (@eq_dvdp c (s \Po r)); first by rewrite expf_neq0 // lead_coef_eq0. by rewrite -comp_polyZ Hq comp_polyM. Qed. -Lemma gcdp_comp_poly r p q : gcdp p q \Po r %= gcdp (p \Po r) (q \Po r). +Lemma gcdp_comp_poly r p q : gcdp p q \Po r %= gcdp (p \Po r) (q \Po r). Proof. apply/andP; split. by rewrite dvdp_gcd !dvdp_comp_poly ?dvdp_gcdl ?dvdp_gcdr. @@ -2452,16 +2286,16 @@ Definition irreducible_poly p := (size p > 1) * (forall q, size q != 1%N -> q %| p -> q %= p) : Prop. Lemma irredp_neq0 p : irreducible_poly p -> p != 0. -Proof. by rewrite -size_poly_eq0 -lt0n => [[/ltnW]]. Qed. +Proof. by rewrite -size_poly_gt0 => [[/ltnW]]. Qed. Definition apply_irredp p (irr_p : irreducible_poly p) := irr_p.2. Coercion apply_irredp : irreducible_poly >-> Funclass. Lemma modp_XsubC p c : p %% ('X - c%:P) = p.[c]%:P. Proof. -have: root (p - p.[c]%:P) c by rewrite /root !hornerE subrr. -case/factor_theorem=> q /(canRL (subrK _)) Dp; rewrite modpE /= lead_coefXsubC. -rewrite GRing.unitr1 expr1n invr1 scale1r {1}Dp. +have/factor_theorem [q /(canRL (subrK _)) Dp]: root (p - p.[c]%:P) c. + by rewrite /root !hornerE subrr. +rewrite modpE /= lead_coefXsubC unitr1 expr1n invr1 scale1r [in LHS]Dp. rewrite RingMonic.rmodp_addl_mul_small // ?monicXsubC // size_XsubC size_polyC. by case: (p.[c] == 0). Qed. @@ -2469,11 +2303,11 @@ Qed. Lemma coprimep_XsubC p c : coprimep p ('X - c%:P) = ~~ root p c. Proof. rewrite -coprimep_modl modp_XsubC /root -alg_polyC. -have [-> | /coprimep_scalel->] := altP eqP; last exact: coprime1p. +have [-> | /coprimep_scalel->] := eqVneq; last exact: coprime1p. by rewrite scale0r /coprimep gcd0p size_XsubC. Qed. -Lemma coprimepX p : coprimep p 'X = ~~ root p 0. +Lemma coprimepX p : coprimep p 'X = ~~ root p 0. Proof. by rewrite -['X]subr0 coprimep_XsubC. Qed. Lemma eqp_monic : {in monic &, forall p q, (p %= q) = (p == q)}. @@ -2482,10 +2316,9 @@ move=> p q monic_p monic_q; apply/idP/eqP=> [|-> //]. case/eqpP=> [[a b] /= /andP[a_neq0 _] eq_pq]. apply: (@mulfI _ a%:P); first by rewrite polyC_eq0. rewrite !mul_polyC eq_pq; congr (_ *: q); apply: (mulIf (oner_neq0 _)). -by rewrite -{1}(monicP monic_q) -(monicP monic_p) -!lead_coefZ eq_pq. +by rewrite -[in LHS](monicP monic_q) -(monicP monic_p) -!lead_coefZ eq_pq. Qed. - Lemma dvdp_mul_XsubC p q c : (p %| ('X - c%:P) * q) = ((if root p c then p %/ ('X - c%:P) else p) %| q). Proof. @@ -2557,7 +2390,7 @@ Proof. by rewrite modpE (eqP monq) unitr1 expr1n invr1 scale1r. Qed. Lemma scalpE p : scalp p q = 0%N. Proof. by rewrite scalpE (eqP monq) unitr1. Qed. -Lemma divp_eq p : p = (p %/ q) * q + (p %% q). +Lemma divp_eq p : p = (p %/ q) * q + (p %% q). Proof. by rewrite -divp_eq (eqP monq) expr1n scale1r. Qed. Lemma divpp p : q %/ q = 1. @@ -2575,8 +2408,7 @@ Qed. Lemma mulpK p : p * q %/ q = p. Proof. by rewrite mulpK ?monic_neq0 // (eqP monq) expr1n scale1r. Qed. -Lemma mulKp p : q * p %/ q = p. -Proof. by rewrite mulrC; apply: mulpK. Qed. +Lemma mulKp p : q * p %/ q = p. Proof. by rewrite mulrC mulpK. Qed. End MonicDivisor. @@ -2596,52 +2428,48 @@ Hypothesis ulcd : lead_coef d \in GRing.unit. Implicit Type p q r : {poly R}. Lemma divp_eq p : p = (p %/ d) * d + (p %% d). -Proof. by have := (divp_eq p d); rewrite scalpE ulcd expr0 scale1r. Qed. +Proof. by have := divp_eq p d; rewrite scalpE ulcd expr0 scale1r. Qed. Lemma edivpP p q r : p = q * d + r -> size r < size d -> q = (p %/ d) /\ r = p %% d. Proof. -move=> ep srd; have := (divp_eq p); rewrite {1}ep. +move=> ep srd; have := divp_eq p; rewrite [LHS]ep. move/eqP; rewrite -subr_eq -addrA addrC eq_sym -subr_eq -mulrBl; move/eqP. have lcdn0 : lead_coef d != 0 by apply: contraTneq ulcd => ->; rewrite unitr0. -case abs: (p %/ d - q == 0). - move: abs; rewrite subr_eq0; move/eqP->; rewrite subrr mul0r; move/eqP. - by rewrite eq_sym subr_eq0; move/eqP->. +have [-> /esym /eqP|abs] := eqVneq (p %/ d) q. + by rewrite subrr mul0r subr_eq0 => /eqP<-. have hleq : size d <= size ((p %/ d - q) * d). rewrite size_proper_mul; last first. - by rewrite mulf_eq0 (negPf lcdn0) orbF lead_coef_eq0 abs. - move: abs; rewrite -size_poly_eq0; move/negbT; rewrite -lt0n; move/prednK<-. - by rewrite addSn /= leq_addl. + by rewrite mulf_eq0 (negPf lcdn0) orbF lead_coef_eq0 subr_eq0. + by move: abs; rewrite -subr_eq0; move/polySpred->; rewrite addSn /= leq_addl. have hlt : size (r - p %% d) < size d. - apply: leq_ltn_trans (size_add _ _) _; rewrite size_opp. - by rewrite gtn_max srd ltn_modp /= -lead_coef_eq0. -by move=> e; have:= (leq_trans hlt hleq); rewrite e ltnn. + apply: leq_ltn_trans (size_add _ _) _. + by rewrite gtn_max srd size_opp ltn_modp -lead_coef_eq0. +by move=> e; have:= leq_trans hlt hleq; rewrite e ltnn. Qed. -Lemma divpP p q r : p = q * d + r -> size r < size d -> - q = (p %/ d). +Lemma divpP p q r : p = q * d + r -> size r < size d -> q = (p %/ d). Proof. by move/edivpP=> h; case/h. Qed. -Lemma modpP p q r : p = q * d + r -> size r < size d -> r = (p %% d). +Lemma modpP p q r : p = q * d + r -> size r < size d -> r = (p %% d). Proof. by move/edivpP=> h; case/h. Qed. Lemma ulc_eqpP p q : lead_coef q \is a GRing.unit -> reflect (exists2 c : R, c != 0 & p = c *: q) (p %= q). Proof. - case: (altP (lead_coef q =P 0)) => [->|]; first by rewrite unitr0. - rewrite lead_coef_eq0 => nz_q ulcq; apply: (iffP idP). - case: (altP (p =P 0)) => [->|nz_p]. - by rewrite eqp_sym eqp0 (negbTE nz_q). - move/eqp_eq=> eq; exists (lead_coef p / lead_coef q). - by rewrite mulf_neq0 // ?invr_eq0 lead_coef_eq0. - by apply/(scaler_injl ulcq); rewrite scalerA mulrCA divrr // mulr1. - by case=> c nz_c ->; apply/eqpP; exists (1, c); rewrite ?scale1r ?oner_eq0. +have [->|] := eqVneq (lead_coef q) 0; first by rewrite unitr0. +rewrite lead_coef_eq0 => nz_q ulcq; apply: (iffP idP). + have [->|nz_p] := eqVneq p 0; first by rewrite eqp_sym eqp0 (negPf nz_q). + move/eqp_eq=> eq; exists (lead_coef p / lead_coef q). + by rewrite mulf_neq0 // ?invr_eq0 lead_coef_eq0. + by apply/(scaler_injl ulcq); rewrite scalerA mulrCA divrr // mulr1. +by case=> c nz_c ->; apply/eqpP; exists (1, c); rewrite ?scale1r ?oner_eq0. Qed. Lemma dvdp_eq p : (d %| p) = (p == p %/ d * d). Proof. apply/eqP/eqP=> [modp0 | ->]; last exact: modp_mull. -by rewrite {1}(divp_eq p) modp0 addr0. +by rewrite [p in LHS]divp_eq modp0 addr0. Qed. Lemma ucl_eqp_eq p q : lead_coef q \is a GRing.unit -> @@ -2653,26 +2481,24 @@ Qed. Lemma modp_scalel c p : (c *: p) %% d = c *: (p %% d). Proof. -case: (altP (c =P 0)) => [-> | cn0]; first by rewrite !scale0r mod0p. +have [-> | cn0] := eqVneq c 0; first by rewrite !scale0r mod0p. have e : (c *: p) = (c *: (p %/ d)) * d + c *: (p %% d). by rewrite -scalerAl -scalerDr -divp_eq. -have s: size (c *: (p %% d)) < size d. - rewrite -mul_polyC; apply: leq_ltn_trans (size_mul_leq _ _) _. - rewrite size_polyC cn0 addSn add0n /= ltn_modp. - by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0. -by case: (edivpP e s) => _ ->. +suff s: size (c *: (p %% d)) < size d by case: (edivpP e s) => _ ->. +rewrite -mul_polyC; apply: leq_ltn_trans (size_mul_leq _ _) _. +rewrite size_polyC cn0 addSn add0n /= ltn_modp -lead_coef_eq0. +by apply: contraTneq ulcd => ->; rewrite unitr0. Qed. Lemma divp_scalel c p : (c *: p) %/ d = c *: (p %/ d). Proof. -case: (altP (c =P 0)) => [-> | cn0]; first by rewrite !scale0r div0p. +have [-> | cn0] := eqVneq c 0; first by rewrite !scale0r div0p. have e : (c *: p) = (c *: (p %/ d)) * d + c *: (p %% d). by rewrite -scalerAl -scalerDr -divp_eq. -have s: size (c *: (p %% d)) < size d. - rewrite -mul_polyC; apply: leq_ltn_trans (size_mul_leq _ _) _. - rewrite size_polyC cn0 addSn add0n /= ltn_modp. - by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0. -by case: (edivpP e s) => ->. +suff s: size (c *: (p %% d)) < size d by case: (edivpP e s) => ->. +rewrite -mul_polyC; apply: leq_ltn_trans (size_mul_leq _ _) _. +rewrite size_polyC cn0 addSn add0n /= ltn_modp -lead_coef_eq0. +by apply: contraTneq ulcd => ->; rewrite unitr0. Qed. Lemma eqp_modpl p q : p %= q -> (p %% d) %= (q %% d). @@ -2683,52 +2509,41 @@ Qed. Lemma eqp_divl p q : p %= q -> (p %/ d) %= (q %/ d). Proof. -case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. +case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divp_scalel e. Qed. Lemma modp_opp p : (- p) %% d = - (p %% d). -Proof. -by rewrite -mulN1r -[- (_ %% _)]mulN1r -polyC_opp !mul_polyC modp_scalel. -Qed. +Proof. by rewrite -mulN1r -[RHS]mulN1r -polyC_opp !mul_polyC modp_scalel. Qed. Lemma divp_opp p : (- p) %/ d = - (p %/ d). -Proof. -by rewrite -mulN1r -[- (_ %/ _)]mulN1r -polyC_opp !mul_polyC divp_scalel. -Qed. +Proof. by rewrite -mulN1r -[RHS]mulN1r -polyC_opp !mul_polyC divp_scalel. Qed. Lemma modp_add p q : (p + q) %% d = p %% d + q %% d. Proof. -have hs : size (p %% d + q %% d) < size d. - apply: leq_ltn_trans (size_add _ _) _. - rewrite gtn_max !ltn_modp andbb -lead_coef_eq0. - by apply: contraTneq ulcd => ->; rewrite unitr0. -have he : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d). - rewrite {1}(divp_eq p) {1}(divp_eq q) addrAC addrA -mulrDl. - by rewrite [_ %% _ + _]addrC addrA. -by case: (edivpP he hs). +have/edivpP [] // : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d). + by rewrite mulrDl addrACA -!divp_eq. +apply: leq_ltn_trans (size_add _ _) _. +rewrite gtn_max !ltn_modp andbb -lead_coef_eq0. +by apply: contraTneq ulcd => ->; rewrite unitr0. Qed. Lemma divp_add p q : (p + q) %/ d = p %/ d + q %/ d. Proof. -have hs : size (p %% d + q %% d) < size d. - apply: leq_ltn_trans (size_add _ _) _. - rewrite gtn_max !ltn_modp andbb -lead_coef_eq0. - by apply: contraTneq ulcd => ->; rewrite unitr0. -have he : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d). - rewrite {1}(divp_eq p) {1}(divp_eq q) addrAC addrA -mulrDl. - by rewrite [_ %% _ + _]addrC addrA. -by case: (edivpP he hs). +have/edivpP [] // : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d). + by rewrite mulrDl addrACA -!divp_eq. +apply: leq_ltn_trans (size_add _ _) _. +rewrite gtn_max !ltn_modp andbb -lead_coef_eq0. +by apply: contraTneq ulcd => ->; rewrite unitr0. Qed. Lemma mulpK q : (q * d) %/ d = q. Proof. -case/edivpP: (sym_eq (addr0 (q * d))); rewrite // size_poly0 size_poly_gt0. +case/esym/edivpP: (addr0 (q * d)); rewrite // size_poly0 size_poly_gt0. by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0. Qed. -Lemma mulKp q : (d * q) %/ d = q. -Proof. by rewrite mulrC; apply: mulpK. Qed. +Lemma mulKp q : (d * q) %/ d = q. Proof. by rewrite mulrC; apply: mulpK. Qed. Lemma divp_addl_mul_small q r : size r < size d -> (q * d + r) %/ d = q. @@ -2741,17 +2556,14 @@ Proof. by move=> srd; rewrite modp_add modp_mull add0r modp_small. Qed. Lemma divp_addl_mul q r : (q * d + r) %/ d = q + r %/ d. Proof. by rewrite divp_add mulpK. Qed. -Lemma divpp : d %/ d = 1. -Proof. by rewrite -{1}(mul1r d) mulpK. Qed. +Lemma divpp : d %/ d = 1. Proof. by rewrite -[d in d %/ _]mul1r mulpK. Qed. Lemma leq_trunc_divp m : size (m %/ d * d) <= size m. Proof. -have dn0 : d != 0. - by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0. -case q0 : (m %/ d == 0); first by rewrite (eqP q0) mul0r size_poly0 leq0n. -rewrite {2}(divp_eq m) size_addl // size_mul ?q0 //; move/negbT: q0. -rewrite -size_poly_gt0; move/prednK<-; rewrite addSn /=. -by move: dn0; rewrite -(ltn_modp m); move/ltn_addl->. +case: (eqVneq d 0) ulcd => [->|dn0 _]; first by rewrite lead_coef0 unitr0. +have [->|q0] := eqVneq (m %/ d) 0; first by rewrite mul0r size_poly0 leq0n. +rewrite {2}(divp_eq m) size_addl // size_mul // (polySpred q0) addSn /=. +by rewrite ltn_addl // ltn_modp. Qed. Lemma dvdpP p : reflect (exists q, p = q * d) (d %| p). @@ -2766,11 +2578,11 @@ Proof. by rewrite dvdp_eq; move/eqP. Qed. Lemma divpKC p : d %| p -> d * (p %/ d) = p. Proof. by move=> ?; rewrite mulrC divpK. Qed. -Lemma dvdp_eq_div p q : d %| p -> (q == p %/ d) = (q * d == p). +Lemma dvdp_eq_div p q : d %| p -> (q == p %/ d) = (q * d == p). Proof. move/divpK=> {2}<-; apply/eqP/eqP; first by move->. -suff dn0 : d != 0 by move/(mulIf dn0). -by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0. +apply/mulIf; rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->. +by rewrite unitr0. Qed. Lemma dvdp_eq_mul p q : d %| p -> (p == q * d) = (p %/ d == q). @@ -2790,11 +2602,7 @@ Lemma divp_mulCA p q : d %| p -> d %| q -> p * (q %/ d) = q * (p %/ d). Proof. by move=> hdp hdq; rewrite mulrC divp_mulAC // divp_mulA. Qed. Lemma modp_mul p q : (p * (q %% d)) %% d = (p * q) %% d. -Proof. -have -> : q %% d = q - q %/ d * d by rewrite {2}(divp_eq q) -addrA addrC subrK. -rewrite mulrDr modp_add // -mulNr mulrA -{2}[_ %% _]addr0; congr (_ + _). -by apply/eqP; apply: dvdp_mull; apply: dvdpp. -Qed. +Proof. by rewrite [q in RHS]divp_eq mulrDr modp_add mulrA modp_mull add0r. Qed. End UnitDivisor. @@ -2807,16 +2615,12 @@ Hypothesis ulcd : lead_coef d \in GRing.unit. Implicit Types p q : {poly R}. Lemma expp_sub m n : n <= m -> (d ^+ (m - n))%N = d ^+ m %/ d ^+ n. -Proof. -by move/subnK=> {2}<-; rewrite exprD mulpK // lead_coef_exp unitrX. -Qed. +Proof. by move/subnK=> {2}<-; rewrite exprD mulpK // lead_coef_exp unitrX. Qed. Lemma divp_pmul2l p q : lead_coef q \in GRing.unit -> d * p %/ (d * q) = p %/ q. Proof. -move=> uq. -have udq: lead_coef (d * q) \in GRing.unit. +move=> uq; rewrite {1}(divp_eq uq p) mulrDr mulrCA divp_addl_mul //; last first. by rewrite lead_coefM unitrM_comm ?ulcd //; red; rewrite mulrC. -rewrite {1}(divp_eq uq p) mulrDr mulrCA divp_addl_mul //. have dn0 : d != 0. by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0. have qn0 : q != 0. @@ -2824,14 +2628,12 @@ have qn0 : q != 0. have dqn0 : d * q != 0 by rewrite mulf_eq0 negb_or dn0. suff : size (d * (p %% q)) < size (d * q). by rewrite ltnNge -divpN0 // negbK => /eqP ->; rewrite addr0. -case: (altP ( (p %% q) =P 0)) => [-> | rn0]. +have [-> | rn0] := eqVneq (p %% q) 0. by rewrite mulr0 size_poly0 size_poly_gt0. -rewrite !size_mul //; move: dn0; rewrite -size_poly_gt0. -by move/prednK<-; rewrite !addSn /= ltn_add2l ltn_modp. +by rewrite !size_mul // (polySpred dn0) !addSn /= ltn_add2l ltn_modp. Qed. -Lemma divp_pmul2r p q : - lead_coef p \in GRing.unit -> q * d %/ (p * d) = q %/ p. +Lemma divp_pmul2r p q : lead_coef p \in GRing.unit -> q * d %/ (p * d) = q %/ p. Proof. by move=> uq; rewrite -!(mulrC d) divp_pmul2l. Qed. Lemma divp_divl r p q : @@ -2839,14 +2641,14 @@ Lemma divp_divl r p q : q %/ p %/ r = q %/ (p * r). Proof. move=> ulcr ulcp. -have e : q = (q %/ p %/ r) * (p * r) + ((q %/ p) %% r * p + q %% p). +have e : q = (q %/ p %/ r) * (p * r) + ((q %/ p) %% r * p + q %% p). by rewrite addrA (mulrC p) mulrA -mulrDl; rewrite -divp_eq //; apply: divp_eq. have pn0 : p != 0. by rewrite -lead_coef_eq0; apply: contraTneq ulcp => ->; rewrite unitr0. have rn0 : r != 0. by rewrite -lead_coef_eq0; apply: contraTneq ulcr => ->; rewrite unitr0. -have s : size ((q %/ p) %% r * p + q %% p) < size (p * r). - case: (altP ((q %/ p) %% r =P 0)) => [-> | qn0]. +have s : size ((q %/ p) %% r * p + q %% p) < size (p * r). + have [-> | qn0] := eqVneq ((q %/ p) %% r) 0. rewrite mul0r add0r size_mul // (polySpred rn0) addnS /=. by apply: leq_trans (leq_addr _ _); rewrite ltn_modp. rewrite size_addl mulrC. @@ -2857,12 +2659,12 @@ case: (edivpP _ e s) => //; rewrite lead_coefM unitrM_comm ?ulcp //. by red; rewrite mulrC. Qed. -Lemma divpAC p q : lead_coef p \in GRing.unit -> q %/ d %/ p = q %/ p %/ d. +Lemma divpAC p q : lead_coef p \in GRing.unit -> q %/ d %/ p = q %/ p %/ d. Proof. by move=> ulcp; rewrite !divp_divl // mulrC. Qed. Lemma modp_scaler c p : c \in GRing.unit -> p %% (c *: d) = (p %% d). Proof. -move=> cn0; case: (eqVneq d 0) => [-> | dn0]; first by rewrite scaler0 !modp0. +case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !modp0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). by rewrite scalerCA scalerA mulVr // scale1r -(divp_eq ulcd). suff s : size (p %% d) < size (c *: d). @@ -2872,8 +2674,7 @@ Qed. Lemma divp_scaler c p : c \in GRing.unit -> p %/ (c *: d) = c^-1 *: (p %/ d). Proof. -move=> cn0; case: (eqVneq d 0) => [-> | dn0]. - by rewrite scaler0 !divp0 scaler0. +case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !divp0 scaler0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). by rewrite scalerCA scalerA mulVr // scale1r -(divp_eq ulcd). suff s : size (p %% d) < size (c *: d). @@ -2900,7 +2701,7 @@ Implicit Type p q r d : {poly F}. Lemma divp_eq p q : p = (p %/ q) * q + (p %% q). Proof. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite modp0 mulr0 add0r. +have [-> | qn0] := eqVneq q 0; first by rewrite modp0 mulr0 add0r. by apply: IdomainUnit.divp_eq; rewrite unitfE lead_coef_eq0. Qed. @@ -2915,20 +2716,18 @@ Lemma divpP p q d r : p = q * d + r -> size r < size d -> q = (p %/ d). Proof. by move/divp_modpP=> h; case/h. Qed. -Lemma modpP p q d r : p = q * d + r -> size r < size d -> r = (p %% d). +Lemma modpP p q d r : p = q * d + r -> size r < size d -> r = (p %% d). Proof. by move/divp_modpP=> h; case/h. Qed. Lemma eqpfP p q : p %= q -> p = (lead_coef p / lead_coef q) *: q. Proof. -have [->|nz_q] := altP (q =P 0). - by rewrite eqp0 => /eqP ->; rewrite scaler0. -move/IdomainUnit.ucl_eqp_eq; apply; rewrite unitfE. -by move: nz_q; rewrite -lead_coef_eq0 => nz_qT. +have [->|nz_q] := eqVneq q 0; first by rewrite eqp0 scaler0 => /eqP ->. +by apply/IdomainUnit.ucl_eqp_eq; rewrite unitfE lead_coef_eq0. Qed. Lemma dvdp_eq q p : (q %| p) = (p == p %/ q * q). Proof. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite dvd0p mulr0 eq_sym. +have [-> | qn0] := eqVneq q 0; first by rewrite dvd0p mulr0 eq_sym. by apply: IdomainUnit.dvdp_eq; rewrite unitfE lead_coef_eq0. Qed. @@ -2937,7 +2736,7 @@ Proof. apply: (iffP idP); last first. case=> c nz_c ->; apply/eqpP. by exists (1, c); rewrite ?scale1r ?oner_eq0. -have [->|nz_q] := altP (q =P 0). +have [->|nz_q] := eqVneq q 0. by rewrite eqp0=> /eqP ->; exists 1; rewrite ?scale1r ?oner_eq0. case/IdomainUnit.ulc_eqpP; first by rewrite unitfE lead_coef_eq0. by move=> c nz_c ->; exists c. @@ -2945,7 +2744,7 @@ Qed. Lemma modp_scalel c p q : (c *: p) %% q = c *: (p %% q). Proof. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite !modp0. +have [-> | qn0] := eqVneq q 0; first by rewrite !modp0. by apply: IdomainUnit.modp_scalel; rewrite unitfE lead_coef_eq0. Qed. @@ -2957,13 +2756,13 @@ Proof. by rewrite mulrC; apply: mulpK. Qed. Lemma divp_scalel c p q : (c *: p) %/ q = c *: (p %/ q). Proof. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite !divp0 scaler0. +have [-> | qn0] := eqVneq q 0; first by rewrite !divp0 scaler0. by apply: IdomainUnit.divp_scalel; rewrite unitfE lead_coef_eq0. Qed. Lemma modp_scaler c p d : c != 0 -> p %% (c *: d) = (p %% d). Proof. -move=> cn0; case: (eqVneq d 0) => [-> | dn0]; first by rewrite scaler0 !modp0. +case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !modp0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). by rewrite scalerCA scalerA mulVf // scale1r -divp_eq. suff s : size (p %% d) < size (c *: d) by rewrite (modpP e s). @@ -2972,8 +2771,7 @@ Qed. Lemma divp_scaler c p d : c != 0 -> p %/ (c *: d) = c^-1 *: (p %/ d). Proof. -move=> cn0; case: (eqVneq d 0) => [-> | dn0]. - by rewrite scaler0 !divp0 scaler0. +case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !divp0 scaler0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). by rewrite scalerCA scalerA mulVf // scale1r -divp_eq. suff s : size (p %% d) < size (c *: d) by rewrite (divpP e s). @@ -3022,30 +2820,28 @@ Lemma eqp_gdcor p q r : q %= r -> gdcop p q %= gdcop p r. Proof. move=> eqr; rewrite /gdcop (eqp_size eqr). move: (size r)=> n; elim: n p q r eqr => [|n ihn] p q r; first by rewrite eqpxx. -move=> eqr /=; rewrite (eqp_coprimepl p eqr); case: ifP => _ //; apply: ihn. -by apply: eqp_div => //; apply: eqp_gcdl. +move=> eqr /=; rewrite (eqp_coprimepl p eqr); case: ifP => _ //. +exact/ihn/eqp_div/eqp_gcdl. Qed. Lemma eqp_gdcol p q r : q %= r -> gdcop q p %= gdcop r p. Proof. move=> eqr; rewrite /gdcop; move: (size p)=> n. elim: n p q r eqr {1 3}p (eqpxx p) => [|n ihn] p q r eqr s esp /=. - move: eqr; case: (eqVneq q 0)=> [-> | nq0 eqr] /=. + case: (eqVneq q 0) eqr => [-> | nq0 eqr] /=. by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. - suff rn0 : r != 0 by rewrite (negPf rn0) eqpxx. - by apply: contraTneq eqr => ->; rewrite eqp0. + by case: (eqVneq r 0) eqr nq0 => [->|]; rewrite ?eqpxx // eqp0 => ->. rewrite (eqp_coprimepr _ eqr) (eqp_coprimepl _ esp); case: ifP=> _ //. -by apply: ihn => //; apply: eqp_div => //; apply: eqp_gcd. +exact/ihn/eqp_div/eqp_gcd. Qed. Lemma eqp_rgdco_gdco q p : rgdcop q p %= gdcop q p. Proof. rewrite /rgdcop /gdcop; move: (size p)=> n. elim: n p q {1 3}p {1 3}q (eqpxx p) (eqpxx q) => [|n ihn] p q s t /= sp tq. - move: tq; case: (eqVneq t 0)=> [-> | nt0 etq]. + case: (eqVneq t 0) tq => [-> | nt0 etq]. by rewrite eqp_sym eqp0 => ->; rewrite eqpxx. - suff qn0 : q != 0 by rewrite (negPf qn0) eqpxx. - by apply: contraTneq etq => ->; rewrite eqp0. + by case: (eqVneq q 0) etq nt0 => [->|]; rewrite ?eqpxx // eqp0 => ->. rewrite rcoprimep_coprimep (eqp_coprimepl t sp) (eqp_coprimepr p tq). case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _. by apply: eqp_div => //; apply: eqp_trans (eqp_rgcd_gcd _ _) _; apply: eqp_gcd. @@ -3053,19 +2849,19 @@ Qed. Lemma modp_opp p q : (- p) %% q = - (p %% q). Proof. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite !modp0. +have [-> | qn0] := eqVneq q 0; first by rewrite !modp0. by apply: IdomainUnit.modp_opp; rewrite unitfE lead_coef_eq0. Qed. Lemma divp_opp p q : (- p) %/ q = - (p %/ q). Proof. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite !divp0 oppr0. +have [-> | qn0] := eqVneq q 0; first by rewrite !divp0 oppr0. by apply: IdomainUnit.divp_opp; rewrite unitfE lead_coef_eq0. Qed. Lemma modp_add d p q : (p + q) %% d = p %% d + q %% d. Proof. -case: (eqVneq d 0) => [-> | dn0]; first by rewrite !modp0. +have [-> | dn0] := eqVneq d 0; first by rewrite !modp0. by apply: IdomainUnit.modp_add; rewrite unitfE lead_coef_eq0. Qed. @@ -3074,7 +2870,7 @@ Proof. by apply/eqP; rewrite -addr_eq0 -modp_add addNr mod0p. Qed. Lemma divp_add d p q : (p + q) %/ d = p %/ d + q %/ d. Proof. -case: (eqVneq d 0) => [-> | dn0]; first by rewrite !divp0 addr0. +have [-> | dn0] := eqVneq d 0; first by rewrite !divp0 addr0. by apply: IdomainUnit.divp_add; rewrite unitfE lead_coef_eq0. Qed. @@ -3099,20 +2895,20 @@ Qed. Lemma leq_trunc_divp d m : size (m %/ d * d) <= size m. Proof. -case: (eqVneq d 0) => [-> | dn0]; first by rewrite mulr0 size_poly0. +have [-> | dn0] := eqVneq d 0; first by rewrite mulr0 size_poly0. by apply: IdomainUnit.leq_trunc_divp; rewrite unitfE lead_coef_eq0. Qed. Lemma divpK d p : d %| p -> p %/ d * d = p. Proof. -case: (eqVneq d 0) => [-> | dn0]; first by move/dvd0pP->; rewrite mulr0. +case: (eqVneq d 0) => [-> /dvd0pP -> | dn0]; first by rewrite mulr0. by apply: IdomainUnit.divpK; rewrite unitfE lead_coef_eq0. Qed. Lemma divpKC d p : d %| p -> d * (p %/ d) = p. Proof. by move=> ?; rewrite mulrC divpK. Qed. -Lemma dvdp_eq_div d p q : d != 0 -> d %| p -> (q == p %/ d) = (q * d == p). +Lemma dvdp_eq_div d p q : d != 0 -> d %| p -> (q == p %/ d) = (q * d == p). Proof. by move=> dn0; apply: IdomainUnit.dvdp_eq_div; rewrite unitfE lead_coef_eq0. Qed. @@ -3122,7 +2918,7 @@ Proof. by move=> dn0 dv_d_p; rewrite eq_sym -dvdp_eq_div // eq_sym. Qed. Lemma divp_mulA d p q : d %| q -> p * (q %/ d) = p * q %/ d. Proof. -case: (eqVneq d 0) => [-> | dn0]; first by move/dvd0pP->; rewrite !divp0 mulr0. +case: (eqVneq d 0) => [-> /dvd0pP -> | dn0]; first by rewrite !divp0 mulr0. by apply: IdomainUnit.divp_mulA; rewrite unitfE lead_coef_eq0. Qed. @@ -3140,43 +2936,42 @@ Proof. by move=> dn0 qn0; apply: IdomainUnit.divp_pmul2l; rewrite unitfE lead_coef_eq0. Qed. -Lemma divp_pmul2r d p q : d != 0 -> p != 0 -> q * d %/ (p * d) = q %/ p. +Lemma divp_pmul2r d p q : d != 0 -> p != 0 -> q * d %/ (p * d) = q %/ p. Proof. by move=> dn0 qn0; rewrite -!(mulrC d) divp_pmul2l. Qed. -Lemma divp_divl r p q : q %/ p %/ r = q %/ (p * r). +Lemma divp_divl r p q : q %/ p %/ r = q %/ (p * r). Proof. -case: (eqVneq r 0) => [-> | rn0]; first by rewrite mulr0 !divp0. -case: (eqVneq p 0) => [-> | pn0]; first by rewrite mul0r !divp0 div0p. +have [-> | rn0] := eqVneq r 0; first by rewrite mulr0 !divp0. +have [-> | pn0] := eqVneq p 0; first by rewrite mul0r !divp0 div0p. by apply: IdomainUnit.divp_divl; rewrite unitfE lead_coef_eq0. Qed. -Lemma divpAC d p q : q %/ d %/ p = q %/ p %/ d. +Lemma divpAC d p q : q %/ d %/ p = q %/ p %/ d. Proof. by rewrite !divp_divl // mulrC. Qed. Lemma edivp_def p q : edivp p q = (0%N, p %/ q, p %% q). Proof. rewrite Idomain.edivp_def; congr (_, _, _); rewrite /scalp 2!unlock /=. -case (eqVneq q 0) => [-> | qn0]; first by rewrite eqxx lead_coef0 unitr0. -rewrite (negPf qn0) /= unitfE lead_coef_eq0 qn0 /=. -by case: (redivp_rec _ _ _ _) => [[]]. +have [-> | qn0] := eqVneq; first by rewrite lead_coef0 unitr0. +by rewrite unitfE lead_coef_eq0 qn0 /=; case: (redivp_rec _ _ _ _) => [[]]. Qed. Lemma divpE p q : p %/ q = (lead_coef q)^-(rscalp p q) *: (rdivp p q). Proof. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite rdivp0 divp0 scaler0. +have [-> | qn0] := eqVneq q 0; first by rewrite rdivp0 divp0 scaler0. by rewrite Idomain.divpE unitfE lead_coef_eq0 qn0. Qed. Lemma modpE p q : p %% q = (lead_coef q)^-(rscalp p q) *: (rmodp p q). Proof. -case: (eqVneq q 0) => [-> | qn0]. +have [-> | qn0] := eqVneq q 0. by rewrite rmodp0 modp0 /rscalp unlock eqxx lead_coef0 expr0 invr1 scale1r. by rewrite Idomain.modpE unitfE lead_coef_eq0 qn0. Qed. Lemma scalpE p q : scalp p q = 0%N. Proof. -case: (eqVneq q 0) => [-> | qn0]; first by rewrite scalp0. +have [-> | qn0] := eqVneq q 0; first by rewrite scalp0. by rewrite Idomain.scalpE unitfE lead_coef_eq0 qn0. Qed. @@ -3201,27 +2996,24 @@ Qed. Lemma modp_mul p q m : (p * (q %% m)) %% m = (p * q) %% m. Proof. -have ->: q %% m = q - q %/ m * m by rewrite {2}(divp_eq q m) -addrA addrC subrK. -rewrite mulrDr modp_add // -mulNr mulrA -{2}[_ %% _]addr0; congr (_ + _). -by apply/eqP; apply: dvdp_mull; apply: dvdpp. +by rewrite [in RHS](divp_eq q m) mulrDr modp_add mulrA modp_mull add0r. Qed. Lemma dvdpP p q : reflect (exists qq, p = qq * q) (q %| p). Proof. -case: (eqVneq q 0)=> [-> | qn0]; last first. +have [-> | qn0] := eqVneq q 0; last first. by apply: IdomainUnit.dvdpP; rewrite unitfE lead_coef_eq0. -rewrite dvd0p. -by apply: (iffP idP) => [/eqP->| [? ->]]; [exists 1|]; rewrite mulr0. +by rewrite dvd0p; apply: (iffP eqP) => [->| [? ->]]; [exists 1|]; rewrite mulr0. Qed. -Lemma Bezout_eq1_coprimepP : forall p q, +Lemma Bezout_eq1_coprimepP p q : reflect (exists u, u.1 * p + u.2 * q = 1) (coprimep p q). Proof. -move=> p q; apply: (iffP idP)=> [hpq|]; last first. +apply: (iffP idP)=> [hpq|]; last first. by case=> [[u v]] /= e; apply/Bezout_coprimepP; exists (u, v); rewrite e eqpxx. case/Bezout_coprimepP: hpq => [[u v]] /=. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0] e. -exists (c2^-1 *: (c1 *: u), c2^-1 *: (c1 *: v)); rewrite /= -!scalerAl. +exists (c2^-1 *: (c1 *: u), c2^-1 *: (c1 *: v)); rewrite /= -!scalerAl. by rewrite -!scalerDr e scalerA mulVf // scale1r. Qed. @@ -3231,7 +3023,7 @@ rewrite /gdcop => nz_q; have [n hsp] := ubnPleq (size p). elim: n => [|n IHn] /= in p hsp *; first by rewrite (negPf nz_q) mul0r dvdp0. have [_ | ncop_pq] := ifPn; first by rewrite dvdp_mulr. have g_gt1: 1 < size (gcdp p q). - rewrite ltn_neqAle eq_sym ncop_pq lt0n size_poly_eq0 gcdp_eq0. + rewrite ltn_neqAle eq_sym ncop_pq size_poly_gt0 gcdp_eq0. by rewrite negb_and nz_q orbT. have [-> | nz_p] := eqVneq p 0. by rewrite div0p exprSr mulrA dvdp_mulr // IHn // size_poly0. @@ -3282,7 +3074,7 @@ Proof. rewrite /rdivp /rscalp /rmodp !unlock map_poly_eq0 size_map_poly. have [// | q_nz] := ifPn; rewrite -(rmorph0 (map_poly_rmorphism f)) //. have [m _] := ubnPeq (size a); elim: m 0%N 0 a => [|m IHm] qq r a /=. - rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f). + rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f). by rewrite -!(map_polyC f) -!rmorphM -rmorphB -rmorphD; case: (_ < _). rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f). by rewrite -!(map_polyC f) -!rmorphM -rmorphB -rmorphD /= IHm; case: (_ < _). @@ -3302,7 +3094,7 @@ Implicit Type a b : {poly F}. Lemma edivp_map a b : edivp a^f b^f = (0%N, (a %/ b)^f, (a %% b)^f). Proof. -case: (eqVneq b 0) => [-> | bn0]. +have [-> | bn0] := eqVneq b 0. rewrite (rmorph0 (map_poly_rmorphism f)) WeakIdomain.edivp_def !modp0 !divp0. by rewrite (rmorph0 (map_poly_rmorphism f)) scalp0. rewrite unlock redivp_map lead_coef_map rmorph_unit; last first. @@ -3346,7 +3138,7 @@ Proof. wlog lt_p_q: p q / size p < size q. move=> IHpq; case: (ltnP (size p) (size q)) => [|le_q_p]; first exact: IHpq. rewrite gcdpE (gcdpE p^f) !size_map_poly ltnNge le_q_p /= -map_modp. - case: (eqVneq q 0) => [-> | q_nz]; first by rewrite rmorph0 !gcdp0. + have [-> | q_nz] := eqVneq q 0; first by rewrite rmorph0 !gcdp0. by rewrite IHpq ?ltn_modp. have [m le_q_m] := ubnP (size q); elim: m => // m IHm in p q lt_p_q le_q_m *. rewrite gcdpE (gcdpE p^f) !size_map_poly lt_p_q -map_modp. @@ -3357,7 +3149,7 @@ Qed. Lemma coprimep_map p q : coprimep p^f q^f = coprimep p q. Proof. by rewrite -!gcdp_eqp1 -eqp_map rmorph1 gcdp_map. Qed. -Lemma gdcop_rec_map p q n : (gdcop_rec p q n)^f = (gdcop_rec p^f q^f n). +Lemma gdcop_rec_map p q n : (gdcop_rec p q n)^f = gdcop_rec p^f q^f n. Proof. elim: n p q => [|n IH] => /= p q. by rewrite map_poly_eq0; case: eqP; rewrite ?rmorph1 ?rmorph0. @@ -3365,7 +3157,7 @@ rewrite /coprimep -gcdp_map size_map_poly. by case: eqP => Hq0 //; rewrite -map_divp -IH. Qed. -Lemma gdcop_map p q : (gdcop p q)^f = (gdcop p^f q^f). +Lemma gdcop_map p q : (gdcop p q)^f = gdcop p^f q^f. Proof. by rewrite /gdcop gdcop_rec_map !size_map_poly. Qed. End FieldMap. @@ -3386,14 +3178,12 @@ Lemma root_coprimep (p q : {poly F}): (forall x, root p x -> q.[x] != 0) -> coprimep p q. Proof. move=> Ncmn; rewrite -gcdp_eqp1 -size_poly_eq1; apply/closed_rootP. -by case=> r; rewrite root_gcd !rootE=> /andP [/Ncmn/negbTE->]. +by case=> r; rewrite root_gcd !rootE=> /andP [/Ncmn/negPf->]. Qed. Lemma coprimepP (p q : {poly F}): reflect (forall x, root p x -> q.[x] != 0) (coprimep p q). -Proof. - by apply: (iffP idP)=> [/coprimep_root|/root_coprimep]. -Qed. +Proof. by apply: (iffP idP)=> [/coprimep_root|/root_coprimep]. Qed. End closed. |