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

Re: Trivial proofs and set lemmas

Malcolm -

Thanks for the question regarding PVS.  Here's a couple of key points that
may help you.  The first is the interpretation of the sequent.  For


{-1}  (intersection(f!1, emptyset) = emptyset)
{-2}  (union(f!1, emptyset) = f!1)
{-3}  f!1(v!1)
{1}   (union(remove(v!1, f!1), add(v!1, emptyset)) = f!1)

This is merely a convenient representation of:

( (intersection(f!1, emptyset) = emptyset) AND
  (union(f!1, emptyset) = f!1) AND
  f!1(v!1) )
  (union(remove(v!1, f!1), add(v!1, emptyset)) = f!1)

So, as you see despite the formula in -1 being trivially true, it wouldn't
gain you anything in the proof if PVS did that simplification for you.
Indeed, we take great care in this regard not to oversimplify the sequent
in certain cases, as this would make certain elegant proofs more
difficult.  Specifically,


if we simplify away A giving you:


you could find later in the proof that a large piece of 'C' could have
been simplified using 'A', which you've now lost.

The second key point is the use of the extensionality principle.  The
proof of your formula "proof2" is, in one line:

 (then (grind)(apply-extensionality)(grind))

The reason why extensionality is important here is that sets (in PVS)
are merely functions.  So the the consequent of your proof:

 (union(remove(v!1, f!1), add(v!1, emptyset)) = f!1)

is really an assertion about the equality of two functions.  The PVS
command (apply-extensionality) introduces an extensionality principle:

  extensionality: LEMMA
     (FORALL (x: D): f(x) = g(x)) IMPLIES f = g

This is from the prelude theory "functions".  Introducing this lemma,
your proof is now reduced to:

Applying extensionality,
this simplifies to: 

[-1]  (intersection(f!1, emptyset) = emptyset)
[-2]  (union(f!1, emptyset) = f!1)
[-3]  f!1(v!1)
{1}   (NOT (v!1 = x!1) AND f!1(x!1) OR v!1 = x!1) = f!1(x!1)
[2]   (union(remove(v!1, f!1), add(v!1, emptyset)) = f!1)

where f!1(x!1) means (as the function f!1 is intuitively a set in this
context) that x!1 is a member of f!1.  The proof from here on is trivial,
and completed by grind.

Hope that helps,

Dr Dave Stringer-Calvert,  Senior Project Manager,  Computer Science Lab
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com