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

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