It’s still defined inasmuch as it is perfectly legitimate to write x/0 and use
that term to define other things in turn. For example, I can define foo = x/0
+ 1 and then quite successfully prove that x/0 < foo.
I would avoid the use of the word undefined in this context; rather x/0 has an
unspecified value. All functions are total so all applications of functions to
all possible arguments have values.
Michael
> On 9 Aug 2019, at 21:46, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
>
> A follow-up of this old topic:
>
> Finally I found the following definitions of `extreal_inv` and `extreal_div`
> based on new_specification():
>
> local
> val lemma = Q.prove (
> `?i. (i NegInf = Normal 0) /\
> (i PosInf = Normal 0) /\
> (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`,
> (* proof *)
> Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
> else if x = Normal 0 then ARB
> else Normal (inv (real x))` \\
> RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
> (* |- extreal_inv NegInf = Normal 0 /\
> extreal_inv PosInf = Normal 0 /\
> !r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
> *)
> val extreal_inv_def = new_specification
> ("extreal_inv_def", ["extreal_inv"], lemma);
> end;
>
> local
> val lemma = Q.prove (
> `?d. (!r. d (Normal r) PosInf = Normal 0) /\
> (!r. d (Normal r) NegInf = Normal 0) /\
> (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv
> (Normal r))))`,
> (* proof *)
> Q.EXISTS_TAC `\x y.
> if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then Normal 0
> else if y = Normal 0 then ARB
> else extreal_mul x (extreal_inv y)` \\
> RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
> (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
> (!r. extreal_div (Normal r) NegInf = Normal 0) /\
> !x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv (Normal r)
> *)
> val extreal_div_def = new_specification
> ("extreal_div_def", ["extreal_div"], lemma);
> end;
>
> In this way, things like `extreal_inv 0` and `extreal_div x 0` are *really*
> undefined.
>
> --Chun
>
> Il 20/02/19 06:48, michael.norr...@data61.csiro.au ha scritto:
>> Your right hand side is no better than ARB really. You say that your aim is
>> to avoid x/0 = y, with y a literal extreal. But if you believe ARB is a
>> literal extreal, then I will define
>>
>> val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
>>
>> and then I can certainly prove that x/0 = pni. If ARB is a literal extreal,
>> surely pni is too.
>>
>> (Recall that ARB's definition is `ARB = @x. T`.)
>>
>> Michael
>>
>>
>> On 20/2/19, 09:31, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
>>
>> 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
>>>
>>
>>
>>
>>
>> _______________________________________________
>> 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
