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

Re: [PVS-Help] Help trying to prove a trivial lemma



Ben,

I guess that you mean

minIndex(values: AR4): {x: Z4 | FORALL(y: Z4): values(x) <= values(y)}

which is an uninterpreted function returning an element of type

{x: Z4 | FORALL(y: Z4): values(x) <= values(y)}


Otherwise, since the expression {x: Z4 | FORALL(y: Z4): values(x) <=
values(y)} denotes a set, PVS introduces a conversion to a singleton set
and returns an element (the only one) in that set.

In either case, you need to prove some TCCs.

The proof involves (skosimp*)  (typepred "minIndex(values!1)") and (grind).

A minor comment: you can define

Z4 : TYPE = below(4).
 
Cesar


On 6/7/12 2:41 PM, "Ben Hocking" <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>
wrote:

>I have the following PVS code:
>=============================================
>trival: THEORY
> BEGIN
>
> Z4: TYPE = {x: nat | x < 4}    % 0, 1, 2, or 3
>                  
>                  
>             
> AR4: TYPE = [Z4 -> real]       % array of 4 reals
>                  
>                  
>             
>
> minIndex(values: AR4): Z4 =
>  {x: Z4 | FORALL(y: Z4): values(x) <= values(y)}
>
> % The smallest value is no larger than any other value
>                  
>                  
>             
> smallestValueIsSmallest: LEMMA
>  FORALL(x: Z4, values: AR4): values(minIndex(values)) <= values(x)
>
> END trival
>=============================================
>I want to prove the smallestValueIsSmallest lemma. I've tried
>(model-check) and (grind), but they don't get me very far.
>
>Thanks,
>-Ben
>