Re: [isabelle] Infinity - infinity = infinity



Another idea from Tobias (and I think also Andreas) is to add a special
simpproc which does case-distinction on enat/ereal/ennreal and calls
linarith. I would assume the simpproc is quite slow but can be disable
by default and just be activated by the user.

 - Johannes

Am Freitag, den 02.12.2016, 16:57 +0100 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
> > 
> > 
> 
> 




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