[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Re: Circular dependencies in judgements of PVS 4.0
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
> 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:
(("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.