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

Re: [PVS-Help] Min value in a set



Jerome,

If you look at the definition of min in finite_sets@finite_sets_minmax you
will see:

  min(SS): {a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}

This is an uninterpreted function.  There is nothing for PVS to expand.

You may use (typepred "min(J!1)") and (typepred "min(K!1)) to get at the
predicate subtype constraining the range of min for each instance in your
sequent.  Alternatively, you could invoke (lemma "min_lem") to bring this
explicit property into your sequent.  "min_lem" is declared in
finite_sets@finite_sets_minmax:

  min_lem: LEMMA (min(SS) = a IFF
                  SS(a) AND (FORALL (x: (SS)): a <= x))

However, even using min_lem you will still be unable to prove your
conjecture min_constant.  It is not true.  There is nothing to force two
arbitrary finite sets of posnat to have the same min.  Consider the two
singleton sets "{1}" and "{2}".  min({1}) = 1 /= 2 = min({2}).

Furthermore, you also will be unable to prove the type correctness
conditions generated for lemma min_constant.  You will not be able to prove
that every finite set over the posnats is nonempty.

Regards,
Paul Miner

On 3/20/08 7:12 PM, "Jerome" <jerome@xxxxxxxxxxxxxx> wrote:

> I'm having trouble expanding 'min' (over a set) within my proof. To
> illustrate, take the following theory:
> 
>   local: THEORY BEGIN
>     natarray: TYPE = [posnat -> nat]
>     indices:  TYPE = finite_set[posnat]
> 
>     min_constant: LEMMA FORALL (J, K: indices): min(J) = min(K)
>   END local
> 
> When trying to prove 'min_constant', after skolemizing, I'd like to
> expand 'min', but I can't:
> 
>   {1}   min(J!1) = min(K!1)
> 
>   Rule? (expand "min")
>   No change on: (EXPAND "min")
>   min_constant :
> 
>     |-------
>   {1}   min(J!1) = min(K!1)
> 
> 
> Why can't I perform the expansion? Even if I explicitly import
> 'finite_sets@finite_sets_minmax' in my theory, I get the same results.
> 
> jerome
> 
> On Wed, Mar 12, 2008 at 07:09:32AM -0500, Butler, Ricky W. (LARC-D320) wrote:
>> Jerome,
>>   It distinguishes between them on the basis of the number of
>> arguments.  Since both are in prelude, no IMPORTING statements are
>> needed.
>> 
>> Note. See theory "finite_sets_minmax" in the "finite_sets" library for
>> a more general min/max over sets.
>>      This can be located in the lib subdirectory of your installation
>> directory.  It is imported as follows
>> 
>>       IMPORTING finite_sets@finite_sets_minmax
>> 
>> The NASA libraries provide min and max over sets over a bounded domain.
>> 
>>       IMPORTING reals@bounded_reals
>> 
>> See http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
>> for information about how to install these.
>> 
>> Rick
>> 
>>> -----Original Message-----
>>> From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
>> [mailto:pvs-
>>> help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf Of Jerome
>>> Sent: Tuesday, March 11, 2008 8:03 PM
>>> To: pvs-help@xxxxxxxxxxx
>>> Subject: [PVS-Help] Min value in a set
>>> 
>>> I would like to use both 'min' operations in the prelude: min over a
>>> set and min of two values - how do I do it? In the former, I think the
>>> min found in 'min_nat' would do the trick, but I'm not sure how to
>>> access it. PVS always seems to think I want the min within 'real_defs'
>>> (which I do, for the latter).
>>> 
>>> jerome
>> 
>