Re: [isabelle] problem with sort inference



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.