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

*To*: pvs-help@csl.sri.com*Subject*: What have I missed ? (a proof failed)*From*: yechiel@CS.Technion.AC.IL (Yechiel Kimchi)*Date*: Wed, 6 May 1998 18:17:27 +0300 (IDT)

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

- Prev by Date:
**Re: 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):