Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9301170342.AA07383@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list)
Subject: Unused assumptions
Date: Sat, 16 Jan 93 19:42:47 PST
From: chou@edu.ucla.cs

Consider the following HOL session:

#set_goal(["a:bool"], "b ==> b");;
"b ==> b"
    [ "a" ]

#e(REPEAT DISCH_TAC);;
OK..
"b"
    [ "a" ]
    [ "b" ]

#e(ASM_REWRITE_TAC [ ]);;
OK..
goal proved
. |- b
|- b ==> b

#top_thm();;
|- b ==> b

Notice that the assumption "a" has been lost!  Why?
Because it is not actually used in the proof, though
one may think ASM_REWRITE_TAC uses every assumption.
This habit of dropping unused assumptions is not limited
to rewriting tactics; many other tactics have similar
behavior.  My question is: Should this be considered
a virtue or a vice?

For my purposes, this behavior is very annoying.
The reason is as follows.  Most theorems I want to
prove has a fixed assumption, call it A.  Hence it
is more convenient to prove theorems of the form:

(1)     A |- ...

than of the form:

(2)     |- A ==> ...

For example, the ... part may be an equality that can be
used as rewrites.  If all my theorems are of form (1),
I can easily use them to rewrite each other, as if the
assumption A does not exist.  However, if I have expressed
my theorems in form (2), I have to DISCH_TAC A in backward
reasoning and UNDISCH A in forward reasoning before the ...
part can be used.  Now, common tactics tend to drop unused
assumptions, which means that I have to be very careful
in order to make sure my theorems are all of form (1),
since A may or may not be actually used in the proof.
The hack I come up with is to have a dummy step in the proof
to ensure that A is "used" (though I'd rather prefer not to
have to do this!), as follows.

#set_goal(["a:bool"], "b ==> b");;
"b ==> b"
    [ "a" ]

#e(EVERY_ASSUM ASSUME_TAC);;    % "Use" a. %
OK..
"b ==> b"
    [ "a" ]
    [ "a" ]

#e(REPEAT DISCH_TAC THEN ASM_REWRITE_TAC [ ]);;
OK..
goal proved
|- b ==> b
. |- b ==> b

#top_thm();;
a |- b ==> b


- Ching Tsun