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

*To*: Jerome <jerome@xxxxxxxxxxxxxx>, <pvs-help@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] Min value in a set*From*: "Miner, Paul S." <p.s.miner@xxxxxxxx>*Date*: Fri, 21 Mar 2008 06:42:55 -0400*Cc*:*In-reply-to*: <20080320231209.GA10123@cs.caltech.edu>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*Thread-index*: AciLQFIAkKpV/PczEdyqxQAWy4ijyw==*Thread-topic*: [PVS-Help] Min value in a set*User-agent*: Microsoft-Entourage/11.3.6.070618

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 >> >

**References**:**Re: [PVS-Help] Min value in a set***From:*Jerome

- Prev by Date:
**Re: [PVS-Help] Min value in a set** - Next by Date:
**[PVS-Help] Override expressions** - Previous by thread:
**Re: [PVS-Help] Min value in a set** - Next by thread:
**[PVS-Help] Override expressions** - Index(es):