Interactive Proof Assistents
(Thursdays, 14.0016.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.
Schedule

October 11th.
We saw the primitive deduction rules of HOLlight, we saw how to
prove commutativity of plus on blackboard.
We almost managed to prove in HOLlight 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 HOLlight 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" ;;

October 18th
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)

October 25th
Here are a few slides about the unification algorithm
and its verification.
ps or
pdf .

November 1st
Holiday.

November 8th
Here is the file with the
definitions and goals for unification.
Here is the corrected version .
(See below for an even correcter version)

November 15th
Another holiday.

November 22nd
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.

November 29th
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 ).
And:
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
of equations.
I proved that: The set of variables in a term, (or a system of equations)
is finite.

December 6th
Piotr Witkowski and Lukasz Stafiniak.

December 13th
I expect that we complete the proof around this time.
Here are updated versions of the slides
( ps or
pdf )
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.

December 18th
(replaces December 20th)
We have difficulties completing the proof of the correctness of
the unification algorithm.

January 8th
(Replaces January 3th)
The verification of the unification algorithm is complete!
Here is the complete proof.
Mizar
For Mizar, I found the following texts very useful:
An
Outline of PC Mizar ,
by Michal Muzalewski.
Mizar: An impression
by Freek Wiedijk,
and Mizar in 9 easy steps , probably by
Piotr Rudnicki.
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
extremely optimistic)
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 higherorder 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:

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 DPLLalgorithm for deciding propositional
logic.

Prove correctness of some data structure. (say an implementation
of priority queues, or redblack trees)

Set theoretic properties, like for example the equivalence of
the wellordering theorem and the axiom of choice, or the
the CantorBernstein 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.
You can choose another project as well.
I intend to use the following systems. If you want, other systems
can be also considered.
HOLlight
HOL stands for HigherOrder Logic.
(See the
homepage of the system
)
HOL is an abbreviation for HigherOrder Logic. It is welldocumented
and it offers a reasonable level of automation. Proofs can be constructed
interactively.
It is called light because it is derived
from an earlier system, developed by Mike Gordon, which apparently
was more complicated.
HOLlight is developed by John Harrison.
Mizar
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
,
see also
here )
The best documentation seems to be
here .
Mizar is based on GrothendieckTarski 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 texteditor.
After that, Mizar reads the text and reports the errors.
Coq
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 higherorder logic through the CurryHoward isomorphism.
The level of automation is lower than HOLlight's, but higher than Mizar's.
The system is welldocumented and the developers are working hard to
introduce more automation.
The homepage is
here .
(We will probably not have time to do any projects in Coq. I will
probably give only a short demonstration)