Skip to content
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

Jump to bottom

[Merged by Bors] - perf: improve some instances in Polynomial #7434

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - perf: improve some instances in Polynomial #7434

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
61c6358
perf: improve some instances in Polynomial
ChrisHughes24 Sep 29, 2023
c5bca0a
line length
ChrisHughes24 Sep 29, 2023
67e284f
add TODOs
ChrisHughes24 Oct 4, 2023
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
49 changes: 35 additions & 14 deletions Mathlib/Data/Polynomial/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -291,18 +291,30 @@ instance natCast : NatCast R[X] :=
#align polynomial.has_nat_cast Polynomial.natCast

instance semiring : Semiring R[X] :=
Copy link
Collaborator

Choose a reason for hiding this comment

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

Would building up through the hierarchy to Semiring R[X] yield even better performance? Or would it be middling?

Copy link
Collaborator

Choose a reason for hiding this comment

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

Same with other ones below.

Copy link
Member Author

Choose a reason for hiding this comment

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

Possibly. I don't see why it would but it is certainly possible that it could because I don't fully understand this stuff

Copy link
Member Author

Choose a reason for hiding this comment

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

How about merging this and I experiment with further improvements in another PR?

Copy link
Collaborator

Choose a reason for hiding this comment

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

Sounds good to me.

Function.Injective.semiring toFinsupp toFinsupp_injective toFinsupp_zero toFinsupp_one
toFinsupp_add toFinsupp_mul (fun _ _ => toFinsupp_smul _ _) toFinsupp_pow fun _ => rfl
--TODO: add reference to library note in PR #7432
{ Function.Injective.semiring toFinsupp toFinsupp_injective toFinsupp_zero toFinsupp_one
toFinsupp_add toFinsupp_mul (fun _ _ => toFinsupp_smul _ _) toFinsupp_pow fun _ => rfl with
toNatCast := Polynomial.natCast
toAdd := Polynomial.add'
toMul := Polynomial.mul'
toZero := Polynomial.zero
toOne := Polynomial.one
nsmul := (. • .)
npow := fun n x => (x ^ n) }
#align polynomial.semiring Polynomial.semiring

instance distribSMul {S} [DistribSMul S R] : DistribSMul S R[X] :=
Function.Injective.distribSMul ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩ toFinsupp_injective
toFinsupp_smul
--TODO: add reference to library note in PR #7432
{ Function.Injective.distribSMul ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩ toFinsupp_injective
toFinsupp_smul with
toSMulZeroClass := Polynomial.smulZeroClass }
#align polynomial.distrib_smul Polynomial.distribSMul

instance distribMulAction {S} [Monoid S] [DistribMulAction S R] : DistribMulAction S R[X] :=
Function.Injective.distribMulAction ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩
toFinsupp_injective toFinsupp_smul
--TODO: add reference to library note in PR #7432
{ Function.Injective.distribMulAction ⟨⟨toFinsupp, toFinsupp_zero (R := R)⟩, toFinsupp_add⟩
toFinsupp_injective toFinsupp_smul with
toSMul := Polynomial.smulZeroClass.toSMul }
#align polynomial.distrib_mul_action Polynomial.distribMulAction

instance faithfulSMul {S} [SMulZeroClass S R] [FaithfulSMul S R] : FaithfulSMul S R[X] where
Expand All @@ -311,8 +323,10 @@ instance faithfulSMul {S} [SMulZeroClass S R] [FaithfulSMul S R] : FaithfulSMul
#align polynomial.has_faithful_smul Polynomial.faithfulSMul

instance module {S} [Semiring S] [Module S R] : Module S R[X] :=
Function.Injective.module _ ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩ toFinsupp_injective
toFinsupp_smul
--TODO: add reference to library note in PR #7432
{ Function.Injective.module _ ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩ toFinsupp_injective
toFinsupp_smul with
toDistribMulAction := Polynomial.distribMulAction }
#align polynomial.module Polynomial.module

instance smulCommClass {S₁ S₂} [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [SMulCommClass S₁ S₂ R] :
Expand Down Expand Up @@ -1154,9 +1168,16 @@ instance intCast : IntCast R[X] :=
#align polynomial.has_int_cast Polynomial.intCast

instance ring : Ring R[X] :=
Function.Injective.ring toFinsupp toFinsupp_injective toFinsupp_zero toFinsupp_one toFinsupp_add
toFinsupp_mul toFinsupp_neg toFinsupp_sub (fun _ _ => toFinsupp_smul _ _)
(fun _ _ => toFinsupp_smul _ _) toFinsupp_pow (fun _ => rfl) fun _ => rfl
--TODO: add reference to library note in PR #7432
{ Function.Injective.ring toFinsupp toFinsupp_injective (toFinsupp_zero (R := R))
toFinsupp_one toFinsupp_add
toFinsupp_mul toFinsupp_neg toFinsupp_sub (fun _ _ => toFinsupp_smul _ _)
(fun _ _ => toFinsupp_smul _ _) toFinsupp_pow (fun _ => rfl) fun _ => rfl with
toSemiring := Polynomial.semiring,
toIntCast := Polynomial.intCast
toNeg := Polynomial.neg'
toSub := Polynomial.sub
zsmul := ((. • .) : ℤ → R[X] → R[X]) }
#align polynomial.ring Polynomial.ring

@[simp]
Expand Down Expand Up @@ -1192,9 +1213,9 @@ theorem C_eq_int_cast (n : ℤ) : C (n : R) = n := by simp
end Ring

instance commRing [CommRing R] : CommRing R[X] :=
Function.Injective.commRing toFinsupp toFinsupp_injective toFinsupp_zero toFinsupp_one
toFinsupp_add toFinsupp_mul toFinsupp_neg toFinsupp_sub (fun _ _ => toFinsupp_smul _ _)
(fun _ _ => toFinsupp_smul _ _) toFinsupp_pow (fun _ => rfl) fun _ => rfl
--TODO: add reference to library note in PR #7432
{ toRing := Polynomial.ring
mul_comm := mul_comm }
#align polynomial.comm_ring Polynomial.commRing

section NonzeroSemiring
Expand Down
Loading