*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Cancellation simprocs*From*: Mathias Fleury <mathias.fleury12 at gmail.com>*Date*: Fri, 3 Mar 2017 09:30:35 +0100*Cc*: Isabelle User <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <dd136cf4-2337-890f-5074-3808c059d652@informatik.tu-muenchen.de>*References*: <cc5b9e49-8068-d9fc-ee11-b63deaeda102@gmail.com> <dd136cf4-2337-890f-5074-3808c059d652@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0) Gecko/20100101 Thunderbird/45.7.1

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 >

**Follow-Ups**:**Re: [isabelle] Cancellation simprocs***From:*Lawrence Paulson

**Re: [isabelle] Cancellation simprocs***From:*Florian Haftmann

**References**:**Re: [isabelle] Cancellation simprocs***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] isar in PIDE : strange behavior
- Next by Date: Re: [isabelle] isar in PIDE : strange behavior
- Previous by Thread: Re: [isabelle] Cancellation simprocs
- Next by Thread: Re: [isabelle] Cancellation simprocs
- Cl-isabelle-users March 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list