Skip to content

Take advantage of the potentially-zero algebra structures #134

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

Merged
pi8027 merged 1 commit into from
Oct 31, 2026
Merged

Take advantage of the potentially-zero algebra structures #134

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
23 changes: 10 additions & 13 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 @@ -846,6 +846,9 @@
Lemma fgscaleAl c g1 g2 : c *: (g1 * g2) = (c *: g1) * g2.
Proof. by rewrite -!mul_malgC mulrA. Qed.

HB.instance Definition _ :=
GRing.LSemiModule_isLSemiAlgebra.Build R {malg R[K]} fgscaleAl.

Lemma mcoeffU1 k k' : (<< k >> : {malg R[K]})@_k' = (k == k')%:R.
Proof. by rewrite mcoeffU. Qed.

Expand Down Expand Up @@ -1011,18 +1014,12 @@
HB.instance Definition _ :=
GRing.PzSemiRing_isNonZero.Build {malg R[K]} fgoner_eq0.

HB.instance Definition _ :=
GRing.LSemiModule_isLSemiAlgebra.Build R {malg R[K]} (@fgscaleAl K R).

(* TODO: remove when requiring MC >= 2.6 *)
HB.instance Definition _ := GRing.RMorphism.on (mcoeff 1 : {malg R[K]} -> R).

End MalgNzSemiRingTheory.

(* -------------------------------------------------------------------- *)
Section MalgComNzSemiRingTheory.
Section MalgComPzSemiRingTheory.

Context (K : monomType) (R : comNzSemiRingType).
Context (K : monomType) (R : comPzSemiRingType).

Fact fgscaleAr c (g1 g2 : {malg R[K]}) : c *: (g1 * g2) = g1 * (c *: g2).
Proof.
Expand All @@ -1035,7 +1032,7 @@
HB.instance Definition _ :=
GRing.LSemiAlgebra_isSemiAlgebra.Build R {malg R[K]} fgscaleAr.

End MalgComNzSemiRingTheory.
End MalgComPzSemiRingTheory.

(* -------------------------------------------------------------------- *)
Section MalgComPzSemiRingTheory.
Expand All @@ -1055,12 +1052,16 @@
End MalgComPzSemiRingTheory.

(* FIXME: HB.saturate *)
HB.instance Definition _ (K : monomType) (R : comNzSemiRingType) :=
GRing.NzSemiRing.on {malg R[K]}.
HB.instance Definition _ (K : conomType) (R : comNzSemiRingType) :=
GRing.NzSemiRing.on {malg R[K]}.
HB.instance Definition _ (K : monomType) (R : pzRingType) :=
GRing.PzSemiRing.on {malg R[K]}.
HB.instance Definition _ (K : monomType) (R : nzRingType) :=
GRing.NzSemiRing.on {malg R[K]}.
HB.instance Definition _ (K : monomType) (R : comPzRingType) :=
GRing.PzSemiRing.on {malg R[K]}.
HB.instance Definition _ (K : conomType) (R : comPzRingType) :=
GRing.PzSemiRing.on {malg R[K]}.
HB.instance Definition _ (K : monomType) (R : comNzRingType) :=
Expand Down Expand Up @@ -1191,10 +1192,6 @@
End Linear.
End MalgMorphism.

(* TODO: remove when requiring MC >= 2.6 *)
HB.instance Definition _ K (R : comNzSemiRingType) (h : {mmorphism K -> R}) :=
GRing.Linear.on (mmap idfun h).

(* -------------------------------------------------------------------- *)
Section MonalgOver.
Section Def.
Expand Down
Loading