I want to explain how to read the HOL Light basics from the source code in
several sections
0) colloquial (informal) math and HOL
1) the definitions of 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.
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 got as far as explaining CONJ, which easily gives a "truth table"
result
|- T ∧ T ⇔ T
***** 0) colloquial (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. One normally discusses these functions in the language of
informal mathematics. For instance, the reference manual describes the
non-primitive inference rule as
BETA_CONV : term -> thm
The conversion BETA_CONV maps a beta-redex `(\x.u)v` to the theorem
|- (\x.u)v = u[v/x]
In informal mathematics, one would phrase this as:
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. However, from
the perspective of thinking of HOL as mathematical foundations, such informal
mathematics makes no sense. Note my use of `For all' in the `Theorem' above.
In informal mathematics we think we know what `for all' and `theorem' mean, but
in HOL, we're trying to carefully define their meanings! Nonetheless, for
parts of HOL that are hard to understand, an informal mathematical style may be
quite helpful. One might even say that the reference manual is written in this
informal mathematical style. And I find boolean matters such as the truth
table for AND and the law of the excluded middle hard to understand.
***** 1) the definitions of type bool and the constant = *****
First, the type bool is defined 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 defines 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 description of HOL Light inference rules is found
in this 545 line segment of the file fusion.ml
module Hol : Hol_kernel = struct
[...]
end;;
Similar code is found in the 150 line segment of the file thm.ml
module Hol : Hol_thm_primitives = struct
[...]
end;;
but I won't discuss this. My guess is that the fusion.ml definitions are used
first for some basic theorem and then the thm.ml definitions are used for more
sophisticated or faster handling of theorems.
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 defined 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) [...]
Another way to produce sequents is with the Hol module function
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 is the constants =
of 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`;;
I think the parser treats prefixes in a special way, but I'm not sure what it
is.
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, I'll adopt an informal mathematical style,
and 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. 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]
AP_TERM, AP_THM and SYM of equal.ml give simple proofs of
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. By the parser.ml definition of the infix =, we have the
sequent
A |- (l = l) = (r = l).
By our REFL sequent above, axiom EQ_MP and A ∪ ∅ = A, we're done.
\qed
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 gives us our first AND "truth table"
result:
Theorem CONJ_EZ:
|- T ∧ T ⇔ T
--
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
