Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Date: Fri, 1 Nov 91 17:07:36 EST
From: garrel@com.oracorp.athens
Message-Id: <9111012207.AA19266@athens.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Gee whiz, folks!

I feel as if I had belched (or something worse) in church.

Having delivered myself of that, I will, for the moment, content myself
with one substantive obervation.

Sure enough, when we consider a sequent, Gamma |- A, Gamma is supposed to
be a set and, therefore, we shouldn't do things that depend on the fact that
the underlying implementation of sequents uses a list.  But goals are
different --- they are concrete objects of type term list # term and, hence,
are inherently ordered.  So it makes sense to produce subgoals in a way that
depends on the ordering present in the goal we start with.

What we don't want to do is get tangled up with notions about ordering
when we write proof functions.  The point of the technical concept of
a theorem's achieving a goal seems be precisely to avoid this kind of
problem, by mediating between sequents and goals in just the right way.
So we write the proof function, without getting tangled up with false
notions about ordering, and then invoke achievement to get back to
the level where we're dealing with ordered objects.

Trepidantly yours,

Garrel