Dear Professor Chun Tian:
I am very interesting the problem. Could you kindly give your kind comments and suggestions on the draft: *viXra:1908.0100 <http://vixra.org/abs/1908.0100>* *submitted on 2019-08-06 20:03:01*, Fundamental of Mathematics; Division by Zero Calculus and a New Axiom ? It seems that the problem is very Fundamental for our Mathematics. With best regards, Sincerely yours, Saburou Saitoh 2019.8.9.21:08 2019年8月9日(金) 20:47 Chun Tian (binghe) <binghe.l...@gmail.com>: > 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 >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
