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

Re: [PVS] Ask for help on a proof



Well, for starters you have an error in the PVS formulation of your conjecture. Take another look :)

-- Scott


Quoting Xiao Han <moshimaru@xxxxxxxxx>:


 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.