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

*To*: pvs-help@csl.sri.com*Subject*: simple problem*From*: Silvia Spoletini <sspolet@tin.it>*Date*: Fri, 09 Jun 2000 18:50:25 +0200*Delivery-Date*: Fri Jun 9 05:48:45 2000

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

- Prev by Date:
**Question on strategies** - Next by Date:
**Re: simple problem** - Prev by thread:
**Re: How understanding better pvs through some examples?** - Next by thread:
**Re: simple problem** - Index(es):