Re: [isabelle] Failing simproc



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!

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)

Stepping through this proof with "show_sorts" enabled reveals the
problem: The inserted "x" has type "?'b3" instead of "?'b1", because
rule_tac automatically renames schematics in the rule to avoid clashes
with schematics in the proof goal.

> So you decided against the generic approach of importing the schematic
> variables? Was it because of efficiency?

I haven't looked at efficiency yet. The more serious problem is that
simprocs that use this approach now are broken! The simprocs in
Provers/Arith/cancel_numerals.ML already try to use
Variable.import_terms and Variable.export to temporarily fix
schematics. But on Dmitriy's original example, natless_cancel_numerals
returns an equation that cannot be used by the simplifier because its
schematic type variables are instantiated.

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.

- Brian





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