Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199507121651.AA127997902@bobcat.cs.byu.edu>
To: info-hol@cs.byu.edu
Subject: Re: Conditionals
Date: Wed, 12 Jul 1995 10:51:41 -0600
From: Phil Windley <windley@cs.byu.edu>


There's more at the end of this message not directly related to the solving
of this particular goal.  HOL experts may want to jump tot the bottom.

--phil--


On Wed, 12 Jul 1995 12:10:26 -0400 Robert Eastham writes
+--------------------
| How do I handle proofs which contain conditionals? For example, I am left
| with a subgoal:
| 
| !t. out(SUC t) = inp t /\ inp(SUC t)
| --------------------------------------
|  !t. out t = ((t=0) => F | (inp (t-SUC 0))) /\ inp t
| 
| How do I finish this proof? A rewrite with the assumptions does not finish
| this.

The problem is not really the conditional, but rather in knowing which
theorems to rewrite with:


set_goal (["!t. out t = ((t=0) => F | (inp (t-SUC 0))) /\ inp t"],
	  "!t. out(SUC t) = inp t /\ inp(SUC t)");;


e(
ASM_REWRITE_TAC [NOT_SUC;SUB_MONO_EQ;SUB_0]
);;


How did I find these?  Well, a combination of experience (knowing where to
look and what to look for) and happenstance.  I knew of NOT_SUC and I
suspected that something like the two theorems dealing with subtraction
existed, so I used the theorem search engine at http://lal.cs.byu.edu to
find them.  If they hadn't I would have had to prove them, as lemmas
(yuck!). 

This points out a larger question for the HOL community.  I suspect
that PVS would solve this straight up.  It certainly solved the last little
exercise we went through a few days ago straight away.  These sorts of
niggling little proofs are just too hard in HOL.

Never mind that FAUST solved the last problem, new users don't anymore know
how to use the FAUST library than they know how to manage the assumption
list.  HOL is just to hard for the non-expert to use and its time we did
something about it.  If we don't, the world is going to be using PVS or
something else like it.  Maybe we don't care...but I, for one, happen to
think that the HOL architecture has some very nice features that I wouldn't
want to give up.

These sorts of things need to be built into HOL, not loaded as libraries
and they need to be accessible in one catch all tactic like the PVS
"grind".   A few years ago we went through an exercise of removing large
portions of the system and putting them in libraries.  I think its time for
the pedulum to swing the other way and for us to put some more things in
the base system.

Suggestions?

(BTW, the arith library doesn't solve this goal, at least not
the straightforward application of it).


--phil--