Email Gateway (Aug 18 2022 at 15:12): Email Gateway (Aug 18 2022 at 15:12):From: Makarius <makarius@sketis.net>
On Fri, 28 May 2010, Stephan Merz wrote:
I'm having a problem with sort inference in Isabelle/HOL: when I enter
lemma "b = a ==> f a (g a) = f b (g b)"
the following types and sorts are inferred:
variables:
g :: 'a => 'c
f :: 'a => 'c => 'b
a, b :: 'a
type variables:
'a, 'b :: type
'c :: {}Note the sort {} for type variable 'c. This prevents me to do something like
lemma "b = a ==> f a (g a) = f b (g b)"
proof -
from fun_cong have "f a = f b ==> f a (g a) = f b (g a)"which yields
*** Type unification failed: Variable 'c::{} not of sort type
*** Type error in application: Incompatible operand type
This behaviour has been there from the very first day of type classes in
Isabelle. Until some years ago it was even more confusing, since Pure had
its own "logic" type class, simular to "type" in HOL.
Since we have a very powerful "user-space type system" mechanism for quite
some time already, I have experimented with a global "type improvement"
for Isabelle/HOL at some point, that specializes pending inference
parameters to something of sort HOL.type. Unfortunately, it did not fully
work out in certain border cases where the fully general types are needed
internally (maybe it can be attempted again at some later stage).
I can get around this problem by stating the lemma in the form
lemma "b = a ==> (f::'a => 'c => 'b) a ((g::'a => 'c) a) = f b (g b)"
that is by explicitly annotating the term with the inferred types (even
without stating sort constraints) -- I assume that is because the
explicitly given type variables receive the default sort "type"
Yes, the "default" sort is attached to any type variable that is explicit
in the text, but does not have a sort constraint yet -- either directly or
via the context.
BTW, the long statement form allows to express your local context
explicitly, without complicating the terms themselves:
lemma
fixes f :: "'a => 'c => 'b"
and g :: "'a => 'c"
assumes "b = a"
shows "f a (g a) = f b (g b)"
Makarius
Email Gateway (Aug 18 2022 at 15:23):From: Stephan Merz <Stephan.Merz@loria.fr>
I'm having a problem with sort inference in Isabelle/HOL: when I enter
lemma "b = a ==> f a (g a) = f b (g b)"
the following types and sorts are inferred:
variables:
g :: 'a => 'c
f :: 'a => 'c => 'b
a, b :: 'a
type variables:
'a, 'b :: type
'c :: {}
Note the sort {} for type variable 'c. This prevents me to do something like
lemma "b = a ==> f a (g a) = f b (g b)"
proof -
from fun_cong have "f a = f b ==> f a (g a) = f b (g a)"
which yields
*** Type unification failed: Variable 'c::{} not of sort type
*** Type error in application: Incompatible operand type
since fun_cong expects functions between types of sort "type".
I can get around this problem by stating the lemma in the form
lemma "b = a ==> (f::'a => 'c => 'b) a ((g::'a => 'c) a) = f b (g b)"
that is by explicitly annotating the term with the inferred types (even without stating sort constraints) -- I assume that is because the explicitly given type variables receive the default sort "type". I understand that the inferred type is more general, but it is actually useless. As a user, I find that behavior quite strange -- bug or feature?
Thanks,
Stephan
Last updated: Apr 18 2024 at 04:17 UTC