Re: [isabelle] Pitfall with type-classes in Isar-Lemma format



On Sat, 21 Jan 2012, Peter Lammich wrote:

I recently ran into the following pitfall:

lemma pitfall1:
 notes [[show_sorts]]
 notes test = refl[where 'a='a]
 fixes x::"'a::default"
 shows "x=x"
 thm test -- "'a has the wrong sort here!"
 using test apply -

Now it outputs:
type variables:
 'a :: type
 'a :: default

and, of course, apply (rule test) fails. When inspecting this failure,
the already confused user gets the following trace from the unifier
(even with show_sorts turned on!)

The following types do not unify:
'a \<Rightarrow> 'a \<Rightarrow> bool
'a \<Rightarrow> 'a \<Rightarrow> bool



I would expect that a type-variable with the same name should also have
the same sort -- at least when I introduce it within the
scope of the very same lemma.

And even more strange, this pitfall can be resolved by just swapping the
notes and the fixes declaration:

lemma pitfall1_resolved:
 fixes x::"'a::default"
 notes [[show_sorts]]
 notes test = refl[where 'a='a]
 shows "x=x"
 by (rule test)

Is this just an exercise in driving the system into an unspecified / uninhabitable state, or does it have some practical significance?

There are many things happening in a compund theorem statement, and the use of the above words of "wrong", "expect", "strange" are meaningless in this context. Where is it ever specified that it should behave like that?
The above forms are very uncommon, so uncommon effects are to be expected.

I am not going to explain here the accidental behaviour of certain boundary cases in complex theorem statements: certain things are simultaneous here, other things are sequential, other things undefined.


Anyway, I've required some time to guess that "trace from the unifier" probably means Pattern.trace_unify_fail := true. But that is a global ML reference, so it already indicates that the related operations are not yet "localized". That means they don't observe the local context resulting from your "notes [[show_sorts]]", which is a bit odd anyway.

So when you say "even with show_sorts turned on", it is actually not turned on for the pattern unification module. When doing the more usual "declare [[show_sorts]]" before the lemma statement you get the sort information printed as expected.


	Makarius





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