[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Proof: limit of strictly monotonic function overnaturals



Thanks a lot! Not only for the actual proof, but also for the nice explanation.

Regards
Yoshi


On Tue, 11 Jan 2005 12:17:28 -0600, Jerry James <james@ittc.ku.edu> wrote:
> Yoshimi Takano <yoshimi.takano@gmail.com> writes:
> > I'm still unexperienced in using PVS, so could anyone please tell me
> > how to prove the following theorem?
> >
> >   f: VAR [nat -> int]
> >
> >   strictly_monotonic(f): bool =
> >     FORALL (n: nat): f(n) < f(n + 1)
> >
> >   unbounded(f): bool =
> >     FORALL (x: int): EXISTS (n: nat): f(n) >= x
> >
> >   strictly_monotonic_unbounded: THEOREM
> >     FORALL f: strictly_monotonic(f) IMPLIES unbounded(f)
> 
> You want to do some kind of induction over 'x' in the expansion of
> 'unbounded'.  However, induction is over the nats, not the ints.
> Observe, though, that for any given 'x', the distance between 'x' and
> 'f(n)' is decreasing for increasing values of 'n'.  This suggests using
> measure induction.  One measure you could try is 'x - f(0)', but this
> doesn't quite work, because that measure might be negative.  Then
> observe that if it is negative, you are done, because then 'f(0)' is the
> element you need to show that you have reached or exceeded 'x'.  This
> leads to the following proof:
> 
>  (expand* "unbounded" "strictly_monotonic")
>  (skosimp)
>  (measure-induct+ "IF x >= f!1(0) THEN x - f!1(0) ELSE 0 ENDIF" ("x"))
>  (("1"
>    (inst - "x!1 - 1")
>    (smash)
>    (("1" (skolem!) (inst - "n!1") (inst + "1 + n!1") (assert))
>     ("2" (inst - "0") (inst + "1") (assert))
>     ("3" (inst + "0") (assert))))
>   ("2" (assert))))
> 
> Regards,
> --
> Jerry James
> Email: james@ittc.ku.edu -or- jamesj@acm.org
> WWW:   http://www.ittc.ku.edu/~james/
>