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

? about the quant rule

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

	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

{-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

	(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