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

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



Hi,

A minor point: the judgement is not really needed here.  Instead of

    minIndexSet(values): set[Z4] =
     {x: Z4 | FORALL(y: Z4): values(x) <= values(y)}

    index_set_is_non_empty: JUDGEMENT minIndexSet(values) HAS_TYPE (nonempty?[Z4])

You can simply use

    minIndexSet(values): nonempty_set[Z4] =
     {x: Z4 | FORALL(y: Z4): values(x) <= values(y)}

This is more efficient (and I find it more readable), though the results
are essentially the same.

Sam

Stan Rosenberg <stan.rosenberg@xxxxxxxxx> 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
> >