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

Re: [PVS-Help] using TCCs in proofs



Dear Cesar Munoz,

Thanks very much for your help.

I added your strategies to pvs-strategies and tried it on several sequents
in a proof.  Each time I get an error (see transcript below).

I'm not familiar with the strategy facility, but I noticed a reference to
*current-theory* in your code.  The formula I'm proving is in a different
theory, which imports the theory containing the declaration (named
"fieldUpdateS") from which I want to use TCCs.  Could this be the problem?
If so, can the strategy be changed to access all theories in the import
chain?

It's possible that the error has nothing to do with your strategy.
My theories involve slightly complicated use of dependent types and
sometimes I get an error about "No methods applicable".  There's an
outstanding bug report or two about it.

thanks,
dave

*****************

Rule?
(try-tccs "fieldUpdateS")
Error: No methods applicable for generic function
       #<standard-generic-function id> with args
       (#<IMPORTING indistinguishable>) of classes (importing)
  [condition type: program-error]

Restart actions (select using :continue):
...

*****************


On Tue, 10 Feb 2004, Cesar A. Munoz wrote:

> Date: Tue, 10 Feb 2004 16:50:42 -0500
> From: Cesar A. Munoz <munoz@nianet.org>
> To: David Naumann <naumann@cs.stevens-tech.edu>
> Cc: pvs-help@csl.sri.com
> Subject: Re: [PVS-Help] using TCCs in proofs
>
> David,
> Put the following lines in pvs-strategies in the directory of your
> current context:
>
> ;; pvs-strategies
> (defstrat one-tcc (decls)
>   (if decls
>       (let ((name (format nil "~A" (id (car decls))))
> 	    (tail (cdr decls)))
> 	(then
> 	 (lisp (format nil "Using TCC: ~A" name))
> 	 (try (then (use name)(grind))
> 	      (fail)
> 	      (skip))
> 	 (one-tcc tail)))
>     (skip))
>   "")
>
> (defstep try-tccs (fname)
>   (let ((ftcc (format nil "~A_TCC" fname))
> 	(l    (length ftcc))
> 	(decls (remove-if-not
> 		#'(lambda(d)
> 		    (let* ((idstr (format nil "~A" (id d)))
> 			   (idx   (mismatch ftcc idstr)))
> 		      (and idx (= idx l))))
> 		(all-decls *current-theory*))))
>     (one-tcc decls))
>   "Tries all the TCCs that match fname"
>   "~%Trying all the TCCs that match fname")
>
> Then, you can call the strategy (try-tccs "f") to use all the TCCs of
> formula f as you want.
>
> You may want to tune the lines:
>
> 	 (try (then (use name)(grind))
> 	      (fail)
> 	      (skip))
>
> to your particular needs.
>
> I have try the strategy with the following example:
>
> foo : THEORY
> BEGIN
>
>   x,y : VAR real
>
>   f(x,y):real = IF y > 0 THEN 1/x ELSE 1/y ENDIF;
>
>   l1: LEMMA FORALL (x: real, y: real): y > 0 IMPLIES x /= 0;
> %|- l1 : PROOF (try-tcc "f") QED
>
>   l2: LEMMA FORALL (y: real): NOT y > 0 IMPLIES y /= 0;
> %|- l2 : PROOF (try-tcc "f") QED
>
> END foo
>
> On Tue, 2004-02-10 at 15:31, David Naumann wrote:
> > Is there a facility or recommended way to deal with the following.
> >
> > I define a function f which involves some complicated dependent types and
> > generates TCCs that aren't proved by the built-in strategies.
> >
> > Now I do a proof involving f and thus get similar TCCs.  Having discharged
> > the TCCs for f, I can now use them in this proof.  But I'm doing it by
> > hand:  look at the obligation, find f's TCC with similar consequent, and
> > invoke
> >
> >    (then (use "f_TCC_number_whatever") (grind))
> >
> > It works but it's tedious.
> >
> > I haven't tried it, but a quick look at the Prover Guide's chapter on
> > strategies suggests I can easily define a strategy that tries the above
> > for each of f's TCCs.  But there are several such f so I'd prefer to
> > generate the strategy automatically.
> >
> >
> --
> Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
> National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
> 144 Research Drive                  http://research.nianet.org/~munoz
> Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855
>
>