Mark, I tried to make your corrections, and here's my new draft, at just 500
lines:
I want to explain how to read the HOL Light basics from the source code in
several sections
0) informal math and HOL
1) the type bool and the constant =
2) sequents, new_basic_definition and the HOL Light inference rules
3) The BETA_CONV proof of general beta-conversion
4) the bool.ml definitions of !, <=>, T, F, /\, ==>, ~, \/
5) the properties of the type bool.
Thanks to Mark Adams for some very helpful corrections.
Section 2 corrects an error I posted about = and T_DEF. Sections 0--4 are
finished. In section 5, which I hope is just reinventing Gordon and Melham's
wheel, I wrote informal math proofs for all T, F, /\ and ==> results in bool.ml
up through MP, and added a "truth table" result
|- T ∧ T ⇔ T
***** 0) informal mathematics and HOL *****
The 10 primitive HOL Light inference rules are expressed as Ocaml functions
which take theorems to theorems, theorems being certain types of Ocaml objects
called sequents. My aim, then, is to try to describe the set of sequents using
the usual informal language of mathematics. The reference manual to a large
extent uses language of informal mathematics, e.g.
BETA_CONV : term -> thm
The conversion BETA_CONV maps a beta-redex `(\x.u)v` to the theorem
|- (\x.u)v = u[v/x]
It's only a small step from this to what I want, this informal mathematical
theorem:
Theorem:
For all variables x and for all terms u and v, we have the sequent
|- (\x.u)v = u[v/x]
I contend that there is a lot of clarity to be gained by discussing HOL in this
informal mathematics style, and I'll do so in section 5 below. We have to
careful, though, because the terms I used `for all' and `theorem' have formal
meanings in in HOL, and that's especially true for `='! Perhaps because of
these competing definitions of terms like `equality' attempts such as mine are
sometimes called `metamathematical', but I don't find that a helpful term.
***** 1) the type bool and the constant = *****
First, the type bool is declared in fusion.ml by the line which creates a
fresh Ocaml (mutable) reference the_type_constants which is a list of pairs (as
Ramana and Mark pointed out)
let the_type_constants = ref ["bool",0; "fun",2]
which means that bool is a type and fun takes two types as arguments and
returns a type. My guess is that fun is bound to -> in parser.ml in the line
let rec pretype i = rightbin sumtype (a (Resword "->")) (btyop "fun") "type" i
The type ind (explained to an abbreviation for Church's type of individuals in
a comment) is defined in nums.ml by
new_type ("ind",0);;
The function new_type is defined in fusion.ml to essentially add a new pair to
the reference the_type_constants. All new constants except = are created by the
function new_constant, which essentially conses a new constant to the mutable
reference list the_term_constants, which declares the first constant =:
let the_term_constants =
ref ["=",Tyapp("fun",[aty;Tyapp("fun",[aty;bool_ty])])]
We see this means that = has type A->A->bool from the fusion.ml code
let constants() = !the_term_constants
let bool_ty = Tyapp("bool",[])
let aty = Tyvar "A"
let mk_type(tyop,args) =
[...] Tyapp(tyop,args) [...]
let mk_vartype v = Tyvar(v)
and inspecting the Ocaml code below and the output:
# hd (rev (constants()));;
val it : string * hol_type = ("=", `:A->A->bool`)
# mk_vartype "A";;
val it : hol_type = `:A`
# mk_type("fun",[mk_vartype "A"; mk_type("fun",[mk_vartype "A";
mk_type("bool",[])])]);;
val it : hol_type = `:A->A->bool`
***** 2) sequents, new_basic_definition and the HOL Light inference rules *****
I'll explain how Tom Hales's compact description of the HOL Light inference
rules in his MS Notices article www.ams.org/notices/200811/tx081101370p.pdf is
found in this 545 line segment of the file fusion.ml
module Hol : Hol_kernel = struct
[...]
end;;
A theorem is an Ocaml object of type thm:
type thm = Sequent of (term list * term)
So a theorem is of the form Sequent ([a1;...;an], t), which we will write as
{a1,...,an} |- t
It will turn out that t will always have type bool.
Sequent is an Ocaml constructor of the OCaml type 'thm' declared in
the module Hol. Thus we have no way to produce theorems except by
sequent-producing functions defined in Hol, including
new_basic_definition, about which the reference manual says:
If t is a closed term and c a variable whose name has not been used as
a constant, then new_basic_definition `c = t` will define a new
constant c and return the theorem |- c = t for that new constant (not
the variable in the given term)
We can see the sequent being produced in the code
let new_basic_definition tm =
match tm with
Comb(Comb(Const("=",_),Var(cname,ty)),r) -> [...]
let dth = Sequent([],safe_mk_eq c r) [...]
We can also produce sequents is with the Hol module function new_axiom and
new_basic_type_definition.
The only other way to produce sequents is with 10 Hol module functions which
produce theorems from earlier theorems:
REFL, TRANS, MK_COMB, ABS, BETA, ASSUME, EQ_MP, DEDUCT_ANTISYM_RULE, INST_TYPE
and INST.
Here are the reference manual description of the 10 function,
with two corrections given by Hales, so
in TRANS, t2 and t2' are alpha-equivalent, and
in EQ_MP, t1 and t1' are alpha-equivalent.
Each reference manual description ends with
COMMENTS
This is one of HOL Light's 10 primitive inference rules.
REFL : term -> thm
Returns theorem expressing reflexivity of equality.
REFL maps any term `t` to the corresponding theorem |- t = t.
TRANS : thm -> thm -> thm
Uses transitivity of equality on two equational theorems.
A1 |- t1 = t2 A2 |- t2' = t3
------------------------------- TRANS
A1 u A2 |- t1 = t3
MK_COMB : thm * thm -> thm
Proves equality of combinations constructed from equal functions and operands.
A1 |- f = g A2 |- x = y
--------------------------- MK_COMB
A1 u A2 |- f x = g y
ABS : term -> thm -> thm
Abstracts both sides of an equation.
A |- t1 = t2
------------------------ ABS `x` [Where x is not free in A]
A |- (\x.t1) = (\x.t2)
BETA : term -> thm
Special primitive case of beta-reduction.
|- (\x. t[x]) x = t[x].
ASSUME : term -> thm
Introduces an assumption.
-------- ASSUME `t`
t |- t
EQ_MP : thm -> thm -> thm
Equality version of the Modus Ponens rule.
A1 |- t1' <=> t2 A2 |- t1
---------------------------- EQ_MP
A1 u A2 |- t2
DEDUCT_ANTISYM_RULE : thm -> thm -> thm
Deduces logical equivalence from deduction in both directions.
A |- p B |- q
----------------------------------
(A - {q}) u (B - {p}) |- p <=> q
INST_TYPE : (hol_type * hol_type) list -> thm -> thm
Instantiates types in a theorem.
A |- t
----------------------------------- INST_TYPE [ty1,tv1;...;tyn,tvn]
A[ty1,...,tyn/tv1,...,tvn]
|- t[ty1,...,tyn/tv1,...,tvn]
INST : (term * term) list -> thm -> thm
Instantiates free variables in a theorem.
A |- t
----------------------------------- INST_TYPE [t1,x1;...;tn,xn]
A[t1,...,tn/x1,...,xn]
|- t[t1,...,tn/x1,...,xn]
Bound variables will be renamed if necessary to avoid capture. All variables
are substituted in parallel, so there is no problem if there is an overlap
between the terms ti and xi.
We can see that Hales is correct about alpha-equivalence from the code, e.g.
let EQ_MP (Sequent(asl1,eq)) (Sequent(asl2,c)) =
match eq with
Comb(Comb(Const("=",_),l),r) when alphaorder l c = 0
-> Sequent(term_union asl1 asl2,r)
| _ -> failwith "EQ_MP"
alphaorder : term -> term -> int
returns 0 if and only if the two terms are alpha-convertible.
***** 3) the BETA_CONV proof of the general case of beta-conversion *****
The fusion.ml code for BETA clearly shows that
BETA (\v. bod) v) = (|- ((\v. bod) v) = bod)
In informal math, we say that for any abstraction (\v. bod), we have the
theorem
|- ((\v. bod) v) = bod
Applying INST [arg,v] to this theorem we have
|- ((\v. bod) arg) = bod[arg,v]
That's the general case of beta-conversion, for any abstraction (\v. bod) and
any term arg.
More formally, by definition of BETA_CONV in equal.ml,
BETA_CONV (\v. bod) arg = INST [arg,v] (|- ((\v. bod) v) = bod) =
(|- (\v. bod) arg) = bod[arg,v])
***** 4) the bool.ml definitions of ! (forall), <=> (iff), T (true), F (false),
/\ (and), ==> (implies), ~ (not), \/ (or) and ? (exists) *****
The binder !A->bool->bool is defined by
let FORALL_DEF = new_basic_definition
`(!) = \P:A->bool. P = \x. T`;;
We infer the type of ! from the fact that = has type A->A->bool. I believe the
definition of binder is that parser.ml will replace an expression
!x. body
for any term body:A->bool with
(!)(\x. body)
The infix <=> is defined to be = when both arguments have type bool by
override_interface ("<=>",`(=):bool->bool->bool`);;
The term T is are defined to have type bool by
let T_DEF = new_basic_definition
`T = ((\p:bool. p) = (\p:bool. p))`;;
Note a subtlety about = here which I messed up in a previous post. The first =
is the Ocaml =, meaning that T_DEF is bound in Ocaml to the value of the
new_basic_definition expression. Each of the other two =s are are instances of
the constant =, which has generic type A->A->bool. Therefore the RHS (\p:bool.
p) = (\p:bool. p) has type bool, and therefore T has type bool.
F is defined to have type bool by
let F_DEF = new_basic_definition
`F = !p:bool. p`;;
The infix /\:bool->bool->bool is defined by
let AND_DEF = new_basic_definition
`(/\) = \p q. (\f:bool->bool->bool. f p q) = (\f. f T T)`;;
because we infer the types of p and q from the type of f.
The infix ==> :bool->bool->bool is defined by
let IMP_DEF = new_basic_definition
`(==>) = \p q. p /\ q <=> p`;;
The prefix ~ is defined by
let NOT_DEF = new_basic_definition
`(~) = \p. p ==> F`;;
The infix \/:bool->bool->bool is defined by
let OR_DEF = new_basic_definition
`(\/) = \p q. !r. (p ==> r) ==> (q ==> r) ==> r`;;
The binder ?: A->bool->bool is defined by
let EXISTS_DEF = new_basic_definition
`(?) = \P:A->bool. !q. (!x. P x ==> q) ==> q`;;
so parser.ml will replace an expression
!x. body
for any term body:A->bool with
(?)(\x. body)
***** 5) An informal mathematical discussion of the type bool *****
The first thing we need is prove that |- ~(T <=> F), and to construct "truth
tables" for the functions ~, /\, \/ and ==>. A truth table for ~ means proving
the two theorems
|- ~F = T
|- ~T = F
This seems to be difficult, and is only accomplished in itab.ml, which defines
the prover ITAUT and the tactic ITAUT_TAC, and this requires tactics.ml,
drule.ml and bool.ml.
Then we need to prove
BOOL_CASES_AX;;
val it : thm = |- !t. (t <=> T) \/ (t <=> F)
This is only accomplished in class.ml, which requires additionally ind_defs.ml,
theorems.ml, simp.ml and the axioms select and extensionality axioms
SELECT_AX and ETA_AX.
As these matters appear hard to me, it seems useful to discuss them in the
usual informal mathematical style, and thus to try to prove informal
mathematical theorems about the set of sequents, or more precisely, some
mathematically defined set which represents sequents. Let's consider a
proto-sequent to be of the form
A |- t
where A is a finite set of terms of type bool, and t is a term of type bool.
Then the set of sequents is the subset of the set of proto-sequents which are
proved to be sequents by the various axioms that construct them.
I'll use the 10 theorems represented by the primitive inference function, and
call them axiom REFL, axiom TRANS, axiom MK_COMB, axiom ABS, axiom BETA, axiom
ASSUME, axiom EQ_MP, axiom DEDUCT_ANTISYM_RULE, axiom INST_TYPE and axiom INST.
In keeping with the informal mathematical style, I'll use the math characters
( ∅, ¬, ∧, ∨, ⇒, ⇔) allowed in HOL4, Isabelle, and readable.ml. So for
instance, our first theorem is
axiom REFL:
For any term t, we have the sequent
|- t = t
We'll engage in the informal mathematics practice of replacing p ∧ q with (∧) p
q, on the grounds that the parser replaces the first by the second. In
informal mathematics, this is justified as "replacing equals with equals", but
our HOL Light mission here is to investigate & formalize equality! So the real
reason we're allowed to replace p ∧ q with (∧) p q is that the parser performs
this replacement automatically. It takes alertness to make informal
mathematical arguments about the existence of formal axiomatic proofs
constructing sequents, but it's worth it for the clarity, the reduction in
notational clutter. Notice above that we can always replace p ∧ q with (∧) p
q, because the parser changes it automatically back. So we have proven the
principle that for all terms p and q of type bool, we can replace p ∧ q with
(∧) p q, and vice versa. Similar principles hold for the other infixes ∨, ⇒
and ⇔.
Similarly we can always replace ⇔:bool->bool->bool with =:bool->bool->bool,
because that's what the parser does because of our override_interface command.
But it resembles the informal mathematics "replacing equals with equals". Thus
we can always replace =:bool->bool->bool with ⇔:bool->bool->bool, as the parser
automatically replaces ⇔ with =. So we have proven a principle: for all terms
t1 and t2 of type bool, we can replace t1 ⇔ t2 with t1 = t2, and vice versa.
Let's first record our informal mathematical theorem BETA_CONV above:
Theorem BETA_CONV:
For any variable v and terms bod and arg, we have the sequent
|- ((\v. bod) arg) = bod[arg,v]
From the code of AP_TERM, AP_THM, SYM, ALPHA and ALPHA_CONV in equal.ml we
easily glean simple proofs of the four theorems
Theorem AP_TERM:
For all terms f, x and y and for all sequents
A |- x = y
we have the sequent
A |- f x = f y.
Proof:
By axiom REFL, we have the sequent
|- f = f.
Now apply axiom MK_COMB to this sequent and our assumption, noting that
A ∪ ∅ = A.
\qed
Theorem AP_THM:
For all terms f, g and x and for all sequents
A |- f = g
we have the sequent
A |- f x = g x.
Proof:
Apply axiom MK_COMB to our assumption and the axiom REFL sequent |- x = x.
\qed
Theorem SYM:
For all terms l and r and for all sequents
A |- l = r
we have the sequent
A |- r = l.
Proof:
For precision, let α be the type of l, which is also the type of r. Applying
=:α->α->bool to our assumption and using theorem AP_TERM, we have the sequent
A |- (= l) = (= r)
By axiom REFL we have the sequent
|- (l = l).
Applying axiom EQ_MP to these two sequents, we have the sequent
A |- (= l) l = (= r) l
since A ∪ ∅ = A. We rewrite this as the sequent
A |- (l = l) = (r = l).
By our REFL sequent above, axiom EQ_MP and A ∪ ∅ = A, we're done.
\qed
Theorem ALPHA:
For all terms tm1 and tm2 that are alpha-equivalent, we have the sequent
|- tm1 = tm2.
Proof:
Axiom REFL applied to tm1 and tm2 gives the sequents
|- tm1 = tm1
|- tm2 = tm2
We are done by axiom ALPHA.
\qed
The next result follows, which we note for completeness, immediately from
theorem ALPHA and the definition of alpha-equivalence, although below we will
only use theorem ALPHA.
Theorem ALPHA_CONV:
For any abstractions λx. t and any variable y of the same type as x which does
not occur free in t, we have the sequent
|- (λx. t) = (\y. t[y/x]).
Now we prove the first results of bool.ml.
Theorem TRUTH:
We have the sequent
|- T
Proof:
By T_DEF and new_basic_definition we have the sequent
|- T = ((λp:bool. p) = (λp:bool. p)).
By theorem SYM have the sequent
|- ((λp:bool. p) = (λp:bool. p)) = T.
By axiom REFL we have the sequent
|- (λp:bool. p) = (λp:bool. p)
Applying axiom EQ_MP to these two sequents, we are done.
\qed
Our next result follows immediately from theorem SYM, theorem TRUTH and axiom
EQ_MP.
Theorem EQT_ELIM:
For all terms tm and all sequents
A |- tm ⇔ T
we have the sequent
A |- tm.
The converse takes a little more work.
Theorem EQT_INTRO:
For all terms tm and all sequents
A |- tm
we have the sequent
A |- tm ⇔ T.
Proof:
By axiom ASSUME and theorem TRUTH we have the sequents
{tm} |- tm
|- T
so by axiom DEDUCT_ANTISYM_RULE we have the sequent
{tm} |- tm ⇔ T.
By axiom ASSUME applied to tm ⇔ T and theorem EQT_ELIM, we have the sequent
{tm ⇔ T} |- tm.
Applying axiom DEDUCT_ANTISYM_RULE to these "converse" sequents, we have the
sequent
|- tm ⇔ (tm ⇔ T)
Applying axiom EQ_MP to this and our assumption, we are done.
\qed
Note this gives a proof 2 lines shorter than the version in bool.ml
let EQT_INTRO th =
let th1 = DEDUCT_ANTISYM_RULE (ASSUME (concl th)) TRUTH in
let th2 = EQT_ELIM(ASSUME(concl th1)) in
let pth = DEDUCT_ANTISYM_RULE th2 th1 in
EQ_MP pth th;;
which I checked actually works.
Theorem CONJ:
For any two terms p and q of type bool with seqents
A1 |- t1
A2 |- t2,
we have the seqent
A1 ∪ A2 |- t1 ∧ t2
Proof:
Choose a variable fof type bool->bool->bool which is not free in t1 or t2.
By our assumptions and theorem EQT_INTRO, we have the sequents
A1 |- t1 ⇔ T
A2 |- t2 ⇔ T
Applying theorem AP_TERM with f to the first gives the sequent
A1 |- f t1 ⇔ f T
Applying axiom MK_COMB to this and the previous sequent yields
A1 ∪ A2 |- f t1 t2 ⇔ f T T
By axiom ABS, we have
A1 ∪ A2 |- (λf. f t1 t2) ⇔ (λf. f T T)
Apply theorem AP_TERM twice to the AND_DEF sequent
|- (∧) = λp q. (λf:bool->bool->bool. f p q) = (λf. f T T)
with the terms t1 and then t2 to obtain the sequent
|- (∧) t1 t2 = (λp q. (λf:bool->bool->bool. f p q) = (λf. f T T)) t1 t2
Applying theorem BETA_CONV twice and axiom TRANS twice, we have the sequent
|- t1 ∧ t2 = ((λf. f t1 t2) ⇔ (λf. f T T)).
By theorem SYM, axiom EQ_MP and our A1 ∪ A2 sequent above, we're done.
\qed
Theorems CONJ, TRUTH and EQT_INTRO immediately gives us our first AND "truth
table" result:
Theorem CONJ_EZ:
|- T ∧ T ⇔ T
The next two results comprise something of a converse of theorem CONJ, and rest
on the well-known LC facts that an ordered pair (x, y) can be implemented as
the abstraction (λf. f x y), and applying an ordered pair to (λp q. p) (resp.
(λp q. q)) gives the projection on the first (resp. 2nd) coordinate.
Theorem CONJUNCT1:
Let l and r be terms and A be a set of assumptions such that
A |- l ∧ r. Then A |- l.
Proof:
Since ∧ has type bool->bool->bool, l and r both have type bool.
By theorem ALPHA, the AND_DEF sequent and axiom TRANS, we have
|- (∧) = (λp' q'. (λf':bool->bool->bool. f' p' q') = (λf'. f' T T))
where f', p' and q' are not free in either l or r. Applying theorem AP_THM
twice to the AND_DEF sequent l, and r we have
|- (∧) l r = (λp' q'. (λf':bool->bool->bool. f' p' q') = (λf'. f' T T)) l r.
Applying theorem BETA_CONV and axiom TRANS twice to the RHS yields
|- l ∧ r = ((λf':bool->bool->bool. f' l r) = (λf'. f' T T)).
Since A |- l ∧ r by assumption, axiom EQ_MP yields the sequent
A |- (λf':bool->bool->bool. f' l r) = (λf'. f' T T)
Choose free variables p and q of type bool that are not free in l or r.
Applying AP_THM to this sequent equation and the term (λp q. p) yields
A |- (λf':bool->bool->bool. f' l r) (λp q. p) = (λf'. f' T T) (λp q. p).
Applying theorem BETA_CONV, axiom TRANS and theorem SYM a number of times, we
obtain the sequent
A |- l = T.
By theorem EQT_ELIM, we're done.
\qed
By the same argument using (λp q. q) instead (λp q. p), we have
Theorem CONJUNCT2:
Let l and r be terms and A be a set of assumptions such that
A |- l ∧ r. Then A |- r.
Now we turn to ⇒.
Theorem MP:
Given two terms t1 and t2, and two sets of assumptions A1 and A2, assume we
have sequents
A1 |- t1 ⇒ t2 and A2 |- t1.
Then we have the sequent
A1 ∪ A2 |- t2.
Proof:
Take the IMP_DEF sequent
|- (⇒) = (λp q. p ∧ q ⇔ p)
Choose variables of type bool p' and q' that are not free in either t1 or t2.
Then by axioms TRANS and REFL and performing the alpha-equivalence with [p'/p;
q'/q], we have
|- (⇒) = (λp' q'. p' ∧ q' ⇔ p')
Applying theorem AP_THM twice to this sequent, t1 and t2, we have
|- (⇒) t1 t2 = (λp' q'. p' ∧ q' ⇔ p') t1 t2.
Using theorem BETA_CONV and axiom TRANS twice each, we have
|- t1 ∧ t2 = (t1 ∧ t2 ⇔ t1).
By our assumption sequent, axiom MP and A ∪ ∅ = A, we have
A |- t1 ∧ t2 ⇔ t1.
By theorem EQT_INTRO and axiom TRANS, we have
A |- t1 ∧ t2 ⇔ T
and by theorem EQT_ELIM, we have
A |- t1 ∧ t2.
By theorem CONJUNCT2, we are done.
\qed
--
Best,
Bill
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
