Re: [PVS-Help] Termination TCC

[Sam Owre <owre@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))).]