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

*To*: stan.rosenberg@xxxxxxxxx*Subject*: Re: [PVS-Help] Help trying to prove a trivial lemma*From*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Date*: Thu, 7 Jun 2012 17:27:36 -0400*Cc*: pvs-help@xxxxxxxxxxx*In-reply-to*: <CABvsF6vamS9WwjBJW-PFiYQP0aFUcQ9s0fBVtcWxo_2r_amKsQ@mail.gmail.com>*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*: <4D133916-5509-45CD-BCC7-65A987592190@dependablecomputing.com> <CABvsF6vamS9WwjBJW-PFiYQP0aFUcQ9s0fBVtcWxo_2r_amKsQ@mail.gmail.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Thanks. I definitely understand the mistake I made with the possibility of there being more than one min index. I'm couldn't figure out how to prove what should be trivial - that there's at least one element that's not larger than any other. Thanks, -Ben On Jun 7, 2012, at 5:11 PM, Stan Rosenberg 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 >> > <trivial.dump>

**References**:**[PVS-Help] Help trying to prove a trivial lemma***From:*Ben Hocking

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

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