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

Proof assistant needed for non-linear arithmetic




One of the more frustrating aspects of using PVS is the machinations
one must go through to prove sequents that involve non-linear
arithmetic.

For example, suppose you are faced with:

   {-1}    n!1 < m!1
     |-------
   {1}    n!1 / m!1 < 1

One must scan through dozens of lemmas in the prelude such as

  both_sides_plus_lt1: LEMMA x + z < y + z IFF x < y

  both_sides_plus_lt2: LEMMA z + x < z + y IFF x < y

  both_sides_minus_lt1: LEMMA x - z < y - z IFF x < y

  both_sides_minus_lt2: LEMMA z - x < z - y IFF y < x

  both_sides_times_pos_lt1: LEMMA x * pz < y * pz IFF x < y

  both_sides_times_pos_lt2: LEMMA pz * x < pz * y IFF x < y

  both_sides_times_neg_lt1: LEMMA x * nz < y * nz IFF y < x

  both_sides_times_neg_lt2: LEMMA nz * x < nz * y IFF y < x

  both_sides_div_pos_lt1: LEMMA x/pz < y/pz IFF x < y

  both_sides_div_pos_lt2: LEMMA pz/px < pz/py IFF py < px

  both_sides_div_pos_lt3: LEMMA nz/px < nz/py IFF px < py

  both_sides_div_neg_lt1: LEMMA x/nz < y/nz IFF y < x

  both_sides_div_neg_lt2: LEMMA pz/nx < pz/ny IFF ny < nx

  both_sides_div_neg_lt3: LEMMA nz/nx < nz/ny IFF nx < ny

till you recognize one that might help, say

    Rule? (LEMMA "both_sides_div_pos_lt1")
    Applying both_sides_div_pos_lt1 
    this simplifies to: 
    foo :  
    
    {-1} (FORALL (pz: posreal, x: real, y: real): x / pz < y / pz IFF x < y)
    [-2] n!1 < m!1
      |-------
    [1]  n!1 / m!1 < 1
   
then you have to carefully instantiate the beast because (INST?) rarely
guesses the right ones:
     
     Rule? (INST -1 "m!1" "n!1" "m!1")
     Instantiating the top quantifier in -1 with the terms: 
      m!1, n!1, m!1,
     this simplifies to: 
     foo :  
     
     {-1}    n!1 / m!1 < m!1 / m!1 IFF n!1 < m!1
     [-2]    n!1 < m!1
       |-------
     [1]    n!1 / m!1 < 1
	  

then of course (FLATTEN) (ASSERT) prove it.

Now wouldn't it be nice if there were a proof assistant running on top of
PVS that you could use as follows:

   {-1}    n!1 < m!1
     |-------
   {1}    n!1 / m!1 < 1

   Rule?   (DIVIDE_BOTH_SIDES_BY "m!1" -1)

The proof assistant would then look through the prelude, find the
appropriate LEMMA and instantiate it for you.

The proof assistant would accept commands that manipulate formulas in the
way one does in an algebra class, such as:

     MULTIPLY_BOTH_SIDES_BY

     DIVIDE_BOTH_SIDES_BY

     ...

It seems to me that this could be developed by graduate students as a
class project or a Master's thesis.?

There are many places where a proof assistant could help.  For example,

Suppose you have an IMPORTED relation (e.g.  (total_order?[T]) ):

    A_theory[N: nat, <= : (total_order?[T])]

Inside this theory, the decision procedures can NOT take advantage of the
fact that this relation is a total order, so formulas such as

       a <= b
       b <= c

     |-----

       a <= c

must be proved by manually instantiating the formulas that are in the
relations theory in the prelude: once again a big pain!

  eq: pred[[T, T]] = (LAMBDA x, y: x = y)

  reflexive?(R): bool = FORALL x: R(x, x)

  irreflexive?(R): bool = FORALL x: NOT R(x, x)

  symmetric?(R): bool = FORALL x, y: R(x, y) IMPLIES R(y, x)

  antisymmetric?(R): bool = FORALL x, y: R(x, y) & R(y, x) => x = y

  connected?(R): bool = FORALL x, y: x /= y IMPLIES R(x, y) OR R(y, x)

  transitive?(R): bool = FORALL x, y, z: R(x, y) & R(y, z) => R(x, z)

A command like (TRANSITIVE "a <= b") could figure out the appropriate
instantiations to establish that a <= b.


Does the PVS community think this would be helpful? practical?


Rick Butler