Interactive Proof Assistents
(Thursdays, 14.00-16.00, room 140)
Although it is called seminar, it will not be a seminar
in the usual sense. The goal is that we get acquainted with systems for
formal proof verification mostly by practicing. We will probably read some
papers as well, but the emphasis is on practice.
We saw the primitive deduction rules of HOL-light, we saw how to
prove commutativity of plus on blackboard.
We almost managed to prove in HOL-light that
! (y:nat). y = ( plus y zero ) ;;
Here is the complete proof.
The main reasoning operations, when searching for a proof,
are MATCH_MP_TAC, and ASSUME_TAC.
MATCH_MP_TAC corresponds to backward reasoning.
If you have goal A1,....,Ap :- B, and a theorem th of form
C1 -> C2 -> ... -> B' s.t. B' can be matched into B,
then e( MATCH_MP_TAC th ) finds the right instance, and replaces
the goal A1, ..., Ap :- B by the list of goals
A1, ..., Ap :- C1, ..., A1, ..., Ap :- Cn.
ASSUME_TAC proceeds by forward reasoning.
If you have goal A1 ..., Ap :- B, and a theorem th of form
A'1 ..., A'p :- C, where all A'i are among the Aj, then
e( ASSUME_TAC th ) replaces the goal by
A_1, ..., A_p, C :- B.
The example in class failed because the equality 'a = plus a zero' could
not be used as rewrite rule.
The theorem reverse_unpleant_assumption proves
' a = plus a zero :- plus a zero = a. '
Using ASSUME_TAC adds the conclusion to the premisses, after which
rewriting can be used.
There is a much deeper lesson to be learnt from this:
Always formulate your theorems in such a way that they can be used
as rewrite rules. Instead of ! y. y = plus y zero, we should have proven
! y. plus y zero = y.
Homework for the next time, is to prove lemma1 in the right direction,
and to prove lemma2:
! x y . ( plus x ( succ y )) = ( succ ( plus x y )).
Installing HOL-light is easy. Download the file, unzip, untar,
type make and follow the instructions in README.
ocaml is already installed in room 137.
Starting the system in room 137 takes app. 5 minutes.
(But at least you can read what the system is doing)
In order to redo the proof of the lecture, type
#use "pluscom.ml" ;;
We practiced in room 137, proving elementary properties of addition,
times, and comparison of natural numbers.
We democratically decided that we will collectively
verify the correctness of the standard algorithm for term unification.
(at least I did not notice any objections)
Here are a few slides about the unification algorithm
and its verification.
Here is the file with the
definitions and goals for unification.
Here is the corrected version .
(See below for an even correcter version)
Marek Materzok proved that: If V does not occur n t, then
( V := t ) is the most general unifier of the equation
V = t.
And: If V does occur in t, but is not equal to t, then
the equation V = t has no unifiers.
Here are the slides of his presentation.
Maciej Pirog proved that: If two systems of equations have the same
unifiers, then they have the same most general unifiers.
Here is an explanation of his proofs.
Maciej Pirog proved that: If V does not occur in t, then
for a system of equations sys,
Varset( sys [ V := t ] ) isstrictsubsetof Varset( sys ).
Card( Varset( sys [ V := t ] )) < Card( Varset( sys )).
I proved that: apply( t, comp( subst1, subst2 )) =
apply( apply( t, subst1 ), subst2 ), and the same for systems
I proved that: The set of variables in a term, (or a system of equations)
Piotr Witkowski and Lukasz Stafiniak.
I expect that we complete the proof around this time.
Here are updated versions of the slides
( ps or
And here is an updated version
of the file unification.ml.
It turned out that nobody did his homework, so we had a short session.
(replaces December 20th)
We have difficulties completing the proof of the correctness of
the unification algorithm.
(Replaces January 3th)
The verification of the unification algorithm is complete!
Here is the complete proof.
For Mizar, I found the following texts very useful:
Outline of PC Mizar ,
by Michal Muzalewski.
Mizar: An impression
by Freek Wiedijk,
and Mizar in 9 easy steps , probably by
I propose that we verify the
following text in Mizar,
about differences and summations.
(Below you can read the original schedule of the seminar, which was
The first half (say 6 lectures) will be used for getting acquainted
with the system and with the underlying logical principles.
I will introduce some theory, (inductive data types, recursion,
some lambda calculus and higher-order logic)
and we try to make some small formalizations in the selected systems.
For example, we introduce the natural numbers, addition, multiplication,
and we try to prove some standard properties of those,
like commutativity, associativity, and distributivity.
For the second half of the seminar, each student should choose a
bigger verification project and a system in which he wants to carry
out this project.
The projects can also be made in groups (of say 2 persons)
Possible projects are:
You can choose another project as well.
I intend to use the following systems. If you want, other systems
can be also considered.
Introduce the natural numbers, the Euclidean algorithm, and
prove unique prime decomposition.
Introduce terms, and prove the existence of most general unifiers.
Prove the correctness of Robinson's algorithm for computing the
most general unifier.
Prove the correctness of the DPLL-algorithm for deciding propositional
Prove correctness of some data structure. (say an implementation
of priority queues, or red-black trees)
Set theoretic properties, like for example the equivalence of
the well-ordering theorem and the axiom of choice, or the
the Cantor-Bernstein theorem.
If you want, you may also try to write your own verifier, but keep
in mind that the time is quite short, and that you should also
be able to verify something in it. However, if you use prolog,
or ocaml, you have a chance of success.
HOL stands for Higher-Order Logic.
homepage of the system
HOL is an abbreviation for Higher-Order Logic. It is well-documented
and it offers a reasonable level of automation. Proofs can be constructed
It is called light because it is derived
from an earlier system, developed by Mike Gordon, which apparently
was more complicated.
HOL-light is developed by John Harrison.
Mizar is a Polish construction. It is called after a
star in Ursa Major which is only 78 light years away.
(When the light that you see now left the star, Ul. Joliot Curie was still
called Uferstrasse. You will probably never see the arrival of the
light that is departing now)
The system was initiated by Andrzej Trybulec in Bialystok in 1973.
(See here for the
homepage of the system
The best documentation seems to be
Mizar is based on Grothendieck-Tarski set theory.
My first impression from studying the documentation is that
understanding this system is going to be quite a challenge, but
some impressive formalizations have been made in it, so we should try.
The system offers no support in constructing the proofs. It is a batch
system. This means that the user has to type the proof in a text-editor.
After that, Mizar reads the text and reports the errors.
The name probably derives from Thierry Coquand and coq (rooster), which
is kind of a French national symbol. Another possibility is that it
means 'calculus of constructions (qonstructions?)' The system implements
intuitionistic higher-order logic through the Curry-Howard isomorphism.
The level of automation is lower than HOL-light's, but higher than Mizar's.
The system is well-documented and the developers are working hard to
introduce more automation.
The homepage is
(We will probably not have time to do any projects in Coq. I will
probably give only a short demonstration)