Stream: new members

Topic: Type Mismatch with coe to fun

Shing Tak Lam (Mar 26 2020 at 15:41):

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_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 (Mar 26 2020 at 15:44):

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 (Mar 26 2020 at 15:49):

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

Kevin Buzzard (Mar 26 2020 at 15:54):

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 (Mar 26 2020 at 15:57):

parameters

Reid Barton (Mar 26 2020 at 15:59):

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.

Last updated: May 11 2021 at 23:11 UTC