[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
More questions about predicate subtypes
I have some more questions about predicate subtypes. What I am trying
to do is to use predicate subtypes to constrain more than one argument
of a function. The following theory hopefully illustrates what I am
p: [obj, t -> bool]
i: [(p) -> int]
f: [(p) -> int] = LAMBDA (x: obj, st: t): i(x, st) + 1
g(x: obj, st: (LAMBDA (s: t): p(x, s))): int = i(x, st) + 1
I am trying to express a function of type [(p) -> int]. I would prefer
the form in which f is written, but I get a TCC
f_TCC1: OBLIGATION FORALL (st: t, x: obj): p(x, st);
and I do not know how to get to the type information that says that
p(x,st) is true. Skolemizing and doing (typepred "(x!1, st!1)") does
For g I get the TCC
g_TCC1: OBLIGATION FORALL (x: obj, st: (LAMBDA (s: t): p(x, s))): p(x, st);
which is provable.
My questions now are:
- Can f_TCC1 be proved?
- Is restricting the last argument using dependent types as in g
completely equivalent to giving the restriction as in the
declaration of f?