[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Thu, 2 May 2013, Stefan Berghofer wrote:

> On 04/12/2013 02:18 PM, Makarius wrote:
>> Just for completeness, I am posting here a self-contained example to expose 
>> the problem.
>> 
>> It looks like I need to discuss it further with Stefan Berghofer, because 
>> he made some reforms there in 2005 that now seem to crash on us.
>
> it is not particularly surprising that the attached example leads to a 
> TYPE exception. A closer look at the disagreement pairs reveals that the 
> variable ?n6 indeed appears with two distinct types.


> Note that before the "reforms" mentioned above, most of the substitution 
> functions used in unify.ML simply ignored types and therefore were 
> likely to produce ill-formed terms when applied to terms containing 
> variables with same name but different types.

What I've had in mind was e.g. this:

changeset:   16652:4ecf94235ec7
user:        berghofe
date:        Fri Jul 01 14:22:33 2005 +0200
files:       src/Pure/envir.ML
description:
Fixed bug: lookup' must use = instead of eq_type to compare types of
variables, otherwise pattern matching algorithm may loop.


Since it contains the critical keywords "fixed bug", I was wondering if it 
could have introduced other surprises.


Anyway, after 2-3 more rounds of investigation, I've found more profound 
weaknesses of pattern.ML and unify.ML concerning unification of types. 
This could lead to situations as sketched above, where types of variables 
were not properly instantiated.  E.g. here:

ML {*
   val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context};

   val a = Syntax.read_term ctxt "?n :: nat ⇒ bool";
   val b = Syntax.read_term ctxt "?n :: ?'b10";

   val res1 = Seq.list_of (Unify.hounifiers (@{theory}, Envir.empty 15, [(a, b)]));
   val res2 = Seq.list_of (Unify.unifiers (@{theory}, Envir.empty 15, [(a, b)]));
   val res3 = Pattern.unify @{theory} (a, b) (Envir.empty 15);
*}


The following change addresses that, although I do not claim to "fix" 
anything -- it is even more critical as usual, since it affects operations 
of the inference kernel.

changeset:   52173:3b9c31867707
user:        wenzelm
date:        Mon May 27 16:52:39 2013 +0200
files:       src/Pure/pattern.ML src/Pure/unify.ML
description:
more thorough type unification: treat equal Vars like other atoms, 
otherwise unify type of term pair (not just accidental body_type of its 
head Vars);


Interestingly, the earlier example now becomes ill-behaved by producing 
lots of unify trace messages:

consts P :: "'a set => bool"
lemma P_Int [intro]:  "P A ==> P B ==> P (A Int B)" sorry
lemma P_UNIV [intro]: "P UNIV" sorry
lemma P_INT [intro]: "ALL x : A. P (B x) ==> P (INT x : A. B x)" sorry
lemma P_UNION [intro]: "ALL x : A. P (B x) ==> P (UN x : A. B x)" sorry

lemma
   fixes x :: "'a" and Q :: "'b => bool" and f :: "'a => 'b"
   shows "EX S. P S & x : S & (ALL xa : S. Q (f xa))"
   apply (auto simp only: )

I can't say if it is to be expected that ho-unification runs into a dead 
alley here.


Before "landing" the above change, I figured out some lack of type 
instantiation in a quite different spot:

changeset:   52172:6228806b2605
user:        wenzelm
date:        Mon May 27 15:57:38 2013 +0200
files:       src/HOL/Tools/Metis/metis_reconstruct.ML
description:
instantiate types as well (see also Thm.first_order_match);


Without it, the change 3b9c31867707 would crash metis proof reconstruction 
in two isolated cases of Isabelle + AFP.


Hopefully it is all a bit more precise now.  Maybe someone wants to 
formalize pattern.ML + unify.ML after > 20 years, to pin down the 
remaining uncertaincies about type instantiation within these non-trivial 
algorithms.


 	Makarius