Stream: Beginner Questions

Topic: Sum of functions


view this post on Zulip Nicolò Cavalleri (Jun 10 2021 at 18:13):

Where is the exact point in the HOL library where it is proven that if the type 'a has an instance as a real_vector then functions valued in 'a also do? How do I find out these kind of things? On Lean ctrl+click on + takes you to the instance where that type has been given addition but in Isabelle it takes you to the point where + is introduced in Isabelle

view this post on Zulip Manuel Eberl (Jun 10 2021 at 19:45):

There is no real_vector instance for functions in either HOL or HOL-Analysis. What library are you using exactly?

view this post on Zulip Manuel Eberl (Jun 10 2021 at 19:48):

There is one in Lp.Functional_Spaces in the AFP…

view this post on Zulip Manuel Eberl (Jun 10 2021 at 19:49):

I don't know if there is a general way to find out where exactly a particular typeclass instance for a particular type constructor was proven.

view this post on Zulip Nicolò Cavalleri (Jun 10 2021 at 22:50):

I am using the smooth manifolds library. I guess

instance "fun" :: (type, real_vector) real_vector
  by standard (auto simp: scaleR_fun_def algebra_simps)

is then the point where such instance is defined... What is exactly the syntax "fun" :: (type, real_vector)?

view this post on Zulip Jakub Kądziołka (Jun 10 2021 at 22:55):

instance a :: (b, c) d means that 't 'u a :: d if 't :: b and 'u :: c

view this post on Zulip Manuel Eberl (Jun 11 2021 at 08:52):

And "fun" is the internal name of the function type constructor. When you write 'a ⇒ 'b, the internal representation of that type is ('a, 'b) fun.

view this post on Zulip Manuel Eberl (Jun 11 2021 at 08:53):

I see, the Smooth Manifold entry defines its own vector space instance for functions – presumably in the same way as the Lp entry.

view this post on Zulip Nicolò Cavalleri (Jun 11 2021 at 10:51):

Can I write the instantiation in an equivalent way as

instantiation "'a ⇒ ('b :: real_vector)" :: real_vector

somehow? It tells me Undefined type name: "'a ⇒ ('b :: real_vector)"

view this post on Zulip Manuel Eberl (Jun 11 2021 at 10:53):

No, you have to write instantiation "fun" :: (type, real_vector) real_vector. The bit before the :: has to be a type constructor.

view this post on Zulip Nicolò Cavalleri (Jun 11 2021 at 10:57):

Ok, my final goal is to put an instance of real_vector on the type ('a × (('a ⇒ real) ⇒ real)) which ignores the first coordinate and treats pairs as if they were they second coordinate. Does this mean that I have to put an instance on a generic product of a type and a real vector space? This will probably collide with the instance of product of vector spaces which is more standard I guess

view this post on Zulip Nicolò Cavalleri (Jun 11 2021 at 10:58):

Indeed it says

Conflict of type arities:
  prod :: (type, real_vector) cancel_ab_semigroup_add and
  prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add

view this post on Zulip Manuel Eberl (Jun 11 2021 at 10:58):

You cannot do that in Isabelle. Typeclass instances must always be for a type constructor.

view this post on Zulip Manuel Eberl (Jun 11 2021 at 10:59):

What you are trying to do would require something like FlexibleInstances and OverlappingInstances in Haskell, which the Isabelle type class system just doesn't support.

view this post on Zulip Manuel Eberl (Jun 11 2021 at 10:59):

The only way around this would be to introduce a type clone of 'a × (('a ⇒ real) ⇒ real) with type_definition, then you can instantiate it in whichever way you want

view this post on Zulip Nicolò Cavalleri (Jun 11 2021 at 11:00):

Manuel Eberl said:

The only way around this would be to introduce a type clone of 'a × (('a ⇒ real) ⇒ real) with type_definition, then you can instantiate it in whichever way you want

Ok thanks this is what I was looking for!

view this post on Zulip Manuel Eberl (Jun 11 2021 at 11:00):

Sorry, type classes in Isabelle are just not very flexible… It's a known problem.

view this post on Zulip Lukas Stevens (Jun 11 2021 at 11:06):

It would be nice to have some kind of deriving via typedef mechanism like in Haskell. This wouldn't require any changes to the core typeclass mechanism.

view this post on Zulip Lukas Stevens (Jun 11 2021 at 13:31):

Lukas Stevens said:

It would be nice to have some kind of deriving via typedef mechanism like in Haskell. This wouldn't require any changes to the core typeclass mechanism.

A topic for a student perhaps?


Last updated: Aug 13 2022 at 06:26 UTC