# Re: More questions about predicate subtypes

Hi,

Kellom{ki Pertti writes:
From: Kellom{ki Pertti <pk@cs.tut.fi>
Date: Tue, 24 Apr 2001 15:42:12 +0300 (EET DST)
Subject: 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
doing:

test: THEORY
BEGIN
obj: TYPE+
t: TYPE+
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
END test

f1: [(p) -> int] = LAMBDA (z : (p)) :
let x = proj_1(z),
st = proj_2(z)
in i(x, st) + 1

(BTW the typechecker refuses x = z`1, I submit that as a bug.)

This produces a tcc

% Subtype TCC generated (at line 15, column 14) for  (x, st)
% unfinished
f1_TCC1: OBLIGATION
FORALL (x, z: (p)):
x = pi1(z) IMPLIES (FORALL (st): st = pi2(z) IMPLIES p(x, st));

that can be proved with

;;; Proof for formula test.f1_TCC1
;;; developed with old decision procedures
(""
(SKOLEM-TYPEPRED)
(SKOSIMP*)
(EXPAND "pi1")
(EXPAND "pi2")
(CASE "(x!1, st!1) = z!1")
(("1" (GRIND)) ("2" (GRIND))))

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
not work.

This tcc is unprovable. I guess you hit one of the examples where
pvs 2.3 produces an unprovable tcc due to the change in the tcc
generation with respect to 2.2.

My questions now are:
- Can f_TCC1 be proved?

Only if you exploit a soundness problem.

- Is restricting the last argument using dependent types as in g
completely equivalent to giving the restriction as in the
declaration of f?

I would say yes, but then it should be possible to prove

eq : Lemma (lambda(x: obj, st: (LAMBDA (s: t): p(x, s))) : i(x,st)) = i

but this fails, because of an unprovable tcc. So the answer is
probably no, because the typechecker handles both alternatives
differently.

Bye,

Hendrik

-----------------------------------------------------------------
Hendrik Tews     Department of Theoretical Computer Science
Dresden University of Technology, Germany

Telefon:   	 +49 351 463 8351
e-mail:    	 tews@tcs.inf.tu-dresden.de
www:       	 http://home.pages.de/~tews/
pgp key:         http://home.pages.de/~tews/pgpkey.asc
-----------------------------------------------------------------