Re: [isabelle] Infinity - infinity = infinity



Dear Jasmin,

Are you sure your definition works?

I don't think cancel_comm_monoid_add will ever hold for enat or ennreal
for a reasonable definition of minus. "a + b - a = b" is independent of
 the definition of minus: if a is â then we always get "â - a = b"

I would love to have better support for minus on enat and ennreal.
Andreas added a couple of years ago support for cancellation of
additive and multiplicative terms. Maybe we can also add something like
 this for minus?

When I added ennreal I also thought about adding additional type
classes for enat and ennreal with a better support for non-cancellable
monoids. I think we can factor out some theorems from existing type
classes, like add_diff_assoc2. Or the second rule of
cancel_comm_monoid_add.

 - Johannes


Am Freitag, den 02.12.2016, 16:01 +0100 schrieb Jasmin Blanchette:
> 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
> 
> 




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