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

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