# Re: [PVS-Help] Explicating dependent types

```Aditya,
This is a well-known behavior of sets in PVS. The type set[T] is just
the type of functions [T->bool] (the characteristic function).
Therefore, when you declare f:set[[(s),(s)]] you are really declaring
f:[[(s),(s)]->bool]. Hence, PVS expects the arguments of f to be of type
(s). For this reason, it generates the TCCs.

To avoid this "unexpected" behavior, it is a good idea to declare sets
on the super-type, rather than on the sub-type. In your case, the type
that you want to declare is:

R: TYPE = {r: [# s: set[T], f:set[[T,T]] #] |
FORALL (x,y:T): r`f(x,y) IMPLIES r`s(x) AND r`s(y)}

l : LEMMA
forall (r:R):forall(p,q:T): r`f(q,q) implies r`s(p) and r`s(q)

No TCCs are generated and the lemma l is trivial.

Cesar

> Hi,
>
> Suppose we define a record consisting of a set 's' and a set 'f' over
> pairs of elements from the set. If a pair (p,q) belongs to f then
> clearly p and  q should belong to s by the dependent typing. I encouter
> a similar kind of proof goal which I'm not able to prove. 'typepred'
> does not change state of the proof goal. Below I'm giving a small
> example theory capturing essence of the problem. The lemma 'l' below
> could not be proven. Rather, PVS generates a TCC saying p and q should
> be of the type r`s.
>
> TH:theory
> begin
> T:type
>
> R:type = [# s:set[T], f:set[[(s),(s)]] #]
>
> l:lemma
> forall (r:R): forall (p,q:T): r`f(p,q) implies r`s(p) and r`(q)
>
> end TH
>
> How does one explicate the dependent typing information?
>
> Regard,