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

Re: need helps!!!

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>


>  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


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:

 (typepred "x!1")
 (expand "odd_nat?")
 (inst + "(j!1+1)^2")


	- Holger