Ha - I stand corrected. Thanks for that. From: Konrad Slind <konrad.sl...@gmail.com> Date: Wednesday, 20 February 2019 at 17:22 To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au> Cc: hol-info <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] 0 / 0 = 0 ???
Just a minor note: ARB is declared as an uninterpreted constant of type 'a. It used to be defined to be @x.T. Konrad. On Tue, Feb 19, 2019 at 11:49 PM <michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote: 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<mailto: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> <mailto: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> >>>> <mailto: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<mailto:hol-info@lists.sourceforge.net> >>> https://lists.sourceforge.net/lists/listinfo/hol-info > _______________________________________________ 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
