Re: [isabelle] Infinity - infinity = infinity



Am Freitag, den 02.12.2016, 17:00 +0100 schrieb Johannes HÃlzl:
> 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"

With `independent` I mean that it does not work no matter how we define
"_ - _": if a = â then we always get "â - â = b". So we will always
find a "b" for which the equation fails.

The extended numbers are quite unintuitive. If I wouldn't have Isabelle
 I would have proved a lot of very nice but unfortunately wrong
theorems   :-)

 - Johannes


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