Re: [Hol-info] Proof related to REAL_BIGNUM

[Chou, Ching-T. <chi...@in...>]

Your original goal cannot true.  For example, if P contains all reals,
then inf P is negative infinity, which is not a real.  But inf P must be
a real, for otherwise "inf P IN P" would not even type-check.

For your goal to be true, either the type "real" has to be extended with
negative infinity, or your goal has to be refined by saying that both P
and Q have real lower bounds.

- Ching Tsun

>-----Original Message-----
>From: hol...@li... [mailto:hol-info-
>bo...@li...] On Behalf Of Osman Hasan
>Sent: Saturday, July 15, 2006 9:51 PM
>To: John Harrison
>Cc: hol...@li...
>Subject: Re: [Hol-info] Proof related to REAL_BIGNUM
>
>Thanks to everyone who responded. Actually, I want to prove the
following
>goal
>
>!(P: (real -> bool)) (Q: real -> bool).
>	(P SUBSET Q) /\ (inf P IN P) =3D=3D>
>        	inf Q <=3D inf P
>
>Where 'inf' refers to the infimim and is defined in the "realTheory" in
>HOL.
>
>In the proof process I ended up with the following subgoal:
>
>    ?z. !x. x IN Q =3D=3D> z <=3D x
>    ------------------------------------
>      0.  P SUBSET Q
>      1.  inf P IN P
>
>Which basically means that I have to give a lower bound for Q, which
>theoratically speaking is negetive infinity. But, I am not sure how to
>express this in HOL.
>
>This is why I was trying to prove the goal that I had specified in my
>previous email. Now, after reading your comments, I am not sure even if
>the above goal is provable or not.
>
>Thanks again,
>--Osman
>
>
>
>
>
>
>
>On Sat, 15 Jul 2006, John Harrison wrote:
>
>>
>> Hi Osman,
>>
>> | I am trying to prove the following theorem in HOL
>> |
>> | |- ?(n:num). !(r:real). r < & n
>>
>> In fact this is false. If there were such a number n, then in
>> particular we would have &n < &n, which is impossible. Here's a
>> proof of the negation (in HOL Light):
>>
>>  MESON[REAL_LT_REFL] `~(?(n:num). !(r:real). r < & n)`;;
>>
>> | It is somewhat related to the REAL_BIGNUM theorem found in the
>realTheory:
>> |
>> | |- !r. ?n. r < &n
>>
>> Right, this is known as the Archimedean property of the reals. The
fact
>> that one is true and the other false just shows how critical the
nesting
>> order of quantifiers can be.
>>
>> Were you just trying to prove the above claim out of curiosity, or
>> was it meant as a lemma on the way to something else? If the latter,
>> perhaps someone can help you with what you really want to prove.
>>
>> John.
>>
>
>
>-----------------------------------------------------------------------
--
>Using Tomcat but need to do more? Need to support web services,
security?
>Get stuff done quickly with pre-integrated technology to make your job
>easier
>Download IBM WebSphere Application Server v.1.0.1 based on Apache
Geronimo
>http://sel.as-us.falkag.net/sel?cmd=3Dlnk&kid=3D120709&bid=3D263057&dat=3D=
12164
2
>_______________________________________________
>hol-info mailing list
>hol...@li...
>https://lists.sourceforge.net/lists/listinfo/hol-info