proposition: Lemma refine_mpoly_sum_eff n k f f' (p : mpoly k T) p' : (forall m, f m 0 = 0) -> refines (Rseqmultinom ==> eq ==> Reffmpoly (T:=T) (n:=n)) f f' -> refines Reffmpoly p p' -> refines Reffmpoly (\sum_(m <- msupp p) f m p@_m) (M.fold (fun m c => mpoly_add_eff (f' m c)) p' mp0_eff).
proof: Proof. move=> Hf ref_f; move: p. apply P.fold_rec. { move=> q' Eq' q Hq. suff -> : q = 0; [by rewrite msupp0 big_nil; apply refine_mp0_eff|]. apply /mpolyP => m. rewrite (refine_find_mpoly Hq (refine_seqmultinom_of_multinom m)). rewrite mcoeff0; case_eq (M.find (seqmultinom_of_multinom m) q') => [s|->]//. rewrite -F.find_mapsto_iff F.elements_mapsto_iff. by rewrite -in_InA_eq_key_elt_iff (proj1 (P.elements_Empty _ ) Eq'). } move=> m' c p'' q q' Hp'' Hq Hq' IH p Hp. pose m := multinom_of_seqmultinom_val k m'; pose cm := c *: 'X_[m]. have ref_m : refines Rseqmultinom m m'. { apply refine_multinom_of_seqmultinom_val. move: (Hq' m'); rewrite F.add_eq_o; [|by apply/mnmc_eq_seqP]; move=> Hm'. apply (@refine_size_mpoly _ _ _ _ Hp). by exists c; apply M.find_2. } have Hc : p@_m = c. { rewrite (refine_find_mpoly Hp ref_m) (Hq' m') F.add_eq_o //. apply E.eq_refl. } pose pmcm := p - cm. have Hpmcm : pmcm@_m = 0. { by rewrite mcoeffB mcoeffZ mcoeffX eqxx Hc mulr1 subrr. } have -> : \sum_(m <- msupp p) f m p@_m = f m c + \sum_(m <- msupp pmcm) f m pmcm@_m. { case_eq (m \in msupp p) => Hmsuppp. { rewrite (big_rem _ Hmsuppp) /= Hc; f_equal. rewrite /pmcm /cm -Hc -(perm_big _ (msupp_rem p m)) /=. apply eq_big_seq => i. rewrite mcoeffB mcoeffZ mcoeffX. rewrite mcoeff_msupp Hc -/cm -/pmcm -Hpmcm. case (@eqP _ m i) => [->|]; [by rewrite eqxx|]. by rewrite mulr0 subr0. } move: Hmsuppp; rewrite /pmcm /cm mcoeff_msupp Hc; move/eqP ->. by rewrite Hf add0r scale0r subr0. } eapply refines_apply. { eapply refines_apply; [by apply refine_mpoly_add_eff|]. apply: (@refines_apply _ _ eq). exact: trivial_refines. } apply IH. rewrite /pmcm /cm -Hc. apply (rem_mpoly_eff Hq Hq' Hp ref_m). Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)