define polynomials recursively

Stream: maths

[Michael Nestor]

I know there is a standard polynomial library, but for self-instructive purposes I am trying to define them like so:

def polynomial (f: ℝ → ℝ) :
  (∃ c: ℝ, f = λ x: ℝ, c) ∨ -- f is constant, or ...
  (∃ g: ℝ → ℝ, ∃ c: ℝ, (polynomial g) ∧ f = λ x: ℝ, x * g(x) + c)

with error unknown identifier 'polynomial'

[Eric Wieser]

Did you mean to write := instead of :?

[Eric Wieser]

That says "let polynomial be a proof of the fact that ..."

[Eric Wieser]

But I expect you meant def polynomial (f: ℝ → ℝ) : Prop :=, "let polynomial be a proposition, defined as ..."

[Michael Nestor]

yes, whoops. but the error persists

[Junyan Xu]

You want inductive

import data.real.basic
inductive is_polynomial : (ℝ → ℝ) → Prop
| const (c : ℝ) : is_polynomial (λ x, c)
| X_mul_add_C (g) (c : ℝ) : is_polynomial g → is_polynomial (λ x, x * g x + c)

[Trebor Huang]

Recursive types are different from inductive types, and you mean the latter this time.

[Trebor Huang]

And there is a third thing called "types defined by recursion", which is also called recursive types sometimes, which is what your initial definition uses. However, your definition uses arbitrary recursion, which leads to inconsistency. You would have to do recursion on some decreasing argument.

[Johan Commelin]

@Michael Nestor There is also a mathematical issue with this definition: you've defined "polynomial function". But a polynomial is not a function. Over finite rings, you only have finitely many polynomial functions, but infinitely many polynomials.