Zulip Chat Archive

Stream: new members

Topic: Type Mismatch with coe to fun


view this post on Zulip 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_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 ℝ

view this post on Zulip 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 ℝ.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Mar 26 2020 at 15:57):

parameters

view this post on Zulip 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