Re: [isabelle] Cl-isabelle-users Digest, Vol 138, Issue 4



Some day I hope it will be possible to implement a system that does what real computers do in this case: infinity minus infinity gives NaN, which stands for Not a Number. Then any combination of NaN with anything else also gives NaN. (See any formal description of IEEE standard floating point arithmetic.) --WDMaurer

Sent from my iPhone

> On Dec 2, 2016, at 12:45 PM, cl-isabelle-users-request at lists.cam.ac.uk wrote:
> 
> Send Cl-isabelle-users mailing list submissions to
>    cl-isabelle-users at lists.cam.ac.uk
> 
> To subscribe or unsubscribe via the World Wide Web, visit
>    https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
> or, via email, send a message with subject or body 'help' to
>    cl-isabelle-users-request at lists.cam.ac.uk
> 
> You can reach the person managing the list at
>    cl-isabelle-users-owner at lists.cam.ac.uk
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Cl-isabelle-users digest..."
> 
> 
> Today's Topics:
> 
>   1. Re:  Infinity - infinity = infinity (Johannes H?lzl)
>   2. Re:  Infinity - infinity = infinity (Tobias Nipkow)
>   3. Re:  Infinity - infinity = infinity (Manuel Eberl)
>   4. Re:  Infinity - infinity = infinity (Lawrence Paulson)
>   5. Re:  Infinity - infinity = infinity (Tobias Nipkow)
> 
> 
> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Fri, 02 Dec 2016 17:33:39 +0100
> From: Johannes H?lzl <hoelzl at in.tum.de>
> Subject: Re: [isabelle] Infinity - infinity = infinity
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <1480696419.29055.13.camel at in.tum.de>
> Content-Type: text/plain; charset="UTF-8"
> 
> 
> Am Freitag, den 02.12.2016, 16:09 +0000 schrieb Lawrence Paulson:
>> As a rule, people should use non-standard analysis rather than the
>> extended naturals or reals. Although the former are more complicated,
>> they preserve all the first order properties of their standard
>> counterparts. In particular, the non-standard naturals are still a
>> semiring.?
> 
> Hm, enat also forms a semiring:
> 
> ? instantiation enat :: "{comm_semiring_1, semiring_no_zero_divisors}"
> 
> 
>> --lcp
> 
>>> On 2 Dec 2016, at 15:57, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>> 
>>> 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
>>>> 
>>>> 
>> 
>> 
> 
> 
> 
> ------------------------------
> 
> Message: 2
> Date: Fri, 2 Dec 2016 17:39:59 +0100
> From: Tobias Nipkow <nipkow at in.tum.de>
> Subject: Re: [isabelle] Infinity - infinity = infinity
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <36b8ca52-c7d9-e330-ad5e-b68b384425b6 at in.tum.de>
> Content-Type: text/plain; charset="utf-8"
> 
> 
>> 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
>>>> 
>>>> 
>>> 
>>> 
>> 
> 
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: smime.p7s
> Type: application/pkcs7-signature
> Size: 5135 bytes
> Desc: S/MIME Cryptographic Signature
> Url : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20161202/65f788ed/attachment.p7s 
> 
> ------------------------------
> 
> Message: 3
> Date: Fri, 2 Dec 2016 18:09:59 +0100
> From: Manuel Eberl <eberlm at in.tum.de>
> Subject: Re: [isabelle] Infinity - infinity = infinity
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <45b1de25-cef0-bf73-faee-6918320f3e8f at in.tum.de>
> Content-Type: text/plain; charset=utf-8
> 
> 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
>>>>> 
>>>>> 
>>>> 
>>>> 
>>> 
>> 
> 
> 
> 
> ------------------------------
> 
> Message: 4
> Date: Fri, 2 Dec 2016 17:39:10 +0000
> From: Lawrence Paulson <lp15 at cam.ac.uk>
> Subject: Re: [isabelle] Infinity - infinity = infinity
> To: Johannes H?lzl <hoelzl at in.tum.de>
> Cc: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <40E6720C-DBE5-4322-BFA7-B297C0008721 at cam.ac.uk>
> Content-Type: text/plain;    charset=utf-8
> 
> But this property is still too weak for your purposes. The properties you state in your original message (as necessary for the decision procedure) are first-order and will hold for the non-standard naturals.
> 
> Of course I understand that they don't suit all purposes, because they don't give a unique "infinity".
> 
> --lcp
> 
>> On 2 Dec 2016, at 16:33, Johannes H?lzl <hoelzl at in.tum.de> wrote:
>> 
>> 
>> Am Freitag, den 02.12.2016, 16:09 +0000 schrieb Lawrence Paulson:
>>> As a rule, people should use non-standard analysis rather than the
>>> extended naturals or reals. Although the former are more complicated,
>>> they preserve all the first order properties of their standard
>>> counterparts. In particular, the non-standard naturals are still a
>>> semiring. 
>> 
>> Hm, enat also forms a semiring:
>> 
>>  instantiation enat :: "{comm_semiring_1, semiring_no_zero_divisors}"
>> 
>> 
>>> --lcp
>> 
> 
> 
> 
> 
> ------------------------------
> 
> Message: 5
> Date: Fri, 2 Dec 2016 18:45:44 +0100
> From: Tobias Nipkow <nipkow at in.tum.de>
> Subject: Re: [isabelle] Infinity - infinity = infinity
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <f60fee3e-6113-a7e4-e0e4-4c53f7554bbb at in.tum.de>
> Content-Type: text/plain; charset="utf-8"
> 
> 
> 
>> On 02/12/2016 18:09, Manuel Eberl wrote:
>> 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 = ?".
> 
> I am not quite sure what you mean by the extra case, but it does not matter 
> because, yes, as I wrote, it is independent of "? - ?".
> 
> Tobias
> 
>> 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
>>>>>> 
>>>>>> 
>>>>> 
>>>>> 
>>>> 
>>> 
>> 
> 
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: smime.p7s
> Type: application/pkcs7-signature
> Size: 5135 bytes
> Desc: S/MIME Cryptographic Signature
> Url : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20161202/29ed5124/attachment.p7s 
> 
> End of Cl-isabelle-users Digest, Vol 138, Issue 4
> *************************************************




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