Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9405260001.AA16054@maui.cs.ucla.edu>
To: hol2000@leopard.cs.byu.edu
Subject: Implication and Universal Quantification (WAS: Accessing Assumptions)
Cc: Paul.Curzon@cl.cam.ac.uk, Sara.Kalvala@cl.cam.ac.uk
Date: Wed, 25 May 94 17:01:14 PDT
From: chou@CS.UCLA.EDU

Paul Curzon wrote:

> I have toyed with ways of doing this, the easiest was just
> to store the ASSUMED assumption in an assignable variable when you eg do
> DISCH_TAC and then bind that to a name of choice. This just involves making
> minor changes to various tactics, but is very hacky. Maybe if you were doing
> things from scratch in HOL2000 it could be done more cleanly.
> You then get proofs such as:
> 
> val Lemma = prove(
> (--`!n. PSIG2LEN n n d ==> ..... `--),
> 
> GEN_TAC THEN
> CATCH_DISCH_TAC THENA (fn _ => 
>   let val psig2len = new_assumption();
>       val th1 = REWRITE_RULE[....] psig2len
> in
> REPEAT STRIP_TAC THEN
> IMP_RES_TAC th1 THEN
> ...
> end)
> );

I think I have proposed something like this in 1992's HUG:

  Ching-Tsun Chou,
  ``A Note on Interactive Theorem Proving with Theorem Continuation Functions'',
  in {\em Higher Order Logic Theorem Proving and Its Applications\/},
  edited by Luc Claesen and Michael Gordon,
  Elsevier Science Publishers B.V., 1992, pp.\ 59--70.


But now I'd like to propose a (hopefully!) new perspective on this problem.
In certain intuitionistic type theories, implication is just a special case
of universal quantification, in the following sense:

  A proof of !x:D. P(x) is a function f that transforms an y in D
  into a proof f(y) of P(y)
  
  A proof of P ==> Q is a function f that transforms a proof p of P
  into a proof f(p) of Q

So:

  To prove !x:D. P(x), we assume we have an y in D and proceed to
  construct a proof f(y) of P(y)
  
  To prove P ==> Q, we assume we have a proof p of P and proceed to
  construct a proof f(p) of Q

Of course HOL neither is intuitionistic nor manipulates proofs
in its object logic.  But the analogy of implication and universal
quantification does suggest us to view the labels of assumptions (eg, p)
as the same kind of thing as the dummy variables (eg, y) introduced
by a proof of a universal quantification.  Now, we seldom have problem
with the choice of dummy variables because HOL tactics, by default,
just use the bound variable of the universal quantification
(ie, y is just x).  This suggests that we should be able to decorate
subterms with labels, eg,

(1)  p:P ==> Q

so that when the subterm is stripped by (say) DISCH_TAC, the label
is already there.  Note that such labels, like the p in (1), are
bound variables and should behave as such.  For instance, if there
is already a term with label p among the assumptions, P should get
label p' when it is stripped.  I do not know whether Sara Kalvala's
annotation scheme (also reported in 1992's HUG) handles this.
Perhaps Sara cares to comment on it?

Incidentally, another consequence of the analogy of implication and
universal quantification is that resolution tactics should work for
universal quantification as well.  For example, if we have the goal
p ?- q and the theorem p ==> r1 \/ r2, we can use IMP_RES_TAC to get
two new goals: p, r1 ?- q and p, r2 ?- q.  By analogy, if we have
the goal x:num ?- q, we should be able to use IMP_RES_TAC and
the theorem !x:num. (x=0) \/ (?y. x=SUC(y)) to obtain two new goals:
x:num, x=0 ?- q and x:num, x=SUC(y) ?- q (assuming y isn't already
free in the goal).  Of couse, x:num is not a boolean term, but perhaps
we can write something like x::num, ie, viewing a type as a predicate.
I think HOL can benefit a lot from this kind of conceptual unification
and simplification.

Cheers,
- Ching Tsun