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

Re: [PVS-Help] Termination TCC

On Tue, Apr 22, 2008 at 6:24 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
I have the following recursive definition:

 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)))
 MEASURE card(I)
END example

When I go to typecheck it, one of the TCC's it gives me is the

 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.

You need to supply the type parameter to the theory.  Try

(lemma "card_remove[index]")
[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))).]

Look at the finite_sets library.  In particular, finite_sets_sum seems to be pretty close to what you are looking for.
Jerry James