# 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.

## Schedule

• #### October 11th.

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" ;;

• #### 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 .

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 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:

• 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 logic.
• 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.
You can choose another project as well. I intend to use the following systems. If you want, other systems can be also considered.

## HOL-light

HOL stands for Higher-Order Logic. (See the 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 interactively. 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

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 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.

## 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 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 here . (We will probably not have time to do any projects in Coq. I will probably give only a short demonstration)