[isabelle-dev] HOL-IMP very slow

[Lawrence Paulson]

Okay, I see that this works the same as before.

Such brittleness is quite believable, but is a sign that the particular proof was fragile anyway (having a large search space and requiring luck to get a solution quickly).

Larry

On 13 Feb 2014, at 12:41, Jasmin Blanchette <jasmin.blanchette at gmail.com> wrote:

> Am 13.02.2014 um 13:35 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:
> 
>> I know it was a problem for machine learning that a free variable in a goal (x say) might appear with multiple types in a problem set. This is connected with the issue you’re describing now. I assume that that was solved somehow.
> 
> All I'm trying to say is that
> 
>    lemma "n ~= Suc n"
>    using [[metis_trace]] by (metis Suc_n_not_n)
> 
> and
> 
>    lemma "x ~= Suc x"
>    using [[metis_trace]] by (metis Suc_n_not_n)
> 
> generate slightly different clauses at the Metis level, as can be seen in the trace. One gets
> 
>    |- v_n = c_Nat_OSuc v_n
> 
> vs.
> 
>    |- v_x = c_Nat_OSuc v_x
> 
> To Metis, "v_n" and "v_x" are nullary function symbols (constants). Some of its heuristics are influenced by the concrete names, or at least their relative ordering. So it mgiht be very fast on the first one and very slow on the second one.
> 
> Jasmin
>