# Re: simple problem

```Silvia,

I got this proof by using the strong induction lemma NAT_induction, and
carefully controlling the expansion of fib.  I'm including the proof
script below.  I'm not sure what kind of common procedure can be gleaned
from this, nor am I claiming this is the best proof, but I thought you'd
like to see it anyway.

Regards,
Sam Owre

(""
(EXPAND "f")
(EXPAND "^" 1 1)
(EXPAND "expt")
(EXPAND "expt")
(EXPAND "expt")
(INDUCT "n" :NAME "NAT_induction")
(("1" (ASSERT))
("2"
(SKOSIMP)
(EXPAND "fib" +)
(LIFT-IF)
(LIFT-IF)
(ASSERT)
(PROP)
(("1" (HIDE -2) (GRIND)) ("2" (HIDE -2) (GRIND))
("3"
(ASSERT)
(INST-CP -1 "j!1-2")
(ASSERT)
(REPLACE -2)
(ASSERT)
(INST -1 "j!1-1")
(ASSERT)
(REPLACE -1)
(ASSERT)
(EXPAND "fib" 2 2)
(ASSERT)
(REPLACE -2)
(ASSERT)
(EXPAND "fib" 2 5)
(ASSERT)
(CASE-REPLACE "(-1) ^ (j!1 - 2) = (-1) ^ j!1")
(("1"
(ASSERT)
(CASE "(-1) ^ (j!1 - 1) + (-1) ^ j!1 = 0")
(("1" (ASSERT)) ("2" (HIDE-ALL-BUT 1) (GRIND))))
("2" (HIDE-ALL-BUT 1) (GRIND))))))
("3" (GRIND))))

> From:    Silvia Spoletini <sspolet@tin.it>
> Subject: simple problem
> Date:    Fri, 09 Jun 2000 18:50:25 +0200
> To:      pvs-help-request@csl.sri.com
>
> 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
```