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

Re: [work] [PVS-Help] inequalities in PVS



If you are using PVS 3.2 or higher, you should consider installing the
NASA PVS Libraries:
http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html

This library includes the packages Manip
(http://shemesh.larc.nasa.gov/people/bld/manip.html) and Field
(http://research.nianet.org/~munoz/Field), which provide several
strategies for simple (and not that simple) manipulations of arithmetic
expressions.

This is a possible proof of your example:  

lem : LEMMA
    FORALL (x:real): 1 < x and x < 1000 implies 
     1000 - x*x < 1000 - x

%|- lem : PROOF
%|- (then (skosimp) (grind-reals) (cancel-by 1 "x!1"))
%|- QED

Hope that it helps,

Cesar


On Wed, 2007-10-17 at 21:42 +0200, A Serebrenik wrote:
> Dear all,
> 
> I wonder what proof command should I use for simple manipulation of 
> inequalities? I would like, e.g. to prove the following sequent:
> {-1}  integer_pred(x!1)
> {-2}  x!1 < 1000
> {-3}  x!1 > 1
> {-4}  x!1 * x!1 > 1
> {-5}  x!1 * x!1 < 1000
>    |-------
> {1}   1000 - x!1 * x!1 < 1000 - x!1
> 
> Using (both-sides - 1000) and (assert) I can reduce the succedent to
> {1'}  -1 * (x!1 * x!1) < -1 * x!1 but this is as far as I get: (both-sides 
> * -1) results in an unexpected:
> {1''}  -1 * (x!1 * x!1) * -1 < -1 * x!1 * -1
> 
> Best regards,
> Alexander Serebrenik
> 
> 
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace         mailto:Cesar.A.Munoz@nasa.gov
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4