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

Re: Rewrite rules don't rewrite this equality.




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           ||                    
==============================++======================