*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Failing simproc*From*: Brian Huffman <huffman at in.tum.de>*Date*: Sun, 22 Jul 2012 11:17:30 +0200*Cc*: Lars Noschinski <noschinl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1207211956110.15809@macbroy21.informatik.tu-muenchen.de>*References*: <50067A05.1040609@in.tum.de> <500682C0.2000407@in.tum.de> <CAAMXsiamg8P0NdVv16efsWYTKHnmSjuG7_rrDra8L2ZKN8g-Og@mail.gmail.com> <50097B0D.7060904@in.tum.de> <CAAMXsiZKw=w73Dkik_yTsjHF0qtO9++Sqgmd6fwzQAUYJ02mMg@mail.gmail.com> <alpine.LNX.2.00.1207211956110.15809@macbroy21.informatik.tu-muenchen.de>

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> >> wrote: >>> >>> 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 >>>> guidelines.) >> >> >> 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: >> >> schematic_lemma >> "(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 >> subst_equals]) >> 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. declare [[show_types]] declare [[simp_trace]] declare [[simp_debug]] notepad begin have "(\<And>ys zs. length ys < Suc (length zs + length ys))" by simp hence True apply simp sorry end [1]Trying procedure "Numeral_Simprocs.natless_cancel_numerals" on: length (:000\<Colon>?'a1 list) < Suc (length (:001\<Colon>?'b1 list) + length :000) ... [1]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 first. - Brian

**References**:**[isabelle] Failing simproc***From:*Dmitriy Traytel

**Re: [isabelle] Failing simproc***From:*Lars Noschinski

**Re: [isabelle] Failing simproc***From:*Brian Huffman

**Re: [isabelle] Failing simproc***From:*Lars Noschinski

**Re: [isabelle] Failing simproc***From:*Brian Huffman

**Re: [isabelle] Failing simproc***From:*Makarius

- Previous by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Date: [isabelle] Isabelle/jedit
- Previous by Thread: Re: [isabelle] Failing simproc
- Next by Thread: Re: [isabelle] Failing simproc
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list