From 9dc4d9b9130ee30c5a16ea1ea0f7d2ef98f2859c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 22 Jul 2024 18:06:05 +0200 Subject: [PATCH] towards muniK --- auxresults.v | 2 +- cylinder.v | 188 ++++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 181 insertions(+), 9 deletions(-) diff --git a/auxresults.v b/auxresults.v index 90b46aa..11483d3 100644 --- a/auxresults.v +++ b/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. diff --git a/cylinder.v b/cylinder.v index bce548a..11ad33d 100644 --- a/cylinder.v +++ b/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