[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
I did the proof with the following script:
(INDUCT-AND-SIMPLIFY "x" :DEFS NIL)
(EXPAND "fatt" +)
(EXPAND "doublefatt" 1 1)
(("1" (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
> From: "Michele Rendine" <email@example.com>
> Date: Tue, 13 Jun 2000 21:22:30 +0200
> To: firstname.lastname@example.org
> 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)
> 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) =
> 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)!!
> 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.
- No Subject
- From: "Michele Rendine" <email@example.com>