Skip to content

[WIP] replace the infrastructure of mpoly with monalg #116

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
pi8027 wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

[WIP] replace the infrastructure of mpoly with monalg #116

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4524b6c
Add cmmap and fmmap: evaluation functions for monomials
pi8027 Apr 9, 2026
2aceb8f
[WIP] replace the infrastructure of mpoly with monalg
pi8027 Aug 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
141 changes: 121 additions & 20 deletions src/monalg.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
From mathcomp Require Import tuple bigop ssralg ssrint ssrnum.
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)

Require Import xfinmap.

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.6.0-rocq-prover-9.2) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.6.0-rocq-prover-9.2) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.6.0-rocq-prover-9.2) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.6.0-rocq-prover-9.2) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.6.0-rocq-prover-9.3) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.6.0-rocq-prover-9.3) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.6.0-rocq-prover-9.3) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.6.0-rocq-prover-9.3) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Set Implicit Arguments.
Unset Strict Implicit.
Expand Down Expand Up @@ -45,7 +45,7 @@
Reserved Notation "g @_ k"
(at level 3, k at level 2, left associativity, format "g @_ k").
Reserved Notation "c %:MP" (format "c %:MP").
Reserved Notation "''X_{1..' n '}'".
Reserved Notation "''X_{1..' n '}'" (n at level 2).
Reserved Notation "'U_(' n )" (format "'U_(' n )").
Reserved Notation "x ^[ f , g ]" (at level 1, format "x ^[ f , g ]").

Expand Down Expand Up @@ -279,6 +279,10 @@
HB.lock Definition mkmalgU (K : choiceType) (G : nmodType) (k : K) (x : G) :=
[malg y in [fset k] => x].

(* FIXME *)
Definition mkmalgU' (K : choiceType) (G : nmodType) (x : G) (k : K) :=
mkmalgU k x.

Arguments mcoeff {K G} x%_monom_scope g%_ring_scope.
#[warning="-deprecated-reference"]
Arguments mkmalg {K G} _.
Expand Down Expand Up @@ -935,6 +939,12 @@
GRing.isMonoidMorphism.Build R {malg R[K]} (@malgC K R)
malgC_is_monoid_morphism.

Fact mkmalgU'_is_mmorphism : mmorphism (@mkmalgU' K R 1).
Proof. by split => // x y; rewrite [RHS]fgmulUU mul1r. Qed.

