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 3 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
3 commits
Select commit Hold shift + click to select a range
9a17443
Generalize expcmn to expmn, which works for any monomType
pi8027 Aug 26, 2025
3a08297
Generalize cmM_eq1 and fmM_eq1 to mulm_eq1
pi8027 Aug 27, 2025
ae119ee
[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
62 changes: 44 additions & 18 deletions src/monalg.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
From mathcomp Require Import seq path choice finset fintype finfun.
From mathcomp Require Import tuple bigop ssralg ssrint ssrnum.

Require Import xfinmap.

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

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

Check warning on line 13 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

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

Set Implicit Arguments.
Unset Strict Implicit.
Expand Down Expand Up @@ -44,7 +44,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 @@ -136,11 +136,30 @@
#[export]
HB.instance Definition _ := Monoid.isLaw.Build M 1 mmul mulmA mul1m mulm1.

Definition expmn (x : M) (n : nat) : M := iterop n *%M x 1%M.

Arguments expmn : simpl never.

Lemma unitmP (x y : M) : reflect (x == 1 /\ y == 1) (x * y == 1).
Proof.
by apply: (iffP eqP)=> [/unitm[-> ->]|[/eqP-> /eqP->]] //; rewrite mulm1.
Qed.

Lemma mulm_eq1 (x y : M) : (x * y == 1) = (x == 1) && (y == 1).
Proof. exact/unitmP/andP. Qed.

Lemma expmnS (x : M) (n : nat) : expmn x n.+1 = x * expmn x n.
Proof. by rewrite /expmn !Monoid.iteropE iterS. Qed.

Lemma expmnD (x : M) (n m : nat) : expmn x (n + m) = expmn x n * expmn x m.
Proof.
elim: n => [|n IHn]; first by rewrite mul1m.
by rewrite addSn !expmnS IHn mulmA.
Qed.

Lemma expmnSr (x : M) (n : nat) : expmn x n.+1 = expmn x n * x.
Proof. by rewrite -addn1 expmnD. Qed.

End Monomial.

#[export]
Expand Down Expand Up @@ -225,12 +244,13 @@
#[deprecated(since="multinomials 2.5.0", note="Use Malg instead")]
Definition mkmalg : {fsfun K -> G with 0} -> {malg G[K]} := @Malg K G.

Definition mkmalgU (k : K) (x : G) := [malg y in [fset k] => x].

Definition msupp (g : {malg G[K]}) : {fset K} := finsupp (malg_val g).

End MalgBaseOp.

HB.lock Definition mkmalgU (K : choiceType) (G : nmodType) (k : K) (x : G) :=
[malg y in [fset k] => x].

Arguments mcoeff {K G} x%_monom_scope g%_ring_scope.
#[warning="-deprecated-reference"]
Arguments mkmalg {K G} _.
Expand Down Expand Up @@ -331,7 +351,7 @@
Lemma mcoeffMn k n : {morph mcoeff k: x / x *+ n} . Proof. exact: raddfMn. Qed.

Lemma mcoeffU k x k' : << x *g k >>@_k' = x *+ (k == k').
Proof. by rewrite [LHS]fsfunE inE mulrb eq_sym. Qed.
Proof. by rewrite unlock [LHS]fsfunE inE mulrb eq_sym. Qed.

Lemma mcoeffUU k x : << x *g k >>@_k = x.
Proof. by rewrite mcoeffU eqxx. Qed.
Expand Down Expand Up @@ -967,6 +987,9 @@
HB.instance Definition _ :=
GRing.LSemiModule_isLSemiAlgebra.Build R {malg R[K]} (@fgscaleAl K R).

(* FIXME: HB.saturate *)
HB.instance Definition _ := GRing.RMorphism.on (mcoeff 1 : {malg R[K]} -> R).

End MalgNzSemiRingTheory.

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -1275,7 +1298,7 @@

(* -------------------------------------------------------------------- *)
HB.mixin Record isMeasure (M : monomType) (mf : M -> nat) := {
mf0 : mf 1%M = 0%N;
mf1 : mf 1%M = 0%N;
mfM : {morph mf : m1 m2 / (m1 * m2)%M >-> (m1 + m2)%N};
mf_eq0I : forall m, mf m = 0%N -> m = 1%M
}.
Expand All @@ -1295,7 +1318,7 @@
Implicit Types (g : {malg G[M]}).

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

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

Expand All @@ -1317,7 +1340,7 @@
Lemma mmeasureC c : mmeasure c%:MP = (c != 0%R) :> nat.
Proof.
rewrite mmeasureE msuppC; case: (_ == 0)=> /=.
by rewrite big_nil. by rewrite big_seq_fset1 mf0.
by rewrite big_nil. by rewrite big_seq_fset1 mf1.
Qed.

Lemma mmeasureD_le g1 g2 :
Expand Down Expand Up @@ -1376,6 +1399,9 @@

End CmonomDef.

Arguments cmonom_val : simpl never.
Bind Scope monom_scope with cmonom.

Notation "{ 'cmonom' I }" := (cmonom I) : type_scope.
Notation "''X_{1..' n '}'" := (cmonom 'I_n) : type_scope.
Notation "{ 'mpoly' R [ n ] }" := {malg R['X_{1..n}]} : type_scope.
Expand All @@ -1393,8 +1419,8 @@

Context (I : choiceType).

HB.instance Definition _ := [isNew for @cmonom_val I].
HB.instance Definition _ := [Choice of cmonom I by <:].
#[hnf] HB.instance Definition _ := [isNew for @cmonom_val I].
#[hnf] HB.instance Definition _ := [Choice of cmonom I by <:].

(* -------------------------------------------------------------------- *)
Implicit Types (m : cmonom I).
Expand All @@ -1407,7 +1433,7 @@
by rewrite [mkcmonom]unlock.
Qed.

Lemma cmP m1 m2 : reflect (forall i, m1 i = m2 i) (m1 == m2).
Lemma cmP m1 m2 : reflect (m1 =1 m2) (m1 == m2).
Proof. by apply: (iffP eqP) => [->//|eq]; apply/val_inj/fsfunP. Qed.

Definition onecm : cmonom I := CMonom [fsfun of _ => 0%N].
Expand All @@ -1419,8 +1445,6 @@

Definition divcm m1 m2 : cmonom I := [cmonom m1 i - m2 i | i in finsupp m1]%M.

Definition expcmn m n : cmonom I := iterop n mulcm m onecm.

Lemma onecmE i : onecm i = 0%N.
Proof. by rewrite fsfun_ffun insubF. Qed.

Expand Down Expand Up @@ -1455,12 +1479,16 @@
by move=> m1 m2 h; split; move: h; last rewrite mulcmC; apply/gen.
Qed.

#[hnf]
HB.instance Definition _ := Choice_isMonomialDef.Build (cmonom I)
mulcmA mul0cm mulcm0 mulcm_eq0.
#[hnf]
HB.instance Definition _ := MonomialDef_isConomialDef.Build (cmonom I) mulcmC.

End CmonomCanonicals.

HB.instance Definition _ (I : countType) := [Countable of cmonom I by <:].

(* -------------------------------------------------------------------- *)
Definition mdeg {I : choiceType} (m : cmonom I) :=
(\sum_(k <- finsupp m) m k)%N.
Expand Down Expand Up @@ -1557,9 +1585,6 @@
Lemma mdeg_eq0 m : (mdeg m == 0%N) = (m == 1%M).
Proof. exact/mf_eq0. Qed.

Lemma cmM_eq1 m1 m2 : (m1 * m2 == 1)%M = (m1 == 1%M) && (m2 == 1%M).
Proof. by rewrite -!mdeg_eq0 mdegM addn_eq0. Qed.

Lemma cm1_eq1 i : (U_(i) == 1)%M = false.
Proof. by rewrite -mdeg_eq0 mdegU. Qed.

Expand Down Expand Up @@ -1658,6 +1683,8 @@

End FmonomDef.

Bind Scope monom_scope with fmonom.

Notation "{ 'fmonom' I }" := (fmonom I) : type_scope.

Local Notation mkfmonom s := (fmonom_of_seq fmonom_key s).
Expand Down Expand Up @@ -1714,6 +1741,8 @@

End FmonomCanonicals.

HB.instance Definition _ (I : countType) := [Countable of fmonom I by <:].

(* -------------------------------------------------------------------- *)
Definition fdeg (I : choiceType) (m : fmonom I) := size m.

Expand Down Expand Up @@ -1766,9 +1795,6 @@
Lemma fdeg_eq0 m : (fdeg m == 0%N) = (m == 1%M).
Proof. exact/mf_eq0. Qed.

Lemma fmM_eq1 m1 m2 : (m1 * m2 == 1)%M = (m1 == 1%M) && (m2 == 1%M).
Proof. by rewrite -!fdeg_eq0 fdegM addn_eq0. Qed.

Lemma fm1_eq1 i : (U_(i) == 1)%M = false.
Proof. by rewrite -fdeg_eq0 fdegU. Qed.

Expand Down
Loading
Loading