[opentheory-users] opentheory-users Digest, Vol 38, Issue 3
ai.robert.wangshuai at gmail.com
Wed Sep 23 08:27:02 UTC 2015
Thanks for the reply. I will look into it again.
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
> > 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
> > ~(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,
> opentheory-users mailing list
> opentheory-users at gilith.com
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...
More information about the opentheory-users