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

*To*: pvs-help@xxxxxxxxxxx*Subject*: [PVS-Help] Re: Circular dependencies in judgements of PVS 4.0*From*: Henning Thielemann <lemming@xxxxxxxxxxxxxxxxxxxxx>*Date*: Wed, 12 Sep 2007 18:28:22 +0200 (CEST)*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

On Wed, 12 Sep 2007, Henning Thielemann 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? > > 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? It becomes even more crazy. I have a function 'rest_all' which removes all instances of an arbitrary element of the multiset (namely the one selected by 'choose'). This is defined in terms of 'remove_all'. I want to proof: finite_rest_all: JUDGEMENT rest_all(A) HAS_TYPE finite_multiset The proof script is: ("" (SKOSIMP) (EXPAND "rest_all") (PROPAX)) That is, 'rest_all' is expanded to 'remove_all' and then the judgement on 'remove_all' is applied automatically. The proof is considered circular with respect to the definition of finite_multiset. This seems to be reasonable, since the proof implicitly relies on the one of finite_remove_all, which is considered circular by PVS. Now, I make the proof a bit more complicated: ("" (SKOSIMP) (CASE "is_finite(intersection(rest_all(A!1),A!1))") (("1" (EXPAND "rest_all" +) (PROPAX)) ("2" (JUDGEMENT-TCC)))) That is, I introduce a provable statement, which I do not need. The main step of the proof is still expanding 'rest_all'. However the proof is now considered 'complete'. I'm lost.

**References**:**[PVS-Help] Circular dependencies in judgements of PVS 4.0***From:*Henning Thielemann

- Prev by Date:
**[PVS-Help] 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):