Re: [isabelle] Performance regression in 2016-1 with character strings.

> We've noticed a serious performance regression involving characters and
> strings in Isabelle-2016-1.
> This can be demonstrated as follows:
> lemma "''ab'' ~= ''ba''"
>    using [[simp_trace]]
>    by simp
> In earlier Isabelle versions, it takes a few dozen steps to prove this
> rule. In 2016-1, the characters
> are compared by expanding rule Char_eq_Char_iff which requires
> normalising "k mod 256" for
> various k, which takes many many steps.

In 96015aecfeba I have addressed this by a dedicated simproc for
equality on characters.  This should be possible to be ported into a
separate theory for Isabelle2016-1.

From the same changeset it can be seen that other tools reyling on
concrete string values like state spaces use to provide their own proof
devices for that.

The deeper reason behind this seems to be that simp rules tailored for
abstract symbolic reasoning are often not suitable for calculating with
concrete values and vice versa.

Unfortunately the most elegant solution, a simproc or simp rules for
congruences Ânum1 mod num3 = num1 mod num2Â did not work out since there
are two many other rules and simprocs interfering with mod.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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