Re: [isabelle] Infinity - infinity = infinity



Do correct me if I am wrong, but in my naÃvetÃ, I would have thought
that one should always be able to accommodate a different definition of
"â - â" in quantifier elimination, at worst by adding an extra case for
"a = â â b = â".

Is that not the case?

Manuel


On 02/12/16 17:39, Tobias Nipkow wrote:
> 
> On 02/12/2016 17:14, Johannes HÃlzl wrote:
>> 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.
> 
> Something like this was actually implemented in Coq
> 
> Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor, and
> Wei-Ngan Chin: Certified Reasoning with Infinity. FM 2015.
> 
> and shows that it can be made independent of the particular choice of
> what "â - â" is. Hence we should not lose quantifier elimination with a
> different choice.
> 
> Tobias
> 
>> 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.