[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 
 BEGIN
     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)

   END th 

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")

-Shankar

>      I have a sample theory:
> 
>   th[N: posnat]
>  begin
>      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.