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

*To*: adridg@sci.kun.nl (Adriaan de Groot)*Subject*: Re: Rewrite rules don't rewrite this equality.*From*: John Hoffman <hoffman@securecomputing.com>*Date*: Tue, 16 Sep 1997 08:43:21 -0500 (CDT)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <199709161331.PAA14881@studs3.sci.kun.nl> from "Adriaan de Groot" at Sep 16, 97 03:31:33 pm

If instead of (assert) you use (reduce) pvs proves your theorem. reduce is the core part of grind. grind basically applies rewrite rules, then calls reduce, which easily dispenses your theorem. John p.s. anyone know why the file "strategies.lisp" is no longer part of the distribution? I miss it.... > > Dear volunteers, > > I'm trying to prove a theorem in which I compute a result inside > an if, and then add that result to something else. PVS revision > 2.408, on a regular Sun running Solaris. Here's my test theory: > > > %%% > test : THEORY > BEGIN > struct : TYPE = [# ins:nat, outs:nat #] > > f(a:struct) : nat = outs(a) ; > > alemma : LEMMA > (forall (a:struct) : > (if ins(a)>0 then f(a) else outs(a) endif)=outs(a) > ) > > dilemma : THEOREM > (forall (a:struct, b:struct) : > (if ins(a)>0 then f(a) else outs(a) endif)+ > (if ins(b)>0 then f(b) else outs(b) endif)= > outs(a)+outs(b) > ) > END test > %%% > > > The idea is that I can apply alemma twice with different > instantiations (ie. a<-a!1, a<-b!1) to prove dilemma. > > %%% > (skolem!)(lemma "alemma" ("a" "a!1"))(lemma "alemma" ("a" "b!1")) > %%% > > However, once I've done that, I end up with this: > > %%% > dilemma : > > [-1] (IF ins(b!1) > 0 THEN f(b!1) ELSE outs(b!1) ENDIF) = outs(b!1) > [-2] (IF ins(a!1) > 0 THEN f(a!1) ELSE outs(a!1) ENDIF) = outs(a!1) > |------- > [1] (IF ins(a!1) > 0 THEN f(a!1) ELSE outs(a!1) ENDIF) > + (IF ins(b!1) > 0 THEN f(b!1) ELSE outs(b!1) ENDIF) > = outs(a!1) + outs(b!1) > > Rule? (assert) > No change on: (ASSERT) > dilemma : > %%% > > > It seems to me that not enough is being rewritten here; running > (grind) rewrites the f() calls and then simplifies, which doesn't > work for the theory I'm really interested in, since it's more > complicated. Am I missing some prover command to do this, > or what? My thanks for your help, > > ade > ==============================++====================== John Hoffman, PhD || Secure Computing Corporation || Sushi is good? 2675 Long Lake Road || Life is good! Roseville, MN 55124 || hoffman@securecomputing.com || Fax :(612)628-2701 || - Origami Sushi Chef Phone:(612)628-2808 || ==============================++======================

- Prev by Date:
**Rewrite rules don't rewrite this equality.** - Next by Date:
**Re: Rewrite rules don't rewrite this equality.** - Prev by thread:
**Rewrite rules don't rewrite this equality.** - Next by thread:
**Re: Rewrite rules don't rewrite this equality.** - Index(es):