[isabelle-dev] Bug in linordered_ring_less_cancel_factor simproc

[Lawrence Paulson]

I have looked at this ancient code again, and think I understand the problem. 

prove_conv is mostly used to prove the conclusion of the simproc. If the two terms are equal, then it is unwanted, so the correct response is to fail. That is why the "aconv" test is there.

But occasionally, prove_conv is used to prove an auxiliary equality; in those cases, it is not clear that proving a trivial equality (t=t) should fail. So a quick fix would be to introduce a boolean argument, indicating whether a trivial result is acceptable or not. The attached code is an example of the situation.

fun proc ss t =
  let
    ...
    val reshape =  (*Move i*u to the front and put j*u into standard form
                       i + #m + j + k == #m + i + (j + k) *)
        if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
          raise TERM("cancel_numerals", [])
        else Data.prove_conv [Data.norm_tac ss] ctxt prems
          (t', Data.mk_bal (newshape(n1,terms1'), newshape(n2,terms2')))
  in
    Option.map (export o Data.simplify_meta_eq ss)
      (if n2 <= n1 then
         Data.prove_conv
           [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
            Data.numeral_simp_tac ss] ctxt prems
           (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
       else
         Data.prove_conv
           [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
            Data.numeral_simp_tac ss] ctxt prems
           (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
  end

Larry

On 10 May 2010, at 12:14, Makarius wrote:

> On Mon, 10 May 2010, Florian Haftmann wrote:
> 
>>> 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?
>> 
>> The aconv has already been present previously:
>> http://isabelle.in.tum.de/repos/isabelle/rev/7cdcc9dd95cb#l8.15
> 
> I think it all goes back to this version:
> http://isabelle.in.tum.de/repos/isabelle/rev/22d4c641ebff#l1.154
> or maybe even earlier.
> 
> IIRC the numeral simprocs belong to the second wave of, after I've introduced the mechanism and produced the more basic ones around functor CancelFactorFun.  Looking there, e.g. http://isabelle.in.tum.de/repos/isabelle/annotate/92cc2f4c7335/src/Provers/Arith/cancel_factor.ML#l71 you see that the internal "conversion" prover does not have this optional result, although at the outermost level simprocs usually try to fail quickly on problems that are out of their scope, e.g. being too trivial or too hard.
> 
> This might be the source of the reflexivity test by Larry, although it might have moved in further than expected.  Maybe Larry recalls what he did 10 years ago in 22d4c641ebff.
> 
> 
>> The numeral simprocs (like more arithemtic matter) are, more or less, a mess.  We don't even know how relevant they are nowadays.  So, if no complaint arises to remove the aconv test and no problems occur, it could be the best option to drop it.
> 
>> Doing it right would mean to investigate d) first, understanding a), implementing the necessary simporcs using a), thus solving c), and perhaps pave the way for tackling b) in the end.  So far no body was adventurous enough to start this ;-)
> 
> Yes, this has been the situation for many years already.  Such ancient things will cause many surprises when changed too quickly, i.e. it is something to do after the release.
> 
> 
> 	Makarius
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev