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

Re: Proofing problem


> My problem is, PVS wants me to proof:
> {-1}  interval > 0
> {-2}  interval <= max_interval
> [-3]  number_intervals > 0
> [-4]  p!1 >= 0
> [-5]  p!1 < number_intervals
>   |-------
> [1]   interval * number_intervals > p!1 * interval - interval
> where interval and number_intervals are of type nat.

On paper, you would complete your proof by first rewriting the right
hand side of [1] to  "interval * (p!1 - 1)" followed by cancelling the
factor "interval" on both sides (bearing in mind that "interval" is
non-zero, by [-1]). The remaining goal 
"number_intervals > p!1 - 1" then follows directly from [-5]. 

To follow this outline with PVS, you need to apply appropriate lemmas.
Fortunately, PVS comes with a large 'prelude', which contains various
useful proved facts. The key to your problem is found in the theory
'real_props'. Use the Emacs-command 
"M-x view-prelude-theory" to have a look at it. Among various other
things, you can find the lemma

  both_sides_times_neg_gt2: LEMMA nz * x > nz * y IFF y > x

which captures the cancellation step mentioned above. You can
accomplish the preceding rewriting step either explicitly, by using
the command 
  (CASE-REPLACE "p!1 * interval - interval = interval * (p!1 - 1)")
or implicitly by using an appropriate instance of the lemma above,
such as:

  (USE "both_sides_times_pos_gt2" 
       :SUBST ("pz" "interval" "y" "p!1-1"))

In each case, the remaining goals are solved by PVS's ground prover


	- Holger

PS.: If you need to do these kind of proofs more often, you might want
to have a look at Ben Di Vito's "Manip" package
(http://shemesh.larc.nasa.gov/people/bld/manip.html), which has just
been announced and provides various proof strategies to automate such

Holger Pfeifer                           Tel.: +49 (0)731 / 50-24124
Abt. Künstliche Intelligenz               Fax: +49 (0)731 / 50-24119
Universität Ulm                     pfeifer@ki.informatik.uni-ulm.de
D-89069 Ulm         http://www.informatik.uni-ulm.de/ki/pfeifer.html