Jerome wrote:
> 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.
>
>