Re: [isabelle] Failing simproc



On Wed, Jul 18, 2012 at 11:32 AM, Lars Noschinski <noschinl at in.tum.de> wrote:
> On 18.07.2012 10:55, Dmitriy Traytel wrote:
>>
>> Hi *,
>>
>> I stumbled upon some funny behaviour which prevents the simplifier in
>> proving "True" in Isabelle2012 (also in 8a1ef12f7e6d). The reduced
>> example is attached.
>
>
> This exception is thrown by the simproc natless_cancel_sums (in
> Nat_Arith.nat_cancel_sums), as the following succeeds:
>
> notepad
> begin
>   ML_prf {* Delsimprocs [nth Nat_Arith.nat_cancel_sums 1] *}
>   have "(\<And>ys zs. length ys < Suc (length zs + length ys))" by simp
>   hence True
>     by simp
>
> The other simprocs in Nat_Arith also seem to be affected.

For the record: This problem was caused by an interaction between
simprocs and schematic type variables. More specifically, some
internal proofs done by Nat_Arith simprocs would fail on terms that
contain schematics. The problem is now fixed in revision 868dc809c8a2.

Authors of simprocs should take note: The simplifier may run simprocs
on terms containing schematics (type and/or term variables) and it is
the responsibility of the simproc to handle this situation properly.

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.)

- Brian





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