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

*To*: pvs_help list_serve <pvs-help@csl.sri.com>*Subject*: ? about the quant rule*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Mon, 13 Jul 1998 12:54:50 -0400 (EDT)

A follow-up on my question about the quant rule (included below). Sorry, I should have been more specific about the context. I have the following theory importing finite sets: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% subset_exchange[T : TYPE] : THEORY BEGIN IMPORTING finite_sets, finite_sets_def[T] S1, S2, S3 : VAR finite_set subset_exchange : LEMMA (forall S1, S2, S3 : (subset?(S3, S1) IMPLIES union(S1, S2) = union(difference(S1, S3), union(S2, S3)))) END subset_exchange %%%%%%%%%%%%%%%%%%%%% The goal is to prove the lemma, subset_exchange. I used skolem!, then flattened the consequent, leaving the following goal/sequent: subset?(S3, S1) |---- union(S1, S2) = union(difference(S1, S3), union(S2, S3)) (the indexing of variables after flatten is a little different). Then I expanded "subset?", and introduced a name for each side of the consequent. Finally I appealed to extensionality for sets, yielding the following goal/sequent: {-1} union(difference(S1!1, S3!1), union(S2!1, S3!1)) = b [-2] union(S1!1, S2!1) = a [-3] (FORALL (f_3: set[T], g_4: set[T]): (FORALL (x_5: T): f_3(x_5) = g_4(x_5)) IMPLIES f_3 = g_4) [-4] (FORALL (x: T): member(x, S3!1) => member(x, S1!1)) |------- [1] union(S1!1, S2!1) = union(difference(S1!1, S3!1), union(S2!1,S3!1)) At this point, as I noted in my earlier message, I wanted to instantiate extensionality (antecedent -3) with 'a' and 'b' in for the occurrences of 'f_3' and 'g_4' (respectively). So at the Rule? prompt, I put: (quant -3 ("a" "b")) And, as I noted before, what I got was the message "ill-formed rule/strategy" I see that in the syntax (from "The PVS Proof Checker: A Reference Manual (Beta Release)) it asks for *expressions* in the list following the fnum argument for Quant. But I tried not only using "a" and "b" but also using the "union" expressions that actually occur in the consequent I wish to prove. I got the same "ill-formed" response. (It was when use of the complex union expressions failed that I decided to introduce names and try instantiating with those.) Well, since I sent the previous query, I tried using the "quant?" rule, with the variables listed along with the names as substituends and THAT worked fine. So now I'm back on course, but I still don't know why my earlier use of Quant wasn't recognized. I'd appreciate some pointers. Thanks in advance. Mark Aronszajn ---------- Forwarded message ---------- Date: Mon, 13 Jul 1998 10:23:31 -0400 (EDT) From: Mark Aronszajn <aronsz@csee.wvu.edu> To: pvs-help@csl.sri.com Cc: aronsz@csee.wvu.edu Subject: ?s about the quant rule, etc. Resent-Date: Mon, 13 Jul 1998 07:27:48 -0700 (PDT) Resent-From: pvs-help@csl.sri.com I have one specific question right now about the quant rule; then I have a more general question... More general first: I am new to PVS. I've been raised using Natural Deduction systems in logic (like Kalish & Montague's box & cancel style). I'm finding it hard to shift over to the sequent calculus used in PVS. Is there anyone out there who could give some help specific to this predicament, someone who's familiar with both styles? And maybe there's a good reference--a textbook, or PVS document--that would be helpful? The specific question has arisen in a proof I'm trying to construct. I need to prove two sets (two unions) are identical, so I invoked extensionality for sets. Then I wanted to instantiate the axiom for the two unions that I want to prove identical. I introduced names, 'a' and 'b' for the two union expressions with (name "a" "union(foo)") (name "b" "union(bar)") This worked fine. I then wanted instantiate putting "a" and "b" in for the two set variables in the set extensionality axiom. So I used (quant -3 ("a" "b")) As far as I can tell this is the precise syntax required for the rule, but I get an "ill-formed rule/strategy" message with no change... Can anyone tell me what's wrong here? THanks in advance for any help on either question. Mark Aronszajn

- Prev by Date:
**?s about the quant rule, etc.** - Next by Date:
**Re: ? about the quant rule** - Prev by thread:
**Re: ? about "complete"/"incomplete" proof status** - Next by thread:
**Re: ? about the quant rule** - Index(es):