Simple polynomial computations

Stream: new members

[Ahmad Alkhalawi]

I was messing around with polynomials and I couldn't figure out how to do some simple computations. For example, I couldn't figure out how to show

example: coeff 1 2 = 0 := by
    sorry

and I felt like the proof I found for

example: leadingCoeff (2:Polynomial ℤ) = 2 := by
  unfold leadingCoeff
  have h: natDegree (2:Polynomial ℤ) = 0 := by
    refine natDegree_eq_zero.mpr ?_
    use 2
    simp
  rw[h]
  simp

should be easier. Is there a simpler way to do this?

[Moritz Firsching]

open Polynomial

example : leadingCoeff (2 : Polynomial ℤ) = 2 := by
  exact leadingCoeff_C 2

seems to work

[Moritz Firsching]

Instead of writing (2 : Polynomial ℤ) you could also write Polynomial.C 2 (or just C 2 since Polynomial is already open)

[Moritz Firsching]

the first one can be done with

example: coeff 1 2 = 0 := by
  simp [coeff_one]

[Luigi Massacci]

We have a tactic for that:

import Mathlib
open Polynomial

example: coeff 1 2 = 0 := by
  compute_degree

example: leadingCoeff (2:Polynomial ℤ) = 2 := by
  rw [leadingCoeff]
  compute_degree!
  compute_degree!

[Luigi Massacci]

Technically leadingCoeff is not explicitly in scope, but it seems like it should be

[Luigi Massacci]

Let us see what @Damiano Testa thinks of it

[Damiano Testa]

I agree on all counts: leadingCoeff is not in scope for compute_degree. The related tactic monicity is a simple macro that preprocesses a Monic goal. Probably there could be an easy win with leadingCoeff goals, but I have not gotten around to it.

[Damiano Testa]

I suspect that a more systematic approach would be to have an internal representation of polynomials as lists of coefficients and outsource all such computations on polynomials to analogous computations on lists.

[Damiano Testa]

This however has been in the air for many years, but no one has really had the time to go through with it.

[Damiano Testa]

There are some promising examples scattered on Zulip, though.

[Ahmad Alkhalawi]

Moritz Firsching said:

open Polynomial

example : leadingCoeff (2 : Polynomial ℤ) = 2 := by
  exact leadingCoeff_C 2

seems to work

Luigi Massacci said:

We have a tactic for that:

import Mathlib
open Polynomial

example: coeff 1 2 = 0 := by
  compute_degree

example: leadingCoeff (2:Polynomial ℤ) = 2 := by
  rw [leadingCoeff]
  compute_degree!
  compute_degree!

This works, thanks for the help