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

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



Thanks. I definitely understand the mistake I made with the possibility of there being more than one min index. I'm couldn't figure out how to prove what should be trivial - that there's at least one element that's not larger than any other.

Thanks,
-Ben

On Jun 7, 2012, at 5:11 PM, Stan Rosenberg wrote:

> Hi Ben,
> 
> I am attaching a dump file with a proof of your lemma and a couple of
> modifications to the theory.  Your definition of minIndex is not quite
> correct; there could be
> more than one "min" index. E.g., all array elements are the same.
> Instead, I would define it like so using Hilbert's choice function:
> 
> minIndexSet(values): set[Z4] =
>  {x: Z4 | FORALL(y: Z4): values(x) <= values(y)}
> 
> minIndex(values: AR4): Z4 = choose(minIndexSet(values))
> 
> I would also add the following type judgement which helps simplify the
> lemma proof:
> 
> index_set_is_non_empty: JUDGEMENT minIndexSet(values) HAS_TYPE (nonempty?[Z4])
> 
> I left the TCC, i.e., showing non-emptiness for you as exercise. Let
> me know if you need help with it.
> 
> Best,
> 
> stan
> 
> On Thu, Jun 7, 2012 at 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
>> 
> <trivial.dump>