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

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

On Fri, Jun 8, 2012 at 9:37 AM, Ben Hocking
<ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> I end up with:
> ======
> {-1}  FORALL (x_1: Z4): NOT (FORALL (y: Z4): values!1(x_1) <= values!1(y))
>  |-------
> Any help in proving that remaining sequent would be appreciated!

You have to show that the range of values has a minimum.  Since the
range is a finite set of reals, you can show that it has a minimum.
Here are the suggested definitions and the supporting lemma:

 s: VAR set[real]
 non_empty_fin?(s): bool = nonempty?(s) and is_finite(s)

 min(s: (non_empty_fin?)): RECURSIVE (s) =
   let a = choose(s)
     if (card(s) = 1) then
       min(a, min(remove(a, s)))
 MEASURE card(s)

 min_is_min: LEMMA forall (s: (non_empty_fin?), x: (s)): min(s) <= x

I can bang out the proofs later in the day in case you get stuck.