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

*To*: Jerome <jerome@xxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] Termination TCC*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Fri, 25 Apr 2008 15:18:15 -0700*Cc*: pvs-help@xxxxxxxxxxx*Comments*: In-reply-to Jerome <jerome@cs.caltech.edu> message dated "Tue, 22 Apr 2008 17:24:24 -0700."*In-reply-to*: <20080423002424.GB7342@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>*References*: <20080423002424.GB7342@cs.caltech.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Jerome, Jerry James already answered your question, but I thought I'd expand on it a little. The first TCC you're getting is because choose expects a nonempty set. It looks to me like you're trying to satisfy this with the TYPE+, but this just says the type is nonempty, which it is, of course, as it contains the empty set. I think what you really want there is indices: TYPE = non_empty_finite_set[index] Which leads to a provable TCC There is a min defined in the prelude theory min_nat that works over sets, and hence finite sets. It is defined as min(S): {a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)} Note that this function is not defined - the type information is all that is needed. You use the 'typepred' command to make use of the property in proofs. If you want max over finite_sets, that is defined in the finite_sets library finite_sets_minmax, which you can access using IMPORTING finite_sets@finite_sets_minmax Regards, Sam Jerome <jerome@xxxxxxxxxxxxxx> wrote: > All, > I have the following recursive definition: > > example: THEORY BEGIN > index: TYPE = posnat > value: TYPE = real > indices: TYPE+ = finite_set[index] > myset: TYPE = [index -> value] > fun: TYPE = FUNCTION[value, value -> value] > > curry(f: fun, m: myset, I: indices): RECURSIVE value = > LET i: index = choose(I) IN > IF singleton?(I) THEN m(i) > ELSE f(m(i), curry(f, m, remove(i, I))) > ENDIF > MEASURE card(I) > END example > > When I go to typecheck it, one of the TCC's it gives me is the > following: > > curry_TCC2: OBLIGATION > FORALL (I: indices, i: index): > NOT singleton?(I) AND i = choose(I) IMPLIES > card[index](remove[index](i, I)) < card[index](I); > > Why isn't this proved with the "card_remove" theorem from the prelude? > I've tried to prove the obligation by hand, and bring in card_remove > manually, but PVS doesn't seem to know about it: > > Rule? (lemma "card_remove") > Found 0 resolutions for card_remove relative to the substitution. > > Any insight would be appreciated. > > jerome > > [Also, if anyone knows of a better way to apply a binary function over > a set of values please speak up. For example, given the set {a, b, c, > d}, I'd like to return min(a, min(b, min(c, d))).]

**References**:**[PVS-Help] Termination TCC***From:*Jerome

- Prev by Date:
**Re: [PVS-Help] Termination TCC** - Next by Date:
**Re: [PVS-Help] Termination TCC** - Previous by thread:
**Re: [PVS-Help] Termination TCC** - Next by thread:
**Re: [PVS-Help] Expected type TCC** - Index(es):