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

Re: [PVS-Help] using TCCs in proofs



Thanks very much.  It works great!
--dave


On Wed, 11 Feb 2004, Cesar A. Munoz wrote:

> Date: Wed, 11 Feb 2004 09:47:28 -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
>
> Dave,
> My mistake. Try the following revisited script:
>
> (defstep try-tccs (fname &optional theory )
>   (let ((ftcc (format nil "~A_TCC" fname))
>         (th   (if theory (get-typechecked-theory theory)
> *current-theory*))
>         (l    (length ftcc))
>         (decls (remove-if-not
>                 #'(lambda(d)
>                     (and (subtype-tcc? d)
>                          (let* ((idstr (format nil "~A" (id d)))
>                                 (idx   (mismatch ftcc idstr)))
>                            (and idx (= idx l)))))
>                 (all-decls th))))
>     (one-tcc decls))
>   "Tries all the TCCs that match fname from theory (default is current
> theory)"
>   "~%Trying all the TCCs that match fname")
>
> By default, it looks at the current theory. If you want definitions in
> other theory try the option :theory, as in (try-tccs "f" :theory "foo").
>
> I have tried the script in 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-tccs "f") QED
>
>   l2: LEMMA FORALL (y: real): NOT y > 0 IMPLIES y /= 0
> %|- l2 : PROOF (try-tccs "f") QED
>
> END foo
>
> faa : THEORY
> BEGIN
>
>   IMPORTING foo
>
>   x,y : VAR real
>
>   l1: LEMMA FORALL (x: real, y: real): y > 0 IMPLIES x /= 0
> %|- l1 : PROOF (try-tccs "f" :theory "foo") QED
>
>   l2: LEMMA FORALL (y: real): NOT y > 0 IMPLIES y /= 0
> %|- l2 : PROOF (try-tccs "f" :theory "foo") QED
>
> END faa
>
> Hope that it helps,
> Cesar
>
> On Tue, 2004-02-10 at 23:26, David Naumann wrote:
> > 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):
> > ...
> >
> > *****************
>
> --
> 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
>
>