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

[PVS-Help] Re: Induction hypothesis vs. specification



Ingo,

> mult: THEORY
>   BEGIN
>     x, y, z: VAR nat
>
>     mult(x, y, z): RECURSIVE nat =
>       IF y = 0 THEN z ELSE mult(x, y - 1, z + x) ENDIF
>     MEASURE y
>
>     mult_ok: LEMMA FORALL (x, y): mult(x, y, 0) = x * y
>     mult_ok2: LEMMA FORALL (x, y, z): mult(x, y, z) = x * y + z
>
>   END mult

> I wonder if it is possible to prove "mult_ok".

Well, obviously mult_ok follows directly from mult_ok2 (with z = 0),
so if you change the order of the two lemmas you could use mult_ok2
to REWRITE your goal. But I guess that's not what your question was
about.

In a proof by induction of mult_ok you'd probably need to strengthen
the induction hypothesis. One way to do this is to use some other
property of mult in the induction step. One such property is

	mult(x, y, z+c) = mult(x,y,c) + z

which itself can be proved very easily in a simple proof by
induction - (induct-and-simplify "y") does the job.

Then the induction step of mult_ok can be accomplished using the sequence

   (skosimp*)
   (expand "mult" 1)
   (rewrite "mult_add" :subst ("c" 0 "z" "x!1"))
   (inst?)
   (assert)

Kind regards,

	- Holger