HB.instance Definition _ :=
isMultiplicative.Build _ _ (@mkmalgU' K R 1) mkmalgU'_is_mmorphism.

Lemma mpolyC1E : 1%:MP = 1 :> {malg R[K]}.
Proof. exact: rmorph1. Qed.

Expand Down Expand Up @@ -1324,22 +1334,18 @@
Arguments monalgOver_pred _ _ _ _ /.

(* -------------------------------------------------------------------- *)
HB.mixin Record isMeasure (M : monomType) (mf : M -> nat) := {
HB.mixin Record isWeakMeasure (M : monomType) (mf : M -> nat) := {
mfM : {morph mf : m1 m2 / (m1 * m2)%M >-> (m1 + m2)%N};
mf_eq0I : forall m, mf m = 0%N -> m = 1%M
}.

#[short(type="measure")]
HB.structure Definition Measure (M : monomType) := {mf of isMeasure M mf}.

#[deprecated(since="multinomials 2.5.0", note="Use Measure.clone instead.")]
Notation "[ 'measure' 'of' f ]" := (Measure.clone _ f _)
(at level 0, only parsing) : form_scope.
#[short(type="weakMeasure")]
HB.structure Definition WeakMeasure (M : monomType) :=
{mf of isWeakMeasure M mf}.

(* -------------------------------------------------------------------- *)
Section MMeasure.
Section WeakMeasure.

Context (M : monomType) (G : nmodType) (mf : measure M).
Context (M : monomType) (G : nmodType) (mf : weakMeasure M).

Implicit Types (g : {malg G[M]}).

Expand All @@ -1356,9 +1362,6 @@
mf (\prod_(x <- r | P x) F x)%M = (\sum_(x <- r | P x) mf (F x))%N.
Proof. exact/big_morph/mf1/mfM. Qed.

Lemma mf_eq0 m : (mf m == 0%N) = (m == 1%M).
Proof. by apply/eqP/eqP=> [|->]; rewrite ?mf1 // => /mf_eq0I. Qed.

Definition mmeasure g := (\max_(m <- msupp g) (mf m).+1)%N.

Lemma mmeasureE g : mmeasure g = (\max_(m <- msupp g) (mf m).+1)%N.
Expand Down Expand Up @@ -1412,12 +1415,47 @@
Lemma mmeasure_msupp0 g : (mmeasure g == 0%N) = (msupp g == fset0).
Proof. by rewrite mmeasure_eq0 msupp_eq0. Qed.

End MMeasure.
End WeakMeasure.

Lemma mmeasureN M (G : zmodType) (mf : measure M) (g : {malg G[M]}) :
Lemma mmeasureN M (G : zmodType) (mf : weakMeasure M) (g : {malg G[M]}) :
mmeasure mf (- g) = mmeasure mf g.
Proof. by rewrite mmeasureE msuppN. Qed.

(* -------------------------------------------------------------------- *)
HB.mixin Record WeakMeasure_isMeasure (M : monomType) (mf : M -> nat) := {
mf_eq0I : forall m, mf m = 0%N -> m = 1%M
}.

#[short(type="measure")]
HB.structure Definition Measure (M : monomType) :=
{mf of WeakMeasure M mf & WeakMeasure_isMeasure M mf}.

HB.factory Record isMeasure (M : monomType) (mf : M -> nat) := {
mfM : {morph mf : m1 m2 / (m1 * m2)%M >-> (m1 + m2)%N};
mf_eq0I : forall m, mf m = 0%N -> m = 1%M
}.

HB.builders Context M mf & isMeasure M mf.
HB.instance Definition _ := isWeakMeasure.Build M mf mfM.
HB.instance Definition _ := WeakMeasure_isMeasure.Build M mf mf_eq0I.
HB.end.

#[deprecated(since="multinomials 2.5.0", note="Use Measure.clone instead.")]
Notation "[ 'measure' 'of' f ]" := (Measure.clone _ f _)
(at level 0, only parsing) : form_scope.

(* -------------------------------------------------------------------- *)
Section Measure.

Context (M : monomType) (G : nmodType) (mf : measure M).

Implicit Types (g : {malg G[M]}).

Lemma mf_eq0 m : (mf m == 0%N) = (m == 1%M).
Proof. by apply/eqP/eqP=> [|->]; rewrite ?mf1 // => /mf_eq0I. Qed.

End Measure.

(* -------------------------------------------------------------------- *)
Section CmonomDef.

Expand All @@ -1427,6 +1465,8 @@

Coercion cmonom_val : cmonom >-> fsfun.

Definition exp_of_cmonom (i : I) (m : cmonom) : nat := cmonom_val m i.

Fact cmonom_key : unit. Proof. by []. Qed.

#[deprecated(since="multinomials 2.5.0", use=CMonom)]
Expand Down Expand Up @@ -1523,6 +1563,9 @@
#[deprecated(since="multinomials 2.5.0", use=expmn)]
Definition expcmn m n : cmonom I := expmn m n.

HB.instance Definition _ i :=
isWeakMeasure.Build _ (exp_of_cmonom i) (fun m1 m2 => mulcmE m1 m2 i).

End CmonomCanonicals.

HB.instance Definition _ (I : countType) := [Countable of cmonom I by <:].
Expand Down Expand Up @@ -1556,6 +1599,9 @@
Lemma cmM i m1 m2 : (m1 * m2)%M i = (m1 i + m2 i)%N.
Proof. exact/mulcmE. Qed.

Lemma cmX i m n : expmn m n i = (n * m i)%N.
Proof. exact: (mfX (exp_of_cmonom _)). Qed.

Lemma cmE_eq0 m i : (m i == 0%N) = (i \notin finsupp m).
Proof. by rewrite memNfinsupp. Qed.

Expand Down Expand Up @@ -1608,7 +1654,6 @@
by case: mdomP=> // ki /eqP; rewrite (big_fsetD1 i) //= addn_eq0 => /andP[/eqP].
Qed.

(* -------------------------------------------------------------------- *)
#[hnf] HB.instance Definition _ := isMeasure.Build (cmonom I)
mdeg mdegM mdeg_eq0I.

Expand All @@ -1630,6 +1675,21 @@
Lemma cm1_eq1 i : (U_(i) == 1)%M = false.
Proof. by rewrite -mdeg_eq0 mdegU. Qed.

Lemma cm_prodEw m (d : {fset I}) : finsupp m `<=` d ->
m = (\prod_(i <- d) expmn U_(i) (m i))%M.
Proof.
move=> le; apply/eqP/cmP => i; rewrite [RHS](mf_prod (exp_of_cmonom _)).
case: mdomP=> im; last first.
apply/esym/big1_fset => /= j jd _; rewrite [LHS]cmX cmU mulnC.
by case: eqP im => // <-; case: mdomP.
rewrite (big_fsetD1 i) /=; first exact: (fsubsetP le).
rewrite /exp_of_cmonom cmX cmUU muln1 big1_fset; last by rewrite addn0.
by move=> j; rewrite !inE => /andP[ji jd] _; rewrite cmX mulnC cmU (negbTE ji).
Qed.

Lemma cm_prodE m : m = (\prod_(i <- finsupp m) expmn U_(i) (m i))%M.
Proof. exact/cm_prodEw. Qed.

End CmonomTheory.

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -1664,15 +1724,13 @@
by rewrite muln_eq0 orbF => z_mi; apply/eqP/z_mi.
Qed.

(* -------------------------------------------------------------------- *)
#[hnf] HB.instance Definition _ := isMeasure.Build 'X_{1..n}
mnmwgt mnmwgtM mnmwgt_eq0I.

#[deprecated(since="multinomials 2.6.0", use=mf1)]
Lemma mnmwgt1 : mnmwgt 1%M = 0%N. Proof. exact/mf1. Qed.

Lemma mnmwgt_eq0 m : (mnmwgt m == 0%N) = (m == 1%M).
Proof. exact/mf_eq0. Qed.
Lemma mnmwgt_eq0 m : (mnmwgt m == 0%N) = (m == 1%M). Proof. exact/mf_eq0. Qed.

End MWeight.

Expand Down Expand Up @@ -1709,6 +1767,33 @@
Definition msizeN (I : choiceType) (G : zmodType) :=
@mmeasureN (cmonom I) G mdeg.

Section CMMap.

Definition cmmap
{I : choiceType} {R : pzSemiRingType} (f : I -> R) (m : cmonom I) :=
\prod_(k <- finsupp m) f k ^+ m k.

@pi8027 pi8027 Apr 14, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So, this is the definition of the evaluation function for commutative monomials. The problem is that, there is no guarantee that support finsupp m is sorted by some order on I; thus, widening the support (by cmmapw below) may change the order of the support, and thus requires R to be commutative.


Context (I : choiceType) (R : comPzSemiRingType) (f : I -> R).

Lemma cmmapw (d : {fset I}) (m : {cmonom I}) :
finsupp m `<=` d -> cmmap f m = \prod_(k <- d) f k ^+ m k.
Proof.
by move=> md; apply: big_fset_incl md _ => x xd; rewrite -cmE_eq0 => /eqP->.
Qed.

Fact cmmap_is_mmorphism : mmorphism (cmmap f).
Proof.
split=> [|x y]; first by rewrite /cmmap mdom1 big_seq_fset0.
rewrite [cmmap f x](cmmapw (fsubsetUl _ (finsupp y))).
rewrite [cmmap f y](cmmapw (fsubsetUr (finsupp x) _)).
by rewrite -big_split/= /cmmap mdomD; apply/eq_bigr => i _; rewrite cmM exprD.
Qed.

HB.instance Definition _ :=
isMultiplicative.Build _ _ (cmmap f) cmmap_is_mmorphism.

End CMMap.

(* -------------------------------------------------------------------- *)
Section FmonomDef.

Expand Down Expand Up @@ -1846,3 +1931,19 @@
Proof. by rewrite -fdeg_eq0 fdegU. Qed.

End FmonomTheory.

Section FMMap.

Context (I : choiceType) (R : pzSemiRingType) (f : I -> R).

Definition fmmap (m : fmonom I) := \prod_(k <- m) f k.

Fact fmmap_is_mmorphism : mmorphism fmmap.
Proof.
split=> [|x y]; first by rewrite /fmmap [1%M]fmoneE/= big_nil.
by rewrite /fmmap [(x * y)%M]fmmulE/= big_cat/=.
Qed.

HB.instance Definition _ := isMultiplicative.Build _ _ fmmap fmmap_is_mmorphism.

End FMMap.
Loading
Loading