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

*To*: "MUNOZ, CESAR (LARC-D320)" <cesar.a.munoz@xxxxxxxx>*Subject*: Re: [PVS-Help] Help trying to prove a trivial lemma*From*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Date*: Fri, 8 Jun 2012 09:37:14 -0400*Cc*: "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>*In-reply-to*: <CBF69893.30BA%cesar.a.munoz@nasa.gov>*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>*References*: <CBF69893.30BA%cesar.a.munoz@nasa.gov>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Thank you for your advice. Using Stan's trick of: ====== index_set_is_non_empty: JUDGEMENT minIndexSet(values) HAS_TYPE (nonempty?[Z4]) ====== Allowed me to prove my original lemma with: (skosimp)(expand "minIndex")(typepred "choose(minIndexSet(values!1))")(expand minIndexSet -2 1)(inst -2 "x!1") Unfortunately, when I try to prove the TCC that the judgment generates using: (skosimp)(expand "minIndex")(expand "nonempty?")(expand "empty?")(expand "member") I end up with: ====== {-1} FORALL (x_1: Z4): NOT (FORALL (y: Z4): values!1(x_1) <= values!1(y)) |------- ====== This being logically equivalent to: ====== {-1} FORALL (x_1: Z4): EXISTS (y: Z4): values!1(x_1) > values!1(y) |------- ====== Since the antecedent is obviously false when x_1 is the smallest value in "values!1" (assuming reals cannot be infinite, and I have tried the same logic after confining the reals to the range (-1000, 1000)), this statement is clearly true, but I don't know how to convince PVS of it. I tried using: (inst -1 "choose(minIndexSet(values!1))") However, not surprisingly, that leads me into an infinite loop, as I once again have to prove "nonempty?[Z4](minIndexSet(values!1))". Any help in proving that remaining sequent would be appreciated! Thanks, -Ben On Jun 7, 2012, at 5:49 PM, MUNOZ, CESAR (LARC-D320) wrote: > Ben, > > I guess that you mean > > minIndex(values: AR4): {x: Z4 | FORALL(y: Z4): values(x) <= values(y)} > > which is an uninterpreted function returning an element of type > > {x: Z4 | FORALL(y: Z4): values(x) <= values(y)} > > > Otherwise, since the expression {x: Z4 | FORALL(y: Z4): values(x) <= > values(y)} denotes a set, PVS introduces a conversion to a singleton set > and returns an element (the only one) in that set. > > In either case, you need to prove some TCCs. > > The proof involves (skosimp*) (typepred "minIndex(values!1)") and (grind). > > A minor comment: you can define > > Z4 : TYPE = below(4). > > Cesar > > > On 6/7/12 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 >> > >

**Follow-Ups**:**Re: [PVS-Help] Help trying to prove a trivial lemma***From:*Stan Rosenberg

**References**:**Re: [PVS-Help] Help trying to prove a trivial lemma***From:*MUNOZ, CESAR (LARC-D320)

- Prev by Date:
**Re: [PVS-Help] Help trying to prove a trivial lemma** - Next by Date:
**Re: [PVS-Help] Help trying to prove a trivial lemma** - Previous by thread:
**Re: [PVS-Help] Help trying to prove a trivial lemma** - Next by thread:
**Re: [PVS-Help] Help trying to prove a trivial lemma** - Index(es):