Email Gateway (Aug 22 2022 at 14:40): Email Gateway (Aug 22 2022 at 14:40):From: Johannes Hölzl <hoelzl@in.tum.de>
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"
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.
Email Gateway (Aug 22 2022 at 14:41):From: Johannes Hölzl <hoelzl@in.tum.de>
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 :-)
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
Email Gateway (Aug 22 2022 at 14:42):From: Lawrence Paulson <lp15@cam.ac.uk>
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.
--lcp
Email Gateway (Aug 22 2022 at 14:43):From: Johannes Hölzl <hoelzl@in.tum.de>
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.
Email Gateway (Aug 22 2022 at 14:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
This really depends on what you want to use the extended numbers for. If you just want to
compute the length of a coinductive list, then enat is better than the hypernats. For
example, the equation
llength (lappend xs ys) = llength xs + llength ys
holds for enat, but not for hypernats, because lappend xs ys = xs if xs is infinite. Also,
I am pretty sure that the Max-Flow-Min-Cut theorem for countable graphs (AFP entry
MFMC_Countable) holds only on extended reals, but not on hyperreals.
Andreas
Email Gateway (Aug 22 2022 at 14:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Another idea of mine was to embed the extended numbers into the non-standard numbers. The
idea was to do this embedding in a simproc and run linarith on the embedded terms. The
embedding only works if some case analyses are done (in particular for terms like \infty -
\infty), but I guess that one can save some case analyses this way. But the details have
not been worked out so far.
Andreas
Email Gateway (Aug 22 2022 at 14:44):From: Johannes Hölzl <hoelzl@in.tum.de>
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@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
InfinityThis 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":
- ⋀a b. a + b - a = b
- ⋀a b c. a - b - c = a - (b + c)
and we lack the third property required by
"comm_semiring_1_cancel":
- ⋀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
Email Gateway (Aug 22 2022 at 14:44):From: Tobias Nipkow <nipkow@in.tum.de>
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
InfinityThis 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":
- ⋀a b. a + b - a = b
- ⋀a b c. a - b - c = a - (b + c)
and we lack the third property required by
"comm_semiring_1_cancel":
- ⋀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
Email Gateway (Aug 22 2022 at 14:44):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 14:45):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 22 2022 at 14:45):From: Tobias Nipkow <nipkow@in.tum.de>
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
InfinityThis 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":
- ⋀a b. a + b - a = b
- ⋀a b c. a - b - c = a - (b + c)
and we lack the third property required by
"comm_semiring_1_cancel":
- ⋀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
Email Gateway (Aug 22 2022 at 14:45):From: Freek Wiedijk <freek@cs.ru.nl>
Hi Larry,
As a rule, people should use non-standard analysis rather
than the extended naturals or reals.
Even more so: Conway's surreal numbers!
(No, I'm not serious.)
Freek
Email Gateway (Aug 22 2022 at 14:48):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Johannes wrote:
Are you sure your definition works?
Not anymore. ;) Nitpick finds counterexamples for pretty much any property I hoped to have. Clearly, I could have spared myself some embarrassment by firing up this tool earlier.
What I'll take home from this is that subtraction on "enat" is necessarily a messy business.
Jasmin
Email Gateway (Aug 22 2022 at 14:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Just to add another remark on this thread:
AFAIU, »∞ - ∞« is similar to »1 / 0«: there is no definition for it that
satisfied fundamental desired algebraic properties.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 14:51):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
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":
and we lack the third property required by "comm_semiring_1_cancel":
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
Email Gateway (Aug 22 2022 at 14:53):From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s
Last updated: Apr 25 2024 at 08:20 UTC