I think there is definitely an advantage in keeping ``x/y`` undefined
(even granted that it will always be possible to prove ``?y. x/0 = y``),
namely that it means that your proofs are much more likely to directly
translate to other formalisms of real numbers where '/' is not total.
Of course there is also a disadvantage, in that it makes proof harder.
But then, arguably, being forced to justify that we are staying within
the "normal" domain of the function is probably a good thing (in a
similar way as being forced to conform to a type system is a good
thing). I understand that, historically, it is this disadvantage of
harder proofs that was the reason for making ``0/0=0`` in HOL. It's
much easier for automated routines if they don't have to consider side
conditions.
Mark.
On 15/02/2019 08:56, Chun Tian (binghe) wrote:
Thanks to all kindly answers.
Even I wanted ``0 / 0 = 0`` to be excluded from at least
"extreal_div_def" (in extrealTheory), I found no way to do that. All I
can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
going to happen, I do case analysis instead.
--Chun
Il 14/02/19 18:12, Konrad Slind ha scritto:
It's a deliberate choice. See the discussion in Section 1.2 of
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692&rep=rep1&type=pdf
On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
<binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>> wrote:
Hi,
in HOL's realTheory, division is defined by multiplication:
[real_div] Definition
⊢ ∀x y. x / y = x * y⁻¹
and zero multiplies any other real number equals to zero, which is
definitely true:
[REAL_MUL_LZERO] Theorem
⊢ ∀x. 0 * x = 0
However, above two theorems together gives ``0 / 0 = 0``, as shown
below:
> REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
val it = ⊢ 0 / 0 = 0: thm
How do I understand this result? Is there anything "wrong"?
(The same problems happens also in extrealTheory, since the
definition
of `*` finally reduces to `*` of real numbers)
Regards,
Chun Tian
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
