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

*To*: "Cesar A. Munoz" <munoz@nianet.org>*Subject*: Re: [PVS-Help] using TCCs in proofs*From*: David Naumann <naumann@cs.stevens-tech.edu>*Date*: Tue, 10 Feb 2004 23:26:16 -0500 (EST)*Cc*: David Naumann <naumann@cs.stevens-tech.edu>, pvs-help@csl.sri.com*In-Reply-To*: <1076449842.32273.107.camel@squirt.nianet.org>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Original-Received*: from quarter.csl.sri.com (mx0.csl.sri.com [130.107.1.30])by postal.csl.sri.com (8.12.9p2/8.12.9) with ESMTP id i1B4Owm0061341for <pvs-help@postal.csl.sri.com>; Tue, 10 Feb 2004 20:24:58 -0800 (PST)(envelope-from naumann@cs.stevens-tech.edu)*Original-Received*: from mailgate-external1.sri.com (mailgate-external1.SRI.COM[128.18.85.101])by quarter.csl.sri.com (8.12.9/8.12.10) with SMTP id i1B4Ov6K000316for <pvs-help@csl.sri.com>; Tue, 10 Feb 2004 20:24:57 -0800*Original-Received*: (qmail 27477 invoked from network);11 Feb 2004 04:24:57 -0000*Original-Received*: from localhost (HELO mailgate-external1.SRI.COM) (127.0.0.1)by mailgate-external1.sri.com with SMTP; 11 Feb 2004 04:24:57 -0000*Original-Received*: from eylenbosch.cs.stevens-tech.edu ([155.246.81.60])by mailgate-external1.SRI.COM (SAVSMTP 3.1.2.35) with SMTP idM2004021020245628673for <pvs-help@csl.sri.com>; Tue, 10 Feb 2004 20:24:56 -0800*Original-Received*: from localhost (localhost [127.0.0.1])by eylenbosch.cs.stevens-tech.edu (Postfix) with ESMTPid 719A773601; Tue, 10 Feb 2004 23:26:16 -0500 (EST)*References*: <Pine.NEB.4.58.0402101515030.2356@eylenbosch.cs.stevens-tech.edu><1076449842.32273.107.camel@squirt.nianet.org>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

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

- Prev by Date:
**Re: [PVS-Help] using TCCs in proofs** - Next by Date:
**Re: [PVS-Help] using TCCs in proofs** - Prev by thread:
**Re: [PVS-Help] using TCCs in proofs** - Next by thread:
**Re: [PVS-Help] using TCCs in proofs** - Index(es):