Interactive Proof Assistents

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 .

• 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

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

HOL-light

Mizar

Coq