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 >
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
