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

*To*: pvs-help@csl.sri.com*From*: Sam Owre <owre@csl.sri.com>*Date*: Tue, 13 Jun 2000 22:57:15 -0700*cc*: pvs-help@csl.sri.com*Delivery-Date*: Tue Jun 13 22:57:20 2000*In-reply-to*: Your message of "Tue, 13 Jun 2000 21:22:30 +0200." <73b12622.262273b1@mail3-srv.jumpy.it>

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.

**References**:**No Subject***From:*"Michele Rendine" <mirendi@jumpy.it>

- Prev by Date:
**No Subject** - Next by Date:
**No Subject** - Prev by thread:
**No Subject** - Next by thread:
**No Subject** - Index(es):