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

simple problem



I have not too many experiences in PVS but I am trying to move my first
step with this tool.
I find some problem with a proof.
This is my problem:
I have defined Fibonacci number in the following way:

fib(n):RECURSIVE posnat=
IF n=1 THEN 1
ELSIF n=2 THEN 1
ELSE fib(n-1)+fib(n-2)
ENDIF
MEASURE n

and then i have tried some tests without any problem.

Then I have defined 
f(n):posnat = fib(n+1)*fib(n-1)
and I have tried to prove this lemma:

fib_p1 LEMMA:
n>1 IMPLIES f(n)=fib(n)^2+(-1)^n

I have used this sequence whitout too much success
Rule? (INDUCT "n")

{-1} n!1>1
--------
{1} n!1>0
{2} f(n!1)=fib(n!1)^2+(-1)^n!1

Rule? (hide 2)

{-1} n!1>1
--------
{1} n!1>0

Rule? (grind)
-------
{1} 0>0 imlies 0>1 implies f(0)=fib(0)^2+(-1)^0

Rule? (grind)
--------------
{1} forall j:
    (j>0 imlies j>1 implies f(j)=fib(j)^2+(-1)^j) implies
    j+1>0 imlies j+1>1 implies f(j+1)=fib(j+1)^2+(-1)^(j+1)

Rule? (skosimp)

{-1} j!1>0 imlies j!1>1 implies f(j!1)=fib(j!1)^2+(-1)^j!1 
{-2} j!1+1>0
{-3} j!1+1>1
----------
{1}
    f(j!1+1)=fib(j!1+1)^2+(-1)^(j!1+1)

and now also if I use lemma nat_induction then I have no result
This is a typical induction proof It is necessary demostrate step base then
it must be done inductive hp and then the proof come, but with my little
experience I am not be able to find it:
Is there a common procedure for this kind of dimostration?
Regards
Paola Spoletini