[opentheory-users] opentheory-users Digest, Vol 38, Issue 3

[Joe Leslie-Hurd]

Hi Robert,

Sorry about the delay in responding to your email.

On Fri, Sep 18, 2015 at 8:44 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe,
>
> Here is the error I get when I try to export things from real.ml:
>
> Exception: Failure "abs const out of type op definition scope: real".
>
> Error in included file /Users/robertwhite/Projects/hol-light/real.ml

This probably happens because there is a reference to a theorem in
realax.ml that hasn't been exported, either deliberately or
accidentally. Which theorem specifically produces this error?

> Another question is that. I noticed that you changed real_div to !x y. ~(y =
> &0) ==> x / y = x * inv y
>
> It was fun to see the original HOL Light version allowing y to be &0. So how
> is that possible?

It is not logically inconsistent to define 1/0 = 0, as HOL Light does.
But since other theorem provers leave 1/0 underspecified, for the
OpenTheory standard library I must take the weakest view and also
leave it underspecified (hence the deviation from the standard
distribution of HOL Light). This will likely entail some changes in
theorems involving inv or div (extra side-conditions, or extra cases
in the proof). I needed to do the same kind of thing with natural
number subtraction (standard HOL Light sets 0 - n = 0 for all n).

> Finally, I don't know how to prove ~(&0 = &1) I find it hard to prove from
> ~(0 = 1). Can you give me some hint? Is that actually a subtyping or
> something cos I noticed that they are of different type:
>
> 0 : num
>
> & 0 : int
>
> inv (&0) : real

The default type for the symbol '&' in HOL Light is :num -> int, not
:num->real as you want. The simplest way to deal with this is to add
type annotations where necessary, like this:

!m n. (&m : real) = &n ==> m = n

Incidentally, this theorem will help you prove ~(&0 = &1).

Hope that helps,

Joe