Computable polynomial representation based on sorted list

Stream: general

[Nick_adfor]

I'm wondering if it can help for this terrible problem about Chebyshev Polynomial...

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Chebyshev.20polynomial

[Patrick Massot]

This is the discussion thread for #announce > Computable polynomial representation based on sorted list @ 💬.

[Notification Bot]

A message was moved here from #announce > Computable polynomial representation based on sorted list by Patrick Massot.

[Hagb (Junyu Guo)]

Nick_adfor said:

I'm wondering if it can help for this terrible problem about Chebyshev Polynomial...

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Chebyshev.20polynomial

No, i think. The library handles "concrete" polynomials that don't depend on hypothesis (including variables like n : ℕ).

[Violeta Hernández]

Hope I'm getting this right... is this the third computable polynomial impl we get this month?

[Hagb (Junyu Guo)]

Violeta Hernández said:

Hope I'm getting this right... is this the third computable polynomial impl we get this month?

I saw the other two implementations. If I read the source code correctly,

• #announce > Auto Polynomial: An Experiment in Reflection for Polynomials @ 💬 represented a univariate polynomial with a List whose elements are coefficients of all (zero or non-zero) terms from exponent 0 to degree (dense representation based on list).
• #announce > Computable MvPolynomial + RingEquiv with MvPolynomial @ 💬 implemented the polynomial representation with Std.ExtTreeMap where a key is exponents of a non-zero term in polynomial, and the value of it is the coefficient of the term (sparse representation based on tree). It works well with decide +native, while for some reasons I don't know, it failed to reduce in kernel when I tested.
• #announce > Computable polynomial representation based on sorted list @ 💬 represented a polynomial with a List whose elements are exponent-coefficient pairs sorted by the exponent with a monomial order (sparse representation based on list).

CC: @Liam Schilling @František Silváši 🦉

[Liam Schilling]

Yes, we implemented a dense representation for use in our tactics. Although, our tactics operate using a generic interface for computable representations of polynomials and thus could immediately use any representation proved to meet the specification.

The following should work, although I'm not at my device to try it so please excuse if it has an error.

example : (X ^ 2 + C (-1) * X * X + X : Int[X]).degree = 1 := by poly_rfl_degree_eq_of_coeffs VIA CoeffList

Importantly, CoeffList could be replaced with any type that instantiates the interface (a type class).

[Liam Schilling]

@František Silváši 🦉's post which also proves RingEquivhas had me thinking: the reason that I don't believe our tactics are an immediate fit for Mathlib is that the interfaces they rely on are very ad hoc. So, I wonder if we could modify our tactics to work by assuming more Mathlib-standard "interfaces" like RingEquiv, and if then they could be integrated into Mathlib.

[Eric Wieser]

Does that work for rings which aren't Int?

[Eric Wieser]

Note that if you only care about computable coefficients, you can prove that with rfl by using the definitions on the wiki

import Mathlib

open scoped DirectSum

abbrev CPolynomial (R) [Semiring R] := ⨁ i : ℕ, R
abbrev CPolynomial.C {R} [CommSemiring R] : R →+* CPolynomial R :=algebraMap R (CPolynomial R)
abbrev CPolynomial.X {R} [Semiring R] : CPolynomial R := .single 1 1
def CPolynomial.degree {R} [Semiring R] [DecidableEq R] (x : CPolynomial R) : ℕ∞ :=
  if x = 0 then ⊥ else x.support.card

open CPolynomial

example : (X ^ 2 + C (-1 : ℤ) * X * X + X : CPolynomial Int).degree = 1 := by rfl

[Liam Schilling]

This tactic unfortunately requires DecidableEq, which it uses to eliminate leading zeros in the CoeffList. I think this could be changed with a little bit of reworking. Still, there are some symbolic examples where the tactic works but I believe CPolynomial would struggle. Like this:

example (a : Int) :
        (C a * X ^ 2 + C (-a) * X * X + X : Int[X]).degree = some 1 := by
    poly_rfl_degree_eq_of_coeffs VIA CoeffsList; simp

[Eric Wieser]

Indeed, there I need

example (a : Int) :
        (C a * X ^ 2 + C (-a) * X * X + X : CPolynomial Int).degree = some 1 := by
  simp only [map_neg]
  ring_nf
  rfl

which obviously isn't going to scale all that far

[Hagb (Junyu Guo)]

Eric Wieser said:

Note that if you only care about computable coefficients, you can prove that with rfl by using the definitions on the wiki

We (#announce > Computable polynomial representation based on sorted list @ 💬) tried to implement a more efficient representation.

Eric Wieser said:

Does that work for rings which aren't Int?

Yes if it is DecidableEq and the coefficients are concrete. We're thinking of establishing homomorphism or embedding from some computable types (such as ℕ, ℤ, ℚ, and ZMod n) to those noncomputable types such as ℝ or abstract ones such as {R : Type*} [CommRing R].

Liam Schilling said:

example (a : Int) :
        (C a * X ^ 2 + C (-a) * X * X + X : Int[X]).degree = some 1 := by
    poly_rfl_degree_eq_of_coeffs VIA CoeffsList; simp

We still cannot handle such kinds of goals which depend on hypothesis (such as a : Int here).

[Notification Bot]

3 messages were moved from this topic to #new members > Chebyshev polynomial by Eric Wieser.