Re: [Hol-info] Proof related to REAL_BIGNUM

[Osman H. <o_...@en...>]

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) ==>
        	inf Q <= 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 ==> z <= 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.
>