Some further updates: With my last definition of `extreal_div`, I still have:
|- !x. x / 0 = ARB
and
|- 0 / 0 = ARB
trivially holds (by definition). This is still not satisfied to me.
Now I tried the following new definition which looks more reasonable:
val extreal_div_def = Define
`extreal_div x y = if y = Normal 0 then
(@x. (x = PosInf) \/ (x = NegInf))
else extreal_mul x (extreal_inv y)`;
literally, it says anything (well, let's ignore zero) divides zero is
equal to either +Inf or -Inf. But actually the choice of +Inf/-Inf is
irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
0 = y`` being proved, in which y is a literal extreal. For example, if I
try to prove ``!x. x / 0 = ARB``:
(* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't
be proved, e.g.
val test_div = prove (
`!x. extreal_div x (Normal 0) = ARB`,
RW_TAC std_ss [extreal_div_def]
>> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
>- RW_TAC std_ss []
>> MATCH_MP_TAC SELECT_ELIM_THM
>> RW_TAC std_ss [] (* 3 gubgoals *)
NegInf = ARB
PosInf = ARB
∃x. (x = PosInf) ∨ (x = NegInf));
*)
at the end I got 3 subgoals like above. I *believe*, no matter what
value I put instead of ARB, at least one of the subgoals must be false.
Thus the theorem should be unprovable. (am I right?)
Can I adopt this new definition of `extreal_div` in the future? Any
objection or suggestion?
--Chun
Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
> 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
