Re: [isabelle] Failing simproc



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.

The simproc under consideration stems from 1997, when I was supervising Stefan Berghofer in a very small student project. According to the Mercurial history, it has not really been improved since then. I first thought that it was covered by Brian's general simproc renovation project for Isabelle2012, but it does not seem the case.

IIRC, the system was more aggressive back then to reject goals with schematic types outright.


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?


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'm not sure, but there might be a bug in Variable.export and related
functions. For example:

ML_val {*
let
 val ctxt = @{context}
 val ts1 = [Thm.term_of @{cpat "size (x::?'a::size)"}]
 val (ts2, ctxt') = Variable.import_terms true ts1 ctxt
 val ts3 = Variable.export_terms ctxt' ctxt ts2
in
 (ts1, ts2, ts3)
end
*}

val it =
  ([Const ("Nat.size_class.size", "?'a \<Rightarrow> nat") $ Free
("x", "?'a")],
   [Const ("Nat.size_class.size", "'a \<Rightarrow> nat") $ Free ("x", "'a")],
   [Const ("Nat.size_class.size", "'a \<Rightarrow> nat") $ Free ("x", "'a")]):
  term list * term list * term list

The export_terms step does nothing at all! (This example actually
works correctly if we replace "x" with "?x" in the input term.)

I'm afraid we can't recommend simproc writers to use the Variable.import/export technique, at least not until we figure this out.

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.

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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.