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

[Henning Thielemann <lemming@xxxxxxxxxxxxxxxxxxxxx>]

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.