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

[PVS-Help] Question



Hi, I've got a question regarding proof subgoals generated. My aim is to prove the following:

verify_for: THEORY

   BEGIN
     
    i,n,m,y: VAR nat

    count(i,n): RECURSIVE nat =
    (if n=0 then 0
     elsif i=0 then count(1,n)
     elsif i=n then n
     else i+count(i+1,n)
     endif)
     MEASURE i

    x: VAR posint

     form_sum: AXIOM count(y,n) = (n-y+1)*(n+y)/2

     difference: THEOREM x<=n AND x-1>=0 IMPLIES count(x-1,n)-count(x,n) = x-1

END verify_for

-------------

The proof looked like this:

  |-------
{1}   FORALL (n: nat, x: posint):
        x <= n AND x - 1 >= 0 IMPLIES count(x - 1, n) - count(x, n) = x - 1

Rule? (induct "x")
Inducting on x on formula 1,
this yields  3 subgoals:
difference.1 : 

  |-------
{1}   x!1 > 0
{2}   FORALL (n: nat):
        x!1 <= n AND x!1 - 1 >= 0 IMPLIES
         count(x!1 - 1, n) - count(x!1, n) = x!1 - 1

Rule? (skolem!)
Skolemizing,
this simplifies to:
difference.1 : 

  |-------
[1]   x!1 > 0
{2}   x!1 <= n!1 AND x!1 - 1 >= 0 IMPLIES
       count(x!1 - 1, n!1) - count(x!1, n!1) = x!1 - 1

Rule? (use "form_sum")
Using lemma form_sum,
this simplifies to:
difference.1 : 

{-1}  count(x!1, n!1) = (n!1 - x!1 + 1) * (n!1 + x!1) / 2
  |-------
[1]   x!1 > 0
[2]   x!1 <= n!1 AND x!1 - 1 > = 0 IMPLIES
       count(x!1 - 1, n!1) - count(x!1, n!1) = x!1 - 1

Rule? (lemma "form_sum")
Applying form_sum
this simplifies to:
difference.1 : 

{-1}  FORALL (n, y: nat): count(y, n) = (n - y + 1) * (n + y) / 2
[-2]  count(x!1, n!1) = (n!1 - x!1 + 1) * (n!1 + x!1) / 2
  |-------
[1]   x!1 > 0
[2]   x!1 <= n!1 AND x!1 - 1 >= 0 IMPLIES
       count(x!1 - 1, n!1) - count(x!1, n!1) = x!1 - 1

Rule? (inst -1 "n!1" "x!1-1")
Instantiating the top quantifier in -1 with the terms:
 n!1, x!1-1,
this simplifies to:
difference.1 : 

{-1}  count(x!1 - 1, n!1) = (n!1 - (x!1 - 1) + 1) * (n!1 + (x!1 - 1)) / 2
[-2]  count(x!1, n!1) = (n!1 - x!1 + 1) * (n!1 + x!1) / 2
  |-------
[1]   x!1 > 0
[2]   x!1 <= n!1 AND x!1 - 1 >= 0 IMPLIES
  & nbsp;    count(x!1 - 1, n!1) - count(x!1, n!1) = x!1 - 1

Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,

This completes the proof of difference.1.

difference.2 : 

  |-------
{1}   0 > 0 IMPLIES
       (FORALL (n: nat):
          0 <= n AND 0 - 1 >= 0 IMPLIES
           count(0 - 1, n) - count(0, n) = 0 - 1)


Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,

This completes the proof of difference.2.

difference.3 : 
.
.
.

This completes the proof of difference.3.

Q.E.D.

-----------

My question is, why would difference.2 be generated as a subgoal when x is specified to be a positive integer in the first place? In an attempt to get over and done with this proof, I inserted the command (assert) but I'm still troubled over why it was generated in the first place.

Thx.


With Windows Live, you can organize, edit, and share your photos.