Discussion:
[isabelle] type unification failed using an old lemma?
A.L. Hicks
2016-08-05 14:29:49 UTC
Hi,

Sorry in advance if this is some trivial error on my part.
I'd like to use the lemma has_vector_derivative_mult in the HOL library

"lemma has_vector_derivative_mult[derivative_intros]:
"(f has_vector_derivative f') (at x within s) ⟹ (g
has_vector_derivative g') (at x within s) ⟹
((λx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a ::
real_normed_algebra)) (at x within s)"
by (rule bounded_bilinear.has_vector_derivative[OF
bounded_bilinear_mult])"

However it seems that using a statement such as

have "((λx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a
:: real_normed_algebra)) (at x within {a .. b})"

leads to a standard type unification error:

Type unification failed: Clash of types "_ ⇒ _" and "real"
Type error in application: incompatible operand type
Operator: op * (f x) :: real ⇒ real
Operand: g' :: real ⇒ real
Coercion Inference:
Local coercion insertion on the operand failed:
No coercion known for type constructors: "fun" and "real"

Am I missing something or is the lemma itself flawed?

As an aside, there is a similar lemma for the has_derivative operator:
has_derivative_mult
which works for statements like
have "((%x. f x * g x) has_derivative (%y. f x * g' y + f' y * g x))
(at x within {a .. b})"
Say I have h=(%x. f x * g x), I can obtain h' such that h has_derivative
h but can't seem to define h' explicitly.

Thanks,
Alex Hicks
Mark Wassell
2016-08-05 15:47:08 UTC
Hi,

have "((λx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a ::
real_normed_algebra)) (at x within {a .. b})"

has "given" g' the type real ⇒ real

Have you perhaps said

(g has_derivative g') rather than (g has_vector_derivative g') ?

Mark
Post by A.L. Hicks
Hi,
Sorry in advance if this is some trivial error on my part.
I'd like to use the lemma has_vector_derivative_mult in the HOL library
"(f has_vector_derivative f') (at x within s) ⟹ (g has_vector_derivative
g') (at x within s) ⟹
real_normed_algebra)) (at x within s)"
by (rule bounded_bilinear.has_vector_derivative[OF
bounded_bilinear_mult])"
However it seems that using a statement such as
real_normed_algebra)) (at x within {a .. b})"
Type unification failed: Clash of types "_ ⇒ _" and "real"
Type error in application: incompatible operand type
Operator: op * (f x) :: real ⇒ real
Operand: g' :: real ⇒ real
No coercion known for type constructors: "fun" and "real"
Am I missing something or is the lemma itself flawed?
has_derivative_mult
which works for statements like
have "((%x. f x * g x) has_derivative (%y. f x * g' y + f' y * g x)) (at
x within {a .. b})"
Say I have h=(%x. f x * g x), I can obtain h' such that h has_derivative h
but can't seem to define h' explicitly.
Thanks,
Alex Hicks