Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: toal@edu.ucla.cs (Ray J. Toal)
Cc: info-hol@edu.uidaho.cs.ted
Subject: Equality and partial functions
In-Reply-To: Your message of Mon, 23 Nov 92 21:09:57 -0800. <9211240509.AA23292@hapuna.cs.ucla.edu>
Date: Tue, 24 Nov 92 10:47:39 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"nene.cl.ca.518:24.11.92.10.47.48"@cl.cam.ac.uk>


Ray Toal asks:

> Are any of the following theorems of HOL? (n:*, s:* list, etc.)

In fact, the negations of all 4 theorems are easily provable (see below).

This is rather counterintuitive because one tends to think in terms of partial
functions. A HOL function is, as Ray says, total, so it returns a value even in
cases where it is intuitively `meaningless'.

Partial functions are ubiquitous in informal mathematics, and I think it's
often instructive to step back and ask exactly what an equation like "s = t"
means:

* "if one side is defined, then so is the other and they are equal"?

* "both sides are defined and they are equal"?

* "if both sides are defined then they are equal"?

It is my understanding that the first of these is the usual meaning in informal
mathematics. At the last HOL meeting I quoted the following theorems about the
real numbers (slightly modified from their HOL form).

       -1
  0 * 0  = 0

[which is false in normal mathematics but true in HOL]

  !x:real. (tan(x) = 0) ==> (?n:int. x = n * pi)

[which is true in normal mathematics but false in HOL]

I seem to recall seeing in some book ("Categories, allegories", I think) a non-
symmetric equality represented by a "Venturi tube" symbol. (But maybe I'm imagining 
it.) As I recall, it meant "if the LHS is defined, so is the RHS and they are
equal", or vice versa. I suspect there are lots of subtle issues associated with
equality if one is sufficiently precise about its use. Using total functions makes
things much simpler, despite its drawbacks.

John Harrison (jrh@cl.cam.ac.uk)

==============================================================================
  let th1 = PROVE
   ("?n:*. n = HD []",
    EXISTS_TAC "HD [] :*" THEN REFL_TAC);;

  let th2 = PROVE
   ("?s:(*)list. s = TL []",
    EXISTS_TAC "TL [] :(*)list" THEN REFL_TAC);;

  let th3 = PROVE
   ("~(!(n:*) s1 s2. (n = HD s2) /\ (s1 = TL s2) ==> (s2 = CONS n s1))",
    CONV_TAC(TOP_DEPTH_CONV NOT_FORALL_CONV) THEN
    MAP_EVERY EXISTS_TAC ["HD [] :*"; "TL [] :(*)list"; "[] :(*)list"] THEN
    REWRITE_TAC[NOT_NIL_CONS]);;

  let th4 = PROVE
   ("~(!(s1:(*)list) s2. (s1 = TL s2) ==> ~NULL s2)",
    CONV_TAC(TOP_DEPTH_CONV NOT_FORALL_CONV) THEN
    MAP_EVERY EXISTS_TAC ["TL [] :(*)list"; "[] :(*)list"] THEN
    REWRITE_TAC[NULL]);;
==============================================================================