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

```Thank you for your advice.

Using Stan's trick of:
======
index_set_is_non_empty: JUDGEMENT minIndexSet(values) HAS_TYPE (nonempty?[Z4])
======

Allowed me to prove my original lemma with:
(skosimp)(expand "minIndex")(typepred "choose(minIndexSet(values!1))")(expand minIndexSet -2 1)(inst -2 "x!1")

Unfortunately, when I try to prove the TCC that the judgment generates using:
(skosimp)(expand "minIndex")(expand "nonempty?")(expand "empty?")(expand "member")
I end up with:
======
{-1}  FORALL (x_1: Z4): NOT (FORALL (y: Z4): values!1(x_1) <= values!1(y))
|-------
======
This being logically equivalent to:
======
{-1}  FORALL (x_1: Z4): EXISTS (y: Z4): values!1(x_1) > values!1(y)
|-------
======
Since the antecedent is obviously false when x_1 is the smallest value in "values!1" (assuming reals cannot be infinite, and I have tried the same logic after confining the reals to the range (-1000, 1000)), this statement is clearly true, but I don't know how to convince PVS of it.

I tried using:
(inst -1 "choose(minIndexSet(values!1))")
However, not surprisingly, that leads me into an infinite loop, as I once again have to prove "nonempty?[Z4](minIndexSet(values!1))".

Any help in proving that remaining sequent would be appreciated!

Thanks,
-Ben

On Jun 7, 2012, at 5:49 PM, MUNOZ, CESAR (LARC-D320) wrote:

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

```