Note that many/most interesting properties of division still pick up
side-conditions involving the non-zero-ness of y. (The attachment is all HOL4's
"simple" theorems about division from realTheory, which establishes the basic
properties of the reals and their operations.)
Michael
On 16/2/19, 04:38, "Mark Adams" <m...@proof-technologies.com> wrote:
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
[(("real", "ABS_DIV"),
(⢠ây. y â 0 â âx. abs (x / y) = abs x / abs y, Thm)),
(("real", "div_rat"),
(⢠x / y / (u / v) =
if (u = 0) ⨠(v = 0) then x / y / unint (u / v)
else if y = 0 then unint (x / y) / (u / v)
else x * v / (y * u), Thm)),
(("real", "div_ratl"),
(⢠x / y / z =
if y = 0 then unint (x / y) / z
else if z = 0 then unint (x / y / z)
else x / (y * z), Thm)),
(("real", "div_ratr"),
(⢠x / (y / z) =
if (y = 0) ⨠(z = 0) then x / unint (y / z) else x * z / y, Thm)),
(("real", "NUM_FLOOR_DIV"),
(⢠0 ⤠x ⧠0 < y â &flr (x / y) * y ⤠x, Thm)),
(("real", "NUM_FLOOR_DIV_LOWERBOUND"),
(⢠0 ⤠x ⧠0 < y â x < &(flr (x / y) + 1) * y, Thm)),
(("real", "real_div"), (⢠âx y. x / y = x * yâ»Â¹, Def)),
(("real", "REAL_DIV_ADD"), (⢠âx y z. y / x + z / x = (y + z) / x,
Thm)),
(("real", "REAL_DIV_DENOM_CANCEL"),
(⢠âx y z. x â 0 â (y / x / (z / x) = y / z), Thm)),
(("real", "REAL_DIV_DENOM_CANCEL2"),
(⢠ây z. y / 2 / (z / 2) = y / z, Thm)),
(("real", "REAL_DIV_DENOM_CANCEL3"),
(⢠ây z. y / 3 / (z / 3) = y / z, Thm)),
(("real", "REAL_DIV_INNER_CANCEL"),
(⢠âx y z. x â 0 â (y / x * (x / z) = y / z), Thm)),
(("real", "REAL_DIV_INNER_CANCEL2"),
(⢠ây z. y / 2 * (2 / z) = y / z, Thm)),
(("real", "REAL_DIV_INNER_CANCEL3"),
(⢠ây z. y / 3 * (3 / z) = y / z, Thm)),
(("real", "REAL_DIV_LMUL"), (⢠âx y. y â 0 â (y * (x / y) = x),
Thm)),
(("real", "REAL_DIV_LMUL_CANCEL"),
(⢠âc a b. c â 0 â (c * a / (c * b) = a / b), Thm)),
(("real", "REAL_DIV_LZERO"), (⢠âx. 0 / x = 0, Thm)),
(("real", "REAL_DIV_MUL2"),
(⢠âx z. x â 0 ⧠z â 0 â ây. y / z = x * y / (x * z), Thm)),
(("real", "REAL_DIV_OUTER_CANCEL"),
(⢠âx y z. x â 0 â (x / y * (z / x) = z / y), Thm)),
(("real", "REAL_DIV_OUTER_CANCEL2"),
(⢠ây z. 2 / y * (z / 2) = z / y, Thm)),
(("real", "REAL_DIV_OUTER_CANCEL3"),
(⢠ây z. 3 / y * (z / 3) = z / y, Thm)),
(("real", "REAL_DIV_REFL"), (⢠âx. x â 0 â (x / x = 1), Thm)),
(("real", "REAL_DIV_REFL2"), (⢠2 / 2 = 1, Thm)),
(("real", "REAL_DIV_REFL3"), (⢠3 / 3 = 1, Thm)),
(("real", "REAL_DIV_RMUL"), (⢠âx y. y â 0 â (x / y * y = x), Thm)),
(("real", "REAL_DIV_RMUL_CANCEL"),
(⢠âc a b. c â 0 â (a * c / (b * c) = a / b), Thm)),
(("real", "REAL_EQ_LDIV_EQ"),
(⢠âx y z. 0 < z â ((x / z = y) â (x = y * z)), Thm)),
(("real", "REAL_EQ_RDIV_EQ"),
(⢠âx y z. 0 < z â ((x = y / z) â (x * z = y)), Thm)),
(("real", "REAL_LE_DIV"), (⢠âx y. 0 ⤠x ⧠0 ⤠y â 0 ⤠x / y,
Thm)),
(("real", "REAL_LE_LDIV"),
(⢠âx y z. 0 < x ⧠y ⤠z * x â y / x ⤠z, Thm)),
(("real", "REAL_LE_LDIV_EQ"),
(⢠âx y z. 0 < z â (x / z ⤠y â x ⤠y * z), Thm)),
(("real", "REAL_LE_RDIV"),
(⢠âx y z. 0 < x ⧠y * x ⤠z â y ⤠z / x, Thm)),
(("real", "REAL_LE_RDIV_EQ"),
(⢠âx y z. 0 < z â (x ⤠y / z â x * z ⤠y), Thm)),
(("real", "REAL_LT_DIV"), (⢠âx y. 0 < x ⧠0 < y â 0 < x / y, Thm)),
(("real", "REAL_LT_LDIV_EQ"),
(⢠âx y z. 0 < z â (x / z < y â x < y * z), Thm)),
(("real", "REAL_LT_RDIV"),
(⢠âx y z. 0 < z â (x / z < y / z â x < y), Thm)),
(("real", "REAL_LT_RDIV_0"), (⢠ây z. 0 < z â (0 < y / z â 0 < y),
Thm)),
(("real", "REAL_LT_RDIV_EQ"),
(⢠âx y z. 0 < z â (x < y / z â x * z < y), Thm)),
(("real", "REAL_POW_DIV"),
(⢠âx y n. (x / y) pow n = x pow n / y pow n, Thm))]: DB.data list
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
