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

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