[isabelle-dev] simproc divide_cancel_factor produces error

[Brian Huffman]

On Thu, Sep 15, 2011 at 7:34 AM, Lars Noschinski <noschinl at in.tum.de> wrote:
> Hi everyone,
>
> in the following snippet, applying the simplifier causes an error:
>
> ------------------------------------------
> theory Scratch
>  imports Complex_Main
> begin
>
> lemma
>  shows "(3 / 2) * ln n = ((6 * k * ln n) / n) * ((1 / 2 * n / k) / 2)"
> apply simp
> ------------------------------------------

I managed to reduce this to a smaller example:

lemma "(x::real) = (if P then y else 2 * x) * 2 / 4"
apply simp

*** Proof failed.
*** (if P then y else 2 * x) * 2 / 4 =
*** 2 * (Numeral1 * (if P then y else 2 * x)) / (2 * (2 * 1))
***  1. \<not> P \<longrightarrow> x * (2 * 2) / 4 = x * 4 / 4
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** (if P then y else 2 * x) * 2 / 4 =
*** 2 * (Numeral1 * (if P then y else 2 * x)) / (2 * (2 * 1))
***  (line 6 of "/home/brianh/Documents/Isabelle/Scratch.thy")
*** At command "apply" (line 6 of "/home/brianh/Documents/Isabelle/Scratch.thy")

I can tell that this particular error arises from the
"divide_cancel_numeral_factor" simproc, because I get the same error
message if I run it with only this simproc enabled:

lemma "(x::real) = (if P then y else 2 * x) * 2 / 4"
apply (tactic {* simp_tac (Simplifier.addsimprocs
  (global_simpset_of @{theory Int},
  [nth Numeral_Simprocs.cancel_numeral_factors 4])) 1 *} )

Apparently the simproc's internal normalization tactic is getting
confused by the presence of the if-then-else term. Looking at the
shape of the unsolved subgoal in the error message, you can see that
the simplifier has performed a split on the if-then-else, which it
probably doesn't need to do.

Right now, I am testing a potential solution: For the norm_tac used in
the cancel-factor simprocs, I am replacing the uses of HOL_ss (which
includes a split rule for if-then-else) with HOL_basic_ss (which
doesn't). Even if the fix works, though, I'm not sure if I want to
commit a patch this close to a release, because we don't have any good
testing infrastructure for these simprocs, and I wouldn't want to
introduce any new bugs.

After the release, I'll have to think about doing a complete overhaul
of all of the cancellation simprocs.

- Brian