# Wrong replace allowed (fwd)

```
I posted the followin in the bug list a short while back (bug number 391),
I just wondered if someone has an idea for a way round this problem?

Thanks
Hanne Gottliebsen
---------- Forwarded message ----------
Date: Thu, 25 Nov 1999 16:51:17 +0000 (GMT)
From: Hanne Gottliebsen <hago@dcs.st-andrews.ac.uk>
To: pvs-bugs@csl.sri.com
Subject: Wrong replace allowed

Hi,

I have two lemmas:

(LAMBDA x : g1(x) + g2(x))
= ((LAMBDA x : g1(x)) + (LAMBDA x : g2(x)))

test : LEMMA
f(LAMBDA x : a + x)

In the proof of test, I successively try to apply lambda_add until in _use
followed by replace_ replace fails.

However, replace continues to match.

Example:

PVS(247):
test :

|-------
{1}   FORALL (a: real, f: [[real -> real] -> bool]): f(LAMBDA x: a + x)

By the following (incomplete proof)

(|test| "" (SKOLEM!)
(("" (ASSERT)
(("" (REPLACE -1 1)
(("" (HIDE -1)
(("" (ASSERT)
(("" (REPLACE -1 1) (("" (POSTPONE) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)

we get

test :

[-1]  (LAMBDA (x: real): x + a!1) =
((LAMBDA (x: real): a!1) + (LAMBDA (x: real): x))
|-------
{1}   f!1((((LAMBDA (x: real): a!1) + (LAMBDA (x: real): x)) +
(LAMBDA (x_572: real): x_572)))

So somehow lambda_add has been used to rewrite

lambda x . x+a

to

lambda x . a + lambda x . x + lambda x . x

It looks like the second replace matches lambda x . x+a to lambda x . a

Below is theories needed to run the example.

Thanks,
Hanne Gottliebsen

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Operations on functions : [ T -> real]  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

real_fun_ops  [ T : TYPE ] : THEORY

BEGIN

f1, f2 : VAR [T -> real]

f3 : VAR [T -> nzreal]

a : VAR real

x : VAR T

%------------------------------------------
%  Conversion : real to constant function
% (Already there in PVS2.3 prelude: K_conversion)
%------------------------------------------

%%  const_fun(a) : [T -> real] = LAMBDA x : a

%%  CONVERSION const_fun

%--------------
%  Operations
%--------------

+(f1, f2) : [T -> real] = LAMBDA x : f1(x) + f2(x);

-(f1)     : [T -> real] = LAMBDA x : -f1(x);

*(f1, f2) : [T -> real] = LAMBDA x : f1(x) * f2(x);

*(a, f1)  : [T -> real] = LAMBDA x : a * f1(x);

-(f1, f2) : [T -> real] = LAMBDA x : f1(x) - f2(x);

/(f1, f3) : [T -> real] = LAMBDA x : f1(x) / f3(x);

/(a, f3)  : [T -> real] = LAMBDA x : a / f3(x);

inv(f3) : [T -> real] = 1 / f3;

abs(f1) : [T -> nonneg_real] = LAMBDA x : abs(f1(x));

%------------------
%  Rewrite rules
%------------------

diff_function : PROPOSITION f1 - f2 = f1 + (- f2)

div_function : PROPOSITION f1 / f3 = f1 * (1 /f3)

scal_function : PROPOSITION a * f1 = K_conversion(a) * f1

scaldiv_function : PROPOSITION a / f3 = K_conversion(a) / f3

negneg_function : PROPOSITION - (- f1) = f1

END real_fun_ops

test1 [ T : TYPE FROM real ] : THEORY

BEGIN

IMPORTING real_fun_ops

x : VAR T

g1, g2 : VAR [T -> real]

(LAMBDA x : g1(x) + g2(x)) = ((LAMBDA x : g1(x)) + (LAMBDA x :
g2(x)))

end test1

test2 : THEORY

BEGIN

IMPORTING test1

x, a : VAR real

f : VAR [[real -> real] -> bool]

test : LEMMA
f(LAMBDA x : a + x)

end test2

---------------------------------------------------------
Hanne Gottliebsen		    Office P337
Dept. of Computer Science	    Ph: +44 1334 46 3265
University of St Andrews	    hago@dcs.st-and.ac.uk
- Who moved the stone?
---------------------------------------------------------

```