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

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



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