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

Re: [PVS-Help] Circular dependencies in judgements of PVS 4.0

I understand that you working on this to learn PVS, but the NASA PVS 
libraries have a large collection of multi-set results (they are called 


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?
> Many thanks for the help in advance
> Henning
> Martin-Luther-Universität Halle-Wittenberg, Institut für Informatik
> Tel. +49 - 345 - 55 24773
> Fax  +49 - 345 - 55 27033