# 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))

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

```