Re: [PVS-Help] Ask for help on a proof

[Jerome <jerome@xxxxxxxxxxxxxx>]

If you can take the reflexive, symmetric, and transitive properties as
axioms, you should declare them as such (after your predicate
declarations):

   reflexive:  AXIOM reflexive?(R)
   symmetric:  AXIOM symmetric?(R)
   transitive: AXIOM transitive?(R)

This way, in your proof, you can use them as in (LEMMA ...) and/or
(REWRITE ...) rules. For example:

   Rule? (LEMMA "symmetric")
   ...
   Rule? (INST?)
   ...

jerome

On Fri, May 16, 2008 at 06:25:56PM +0800, Xiao Han wrote:
>Hi there,
>   I am new to PVS.  I am working on an assignment about using PVS to prove
>a theorem.
>   Equivalence relations satisfy the following axioms: reflexive, symmetric
>and transitive.  Here equivalence relations are denoted by ???.
>  The theorem is
>
>  forall x and y, ¬x???y ??? (forall z, x???z???¬y???z )
>
>  I wrote the specification as follows:
>
>relations[t: TYPE] : THEORY
>BEGIN
>    x, y, z: VAR t
>    R : VAR PRED[[t,t]]
>
>    reflexive?(R): bool = (FORALL x: R(x, x))
>    symmetric?(R): bool = (FORALL x, y:R(x, y) IMPLIES R(y, x))
>    transitive?(R): bool =
>        (FORALL x, y, z: R(x, y) AND R(y, z) IMPLIES R(x, z))
>
>    equivalent_relation?(R): bool =
>        reflexive?(R) AND symmetric?(R) AND transitive?(R)
>     er: (equivalent_relation?[[t,t]])
>
>    TODO: CONJECTURE ( FORALL (x: t), (y: t): NOT er(x, y) IMPLIES ( FORALL
>(z: t): er(x, z) IMPLIES er(y, z) ) )
>END relations
>
>    After using (grind) I got
>
>TODO :
>
>  |-------
>{1}   (FORALL (x: t), (y: t):
>         NOT er(x, y) IMPLIES
>          (FORALL (z: t): er(x, z) IMPLIES NOT er(y, z)))
>
>Rule? (grind)
>Trying repeated skolemization, instantiation, and if-lifting,
>this simplifies to:
>TODO :
>
>{-1}  er(x!1, z!1)
>{-2}  er(y!1, z!1)
>  |-------
>{1}   er(x!1, y!1)
>
>Rule?
>
>I should use the symmetric axiom to continue the proof but I do not know
>how:
>
>Rule? (use "symmetric?")
>Using lemma symmetric?,
>this simplifies to:
>TODO :
>
>{-1}  symmetric? = (LAMBDA (R): (FORALL x, y: R(x, y) IMPLIES R(y, x)))
>[-2]  er(x!1, z!1)
>[-3]  er(y!1, z!1)
>  |-------
>[1]   er(x!1, y!1)
>
>Is it correct to use a lemma?  If so, what to do next?
>
>Many thanks.