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

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



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
>

Attachment: trivial.dump
Description: Binary data