Nicolò Cavalleri (Jun 10 2021 at 18:13): 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
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?
Manuel Eberl (Jun 10 2021 at 19:48):There is one in Lp.Functional_Spaces in the AFP…
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.
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)?
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
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.
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.
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)"
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.
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
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
You cannot do that in Isabelle. Typeclass instances must always be for a type constructor.
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.
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
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)withtype_definition, then you can instantiate it in whichever way you want
Ok thanks this is what I was looking for!
Manuel Eberl (Jun 11 2021 at 11:00):Sorry, type classes in Isabelle are just not very flexible… It's a known problem.
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.
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: Apr 19 2024 at 01:05 UTC