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

*To*: yechiel@CS.Technion.AC.IL (Yechiel Kimchi)*Subject*: Re: What have I missed ? (a proof failed)*From*: John Hoffman <hoffman@securecomputing.com>*Date*: Wed, 6 May 1998 11:20:13 -0500 (CDT)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <199805061517.SAA01603@CS.Technion.AC.IL> from "Yechiel Kimchi" at May 6, 98 06:17:27 pm

> 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) AND 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 like.... 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 ============================== John Hoffman, PhD Secure Computing Corporation 2675 Long Lake Road Roseville, MN 55113 hoffman@securecomputing.com Fax :(612)628-2701 Phone:(612)628-2808 ==============================

**References**:**What have I missed ? (a proof failed)***From:*yechiel@CS.Technion.AC.IL (Yechiel Kimchi)

- Prev by Date:
**What have I missed ? (a proof failed)** - Next by Date:
**Re: What have I missed ? (a proof failed)** - Prev by thread:
**Re: What have I missed ? (a proof failed)** - Next by thread:
**Re: What have I missed ? (a proof failed)** - Index(es):