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

No Subject

Michele,

I did the proof with the following script:

(""
 (INDUCT-AND-SIMPLIFY "x" :DEFS NIL)
 (("1"
   (EXPAND "fatt" +)
   (EXPAND "doublefatt" 1 1)
   (LIFT-IF)
   (PROP)
   (("1" (GRIND)) ("2" (GRIND))))
  ("2" (GRIND))))

I first tried to use (INDUCT-AND-SIMPLFY "x") which frequently works, but
in this case the prover gets into an infinite loop (I used C-c C-c to
interrupt it, and (restore) to get back to the previous proof state).
I then used :DEFS NIL to inhibit definition expansion, so that I could
control it directly.

Hope this helps
Sam Owre

> From:    "Michele Rendine" <mirendi@jumpy.it>
> Date:    Tue, 13 Jun 2000 21:22:30 +0200
> To:      pvs-help@csl.sri.com
> 
> I’m having problems with PVS : I’ve defined a recursive function, 
> called “doublefatt”, in this way :
> 
> doublefatt(x) : RECURSIVE posnat =
> 	      IF x=0 THEN 1
> 	      ELSIF x=1 THEN 1
> 	      ELSE x*doublefatt(x-2)
> 	      ENDIF
> MEASURE x
> 
> Then, I’ve defined also the factorial and I’ve tried to prove the 
> following property :
> 
> prop : THEOREM  FORALL ( x : posnat) : x>0 IMPLIES fatt(x) =  
>        doublefatt(x)*doublefatt(x-1)
>  
> The demonstration of this property is very simple if we use an 
> inductive approach :
> 
> Base : 1! = 1!*0!   TRUE
> 
> Inductive Hp : " m<n   m! = m!!*(m-1)!!
> 
> Then : n! = n* (n-1)! = n*(n-1)!!*(n-2)!! = (n-1)!!*n*(n-2)!! = (n-1)!!
> *n!!
> 
> How is possible to obtain the same result with PVS ?
> Does it exists a standard way to obtain inductive proves? 
> Thank you for your attenction.