On Wed, 12 Feb 2014, Jasmin Christian Blanchette wrote:
Am 12.02.2014 um 16:40 schrieb Dmitriy Traytel <[email protected]>:
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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
