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

[PVS-Help] Proof: limit of strictly monotonic function over naturals



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/