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

*To*: pvs-help@csl.sri.com*Subject*: Re: Trivial proofs and set lemmas*From*: Dave Stringer-Calvert <dave_sc@csl.sri.com>*Date*: Tue, 30 Jan 2001 20:36:59 -0800*cc*: pvs-help@csl.sri.com*In-Reply-To*: Message from Malcolm Dowse <dowsem@tcd.ie> of "Tue, 30 Jan 2001 21:20:31 GMT." <20010130212031.A215884@alf2.tcd.ie>

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 example: proof2.1: {-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) ) IMPLIES (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, ( A AND B ) IMPLIES C if we simplify away A giving you: B IMPLIES C 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: proof2.1: [-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, Dave --- 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

- Prev by Date:
**Trivial proofs and set lemmas** - Next by Date:
**Optimal RAM for PVS** - Prev by thread:
**Trivial proofs and set lemmas** - Next by thread:
**Defining help functions for strategies** - Index(es):