I'm going to use the following definition for `extreal_div`: (* old definition of `extreal_div`, which allows `0 / 0 = 0` val extreal_div_def = Define `extreal_div x y = extreal_mul x (extreal_inv y)`;
new definition of `extreal_div`, excluding the case `0 / 0`: *)
val extreal_div_def = Define
`extreal_div x y = if (y = Normal 0) then ARB
else extreal_mul x (extreal_inv y)`;
previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <> 0` as
antecedent, which makes perfectly senses.
P.S. the division of extended reals in HOL4 are not used until the
statement and proof of Radon-Nikodým theorem, then the conditional
probability.
--Chun
Il 15/02/19 17:39, Mark Adams ha scritto:
> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
