Re: [isabelle] Infinity - infinity = infinity



Just to add another remark on this thread:

AFAIU, Ââ - â is similar to Â1 / 0Â: there is no definition for it that
satisfied fundamental desired algebraic properties.

	Florian

Am 02.12.2016 um 16:57 schrieb Tobias Nipkow:
> Jasmin, there is a reason why I would not do this:
> 
> Aless Lasaruk and Thomas Sturm.
> Effective Quantifier Elimination for Presburger Arithmetic with Infinity
> 
> This paper shows that our current enat has quantifier elimination
> (although we have not inplemented it, and it would be some work, but not
> infeasible). In their system, "â - â = â". Unless we know that your
> proposed modification still has quantifier elimination, I would be
> reluctant to give up that strong property.
> 
> Tobias
> 
> On 02/12/2016 16:01, Jasmin Blanchette wrote:
>> Dear all,
>>
>> As noted before on this mailing list, automation for "enat"
>> ("Library/Extended_Nat.thy") is quite poor. Often, the only way to
>> proceed is to perform case distinctions on all "enat" and use auto on
>> the emerging subgoals.
>>
>> My impression is that many type classes are not available because of
>> the definition of subtraction. Because "â - â = â" (where "â" is the
>> infinity symbol), we lack one of the two properties required by
>> "cancel_comm_monoid_add":
>>
>>  1. âa b. a + b - a = b
>>  2. âa b c. a - b - c = a - (b + c)
>>
>> and we lack the third property required by "comm_semiring_1_cancel":
>>
>>  3. âa b c. a * (b - c) = a * b - a * c
>>
>> Counterexample for 1: a = â, b = 0.
>> Counterexample for 3: a = â, b = c = 1.
>>
>> These omissions affect further layers in the type class hierarchy --
>> e.g. we cannot use "ordered_cancel_comm_monoid_diff", even though some
>> of its theorems (e.g. "add_diff_assoc2") turn out to hold.
>>
>> My proposal is to change the definition of subtraction so that "â - â
>> = 0" and to instantiate the missing type classes. I believe this would
>> make "enat" much less painful to use, and mathematically I'm not so
>> convinced that "â - â = â" is such a great idea anyway. Indeed, I have
>> recently implemented ordinals below Î_0 in Isabelle and was able to
>> have much better automation than with "enat", and there we have Ï - Ï
>> = 0.
>>
>> "enat" occurs in about 70 ".thy" files in Isabelle and the AFP, so
>> this change (including the type class instantiations) seems quite
>> manageable. We (= Mathias and I) would wait until after the 2016-1
>> release to avoid any interference.
>>
>> Any opinions for or against?
>>
>> Jasmin
>>
>>
> 

-- 

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.