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

What have I missed ? (a proof failed)



Shalom PVS People,

Here is a simple example of a stack, based on your tutorials,
which I fail to prove a simple CONJECTURE.
I was sure missing a simple method, while looking at the documentation/HELP etc.
but I cannot figure out what it was.

Thanks in advance
Yechiel
--------------------------------------------------------------------------------

			     Happy Independence Day
			    Israel is 50 years young

			    TIME cannot be saved !!!
	You can either borrow it - and PAY high interest in return,
		or     invest it - and GET high interest in return.

	Yechiel M. Kimchi			yechiel@cs.technion.ac.il
	Faculty Comp. Sc.			The Technion, Haifa, 32000 IL
	Office: (04) 829 4333			FAX: +(972) 4 822 1128	
	Homepage: http://www.cs.technion.ac.il/users/yechiel/
--------------------------------------------------------------------------------


Here is the problem (the full theory is enclosed below):

I want to prove

	push_pop : CONJECTURE  pop(push(x, s)) = s

where, on top of the definitions I have an AXIOM

    equal_ax : AXIOM
		(FORALL s, st : (size(s) = size(st) AND (FORALL i:
			(i < size(s) => lmnts(s)(i) = lmnts(st)(i))))
			IMPLIES s = st)

Here how the proof goes:

push_pop :  

  |-------
{1}    (FORALL (s: stack, x: T): pop(push(x, s)) = s)

Rule? (grind :theories("stack_0"))
Date is Wed May 6 07:48:03 IDT 1998	;;  It activates my .cshrc :-]

size rewrites size(s)
  to  PROJ_1(s)
lmnts rewrites lmnts(s)
  to  PROJ_2(s)
push rewrites push(x, s)
  to  (1 + PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
size rewrites size(1 + PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
  to  1 + PROJ_1(s)
lmnts rewrites lmnts(1 + PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
  to  PROJ_2(s) WITH [(PROJ_1(s)) := x]
pop rewrites pop(1 + PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
  to  (PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
size rewrites size(PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
  to  PROJ_1(s)
lmnts rewrites lmnts(PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
  to  PROJ_2(s) WITH [(PROJ_1(s)) := x]
size rewrites size(PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
  to  PROJ_1(s)
size rewrites size(s)
  to  PROJ_1(s)
lmnts rewrites lmnts(PROJ_1(s), PROJ_2(s) WITH [(PROJ_1(s)) := x])
  to  PROJ_2(s) WITH [(PROJ_1(s)) := x]
lmnts rewrites lmnts(s)
  to  PROJ_2(s)
Date is Wed May 6 07:48:07 IDT 1998	;; It activates my .cshrc again

size rewrites size(PROJ_1(s!1), PROJ_2(s!1) WITH [(PROJ_1(s!1)) := x!1])
  to  PROJ_1(s!1)
size rewrites size(s!1)
  to  PROJ_1(s!1)
lmnts rewrites lmnts(PROJ_1(s!1), PROJ_2(s!1) WITH [(PROJ_1(s!1)) := x!1])
  to  PROJ_2(s!1) WITH [(PROJ_1(s!1)) := x!1]
lmnts rewrites lmnts(s!1)
  to  PROJ_2(s!1)
Date is Wed May 6 07:48:09 IDT 1998	;; Twice more

Date is Wed May 6 07:48:10 IDT 1998

Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to: 
push_pop :  

  |-------
{1}    (PROJ_1(s!1), PROJ_2(s!1) WITH [(PROJ_1(s!1)) := x!1]) = s!1

Rule? 

It seems that a direct application of the AXIOM (equal_ax) suffices
and should be done automatically (since I asked (grind :theories("stack_0"))).
But it did not, and neither I found a command that will direct
the prover to using it.

What did I do wrong ?


--------------------------------------------------------------------------------
Here is the full theory:

stack_0[T: TYPE]: THEORY
  BEGIN
    stack: TYPE = [ nat, ARRAY[nat -> T] ]	% a type

    s, st: VAR stack				% variables
    x, y : VAR T
    i, j : VAR nat

    e    : T					% a constant
    empty: stack = (0, (LAMBDA j: e))

    lmnts(s)    : ARRAY[nat -> T] = proj_2(s)
    size(s)     : nat             = proj_1(s)
    nonempty?(s): bool            = (size(s) > 0)

    push(x, s)  : (nonempty?)     =
			 (size(s)+1, lmnts(s) WITH [(size(s)) := x])
    ns   : VAR (nonempty?)
    top(ns)     : T               = lmnts(ns)(size(ns)-1)
    pop(ns)     : stack           = (size(ns)-1, lmnts(ns))

    equal_ax : AXIOM
		(FORALL s, st : (size(s) = size(st) AND (FORALL i:
			(i < size(s) => lmnts(s)(i) = lmnts(st)(i))))
			IMPLIES s = st)

    push_pop : CONJECTURE  pop(push(x, s)) = s

  END stack_0