Discussion:
[isabelle] type unification failed using an old lemma?
A.L. Hicks
2016-08-05 14:29:49 UTC
Raw Message
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
Raw Message
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

On 5 August 2016 at 15:24, A.L. Hicks <***@cam.ac.uk> wrote:

> 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
>
>