towards muniK

auxresults.v

@@ -1211,7 +1211,7 @@ End MoreRoot.
 
 Local Open Scope ring_scope.
 
-Lemma subrBB (S : comRingType) (a b c : S) :
+Lemma subrBB (S : zmodType) (a b c : S) :
   (b - a) - (c - a) = b - c.
 Proof. by rewrite opprB addrC addrCA addrAC subrr add0r. Qed.
 

cylinder.v

@@ -1315,9 +1315,181 @@ rewrite -coef_map.
 by move/leq_sizeP: ifp; apply.
 Qed.
 
-(*Lemma muniK (n : nat) (A : ringType) : cancel (@muni n A) (@mmulti n A).
+(* TODO: find a suitable name *)
+Lemma big_neq_0 [S : Type] [idx : S] [op : Monoid.law idx] 
+    [I : eqType] (r : seq I) [P : pred I] [F : I -> S] (i : I):
+    uniq r ->
+    (forall j, P j -> j != i -> F j = idx) ->
+    \big[op/idx]_(j <- r | P j) F j = if P i && (i \in r) then F i else idx.
 Proof.
-move=> p.
+move=> + iP; elim: r => [|j r IHr].
+  by rewrite in_nil big_nil andbF.
+rewrite big_cons; move: (iP j).
+have [-> _ /= /andP[] ir ru {j}|ji] := eqVneq j i.
+  rewrite mem_head andbT big_mkcond big_seq -big_mkcondl.
+  under eq_bigr => j /andP[] Pj jr.
+    have ->: F j = idx.
+      move: jr; have [->|/(iP j Pj) -> _ //] := eqVneq j i.
+      by rewrite (negPf ir).
+    over.
+  rewrite big_const_idem ?Monoid.mulm1//.
+  exact/Monoid.mulm1.
+rewrite in_cons eq_sym (negPf ji)/= => /[swap] /andP[_] /IHr ->.
+case: (P j) => [/(_ isT isT) ->|_ //].
+by rewrite Monoid.mul1m.
+Qed.
+
+Lemma mcoeff_muni (n : nat) (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.
+Qed.
+
+Lemma mcoeff_mwiden n (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 _].
+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.
+  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 mcoeff_mmulti (n : nat) (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.
+under eq_bigr => /=.
+(big_neq_0 (
+(BMultinom m0, BMultinom (leqnn (mdeg m).+1))
+
+
+
+(* Lemma size_muni (n : nat) (A : ringType) (p : {mpoly A[n.+1]}) :
+  size (muni p) = \max_(m <- msupp p) m ord_max.
+Proof.
+apply/anti_leq/andP; split.
+  apply/leq_sizeP => i.
+  Search (\max_(_ <- _) _).
+Search size {poly _} "P".
+ *)
+
+Lemma muniK (n : nat) (A : ringType) : cancel (@muni n A) (@mmulti n A).
+Proof.
+move=> p; apply/mpolyP => m.
+
+Search mcoeff.
 apply/mpolyP => m.
 rewrite raddf_sum/=.
 under eq_bigr => i _.
@@ -1354,8 +1526,7 @@ case: (ltnP (m ord_max) (size (muni p))) => mlt; last first.
     over.
   rewrite big_pred0_eq.
   apply/esym/eqP; rewrite mcoeff_eq0.
-  Search Measure.type.
-  Check (@mmeasure_mnm_ge _ _ (fun m : 'X_{1.. n.+1} => m ord_max)).
+  Search size muni.
   Search msupp.
 
 
@@ -1817,10 +1988,11 @@ move=> p; case=> /= s /imfsetP [/=] t /bigfcupP [] {}s _ + ->.
 case: (roots2_on (S'const s)) => /= [] r [] rsort rroot tpart.
 have [p0|p0] := eqVneq (evalpmp (\val (pick s)) (muni (\val p))) 0.
   move=> x y xt yt.
-have t0 x : x \in (SAset_cast n.+1 t) -> (val p).@[tnth (ngraph x)] = 0 ->
-    forall y, y \in (SAset_cast n.+1 t) -> (val p).@[tnth (ngraph y)] = 0.
-  move=> xt px0.
-  have: (\row_i x ord0 (lift ord_max i) \in rootsR (evalpmp x (\prod_(p : P' s) val p))).
+  Search meval mmulti.
+have t0 u : u \in (SAset_cast n.+1 t) -> (val p).@[tnth (ngraph u)] = 0 ->
+    forall v, v \in (SAset_cast n.+1 t) -> (val p).@[tnth (ngraph v)] = 0.
+  move=> ut pu v.
+  have: (\row_i u ord0 (lift ord_max i) \in rootsR (evalpmp (\row_i u ord0 (lift ord_max i)) (\prod_(p : P' s) val p))).
   Search tuple_of _.-1.
 
 pose proots : {SAset R^n.+1} := [set| nquantify n.+1