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

[Robert White]

Dear Joe,

Thanks for the reply. I will look into it again.

Robert

On 22 September 2015 at 20:16, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>



-- 

Regards,
Robert

New homepage at Github: https://airobert.github.io/
New email address at ILLC: shuai.wang at student.uva.nl
Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150923/57541925/attachment.html>