Re: [isabelle] Cancellation simprocs



Hello Florian,

On 02/03/2017 10:47, Florian Haftmann wrote:
> Hi Mathias,
>
>> To solve the problem, I have locally activated GeMS where I have
>> hard-coded that the simproc does not apply on types where LPS applies.
>> It worked without problem. However, I am not sure that testing the AFP
>> and the Isabelle distribution is sufficient to declare that (3) does not
>> cause problems.
>> Does somebody have an opinion on the matter? Or should I just proceed
>> and activate my GeMS simproc on all cancel_comm_monoid_add types (except
>> those where LPS applies)?
> operationally this should be OK.  But the overall design seems not very
> convincing.
>
> I have no ready-to-proceed suggestion at hand, but a few thoughts:
>
> * LPS is the only one to operate on nat / int directly rather than an
> algebraic structure.  Can this be lifted, and how would the overall
> picture then look like?
For nat: it cannot be lifted. The replacement from Suc to +1 is done
while iterating over the term. So no simple way to do lifting.

For int: it already works on linordered_idom.


I have to think about the general picture if we really want to reduce
duplication (with the risk of breaking proofs).

> * Can there be *one* implementation of GeMS and LPS with a case
> distinction or something like that?  That would still be better two
> concurring implementations.
I tried that. It should work but getting full compatibility is very *hard*:
* the code is non-trivial (e.g., whether Suc is replaced by +1 is
handled internally).
* there is some normalisation done after cancellation (I don't really
know why).
* the simprocs on natural numbers are crucial for the linarith, meaning
that even small differences can have huge consequences.
* LPS does not always do what people would expect, e.g.
~~/HOL/ex/Simproc_Tests.thy:
       (* FIXME "Suc (i + 3) \<equiv> i + 4" *)
       assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
          by (tactic \<open>test @{context} [ at {simproc
nat_combine_numerals}]\<close>) fact

If we want to replace LPS, should we aim at full compatibility to avoid
breaking proofs or try to fix the FIXMEs from Simproc_Test?

> * Note that technically the cancellation simproc implementations are
> notoriously outdated;  the state of the are is to implement such a
> simproc in a locale and then interpret it onto the desired instances.
> Detail can be found in Amine Chaieb and Makarius Wenzel: Context aware
> Calculation and Deduction --- Ring Equalities via GrÃbner Bases in
> Isabelle.  And in src/HOL/Semiring_Normalization.thy
That should make the implementation a bit cleaner. I'll look into that.


Best,
Mathias
> Best,
> 	Florian
>





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