Re: [PVS-Help] inequalities in PVS

[Ben Di Vito <Benedetto.L.DiVito@xxxxxxxx>]

Alexander,

This problem and many like it can be solved using strategy packages that 
we've developed at NASA Langley and NIA.  If you are a user of the NASA 
Langley libraries found at

  http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html

you probably have the strategy packages Manip and Field already loaded.  
If not, you can retrieve the libraries or just the strategies from the 
web site.

A proof of your conjecture is easy to obtain using these strategies, 
which were designed to help with cases requiring detailed manipulation 
such as yours.  Learning to use them requires some investment of your 
time, of course, but if you expect to do a lot of proving, you would 
realize a benefit from the effort.

So here is how it goes:

{-1}  x!1 < 1000
{-2}  x!1 > 1
{-3}  x!1 * x!1 > 1
{-4}  x!1 * x!1 < 1000
  |-------
{1}   1000 - x!1 * x!1 < 1000 - x!1

Rerunning step: (field 1)
both_sides_minus_lt2 rewrites 1000 - x!1 * x!1 < 1000 - x!1
  to x!1 < x!1 * x!1

Simplifying formula 1 with FIELD,
this simplifies to:
m1 : 

[-1]  x!1 < 1000
[-2]  x!1 > 1
[-3]  x!1 * x!1 > 1
[-4]  x!1 * x!1 < 1000
  |-------
{1}   x!1 < x!1 * x!1

Rerunning step: (op-ident 1 l)

Applying identity operation to rewrite selected expression,
this simplifies to:
m1 : 

[-1]  x!1 < 1000
[-2]  x!1 > 1
[-3]  x!1 * x!1 > 1
[-4]  x!1 * x!1 < 1000
  |-------
{1}   (x!1 * 1 < x!1 * x!1)

Rerunning step: (cancel 1)

Canceling terms from both sides of selected formulas,
this simplifies to:
m1 : 

[-1]  x!1 < 1000
[-2]  x!1 > 1
[-3]  x!1 * x!1 > 1
[-4]  x!1 * x!1 < 1000
  |-------
{1}   1 < x!1

Rerunning step: (assert)
Simplifying, rewriting, and recording with decision procedures,
Q.E.D.

---------

The strategy "field" performs many reductions automatically, although it 
mostly helps when divisions are present.  In this case it rearranges the 
conclusion the way we would like it.  Next we want to cancel an "x" from 
both sides, but first we need to create a more symmetric formula to set 
up the cancellation.  The strategy "op-ident" is the helper and "cancel" 
does what we need to eliminate the "x".  The rest is handled by assert.

Regards,

Ben Di Vito

1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681   USA

voice: +1-757-864-4883     fax: +1-757-864-4234
b.divito@nasa.gov
http://shemesh.larc.nasa.gov/people/bld


---------

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
>
>