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

*To*: Henning Thielemann <lemming@xxxxxxxxxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] Circular dependencies in judgements of PVS 4.0*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Wed, 12 Sep 2007 11:20:34 -0700*Cc*: pvs-help@xxxxxxxxxxx*Comments*: In-reply-to Henning Thielemann <lemming@henning-thielemann.de>message dated "Wed, 12 Sep 2007 17:56:58 +0200."*In-reply-to*: <Pine.SOC.4.64.0709121731230.4867@turing.informatik.uni-halle.de>*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>*References*: <Pine.SOC.4.64.0709121731230.4867@turing.informatik.uni-halle.de>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Henning, Henning Thielemann <lemming@henning-thielemann.de> wrote: > Before digging into my particular problem, I have a general > question. pvs-system-guide.pdf, section "2.2 Parsing and Typechecking" > states that TCCs must be proved before theorems in a theory. If so, why am > I allowed to use lemmas of a theory in proofs of a TCC? In contrast to > that, if I prove a lemma and try to use a lemma which is defined later in > the same PVS file, the interactive PVS prover considers the later lemma as > non-existent. As a side note: I would also like to use lemmas of a theory > in proofs of TCCs of the same theory. If the order is like those of "Proof > Status", that is > lemmaA_TCC1 > lemmaA > lemmaB_TCC1 > lemmaB_TCC2 > lemmaB > would there be any chance of a circular reasoning? This should be made clearer in the document - if a given formula generates TCCs, they precede the formula in the logical context, so the formula may not be used to discharge them. However, any lemmas preceding the given formula may be used to discharge such TCCs. Technically, there should be no way to get a circular proof, the code has been left in to catch bugs (see below). > Now the particular problem: I'm working on a theory of multi-sets, which I > have designed analogously to Prelude's "sets" and "finite_sets" > theories. (I'm afraid, I'm duplicating work, however it is a nice exercise > to get started with PVS.) I have the functions 'remove', which removes one > element from a multiset, and 'remove_all', which removes all instances of > an element from a multiset. Now I have the judgements > > x: VAR T > > A: VAR finite_multiset > > finite_remove: JUDGEMENT remove(x, A) HAS_TYPE finite_multiset > > finite_remove_all: JUDGEMENT remove_all(x, A) HAS_TYPE finite_multiset > > The proofs of the statements are practically identical, because both > 'remove' and 'remove_all' generate subsets of A. However the proof of > 'finite_remove' is considered complete, whereas the one of > 'finite_remove_all' is considered incomplete, due to an circularity with > the definition of 'finite_multiset'. I compared the proof and definition > chains of 'finite_remove' and 'finite_remove_all' and I found no > differences with respect to the objects of the same module. I reduced the > proof of 'finite_remove_all' in order to see, which lemma invokation > causes the circularity. I ended up with a simple (POSTPONE) and the proof > is still considered circular (although now UNPROVED). How can I find out > more about the circularity? This is actually a bug reported in http://pvs.csl.sri.com/cgi-bin/pvs-bug?id=978 The bug is due to the improper treatment of judgements in checking for circularities. The (rather long) patch is available at the end of the above page. To use, simply copy the patch into ~/.pvs.lisp (creating it if necessary), and restart PVS. Hope this helps, Sam Owre

- Prev by Date:
**[PVS-Help] Re: Circular dependencies in judgements of PVS 4.0** - Next by Date:
**Re: [PVS-Help] Circular dependencies in judgements of PVS 4.0** - Prev by thread:
**[PVS-Help] Circular dependencies in judgements of PVS 4.0** - Next by thread:
**Re: [PVS-Help] Circular dependencies in judgements of PVS 4.0** - Index(es):