Download HOL Light Tutorial PDF

TitleHOL Light Tutorial
LanguageEnglish
File Size766.3 KB
Total Pages231
Document Text Contents
Page 1

HOL Light Tutorial (for version 2.10)

John Harrison
Intel JF1-13

[email protected]

December 14, 2005

Abstract

The HOL Light theorem prover can be difficult to get started with. While
the manual is fairly detailed and comprehensive, the large amount of background
information that has to be absorbed before the user can do anything interesting is
intimidating. Here we give an alternative ‘quick start’ guide, aimed at teaching
basic use of the system quickly by means of a graded set of examples. Some
readers may find it easier to absorb; those who do not are referred after all to the
standard manual.

“Shouldn’t we read the instructions?”
“Do I look like a sissy?”

Calvin & Hobbes, 19th April 1988

1

Page 2

Contents

1 Installation 5
1.1 Cygwin . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.2 OCaml . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3 HOL Light . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 Checkpointing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.5 Other versions of HOL . . . . . . . . . . . . . . . . . . . . . . . . . 9

2 OCaml toplevel basics 10

3 HOL basics 12
3.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3.2 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.3 Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14
3.4 Derived rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16

4 Propositional logic 17
4.1 Proving tautologies . . . . . . . . . . . . . . . . . . . . . . . . . . .19
4.2 Low-level logical rules . . . . . . . . . . . . . . . . . . . . . . . . . 21
4.3 Logic design and veri�cation . . . . . . . . . . . . . . . . . . . . . . 22

5 Equations and functions 24
5.1 Curried functions . . . . . . . . . . . . . . . . . . . . . . . . . . . .26
5.2 Pairing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5.3 Equational reasoning . . . . . . . . . . . . . . . . . . . . . . . . . .28
5.4 De�nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

6 Abstractions and quanti�ers 31
6.1 Quanti�ers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6.2 First-order reasoning . . . . . . . . . . . . . . . . . . . . . . . . . .35

7 Conversions and rewriting 37
7.1 Conversionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .38
7.2 Depth conversions . . . . . . . . . . . . . . . . . . . . . . . . . . . .39
7.3 Matching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
7.4 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

8 Tactics and tacticals 44
8.1 The goalstack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .45
8.2 Inductive proofs about summations . . . . . . . . . . . . . . . . . . .52

9 HOL’s number systems 54
9.1 Arithmetical decision procedures . . . . . . . . . . . . . . . . . . . .56
9.2 Nonlinear reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . .58
9.3 Quanti�er elimination . . . . . . . . . . . . . . . . . . . . . . . . . . 61

2

Page 115

In addition,wp must distribute over conjunction and disjunction. The former must
hold even for a nondeterministic programming language, but for the latter determinism
is essential:

let WP_DISJUNCTIVE = prove
(‘(wp c p) UNION (wp c q) = wp c (p UNION q)‘,

REWRITE_TAC[FUN_EQ_THM; IN; wp; wlp; IN_ELIM_THM; UNION; terminates] THEN
MESON_TAC[DETERMINISM]);;

One can obtain explicit expressions for the weakest preconditions of commands.
For example, attractively, the weakest precondition of a sequence of commands is just
the composition of the two weakest preconditions of the components:

let WP_SEQ = prove
(‘!c1 c2 q. wp (c1 ;; c2) = wp c1 o wp c2‘,

REWRITE_TAC[wp; wlp; terminates; FUN_EQ_THM; o_THM] THEN REPEAT GEN_TAC THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [sem_CASES] THEN
REWRITE_TAC[injectivity "command"; distinctness "command"] THEN
MESON_TAC[DETERMINISM]);;

16.4 Axiomatic semantics

We can now return to the prototypical programming problem. We are supposed to
produce a programc guaranteeing some predicateq on the output state given an as-
sumptionp on the input state. We can say that a command is a valid solution to this
problem precisely if the input predicatep is contained in the weakest precondition for
q:

let correct = new_definition
‘correct p c q <=> p SUBSET (wp c q)‘;;

