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

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

On Wed, 2005-07-20 at 20:43, Aditya Kanade wrote:
> 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,
> Aditya.
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way                 http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988