[isabelle-dev] HOL-IMP very slow

[Makarius]

On Wed, 12 Feb 2014, Jasmin Christian Blanchette wrote:

> Am 12.02.2014 um 16:40 schrieb Dmitriy Traytel <traytel at in.tum.de>:
>
>> Should be fine again (or at least better) with b445c39cc7e9. Thanks for 
>> the notification.

OK, everything back to normal.


> For the record: The goal state before and after had different variable 
> names in it. These become Skolem constants to Metis (in the FO logic 
> sense, not in the Isabelle sense). The Metis prover, like most if not 
> all ATPs, is sensitive to the (relative order of the) names of the 
> symbols -- e.g. it may apply different rules in a different order.
>
> It would be possible, and indeed a good idea, to insulate ourselves from 
> this by having the "metis" proof method name Skolems serially ("sk1", 
> "sk2", etc.) before invoking the Metis prover [*]. This would probably 
> trigger a couple of bad cases like we saw today, but as a result we 
> would be immune from the disease.

In principle the concept of "bound" variable in the context can do that, 
see also Variable.next_bound.  It enumerates local variables in a way such 
that the usual term order (the one of the Simplifier) coincides with the 
enumeration order.

The context also takes care to print these frees in green, as if they were 
actual bounds under a lambda.  (I have recently made this a general 
principle, not just some special hack of the Simplifier to print terms 
privately.)


Here is an example:

ML {*
   val ctxt = @{context};
   val xs =
     replicate 100 ()
     |> map (fn _ => ("x" ^ string_of_int (random_range 1 100), @{typ 'a}));

   val (xs', ctxt') = fold_map Variable.next_bound xs ctxt;

   val x = hd xs;
   val x' = hd xs';
   writeln (Syntax.string_of_term ctxt' (Free (x', snd x)))
*}

So for the user, the original names are mostly preserved (according to the 
insider joke "as they are printed"), while for the system the row of names 
is always in a standard form.


This mechanism was originally introduced for the Simplifier, to go under 
abstractions in a robust manner.  (When it was introduced it was actually 
not that robust, and broke down for > 255 names, as discovered by David 
von Oheimb when he did the first version of Bali.)

Name.is_bound is used to detect these funny pseudo-bounds -- excactly once 
in hypsubst.ML that is probably irrelevant here.  (Although hypsubst is 
also open to surprises as we now know.)


> Metis is a FO ATP developed by Hurd. "metis" is a higher-order proof 
> method (and tactic) that translates HOL to FOL (like Sledgehammer does), 
> developed by Paulson & Susanto.

Do you understand yourself how that works?


 	Makarius