Email Gateway (Aug 22 2022 at 19:02): Email Gateway (Aug 22 2022 at 19:02):From: Christian Sternagel <c.sternagel@gmail.com>
A short answer is: there is no "division by zero calculus".
In Isabelle/HOL a constant is whatever you define it to be. If you
define a constant, let's call it "division", like
division x y = (if y = 0 then 0 else Max {k::nat. k * y ≤ x})
then, of course, you can prove for this constant that it satisfies
division x 0 = 0
because that is just its definition.
Whether this has any connection to what mainstream math understands as
division is an entirely orthogonal issue.
cheers
chris
Email Gateway (Aug 22 2022 at 19:02):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Hi,
despite the non-politeness in the original question, you also didn't
answer it in a direct way.
Let's talk about the standard division constants defined for reals in
Isabelle/HOL, the type used by almost all mathematics formalization of
Analysis in Isabelle/HOL and AFP.
Is it true or false, that in Isabelle/HOL "x / 0 = 0" holds for whatever x?
P. S. weeks ago I was a little surprised that, in HOL4 (and also HOL
Light), one can prove 0 / 0 = 0, but x / 0 = 0 remains false
unless x = 0. Then I'm more surprised to know that Isabelle even
allows "x / 0 = 0" for all x, just to make sure automatic rewrites can
work. Yet Isabelle still has the largest portion of formal mathematics
library among all other theorem provers.
--Chun
Il 27/02/19 14:45, Christian Sternagel ha scritto:
signature.asc
Email Gateway (Aug 22 2022 at 19:03):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
That’s interesting for me to hear. Back in 2007 I attended a Mizar
tutorial as part of the TYPES Summer School. There Adam Naumowicz
presented the large body of mathematics formalized with Mizar as one of
Mizar’s biggest selling points. Well, that was 12 years ago; so I’d like
to hear how the current situation is.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:03):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
sorry, that "largest" part was just my guess.
--Chun
Il 27/02/19 17:27, Wolfgang Jeltsch ha scritto:
signature.asc
Email Gateway (Aug 22 2022 at 19:03):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Okay.
That said, there was some e-mail on this mailing list recently that
talked about some effort of porting Mizar proofs to Isar. Does anyone
know more details about this effort and its background?
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:03):From: Makarius <makarius@sketis.net>
On 27/02/2019 17:27, Wolfgang Jeltsch wrote:
Am Mittwoch, den 27.02.2019, 17:00 +0100 schrieb Chun Tian (binghe):
Yet Isabelle still has the largest portion of formal mathematics
library among all other theorem provers.That’s interesting for me to hear. Back in 2007 I attended a Mizar
tutorial as part of the TYPES Summer School. There Adam Naumowicz
presented the large body of mathematics formalized with Mizar as one of
Mizar’s biggest selling points. Well, that was 12 years ago; so I’d like
to hear how the current situation is.
Here is a rough overview what happened in Isabelle/AFP since 2004:
https://www.isa-afp.org/statistics.html
From that perspective, very little has happened before 2007. There are
also a few non-AFP projects like IsaFoR, IsaFoL, seL4.
Alltogether probably about the same order of magnitude than Mizar today,
but this is really just a crude guess based on discussions with the guys
behind Isabelle/Mizar, see also http://cl-informatik.uibk.ac.at/users/cek/
And size alone does not say much: the kind of material is probably quite
different in Isabelle/HOL vs. Mizar.
Makarius
Email Gateway (Aug 22 2022 at 19:03):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
For me, the level of automation is the most important feature in order to
choose a proof assistant. If I need a mathematical result, I can assume, in
a temporary way, that it was already proved, using the keyword "sorry".
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 19:04):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Chun,
sorry for being too indirect. Yes, "x / 0 = 0" is true in Isabelle/HOL.
But the important point about this is that the constant for division was
defined in this way. Which means that this (for some unintuitive)
property is "correct by construction".
The latter was my main point. For every formalization it is important to
study the formalized definitions and not just assume that they exactly
correspond to ones own expectations.
Email Gateway (Aug 22 2022 at 19:04):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Hi Christian,
thanks for the confirmation in a direct way. Let me share a small story
and have my point at last:
I was proving a small lemma in measure theory in HOL4, in which I met a
subgoal like
"0 / x = 0"
I could directly finish the goal, but in the pencil-and-paper proof it
needs to further prove that "x <> 0". But it turns out that
"x = measure m s",
and to prove it's not zero (actually > 0), I need to first prove that
"s" is measurable, then a lot of efforts were spent on this further
subgoal, because s is also a complicated term.
Similar situations also happened once I undefined "PosInf + NegInf",
"PosInf - PosInf" and "NegInf - NegInf" in HOL4's extrealTheory (they're
allowed in Isabelle/HOL), the proofs become longer but sometimes it's
just to prove something is not PosInf/NegInf but things much deeper.
If the aim of a formal system is to verify the correctness of some
mathematical theorems, but a piece (no matter big or small) in the
informal proof can be directly omitted because of some different
arithmetic definitions between the formal system and "real" math,
although the formal system is for sure consistent, but can you still
safely say that theorem is 100% correct/verified?
That's my point.
--Chun
Il 28/02/19 09:25, Christian Sternagel ha scritto:
signature.asc
Email Gateway (Aug 22 2022 at 19:04):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Chun wrote:
If the aim of a formal system is to verify the correctness of some
mathematical theorems, but a piece (no matter big or small) in the
informal proof can be directly omitted because of some different
arithmetic definitions between the formal system and "real" math,
although the formal system is for sure consistent, but can you still
safely say that theorem is 100% correct/verified?
If there is a difference in an arithmetic definition between the formal
system and real mathematics, the formal system is wrong. This is not the
case of x/0, because it is not defined in traditional mathematics. You just
need to define it as x/0 = 0 and the work is done. It is not the same to
change a definition and to define something that was undefined in the past.
In mathematics, you can always define something that was undefined in the
past, but you need to check the effect of this definition in the theorems.
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 19:04):From: Johannes Hölzl <johannes.hoelzl@gmx.de>
Am Mittwoch, den 27.02.2019, 17:00 +0100 schrieb Chun Tian (binghe):
Hi,
despite the non-politeness in the original question, you also didn't
answer it in a direct way.Let's talk about the standard division constants defined for reals in
Isabelle/HOL, the type used by almost all mathematics formalization of
Analysis in Isabelle/HOL and AFP.Is it true or false, that in Isabelle/HOL "x / 0 = 0" holds for whatever x?
Yes, "x / 0 = 0" for all "x : real".
P. S. weeks ago I was a little surprised that, in HOL4 (and also HOL
Light), one can prove0 / 0 = 0, butx / 0 = 0remains false
unlessx = 0. Then I'm more surprised to know that Isabelle even
allows "x / 0 = 0" for all x, just to make sure automatic rewrites can
work. Yet Isabelle still has the largest portion of formal mathematics
library among all other theorem provers.
Huh, why do you think that
"""x / 0 = 0 remains false unless x = 0."""?
It can be easily proved in HOL4 and HOL Light.:
In HOL4:
First, by definition: x / y = x * inv y
https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/real/realScript.sml#L85
and then inv 0 = 0 (REAL_INV_EQ_0)
https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/real/realScript.sml#L687
In HOL Light:
https://github.com/jrh13/hol-light/blob/master/real.ml#L812
let REAL_DIV_EQ_0 = prove
(!x y. x / y = &0 <=> x = &0 \/ y = &0,
REWRITE_TAC[real_div; REAL_INV_EQ_0; REAL_ENTIRE]);;
so to show that x / 0 = 0 it is enough to show that x = 0 \/ 0 = 0,
which is obviously true.
--Chun
Il 27/02/19 14:45, Christian Sternagel ha scritto:
A short answer is: there is no "division by zero calculus".
In Isabelle/HOL a constant is whatever you define it to be. If you
define a constant, let's call it "division", likedivision x y = (if y = 0 then 0 else Max {k::nat. k * y ≤ x})
then, of course, you can prove for this constant that it satisfies
division x 0 = 0
because that is just its definition.
Whether this has any connection to what mainstream math understands as
division is an entirely orthogonal issue.cheers
chris
On 2/26/19 10:37 PM, Saburou Saitoh wrote:
Dear Beautiful Isabelle/HOL:
I got a surprising news through Professor Hiroshi Okumura on 16 February,
2016 in Research Gate:José Manuel Rodríguez Caballero
Added an answer
In the proof assistant Isabelle/HOL we have x/0 = 0 for each number x. This is
advantageous in order to simplify the proofs. You can download this proof
assistant here: *https://isabelle.in.tum.de/and Caballero kindly introduced further several surprising examples on
the division
by zero calculus.Of course, I know many beautiful ladies love secret. However, in some
restriction, I would like to know some details like:When did the system derive the output 1/0 = 0?
When did the system derive the output \tan(\pi/2) = 0?
When did the system derive the output \log 0 = 0?
And some more any.
It seems that their results are historical, because the results are not
still accepted (admitted) over the world, in particular, in mathematics.With best regards,
Sincerely yours,
Saburou Saitoh2019.2.27.6:38
Email Gateway (Aug 22 2022 at 19:04):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Hi Johannes,
thank you so much, I really didn't notice this. So the real arithmetic
in HOL4, HOL Light and Isabelle/HOL, they're actually the same!
Best regards,
Chun Tian
Il 28/02/19 10:30, Johannes Hölzl ha scritto:
signature.asc
Email Gateway (Aug 22 2022 at 19:05):From: Walther Neuper <walther.neuper@jku.at>
Dear Saburou,
if you want a serious answer, you have to ask a serious question. And
"love secrets" are not considered serious on this list.
Assuming, that the question is meant serious by you as a mathematician,
and that you want a serious answer, I suggest to check the context of
this list. A serious starting point would be a recent discussion
following the message
https://www.mail-archive.com/hol-info@lists.sourceforge.net/msg05468.html
Hope that helps,
Walther
Email Gateway (Aug 22 2022 at 19:05):From: Lawrence Paulson <lp15@cam.ac.uk>
Oddly enough, I took the opposite lesson from your example: it illustrates how small changes in definitions can make a huge impact on the amount of work that must be done.
Note that the product xy is undefined if either x or y is undefined. Therefore if
x = measure m S and y = 0
then, strictly speaking, we have no right to say xy = 0 unless we have first shown that x is defined, therefore that the set S is measurable, etc. Of course nobody would do this. And yet your own example can be rewritten in this form, with 1 / measure m s for the possibly undefined term.
Larry Paulson
Email Gateway (Aug 22 2022 at 19:05):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Hi,
you're mostly right, except that in my framework (the modified
extrealTheory in HOL4) my own example actually cannot be rewritten into
this form, simply because x / y = x * (inv y) doesn't hold when y = 0.
Yet I still have !x. 0 * x = 0 as a theorem, but this is fine, since
the key is to have "undefined" not defined anywhere, thus no way to
express "!x. x is defined ==> 0 * x = 0``.
P.S. I have no intents to push Isabelle (or even HOL4) to abandon
division-by-zero arithmetic for integers (nats) and reals. Even for
extended reals, I'm going to use a compile-time flag to switch between
two versions of definitions, while I can technically make sure that all
my proof code work with both versions.
--Chun
Il 28/02/19 12:10, Lawrence Paulson ha scritto:
signature.asc
Email Gateway (Aug 22 2022 at 19:15):From: Saburou Saitoh <saburou.saitoh@gmail.com>
Dear Beautiful Isabelle/HOL:
I got a surprising news through Professor Hiroshi Okumura on 16 February,
2016 in Research Gate:
José Manuel Rodríguez Caballero
Added an answer
In the proof assistant Isabelle/HOL we have x/0 = 0 for each number x. This is
advantageous in order to simplify the proofs. You can download this proof
assistant here: *https://isabelle.in.tum.de/
and Caballero kindly introduced further several surprising examples on
the division
by zero calculus.
Of course, I know many beautiful ladies love secret. However, in some
restriction, I would like to know some details like:
When did the system derive the output 1/0 = 0?
When did the system derive the output \tan(\pi/2) = 0?
When did the system derive the output \log 0 = 0?
And some more any.
It seems that their results are historical, because the results are not
still accepted (admitted) over the world, in particular, in mathematics.
With best regards,
Sincerely yours,
Saburou Saitoh
2019.2.27.6:38
Email Gateway (Aug 22 2022 at 19:15):From: Lars Hupel <hupel@in.tum.de>
Dear Saburou Saitoh,
Of course, I know many beautiful ladies love secret.
this kind of language is both off-topic for this mailing list and
inappropriate for most mailing lists.
Cheers
Lars
Last updated: Apr 18 2024 at 20:16 UTC