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

[PVS-Help] Judgements Over Dependent Types



Hi,

(I am not subscribed to the list, so please keep me on CC)

I am trying out PVS for the first time and, while trying to formalize some things involving dependent types, I came across a more complicated version of the following problem:

Consider a set S, a function f : S -> below[k] and a function allNotJ that, given S, k, f and some posnat j below k, returns the set of all elements of S whose value under f is not j (i.e., returns S \ f^{-1}(j)).

It is obvious from those definitions that the restriction of f to the subset of S returned by allNotJ(S, k, f, k - 1) is a function of type [(allNotJ(S, k, f, k - 1)) -> below[k - 1]].

Is there a way to express this via type judgements? I tried in the attached file, but I have all sort of problems with these dependent types. If somebody could shed some light or suggest a different approach, that would be very appreciated.

Thanks in advance for your help.

David E. Narvaez

Attachment: minimal.pvs
Description: Binary data