Testing polynomial definition (from natural numbers to integers)

Question

For my first formalization. I want to define polynomials in Lean. The first attempt is shown below:

def polynomial (f : ℕ  → ℤ  ) (p:  (∃m:ℕ , ∀ n : ℕ,  implies (n≥m) (f n = (0:ℤ )  ) )):= f

Now a want to test my definition using:

def test : ℕ → ℤ 
| 0 := (2:ℤ )
| 1 := (3:ℤ )
| 2 := (4:ℤ )
| _ := (0:ℤ )

But I am having trouble constructing the proof term:

 def prf : (∃m:ℕ , ∀ n : ℕ,  implies (n≥m ) (test n = (0:ℤ )  ) ):=
 exists.intro (3:ℕ ) (
 assume n : ℕ,
 nat.rec_on (n:ℕ) 
 ()
 ()
 )

Also feedback on the definition itself is welcome.

Answer 1

The formulation of def polynomial does not work. You tag your function to be a polynomial, but this can not be used from the logic itself. Especially, it doesn't allow us to set up type class instances for polynomials.

What we want is a subtype instead:

def polynomial (A : Type) [ring A] : Type :=
{p : ℕ -> A // ∃ m : ℕ, ∀ n ≥ m, p n = 0}

with this we can setup a instance

instance {A : Type} [ring A] : polynomial A := ...