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> 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 > 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
