Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@leopard.cs.byu.edu
Cc: tfm@dcs.gla.ac.uk
Subject: A Little Puzzle.
Date: Fri, 07 Oct 1994 18:30:00 +0100
From: "Tom. F. Melham" <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:016070:941007180404"@cl.cam.ac.uk>

Here's a wee puzzle for interested HOL-users to try their hand
at.  I think its solution gives a very nice illustration of what
can be involved when you have to translate an informal proof into
a formal one suitable for doing on the computer.  

Here's the theorem:

  Suppose g:A->B and f:A->C are total functions such that
  for all x:A and y:A, g(x) = g(y) implies f(x) = f(y).
  Then there exists a total function h:B->C such that

     |- !x:A. h(g(x)) = f(x)                      [1]

The *informal* proof is just this: formula 1 is a legitimate
definition of h because it assigns a unique value to any g(x),
since whenever g(x) = g(y), f(g(x)) = f(x) = f(y) = f(g(y)).
Pick a fixed value in C for h to map elements outside the image
of g to.

The above informal proof is, in fact, a bit *more* detailed than
some you might see in a maths text.  The challenge is to do the
proof formally. Specifically, the required HOL theorem is

     |- !g f. (!x y. (g x = g y) ==> (f x = f y)) 
                 ==>
              ?h. !x. h(g x) = f x

Hint: this example also illustrates how rash use of epsilon can
get you into trouble.  

If people are interested, I'll post my proof later.

Tom