[isabelle-dev] Bug in linordered_ring_less_cancel_factor simproc

[Brian Huffman]

Hello,

With tracing turned on, one can see that the following lemma is solved
with the help of the linordered_ring_less_cancel_factor simproc (which
is defined in HOL/Tools/numeral_simprocs.ML):

lemma RR: "(0::'a::linordered_idom) < z ==> (x*z < y*z) = (x < y)"
by simp

Similarly, the following lemmas are solved by the same simproc:

lemma RL: "(0::'a::linordered_idom) < z ==> (x*z < z*y) = (x < y)"
by simp

lemma LR: "(0::'a::linordered_idom) < z ==> (z*x < y*z) = (x < y)"
by simp

But this last combination doesn't work:

lemma LL: "(0::'a::linordered_idom) < z ==> (z*x < z*y) = (x < y)"
by simp (* empty result sequence *)

The situation with linordered_ring_le_cancel_factor is similar (just
replace "<" with "<=" in the conclusion of each lemma). The same
problem probably occurs with other cancellation simprocs as well, but
I haven't tried them all.

After some investigation, I have concluded that the problem has to do
with Arith_Data.prove_conv. Here is the relevant code from
HOL/Tools/arith_data.ML:

fun prove_conv_nohyps tacs ctxt (t, u) =
  if t aconv u then NONE
  else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
  in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;

fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;

I believe the "t aconv u" test is to blame. Arith_Data.prove_conv is
called to move the common term to the left, so it matches the rules
mult_less_cancel_left_pos or mult_less_cancel_left_neg. But if the
common term is already on the left (as is the case with lemma LL) the
"aconv" test ensures that the simproc will fail.

Here is the changeset that introduced the "aconv" test:
http://isabelle.in.tum.de/repos/isabelle/rev/7cdcc9dd95cb

I'm not sure why the "aconv" test is there, so I don't want to remove
it myself. Could someone else please look into this?

- Brian

P.S.

I have a couple of other complaints about the situation with simprocs.
Testing simprocs is much more difficult than it should be.

First of all, the ML antiquotation @{simproc
linordered_ring_less_cancel_factor simproc} doesn't work. Why? The
simproc is listed by name when I ask ProofGeneral to print out the
simpset. With no way to refer to the existing simproc from ML, I had
to cut-and-paste a copy of all the simproc ML code in order to test it
individually.

Also, we really need to have some proper regression tests for
simprocs. Currently the only tests for these simprocs are in a
commented-out (!) section of Tools/numeral_simprocs.ML.