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

Re: seeking proof of a trivial fact



> b41 : lemma forall (x, y: real): x >=0 and y <= 1 
>   => x * y  <= x 

> Why this lemma is not trivial in PVS ?

Because it involves nonlinear arithmetic, which is not decided in PVS
(and, in its full generality, is undecidable in combination with the
other theories decided by PVS).

To prove it, you need to invoke the lemmas in the prelude theory
real_props.  For example, the following does it.

 (SKOSIMP)
 (LEMMA "both_sides_times_pos_ge1")
 (INST - "x!1" "1" "y!1")
 (("1" (ASSERT)) ("2" (ASSERT)))

You might want to investigate the NASA field and manip strategy
packages, which are designed precisely to ease these difficulties.
See http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html

Lack of automation for nonlinear arithmetic is one of the biggest
complaints we receive about PVS, and we working to improve the way it
is handled by the decision procedures.

John Rushby