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