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

Re: What have I missed ? (a proof failed)

> 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 ?

Your theorem isn't true, because equality of your stacks isn't what
you are think it is.

s1,s2 : stack

means s1 = s2 if

size(s1) = size(s2)

	% (not a problem in your theorem)
lmnts(s1) = lmnts(s2)

	lmnts is a map from naturals to T.

So, you have to know that the ENTIRE two maps are equal.  Not just the
portions of the maps restricted to the domain [1..size(s)].

Your theorem, 

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

is only true, if

lmnts(s)(size(s)) = x

You can fix this by redefining equality of stacks.

Or you can fix it by redefining your base stack type to something

new_stack : TYPE = (lambda (s:stack) : forall (n : nat) : n >= size(s) IMPLIES lmnts(s)(n) = e)

and change the definition of pop appropriately as well.

Good luck


John Hoffman, PhD             
Secure Computing Corporation  
2675 Long Lake Road           
Roseville, MN  55113          
Fax  :(612)628-2701