[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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_add : LEMMA
      (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!)
  (("" (USE "lambda_add[real]")
    (("" (ASSERT)
      (("" (REPLACE -1 1)
        (("" (HIDE -1)
          (("" (USE "lambda_add[real]")
            (("" (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_add : LEMMA
	(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?
---------------------------------------------------------