# Re: Type-correctness conditions in HOL

```Joe Hurd writes:
From: Joe Hurd <Joe.Hurd@cl.cam.ac.uk>
Date: Wed, 02 Aug 2000 17:45:44 +0100
Subject: Type-correctness conditions in HOL

term_TCC1: OBLIGATION FORALL (x : A) : P(x);

Which may well be false. Can this `too-strong' TCC cause any problems
in PVS?

In principle yes. It might be, that you can't complete
the proof chain for a theorem because of an unprovable TCC
although the theorem itself is true. This happend to me serveral
times. But compared to the cases where I got unprovable TCC's
because my theories were wrong, it is negligible.

In my opinion it is reasonable to expect that the user provides
enough context information for the generation of the TCC's. In
your example the user should write

term1 : bool = EXISTS (x : A) : P(x) and (LAMBDA (y : (P)) : TRUE)( x )

A second example where unprovable TCC's are generated, because
the user provides wrong information is the following:

t1 : bool = Forall( n : nat ) : 10 >= 10 / n or n = 0

PVS generated the unprovable TCC n /= 0. But I think it is
reasonable to expect the user to write instead

t2 : bool = Forall( n : nat ) : n = 0 or 10 >= 10 / n

and for t2 PVS does not generate a TCC.

I think it is more interesting to look at cases, where PVS
generates unprovable TCC's, although all the relevant information
is available. Consider

Prop : Theory
Begin
f : Var [nat -> [nat -> nat]]

prop?(f) : bool = f(0)(0) < f(1)(1)

g : [int -> [int -> int]] = lambda(m : int) : Lambda(n:int) : m + n + 4

g_prop : Lemma prop?(g)
end Prop

Here PVS generates the unprovable TCC

% Subtype TCC generated (at line 13, column 23) for  restrict(g)
% untried
g_prop_TCC1: OBLIGATION
FORALL (x1: nat):
(FORALL (x: int): x >= 0) AND
(FORALL (x2: int): restrict[int, nat, [int -> int]](g)(x1)(x2) >= 0);

although from the type information it is clear, that

FORALL (x: nat):
(FORALL (y: nat): g(x)(y) >= 0);

would be sufficient to ensure soundness.

Bye,

Hendrik

-----------------------------------------------------------------
Hendrik Tews     PhD student  in theoretical computer science
at 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
-----------------------------------------------------------------

```

References: