[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] measure induction
I've corrected the theory so that it typechecks.
th[N: posnat]: THEORY
i, j : var below[N]
f: var [below[N]-> nonneg_real]
r: VAR nonneg_real
maxf(f,r)(i): recursive nonneg_real =
if i = N-1 then max(f(i),r) else maxf(f,max(f(i),r))(i+1) endif
measure N - i
max_test: conjecture (j<= i OR f(i)<= r) => f(i) <= maxf(f,r)(j)
Note that you have to generalize the statement replacing parameters
like 0 with variables in order for the induction to work.
Once you do this, it is proved using
(measure-induct-and-simplify "N-j" ("j") :expand "maxf")
> I have a sample theory:
> th[N: posnat]
> i : var below[N]
> f: var [below[N]-> noneg_real]
> maxf(f,r: nonneg_real)(i): recursive noneg_real =
> if i = N then max(f(i),r) else maxf(f,max(f(i),r))(i+1) endif
> measure N - i
> max_test: conjecture f(i) <= maxf(f,0)(0)
> end th
> I think the conjecture "max_test" must hold on, but how can I prove it?
> I generalize the parameter "N" and (induct "N"), but the subgoal require me to prove
> f(i) <= maxf(f,f(0))(1).
> If I give the concrete parameter, for instance 3, to instance "N", and the max_test can be proved using (grind).
> thanks you in advance.