Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Date: Thu, 31 Oct 91 21:42:52-0100
Message-Id: <9110312242.AA06641@esat.kuleuven.ac.be>
From: ploegaer@be.imec
To: info-hol@edu.uidaho.cs.ted
Subject: referring to assumptions cont'ed


It is pretty hard to give a collection of convincing "rules" why one
should *not* refer to the explicit ordering of the assumptions. It is
more an experience I got by using HOL. Probably some real expert might
be able to. Nevertheless I will try to summarize my ideas. All
comments are wellcome ...

Hope you don't mind my lengthy reply (didn't know whether to email
Garrell or to post this, posted it because I hope that some experts
might comment on this: PROOF STYLE is  a neglected, though I think
important, topic which is not covered in the documentation)

Wim

----------------------------------------------------------------------

I fully agree it looks very attractive and "natural" in beginning. I
fell into the same trap, and I still "suffer" from the consequences. I
was partly "educated" (in HOL) by Ton Kalker from Philips Research.
Ton wrote the libraries auxiliary, quotient, well_order, card and zet.
As he heavily uses explicit reference to the order of the assumptions,
it cannot be denied that this proof-style is pretty powerful. Another
fact that cannot be denied is that the only libraries that caused real
porting problems where those he wrote (ok, CSP also did, but that was
because Tom rewrote the underlying theory of that library). As most of
my "early work" (a) used his tactics (b) is based on his libraries, I
had serious problems when "at once" the libraries disappeared from the
system. (admitted, I could have frozen my system to version 1.11, but
the changes, though drastic, were a real improvement).

The reason that things broke was the change in the behavior of
the resolution mechanism: the current implementation generates
different assumptions, a different number of assumptions and puts them
on the assumption list in a different order. Guess you can imagine the
effect of this change on tactics such as:

- rewrite goal with assumptions a,b, ...
- rewrite assumptions a.b,.. with assumptions c,d, ...
- apply rule to assumptions a,b, ...

... (guess these are what Garrell calls
> tactics intended for use at the top level of the subgoal package
)

You can conclude from this that using the explicit order of the
assumptions will only cause problems if the behavior of some basic
mechanims changes. But, as the manual clearly states that the
assumptions form a *set*, this kind of changes might occur again in
some later version of HOL. Thus, if you want to write code that lasts
for a while, you should bare this in mind.

A related matter is the portability to the other 2 HOL versions (SRI
and Calgary HOL). As I never used these systems I do not know whether
they are fully compatible in this respect, but I would not be
surprised if they aren't.

Another important consideration is the readability of the code.
I must admit that reading proofs is not all that easy. Allthough it is
possible ... in case the proof is written in a "clean way". I'll try
to give an example.

say you are proving

 P[alfa]
   [as1(alfa)]
   [as2]
    ...
   [P [x]]
   ...
   [asn]

and you have the theorem

  thm1 |-as1(alfa) /\ as2 ==> x = alfa

you can write

e(  IMP_RES_TAC thm1 THEN
    FIRST_ASSUM (SUBS1_TAC o SYM) THEN
    FIRST_ASSUM ACCEPT_TAC);;


.. the behavior of this is pretty clear if you know what
FIRST_ASSUM does .. I think

or

e(  IMP_RES_TAC thm1 THEN
    REWRITE_RULE_ASSUM_TAC [n] [m]  THEN
        --> rewrite theorem n with theorem m,
            where you have to do resolution first, than count
            the position of both assumptions and than go on
    ASM_REWRITE_TAC [] --> as I did not you use FIRST_ASSUM on the
                           previous line, I don't see a reason to
                           use it here
);;


How to read this ?? You simple CAN'T without running hol because you
do not know what the second line does.

This is only a very small example. Imagine the effect of several
resolutions and several rewrites with/of assumptions. If you start
working with the assumptions, you will automatically get that type of
proofs (trying to work to a "F" in the assumptions).

Both the considerations on portability and readibility cause me to
compare the use of reference to the order of the assumptions with the
use of a GOTO in a conventional programming language: it is not wrong,
but ...


Some more considerations:

- The assumption list is a set, using explicit reference to the order
of the assumptions is thus against the philosophy of the logic.

- It is a sign of a bad proof style: if you have to rewrite an
assumption, you should have done it before you put them on the assumption
list (or you should not have made it an assumption at all)

  ->e.g.: instead of doing a couple of IMP_RES_TAC's , followed by
  rewriting the assumptions such that match the goal, you might
  consider to rewrite the goal itself first such that it has the
  required form  and than you can finish off the proof with the
  resolution.


A very good example of the problems you run into when you work with
assumptions is the proof of the SCHROEDER_BERNSTEIN_THM in
contrib/v11_lib/CARD/card11/mk_card.ml. If you know that

e(DEFINE "x = fun");;

defines the variable "x" to be equal to "fun" (and thus adds an
assumption "x= fun"), one is able to follow the proof (not easily, but
it is possible) till line 244 of that file, but then ...


----------------------------------------------------------------------
Ploegaerts Wim                                e-mail: ploegaer@imec.be
Imec vzw.                                     Tel.:   (32) 16/281 525
Kapeldreef 75                                 Fax.:   (32) 16/281 515
3001   Leuven,  Belgium                       Telex:  26.152