change subresultant convention + cleanup proofs

auxresults.v

@@ -1,4 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import order fintype generic_quotient path ssrint.
 From mathcomp Require Import div tuple bigop ssralg ssrnum matrix poly polydiv.
@@ -1869,37 +1870,29 @@ apply/eq_bigr => i _.
 by rewrite !rmorphM/= !rmorphXn/= mevalXU mevalC meval_mwiden.
 Qed.
 
-Lemma horner_mmulti (x : {mpoly R[n]}) (v : 'I_n -> R)
-  (P : {poly {mpoly R[n]}}) :
-  P.[x].@[v] = (mmulti P).@[fun i =>
-    match ltnP i n with
-    | LtnNotGeq ilt => v (Ordinal ilt)
-    | _ => x.@[v]
-    end].
-Proof.
-rewrite /mmulti -{1}[P]coefK horner_poly !rmorph_sum/=.
-apply eq_bigr => i _.
-rewrite !rmorphM/= !rmorphXn/= mevalXU/=.
-case: (ltnP n n) => [/[dup]|_]; first by rewrite {1}ltnn.
-congr (_ * _)%R; rewrite meval_mwiden; apply/meval_eq => j.
-case: (ltnP _ _) => /= [jn|]; first by congr (v _); apply/val_inj.
-by rewrite leqNgt (ltn_ord j).
-Qed.
-
 Lemma meval_sum [I : Type] {K : ringType} (v : 'I_n -> K) (r : seq I)
     (F : I -> {mpoly K[n]}) (P : pred I) :
   (\sum_(i <- r | P i) F i).@[v] = \sum_(i <- r | P i) (F i).@[v].
+Proof. by rewrite raddf_sum. Qed.
+
+Lemma mnmwidenE (m : 'X_{1.. n}) (i : 'I_n.+1) :
+  mnmwiden m i =
+  match ltnP i n with
+  | LtnNotGeq ilt => m (Ordinal ilt)
+  | _ => 0%N
+  end.
 Proof.
-elim: r => [|i r IHr]; first by rewrite !big_nil meval0.
-rewrite !big_cons; case: (P i) => [|//].
-by rewrite mevalD IHr.
+case: (ltnP i n) => ilt.
+  by rewrite -[RHS]mnmwiden_widen; congr (mnmwiden _ _); apply/val_inj.
+rewrite -[RHS](mnmwiden_ordmax m); congr (mnmwiden _ _); apply/val_inj.
+apply/anti_leq/andP; split=> //.
+by move: (ltn_ord i); rewrite ltnS.
 Qed.
 
 Lemma mmulti_is_additive [S : ringType] :
   additive (@mmulti n S).
 Proof.
-move=> /= p q.
-rewrite /mmulti.
+move=> /= p q; rewrite /mmulti.
 rewrite (big_ord_widen
     (maxn (size p) (size q))
     (fun i => mwiden (p - q)`_i * 'X_ord_max ^+ i)%R); last first.
@@ -1922,190 +1915,108 @@ have ifE (x : {poly {mpoly S[n]}}): (if (i < size x)%N then x`_i else 0) = x`_i.
 by rewrite 3!ifE coefB mwidenB mulrBl.
 Qed.
 
+HB.instance Definition _ (S : ringType) :=
+  GRing.isAdditive.Build _ _ (@mmulti n S) (@mmulti_is_additive S).
+
+Lemma mnmPE m (u v : 'X_{1.. m}) : (u == v) = [forall i : 'I_m, u i == v i].
+Proof.
+apply/eqP/forallP => /= [-> i|uv]; first exact: eqxx.
+apply/val_inj/eq_from_tnth => i.
+by move: (uv i) => /eqP; rewrite !mnm_tnth.
+Qed.
+
+Lemma forall_ordS (m : nat) (p : pred 'I_m.+1) :
+  [forall i, p i] = (p ord_max && [forall i : 'I_m, p (widen_ord (leqnSn m) i)]).
+Proof.
+apply/forallP/andP => /= [pP|[] pm /forallP pP i].
+  split; first exact/pP.
+  by apply/forallP => i; apply/pP.
+case: (ltnP i m) => im.
+  by move: (pP (Ordinal im)); congr p; apply/val_inj.
+move: pm; congr p; apply/val_inj/le_anti/andP; split; first exact im.
+by move: (ltn_ord i); rewrite ltnS.
+Qed.
+
 Lemma mcoeff_muni (A : ringType) (p : {mpoly A[n.+1]})
     (i : nat) (m : 'X_{1.. n}) :
   (muni p)`_i@_m = p@_(Multinom (rcons_tuple m i)).
 Proof.
-rewrite /muni coef_sum/= raddf_sum/=.
-rewrite (big_neq_0 (i:=Multinom (rcons_tuple m i))) => //; first last.
-  move=> /= u _ um.
-  rewrite coefM (big_neq_0 (i:=ord0)) => //; first last.
-  + move=> /= j _; rewrite -(inj_eq val_inj) => /= j0.
-    by rewrite coefC (negPf j0) mul0r.
-  + exact/index_enum_uniq.
-  rewrite mem_index_enum/= coefC eqxx mcoeffM.
-  have m0: (@mdeg n 0 < (mdeg m).+1)%N by rewrite mdeg0.
-  rewrite (big_neq_0
-    (i:=(BMultinom m0, BMultinom (leqnn (mdeg m).+1)))) => //=; first last.
-  + case=> /= ul ur /eqP mE; rewrite xpair_eqE !bmeqP/= mcoeffC.
-    move: mE; have [->|_ _ _] := eqVneq (bmnm ul) 0%MM.
-      by rewrite add0m => <-; rewrite eqxx.
-    by rewrite mulr0 mul0r.
-  + exact/index_enum_uniq.
-  rewrite add0m eqxx mem_index_enum/= mcoeffC eqxx mulr1.
-  rewrite /mmap1/= big_ord_recr/=.
-  have ->: (cast_ord (esym (addn1 n)) ord_max) = rshift n (@ord0 0).
-    by apply/val_inj; rewrite /= addn0.
-  rewrite (unsplitK (inr _)).
-  set v := Multinom (@mktuple n _ (fun i => u (widen_ord (leqnSn n) i))).
-  under eq_bigr => k _.
-    have ->: (cast_ord (esym (addn1 n)) (widen_ord (leqnSn n) k)) = lshift 1 k.
-      exact/val_inj.
-    rewrite (unsplitK (inl _)) -polyC_exp.
-    have ->: u (widen_ord (leqnSn n) k) = v k.
-      by rewrite /v/= mnmE.
-    over.
-  rewrite /= -rmorph_prod/= mul_polyC coefZ subn0 coefXn.
-  have [iu|iu] := eqVneq i (u ord_max); last first.
-    by rewrite mulr0 mcoeff0 mulr0.
-  rewrite mulr1 -mpolyXE_id mcoeffX.
-  have [vm|_] := eqVneq v m; last exact/mulr0.
-  move/eqP: um; elim; apply/mnmP => j.
-  rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple.
-  move: (ltn_ord j); rewrite ltnS leq_eqVlt => /orP[/eqP/esym|] jn.
-    rewrite -jn ltnn subnn/=.
-    by move/esym: iu; congr (u _ = i); apply/val_inj => /=.
-  rewrite jn -vm -/(nat_of_ord (Ordinal jn)) -mnm_nth mnmE.
-  by congr (u _); apply/val_inj.
-move=> /=; case: ifP => mp; last first.
-  by apply/esym/memN_msupp_eq0; rewrite mp.
-rewrite mul_polyC coefZ mul_mpolyC mcoeffZ.
-rewrite /mmap1 big_ord_recr/=.
-have ->: (cast_ord (esym (addn1 n)) ord_max) = rshift n (@ord0 0).
-  by apply/val_inj; rewrite /= addn0.
-rewrite (unsplitK (inr _)).
-under eq_bigr => k _.
-  have ->: (cast_ord (esym (addn1 n)) (widen_ord (leqnSn n) k)) = lshift 1 k.
-    exact/val_inj.
-  rewrite (unsplitK (inl _)) -polyC_exp multinomE (tnth_nth 0)/=.
-  rewrite -cats1 nth_cat size_tuple (ltn_ord k) -mnm_nth.
-  over.
-rewrite /= -rmorph_prod/= mul_polyC coefZ -mpolyXE_id.
-rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple ltnn subnn/=.
-by rewrite coefXn eqxx mulr1 mcoeffX eqxx mulr1.
+rewrite (mpolyE p) !raddf_sum/= coef_sum raddf_sum/=.
+apply/eq_bigr => u _.
+rewrite muniZ coefZ mul_mpolyC !mcoeffZ; congr (_ * _).
+rewrite muniE msuppX big_seq1 !mcoeffX eqxx scale1r coefZ coefXn.
+rewrite mulr_natr raddfMn/= mcoeffX -[LHS]mulr_natr -natrM mulnb; congr ((_ _)%:R).
+rewrite !mnmPE forall_ordS multinomE /tnth/= nth_rcons size_tuple ltnn eqxx.
+rewrite eq_sym andbC; congr (_ && _).
+apply/eq_forallb => /= j.
+rewrite !multinomE tnth_map /tnth/= nth_rcons size_tuple ltn_ord nth_enum_ord.
+rewrite [X in _ == X]mnm_tnth /tnth/=; congr (_ == _).
+by apply/set_nth_default; rewrite size_tuple.
 Qed.
 
 Lemma mcoeff_mwiden (A : ringType) (p : {mpoly A[n]}) (m : 'X_{1.. n.+1}) :
   (mwiden p)@_m
   = p@_(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i))))
     *+ (m ord_max == 0).
 Proof.
-rewrite /mwiden/= /mmap raddf_sum/=.
-rewrite (big_neq_0
-  (i:=(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))))); first last.
-- move=> /= u _ um.
-  rewrite mul_mpolyC mcoeffZ /mmap1.
-  have ->: (\prod_(i < n) 'X_(widen_ord (leqnSn n) i) ^+ u i)
-      = 'X_[Multinom (rcons_tuple u 0)] :> {mpoly A[n.+1]}.
-    rewrite [RHS]mpolyXE_id big_ord_recr/= multinomE (tnth_nth 0)/= -cats1.
-    rewrite nth_cat size_tuple ltnn subnn/= expr0 mulr1.
-    apply/eq_bigr => i _.
-    rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple (ltn_ord i).
-    by rewrite -mnm_nth.
-  rewrite mcoeffX.
-  suff /negPf ->: [multinom rcons_tuple u 0] != m by apply/mulr0.
-  move: um; apply/contraNN => /eqP <-.
-  apply/eqP/mnmP => i; rewrite mnmE multinomE (tnth_nth 0)/= -cats1 nth_cat.
-  by rewrite size_tuple (ltn_ord i) -mnm_nth.
-- exact/msupp_uniq.
-move=> /=; case: ifP => mp; last first.
-  by rewrite memN_msupp_eq0 ?mp// mul0rn.
-rewrite mul_mpolyC mcoeffZ -mulr_natr; congr (_ * _).
-set u := [multinom _].
+rewrite (mpolyE p).
+rewrite !raddf_sum/= -(mpolyE p) -sumrMnl.
+apply/eq_bigr => u _.
+rewrite mul_mpolyC !mcoeffZ -mulrnAr; congr (_ * _).
 set x := mmap1 _ _.
 have ->: x = 'X_[Multinom (rcons_tuple u 0)].
   rewrite [RHS]mpolyXE_id big_ord_recr/= multinomE (tnth_nth 0)/= -cats1.
-  rewrite nth_cat size_tuple card_ord ltnn subnn/= expr0 mulr1.
+  rewrite nth_cat size_tuple ltnn subnn/= expr0 mulr1.
   apply/eq_bigr => i _.
-  rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple card_ord.
-  by rewrite (ltn_ord i) nth_map_ord mnmE.
-rewrite mcoeffX; congr ((_ _)%:R).
-apply/eqP/eqP => [|m0].
-  move=> /mnmP/(_ ord_max); rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat.
-  by rewrite size_map size_enum_ord ltnn subnn.
-apply/mnmP => i.
-rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_map size_enum_ord.
-move: (ltn_ord i); rewrite ltnS leq_eqVlt => /orP[/eqP iE|ilt].
-  by rewrite iE ltnn subnn/=; move/esym: m0; congr (0 = m _); apply/val_inj.
-rewrite ilt -/(nat_of_ord (Ordinal ilt)) nth_map_ord.
-by congr (m _); apply/val_inj.
-Qed.
-
-Lemma mnmwidenE (m : 'X_{1.. n}) (i : 'I_n.+1) :
-  mnmwiden m i =
-  match ltnP i n with
-  | LtnNotGeq ilt => m (Ordinal ilt)
-  | _ => 0%N
-  end.
-Proof.
-case: (ltnP i n) => ilt.
-  by rewrite -[RHS]mnmwiden_widen; congr (mnmwiden _ _); apply/val_inj.
-rewrite -[RHS](mnmwiden_ordmax m); congr (mnmwiden _ _); apply/val_inj.
-apply/anti_leq/andP; split=> //.
-by move: (ltn_ord i); rewrite ltnS.
+  rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple.
+  by rewrite (ltn_ord i) mnm_tnth (tnth_nth 0).
+rewrite !mcoeffX -[RHS]mulr_natr -natrM mulnb; congr ((_ _)%:R).
+rewrite !mnmPE forall_ordS multinomE /tnth/= nth_rcons size_tuple ltnn eqxx.
+rewrite eq_sym andbC; congr (_ && _).
+apply/eq_forallb => /= i.
+rewrite !multinomE tnth_map tnth_ord_tuple /tnth/= nth_rcons size_tuple.
+rewrite (ltn_ord i) [u i]mnm_tnth /tnth/=; congr (_ == _).
+by apply/set_nth_default; rewrite size_tuple.
 Qed.
 
 Lemma mcoeff_mmulti (A : ringType) (p : {poly {mpoly A[n]}})
     (m : 'X_{1.. n.+1}) :
   (mmulti p)@_m
   = p`_(m ord_max)@_(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))).
 Proof.
-rewrite raddf_sum/=.
-rewrite (big_ord_iota _ _ xpredT
-          (fun i : nat => (mwiden p`_i * 'X_ord_max ^+  i)@_m))/=.
-rewrite (big_neq_0 (i:=m ord_max)); last first.
-- move=> /= i _ im.
-  rewrite mcoeffM big_mkcond.
-  suff H (u : 'X_{1.. n.+1 < (mdeg m).+1, (mdeg m).+1}):
-      (if m == ((u.1)%PAIR + (u.2)%PAIR)%MM
-          then (mwiden p`_i)@_(u.1)%PAIR * ('X_ord_max ^+ i)@_(u.2)%PAIR
-          else 0) = 0.
-    under eq_bigr do rewrite H.
-    rewrite big_const_idem//; exact/addr0.
-  case: ifP => //.
-  case: u => /= l r /eqP/(congr1 (fun f : 'X_{1.. n.+1} => f ord_max)).
-  rewrite mnmDE mcoeffXn mcoeff_mwiden.
-  have [-> mn|l0 _] := eqVneq (l ord_max) 0; last first.
-    by rewrite mulr0n mul0r.
-  case/boolP: ((U_(ord_max) *+ i)%MM == r) => [|_]; last exact/mulr0.
-  rewrite mulr1 => /eqP/mnmP/(_ ord_max).
-  rewrite mulmnE mnm1E eqxx mul1n => ir.
-  by move: im; rewrite mn -ir => /eqP.
-- exact/iota_uniq.
-rewrite mem_iota/=; case: (ltnP (m ord_max) (size p)) => [mp|]; last first.
-  by move=> /leq_sizeP/(_ (m ord_max) (leqnn _)) ->; rewrite mcoeff0.
-rewrite mcoeffM.
-have mm:
-    (mdeg (mnmwiden (Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))))
-    < (mdeg m).+1)%N.
-  rewrite ltnS !mdegE; apply/leq_sum => /= i _.
-  rewrite mnmwidenE; case: (ltnP i n) => [ilt|//].
-  by rewrite mnmE; move: (leqnn (m i)); congr (m _ <= _)%N; apply/val_inj.
-have mn: (mdeg (U_(@ord_max n) *+ m ord_max)%MM < (mdeg m).+1)%N.
-  rewrite ltnS !mdegE; apply/leq_sum => /= i _.
-  rewrite mulmnE mnm1E.
-  have [->|_ //] := eqVneq ord_max i.
-  rewrite mul1n; exact/leqnn.
-have mE: m =
-   (mnmwiden [multinom [tuple m (widen_ord (leqnSn n) i)  | i < n]] +
-    U_(ord_max) *+ m ord_max)%MM.
-  apply/mnmP => i.
-  rewrite mnmE mulmnE mnm1E mnmwidenE -(inj_eq val_inj)/= eq_sym.
-  case: (ltnP i n) => [|ni].
-    have [-> /[dup]|_ ilt] := eqVneq (i : nat) n; first by rewrite {1}ltnn.
-    by rewrite mnmE addn0; congr (m _); apply/val_inj.
-  suff ->: i = ord_max by rewrite eqxx mul1n.
-  apply/val_inj/anti_leq/andP; split=> //.
-  by move: (ltn_ord i); rewrite ltnS.
-rewrite (big_neq_0 (i:=(BMultinom mm, BMultinom mn))).
-- by rewrite /= -mE eqxx mem_index_enum/= mwiden_mnmwiden mcoeffXn eqxx mulr1.
-- exact/index_enum_uniq.
-case=> /= l r /eqP; rewrite mcoeffXn xpair_eqE
-  -![_ == BMultinom _](inj_eq val_inj).
-have [<-|i _ _] := eqVneq (U_(ord_max) *+ m ord_max)%MM r; last exact/mulr0.
-move=> mlr /negP; rewrite andbT; elim.
-apply/eqP/(@addIm _ (U_(ord_max) *+ m ord_max)%MM).
-by rewrite -mlr.
+rewrite -(coefK p) poly_def coef_sum !raddf_sum/= -poly_def (coefK p).
+apply/eq_bigr => i _.
+rewrite coefZ coefXn mpolyXn mulr_natr raddfMn/=.
+case: (ltnP (m ord_max) i) => [mi|im].
+  rewrite (negPf (ltn_neq mi)) mulr0n.
+  move xE: _@_m => x; rewrite -[RHS](mulr0 x) -xE mcoeffM mulr_suml => {x xE}.
+  apply/eq_bigr => -[] /= u v /eqP mE.
+  rewrite mulr0 mcoeffX mcoeff_mwiden.
+  move: mi; rewrite {1}mE mnmDE.
+  have [-> vi|_ _] := eqVneq (u ord_max) 0; last by rewrite mulr0n mul0r.
+  rewrite mnmPE forall_ordS mulmnE mnm1E eqxx eq_sym mul1n (negPf (ltn_neq vi)).
+  exact/mulr0.
+move uE: (Multinom _) => u.
+have /eqP ->:
+    m == (U_(ord_max) *+ i + [multinom (rcons_tuple u (m ord_max - i)%N)])%MM.
+  rewrite mnmPE; apply/forallP => /= j; apply/eqP.
+  rewrite mnmDE mulmnE mnm1E multinomE /tnth/= nth_rcons size_tuple.
+  case: (ltnP j n) => jn.
+    rewrite -(inj_eq val_inj)/= [n == j]eq_sym (negPf (ltn_neq jn)) -uE.
+    rewrite -(tnth_nth _ _ (Ordinal jn)) -mnm_tnth multinomE tnth_mktuple.
+    by congr (_ _); apply/val_inj.
+  rewrite eq_sym/= -(inj_eq val_inj); suff ->: j = ord_max.
+    by rewrite eqxx/= mul1n subnKC.
+  apply/val_inj/le_anti/andP; split=> //.
+  by move: (ltn_ord j); rewrite ltnS.
+rewrite mcoeffMX mcoeff_mwiden mnmDE mulmnE mnm1E eqxx mul1n.
+rewrite -[X in (_ + _)%N == X]addn0 eqn_add2l.
+under eq_mktuple => j.
+  rewrite multinomE /tnth/= nth_rcons size_tuple ltn_ord -tnth_nth -uE.
+  rewrite -mnm_tnth multinomE.
+  over.
+under eq_mktuple do rewrite tnth_mktuple.
+by rewrite uE.
 Qed.
 
 Lemma muniK (A : ringType) : cancel (@muni n A) (@mmulti n A).
@@ -2132,7 +2043,6 @@ rewrite mnmE multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple (ltn_ord j).
 by rewrite -mnm_nth.
 Qed.
 
-
 End MoreMultinomials.
 
 Section MoreRealClosed.