Re: [isabelle] Cancellation simprocs



Hi Matthias,

> * 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?

linarith is indeed a world on its own and IMHO it would be OK if
linarith would retain its current simproc, even if that is not used any
where else.

For a generalized simproc it would be fine if some proofs have to be
amended, if the number of breaking proofs does not rise to high; this
happens routinely when maintaining proof automation.  The usual approach
to figure out is:

* Make the intended change.
* See whether HOL can get run with reasonable effort.
* Build as much as possible from distro and AFP.  Iterate over breaking
proofs.
* Over time you get an idea what the impact of the change is:
  * How many breaking proofs?
  * How big is the amount of Âawkward breaking proofs compared to
Âstreamlined breaking proofs?
  * Is there are recurring pattern how proofs can be repaired?
  * Is there yet another thing to change e.g. concerning the simplifier
setup to get to a cleaner situation again?
  * â

>> * 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.

I'll appreciate that.

Cheers,
	Florian

> 
> 
> Best,
> Mathias
>> Best,
>> 	Florian
>>
> 
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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