[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Explicating dependent types
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.
R:type = [# s:set[T], f:set[[(s),(s)]] #]
forall (r:R): forall (p,q:T): r`f(p,q) implies r`s(p) and r`(q)
How does one explicate the dependent typing information?