[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)].
> 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.
John Hoffman, PhD
Secure Computing Corporation
2675 Long Lake Road
Roseville, MN 55113