Re: [isabelle] Failing simproc
On Sat, Jul 21, 2012 at 8:19 PM, Makarius <makarius at sketis.net> wrote:
> On Sat, 21 Jul 2012, Brian Huffman wrote:
>> On Fri, Jul 20, 2012 at 5:36 PM, Lars Noschinski <noschinl at in.tum.de>
>>> On 20.07.2012 15:06, Brian Huffman wrote:
>>>> A simproc must never instantiate any schematic variable. Some
>>>> guidelines for simproc writers: Internal proofs should use the
>>>> simplifier only in "safe" mode, i.e. only using the "safe" solvers,
>>>> which avoid instantiating schematics. Also, avoid instantiating rules
>>>> with terms from the input and then using those rules with rtac,
>>>> because schematic variables in a rule are not preserved when the rule
>>>> is applied. (The Nat_Arith simprocs failed to follow either of these
>> Perhaps I can explain this better. Here's how the Nat_Arith
>> cancellation simprocs worked before yesterday's rev. 868dc809c8a2 --
>> note that this technique is *wrong* and simproc writers must avoid it!
> What is wrong, fixed, broken now? I am confused.
What's wrong: The implementation of the simprocs in
HOL/Tools/nat_arith.ML of Isabelle2012. (In particular, the function
gen_uncancel_tac is not robust in the presence of schematics.) Writers
of new simprocs should not emulate this code.
What's fixed: Since rev. 868dc809c8a2, the simprocs in
HOL/Tools/nat_arith.ML work correctly on goals with schematics.
>> The idea is to prove e.g. "(a + x + b < c + x + d) = (a + b < c + d)"
>> by inserting "x" on the right, and then doing ac rewriting. The
>> simproc does the same steps as this proof script:
>> "(a + size (x::?'b1::size) + b < c + size (x::?'b1::size) + d) = (a
>> + b < c + d)"
>> apply (rule_tac ?k.1 = "size x" in nat_add_left_cancel_less [THEN
>> apply (simp only: add_ac)
> Goals with schematic type variables routinely lead to undefined behaviour.
> Schematic types for fixed term variables are especially pathologic. Does
> this example have any practical relevance?
Yes, it does.
Sometimes users have proof goals containing schematics. Sometimes they
run the simplifier on such goals. This can result in simprocs being
asked to rewrite terms containing schematics. For example, a simproc
may need to internally prove the equality "(a + size (x::?'b1::size) +
b < c + size (x::?'b1::size) + d) = (a + b < c + d)".
Keep in mind that the proof script above is not a *user* proof; it
represents the internal proof done by a simproc.
> Anyway, a more profound deficiency of this modest simproc is this: It is
> supposed to normalize certain outer algebraic structure, but it retains the
> concrete subterms. Thus the normalization might do non-sense with the
> accidental substructure, not just with its hidden polymorphism as above.
> This was already known in 1997, but we did not have the technology so do
> better on the spot. Today in 2012, it should be trivial to use the local
> context of the simproc (from the "ss") to introduce fresh fixes for the
> terms (ts, us, vs), then prove the result in its generalized form with fully
> opaque subterms, finally export the resulting equation to hand it back to
> the simplifier. Thus the local goal is fully fixed with fixed types, and
> the result as schematic and poylmorphic as required. The simplifier will
> apply higher-order matching to recover the concrete instance.
I think your idea would work. However it seems like it would be
non-trivial to implement: You would have to determine the high-level
structure of the original term, identify which of the complex subterms
are equal, and then build new, abstract terms with fresh variables in
the right places. Do you think we should recommend this technique as a
standard best-practice for simproc writers?
The technique used by the simprocs in
HOL/Tools/nat_numeral_simprocs.ML (based on an ML functor from
Provers/Arith/cancel_numerals.ML) is much easier to use: Just do a
Variable.import_terms at the beginning to locally fix the schematics,
and then run Variable.export on the resulting equation.
I think the Variable.import/export technique would make a good
official recommendation for simproc writers (something for the
Cookbook, maybe) if it only worked right! This is why I complained of
a possible bug in Variable.export.
In Dmitriy's original example, the simp trace reveals that the
natless_cancel_numerals simproc (which uses the import/export
technique) returns an unusable rule where some of the locally-fixed
type variables have not been properly generalized again.
have "(\<And>ys zs. length ys < Suc (length zs + length ys))" by simp
hence True apply simp sorry
Trying procedure "Numeral_Simprocs.natless_cancel_numerals" on:
length (:000\<Colon>?'a1 list) < Suc (length (:001\<Colon>?'b1 list) +
Procedure "Numeral_Simprocs.natless_cancel_numerals" produced rewrite rule:
length (:000\<Colon>'a list) < Suc (length (:001\<Colon>'b list) +
length :000) \<equiv>
(0\<Colon>nat) < Suc (length :001)
> A fixed term variable x::?'a with schematic type should normally not occur
> during logical inference. It conceptually means that the type-inference
> phase did not finish its job before entering the logic. It might also mean
> that old and new tools were combined in a odd way, without the "proper
> context" or things not declared properly in the context.
Oh, but it can, and it does! This situation is clearly shown in the
simp trace above, which was produced by Dmitriy's completely
reasonable proof script.
> Fixed type variables within fixed term variables are still fixed, according
> to Hindley-Milner polymorphism. So the above export looks right. If
> subterms with their potential hidden polymorphism are made abstract as
> sketched above, such problems will not occur.
Of course, if we completely redesigned all of our simprocs, we could
avoid all these problems.
What we need, though, is a simple, practical technique that any
simproc writer can use. The Variable.import/export technique would be
just the thing, but we need to address the bugs in Variable.export
This archive was generated by a fusion of
Pipermail (Mailman edition) and