• To: pvs@csl.sri.com
• Subject: inst? and overloaded operators
• From: Pertti Kellomäki <pk@cs.tut.fi>
• Date: Thu, 17 Apr 2003 15:26:48 +0300
• Sender: pvs-owner@csl.sri.com
• User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.1) Gecko/20021003

```Hi all,

I ran into the following problem in a proof. Consider the
following theories:

intval : DATATYPE
BEGIN
intval(v : int) : intval?
END intval

intval_test : THEORY
BEGIN
IMPORTING intval

intval_peeling : lemma
injective?(intval) =>
forall (f : [[int,int] -> int]) :
forall (i1, i2, i3, i4 : int) :
intval(i1) = intval(i2) and intval(i3) = intval(i4)
=> intval(f(i1,i3)) = intval(f(i2,i4))

intval_plus_peeling : lemma
injective?(intval) =>
forall (i1, i2, i3, i4 : int) :
intval(i1) = intval(i2) and intval(i3) = intval(i4)
=> intval(i1+i3) = intval(i2+i4)
END intval_test

First the simple question: is there a direct way to
say in the datatype declaration that I want intval(X)=intval(Y)
to imply X=Y? It does not appear to be the case now.

My longer question concerns instantiation.
Clearly I can use intval_peeling as a lemma when proving
intval_plus_peeling. If I do instantiation by hand in the
proof, e.g. do (inst -1 "+" "i1!1" "i2!1" "i3!1" "i4!1"),
then everything works fine. However, if I let PVS do
instantiation with inst?, it produces two branches, one of
which is the unprovable subgoal

[-1]  injective?(intval)
[-2]  intval(i1!1) = intval(i2!1)
[-3]  intval(i3!1) = intval(i4!1)
|-------
{1}   ((FORALL (x: numfield):
real_pred(x) AND rational_pred(x) AND integer_pred(x))
AND
(FORALL (x: numfield):
real_pred(x) AND rational_pred(x) AND integer_pred(x)))
AND
(FORALL (x1: [numfield, numfield]):
real_pred(+(x1)) AND rational_pred(+(x1))
AND integer_pred(+(x1)))
[2]   intval(i1!1 + i3!1) = intval(i2!1 + i4!1)

Is there a way around this or do I just have to instantiate
manually?

Thanks.
--
pertti

```