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

*To*: pvs-help@csl.sri.com*Subject*: Re: need helps!!!*From*: Holger Pfeifer <pfeifer@ares.informatik.uni-ulm.de>*Date*: Thu, 20 Mar 2003 11:18:13 +0100*Organization*: =?iso-8859-15?q?Universit=E4t?= Ulm*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: KMail/1.4.3

In response to Kun's question. I forgot to CC: the list. - Holger ---------- Forwarded Message ---------- Subject: Re: need helps!!! Date: Thu, 20 Mar 2003 11:12:47 +0100 From: Holger Pfeifer <pfeifer@ki.informatik.uni-ulm.de> To: "Kun Wei" <k.wei@eim.surrey.ac.uk> Kun, > odd_nat?(i):bool=exists j: i=2*j+1 > odd_nat:TYPE=(odd_nat?) > > division_4:THEOREM > (FORALL x:odd_nat:(exists y:nat: (x+1)*(x+1)=4*y)) > > Ok, I use "induct "x"" to prove this theorem. [...] I got the > problems in the third subgoal. Because the induction method is we > assume the j is right,then we reason (j+1) is right also. but in > this case, I was dealing with odd number, the increment is two When starting an induction proof, PVS selects an induction scheme according to the type of the induction variable you provide. But you may also choose a different induction scheme if PVS' choice does not work. Use the :name keyword to the (INDUCT "x") command, such as in (INDUCT "x" :name "<name_of_induction_scheme>") See the PVS prelude file (M-x vpf) for various other induction schemes. In your case, you might want to try the strong version of induction over naturals, "NAT_induction": (INDUCT "x" :name "NAT_induction") This strong version, NAT_induction: LEMMA (FORALL j: (FORALL k: k < j IMPLIES p(k)) IMPLIES p(j)) IMPLIES (FORALL i: p(i)) allows you to instantiate the induction hypothesis with any number less than j, so that you can derive the property for j from the assumption that it holds for j-2. However, proving your theorem by induction seems a little overdone. For odd x, the task is to find y such that (2*j+1+1)*(2*j+1+1)=4*y The left-hand side rewrites to 2*(j+1) * 2*(j+1) and thus y = (j+1)^2 does the job. In PVS, you need to use the (TYPEPRED) command to make the type definition of x explicit; here's the complete proof script: (skosimp*) (typepred "x!1") (expand "odd_nat?") (skosimp*) (inst + "(j!1+1)^2") (grind) Regards, - Holger -------------------------------------------------------

- Prev by Date:
**need helps!!!** - Next by Date:
**Assembly program verification in PVS** - Prev by thread:
**need helps!!!** - Next by thread:
**Strange error in loading a theory** - Index(es):