<div dir="ltr">Dear Joe,<div><br></div><div>Thanks for the reply. I will look into it again.</div><div><br></div><div>Robert</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 22 September 2015 at 20:16, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert,<br>
<br>
Sorry about the delay in responding to your email.<br>
<span class=""><br>
On Fri, Sep 18, 2015 at 8:44 AM, Robert White<br>
<<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
> Dear Joe,<br>
><br>
> Here is the error I get when I try to export things from <a href="http://real.ml" rel="noreferrer" target="_blank">real.ml</a>:<br>
><br>
> Exception: Failure "abs const out of type op definition scope: real".<br>
><br>
> Error in included file /Users/robertwhite/Projects/hol-light/<a href="http://real.ml" rel="noreferrer" target="_blank">real.ml</a><br>
<br>
</span>This probably happens because there is a reference to a theorem in<br>
<a href="http://realax.ml" rel="noreferrer" target="_blank">realax.ml</a> that hasn't been exported, either deliberately or<br>
accidentally. Which theorem specifically produces this error?<br>
<span class=""><br>
> Another question is that. I noticed that you changed real_div to !x y. ~(y =<br>
> &0) ==> x / y = x * inv y<br>
><br>
> It was fun to see the original HOL Light version allowing y to be &0. So how<br>
> is that possible?<br>
<br>
</span>It is not logically inconsistent to define 1/0 = 0, as HOL Light does.<br>
But since other theorem provers leave 1/0 underspecified, for the<br>
OpenTheory standard library I must take the weakest view and also<br>
leave it underspecified (hence the deviation from the standard<br>
distribution of HOL Light). This will likely entail some changes in<br>
theorems involving inv or div (extra side-conditions, or extra cases<br>
in the proof). I needed to do the same kind of thing with natural<br>
number subtraction (standard HOL Light sets 0 - n = 0 for all n).<br>
<span class=""><br>
> Finally, I don't know how to prove ~(&0 = &1) I find it hard to prove from<br>
> ~(0 = 1). Can you give me some hint? Is that actually a subtyping or<br>
> something cos I noticed that they are of different type:<br>
><br>
> 0 : num<br>
><br>
> & 0 : int<br>
><br>
> inv (&0) : real<br>
<br>
</span>The default type for the symbol '&' in HOL Light is :num -> int, not<br>
:num->real as you want. The simplest way to deal with this is to add<br>
type annotations where necessary, like this:<br>
<br>
!m n. (&m : real) = &n ==> m = n<br>
<br>
Incidentally, this theorem will help you prove ~(&0 = &1).<br>
<br>
Hope that helps,<br>
<div class="HOEnZb"><div class="h5"><br>
Joe<br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>Regards,</div><div>Robert </div><div><br></div><div>New homepage at Github: <a href="https://airobert.github.io/" target="_blank">https://airobert.github.io/</a><br></div><div><span style="font-size:12.8px">New email address at ILLC: </span><a href="mailto:shuai.wang@student.uva.nl" style="font-size:12.8px" target="_blank">shuai.wang@student.uva.nl</a><br></div><div><span style="font-size:12px;line-height:20px">Carolina MacGillavrylaan </span><span style="font-size:12px;line-height:20px">2246</span><span style="font-size:12px;line-height:20px"> , 1098 XK AMSTERDAM  HP: </span><span style="color:rgb(20,24,35);font-family:helvetica,arial,sans-serif;font-size:13px;line-height:17.94px;white-space:pre-wrap">0652691901</span><br></div><div><br></div></div></div></div></div></div></div></div></div></div></div></div>
</div>