Type Mismatch with coe to fun

Stream: new members

[Shing Tak Lam]

import data.polynomial
       data.real.basic

open polynomial

structure polynomial_derivation (R : Type) [comm_ring R] :=
(to_fun : polynomial R → polynomial R) -- Delta
(map_add' : ∀ (f g : polynomial R), to_fun (f + g) = to_fun f + to_fun g)
(map_C_mul' : ∀ (k : R) (f : polynomial R), to_fun (polynomial.C k * f) = polynomial.C k * to_fun f)
(map_mul' : ∀ (f g : polynomial R), to_fun (f * g) = f * to_fun g + g * to_fun f)

namespace polynomial_derivation

variables {R : Type} [comm_ring R]

instance : has_coe_to_fun (polynomial_derivation R) :=
{ F := λ _, polynomial R → polynomial R,
  coe := to_fun
}

end polynomial_derivation

variable Δ : polynomial ℝ → polynomial ℝ
include Δ

variable Δ1 : Δ X = C 1
variable Δ2 : ∀ (f g : polynomial ℝ), Δ(f + g) = Δ f + Δ g
variable Δ3 : ∀ (k : ℝ) (f : polynomial ℝ), Δ(C k * f) = C k * Δ f
variable Δ4 : ∀ (f g : polynomial ℝ), Δ(f * g) = f * Δ g + g * Δ f
include Δ1 Δ2 Δ3 Δ4

definition d : polynomial_derivation ℝ :=
{ to_fun := Δ,
  map_add' := Δ2,
  map_C_mul' := Δ3,
  map_mul' := Δ4 }

theorem d_is_differentiation (p : polynomial ℝ) : d p = derivative p := sorry

There is a type mismatch at d p in the last line. The error message is

type mismatch at application
  d p
term
  p
has type
  polynomial ℝ
but is expected to have type
  polynomial ℝ → polynomial ℝ

[Shing Tak Lam]

I would think that since polynomial_derivation has _coe_to_fun, I would expect that d p = d.to_fun p = Δ p. And Δ : polynomial ℝ → polynomial ℝ. So Δ p : polynomial ℝ.

[Shing Tak Lam]

Figured it out (maybe?) The variables are hypotheses in d, so I need to use (d Δ Δ1 Δ2 Δ3 Δ4) p

[Kevin Buzzard]

Isn't there any way you can get Delta and all the Delta_i to be included automatically?What does include do if not this?

[Reid Barton]

parameters

[Reid Barton]

include makes sure that Δ1 Δ2 Δ3 Δ4 are included as arguments at the definition of d. It doesn't do anything at the use sites of d.