*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Cl-isabelle-users Digest, Vol 138, Issue 4*From*: "W. Douglas Maurer" <maurer at email.gwu.edu>*Date*: Fri, 2 Dec 2016 17:26:05 -0500*In-reply-to*: <mailman.71917.1480700746.20655.cl-isabelle-users@lists.cam.ac.uk>*References*: <mailman.71917.1480700746.20655.cl-isabelle-users@lists.cam.ac.uk>

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

**Follow-Ups**:**Re: [isabelle] Cl-isabelle-users Digest, Vol 138, Issue 4***From:*Eugene W. Stark

**Re: [isabelle] Cl-isabelle-users Digest, Vol 138, Issue 4***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Infinity - infinity = infinity
- Next by Date: Re: [isabelle] Cl-isabelle-users Digest, Vol 138, Issue 4
- Previous by Thread: Re: [isabelle] Infinity - infinity = infinity
- Next by Thread: Re: [isabelle] Cl-isabelle-users Digest, Vol 138, Issue 4
- Cl-isabelle-users December 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list