# type vs. set

```I am having difficulties proving a particular TCC, and as far as I can see
my problem comes from not being able to deduce from (fullset[T])(u) that
T_pred(u) is true.

I am using PVS2.3

Here is an example:

notation : THEORY

BEGIN

x, y, z : VAR real

T : VAR set[real]

closed_interval(x,y) : set[real] = { z : real | x <= z AND z <= y }

compact_interval_subset?(x,y,T) : bool =
x <= y AND subset?(closed_interval(x,y),T)

END notation

test[ T : NONEMPTY_TYPE FROM real ] : THEORY

BEGIN

IMPORTING notation

R((f:[T -> real]), (c:T), (d: {x:T | compact_interval_subset?(c,x,fullset[T])} ))
: [(closed_interval(c,d)) -> real] = LAMBDA (u : (closed_interval(c,d))) : f(u)

END test

To explain: R is the restriction of f to a compact (closed and
bounded) interval, which is also a subset of fullset[T].

The generated TCC is:

R_TCC1: OBLIGATION
FORALL (c: T, d: {x: T | compact_interval_subset?(c, x, fullset[T])},
u: (closed_interval(c, d))):
T_pred(u);

This is a reasonable TCC, and it is obviously true (once one unfolds the
definitions!).

Using grind gives this:

{-1}  T_pred(c!1)
{-2}  T_pred(d!1)
{-3}  c!1 <= d!1
{-4}  c!1 <= u!1
{-5}  u!1 <= d!1
|-------
{1}   T_pred(u!1)

which looks hopeless to me.

By hand one can easily get to:

[-1]  T_pred(c!1)
[-2]  T_pred(d!1)
[-3]  c!1 <= d!1
{-4}  member(u!1, closed_interval(c!1, d!1)) => member(u!1, fullset[T])
[-5]  closed_interval(c!1, d!1)(u!1)
|-------
[1]   T_pred(u!1)

However, any further expansion only leads to the same result as grind
above (not a big surprise, I guess).

Now, can I actually prove this TCC, or can I change my definition of R to
something equivalent which will work?

Thanks,
Hanne
---------------------------------------------------------
Hanne Gottliebsen		    Office P337
Dept. of Computer Science	    Ph: +44 1334 46 3265
University of St Andrews	    hago@dcs.st-and.ac.uk
- Who moved the stone?
---------------------------------------------------------

```