This leads us to yet another approach to the semantics of programming languages,
developed by Hoare (1969) from related work by Floyd (1967). Rather than aim at
explicit statements about the state transition relations resulting from commands, we
simply state rules that allow us to deduce valid ‘Hoare triples’correct p c q ,
more usually written informally asp {c} q or {p} c {q}. We can derive a suitable set
of rules directly from our existing semantic definitions, rather than postulate them from
scratch. Two of the simplest rules areprecondition strengthening(we can assume a
stronger precondition than necessary) andpostcondition weakening(we will guarantee
a weaker postconditon than any that we can deduce):

let CORRECT_PRESTRENGTH = prove
(‘!p p’ c q. p SUBSET p’ /\ correct p’ c q ==> correct p c q‘,

REWRITE_TAC[correct; SUBSET_TRANS]);;

let CORRECT_POSTWEAK = prove
(‘!p c q q’. correct p c q’ /\ q’ SUBSET q ==> correct p c q‘,

REWRITE_TAC[correct] THEN MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;

Similarly, we can quite easily derive the usual Hoare rule for sequences:

let CORRECT_SEQ = prove
(‘!p q r c1 c2.

correct p c1 r /\ correct r c2 q ==> correct p (c1 ;; c2) q‘,
REWRITE_TAC[correct; WP_SEQ; o_THM] THEN
MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;

115

Page 116

We will develop these ideas more in the next section in a slightly different context.

17 Shallow embedding

In the previous section we explicitly de�ned the syntax of a programming language
and its semantic map within HOL. The syntactic constructs and their meanings were
quite different things, with the semantic map mediating between them. A contrasting
approach is to regard a programming language as merely a notation for describing that
semantics directly. For example, an assignment statement x := e does not denote
a syntactic object, but rather is a shorthand for, say, a state mapping, state transition
relation or weakest precondition that we associate with it.

This approach, and indeed the embedding of programming language semantics in
theorem provers generally, was pioneered by Gordon (1989), the inventor of the orig-
inal HOL. For some time it was known as semantic embedding, and the fullblown
formalization of the semantic map as syntactic embedding. However, since Boulton,
Gordon, Gordon, Harrison, Herbert, and Van Tassel (1993) the customary terminology
has been to describe the formalization of the syntax and the semantic map (as in the
previous section) as deep embeddingand the direct semantic embedding as shallow
embedding.

It is worth noting that shallow embedding provides a natural formalization of the at-
titudes expressed by Dijkstra (1976), where a �programming language� (he deprecates
the very term) is viewed as an algorithmically-oriented system of mathematical nota-
tion �rst and foremost. Such a notation is meaningful in isolation from any particular
implementation, and indeed the role of a real programming language compiler on a real
machine is to provide a suf�ciently close approximation to the abstract mathematical
counterpart. (Perhaps, for example, imposing some limitations on sizes of integers.)

17.1 State and expressions

Crudely speaking, to move from a deep to a shallow embedding we want to keep the
same basic theorems as in the deep embedding but with the semantic maps value and
sem erased. Expressions are now simply mappings from states to values. Commands
are just their weakest preconditions. (We could use various other direct semantic no-
tions, but this one �ts best with our future plans � see Dijkstra and Scholten (1990)
for some discussion of this point.)

The syntax of expressions in our deep-embedded language was somewhat restricted:
we only had one type, that of natural numbers, and we had to consider it as a Boolean
using C-style hacking. These restrictions were mainly for technical simplicity: we
could have considered a much wider variety of types and operators. But then the
statements and proofs, while still straightforward conceptually, begin to suffer from
a proliferation of cases. In a shallow embedding, there’s nothing to stop us using quite
arbitrary HOL expressions, even noncomputable ones, and we never need to settle on a
�xed repertoire of types and operators at the outset. Of course, this has the apparently
undesirable feature that one can write ‘programs’ that do not correspond to executable

116

Page 230

Parrilo, P. (2001) Semide�nite programming relaxations for semialgebraic
problems. Available from the Web at citeseer.nj.nec.com/
parrilo01semidefinite.html .

Paulson, L. C. (1983) A higher-order implementation of rewriting. Science of Com-
puter Programming, 3, 119�149.

Paulson, L. C. (1987) Logic and computation: interactive proof with Cambridge LCF,
Volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge Uni-
versity Press.

Peres, A. (1991) Two simple proofs of the Kochen-Specker theorem. Journal of
Physics, A24, 175�178.

Ridge, T. (2005) A mechanically veri�ed, ef�cient, sound and complete theorem
prover for �rst order logic. Available via http://homepages.inf.ed.ac.
uk/s0128214/ .

Rivest, R. L., Shamir, A., and Adelman, L. M. (1978) A method for obtaining digital
signatures and public-key cryptosystems. Journal of the ACM, 21, 120�126.

Rudnicki, P. (1987) Obvious inferences. Journal of Automated Reasoning, 3, 383�393.

Rudnicki, P. (1992) An overview of the MIZAR project. Available on the Web as
http://web.cs.ualberta.ca/˜piotr/Mizar/MizarOverview.ps .

Russell, B. (1919) Introduction to mathematical philosophy. Allen & Unwin.

Scott, D. (1993) A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical
Computer Science, 121, 411�440. Annotated version of a 1969 manuscript.

Scott, D. and Strachey, C. (1971) Toward a mathematical semantics for computer lan-
guages. Programming Research Group Technical Monograph PRG-6, Oxford Univ.
Computing Lab.

Slind, K. (1991) An implementation of higher order logic. Technical Report 91-419-
03, University of Calgary Computer Science Department, 2500 University Drive N.
W., Calgary, Alberta, Canada, TN2 1N4. Author’s Masters thesis.

Slind, K. (1997) Derivation and use of induction schemes in higher-order logic. In
Gunter, E. L. and Felty, A. (eds.), Theorem Proving in Higher Order Logics: 10th
International Conference, TPHOLs'97, Volume 1275 of Lecture Notes in Computer
Science, Murray Hill, NJ, pp. ?�? Springer-Verlag.

Smullyan, R. M. (1992) Gödel's Incompleteness Theorems, Volume 19 of Oxford Logic
Guides. Oxford University Press.

Soko�owski, S. (1983) A note on tactics in LCF. Technical Report CSR-140-83, Uni-
versity of Edinburgh, Department of Computer Science.

230

Page 231

Solovay, R. M. (1976) Provability interpretations of modal logic. Israel Journal of
Mathematics, 25, 287�304.

Stickel, M. E. (1988) A Prolog Technology Theorem Prover: Implementation by an
extended Prolog compiler. Journal of Automated Reasoning, 4, 353�380.

Tarski, A. (1936) Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philo-
sophica, 1, 261�405. English translation, ‘The Concept of Truth in Formalized
Languages’, in Tarski (1956), pp. 152�278.

Tarski, A. (1955) A lattice-theoretical �xpoint theorem and its applications. Paci�c
Journal of Mathematics, 5, 285�309.

Tarski, A. (ed.) (1956) Logic, Semantics and Metamathematics. Clarendon Press.

Trybulec, A. and Blair, H. A. (1985) Computer aided reasoning. In Parikh, R. (ed.),
Logics of Programs, Volume 193 of Lecture Notes in Computer Science, Brooklyn,
pp. 406�412. Springer-Verlag.

Wiedijk, F. (2001) Mizar light for HOL Light. In Boulton, R. J. and
Jackson, P. B. (eds.), 14th International Conference on Theorem Prov-
ing in Higher Order Logics: TPHOLs 2001, Volume 2152 of Lecture
Notes in Computer Science, pp. 378�394. Springer-Verlag. Online at
http://link.springer.de/link/service/series/0558/tocs/t2152.htm .

Winskel, G. (1993) The formal semantics of programming languages: an introduction.
Foundations of computing. MIT Press.

Wos, L. (1998) Programs that offer fast, �awless, logical reasoning. Communications
of the ACM, 41(6), 87�102.

Wos, L. and Pieper, G. W. (1999) A Fascinating Country in the World of Computing:
Your Guide to Automated Reasoning. World Scienti�c.

Wright, J. v., Grundy, J., and Harrison, J. (eds.) (1996) Theorem Proving in Higher
Order Logics: 9th International Conference, TPHOLs'96, Volume 1125 of Lecture
Notes in Computer Science, Turku, Finland. Springer-Verlag.

Wright, J. v., Hekanaho, J., Luostarinen, P., and Langbacka, T. (1993) Mechanizing
some advanced re�nement concepts. Formal Methods in System Design, 3, 49�82.

231

Similer Documents