A simple proof checker for teaching

For the last few years I have been teaching functional programming to first year students. One of the main benefits of using functional programming is that you can prove simple, but non-trivial, properties of simple programs, for example, that the empty list is right-neutral for append:

append xs [] = xs

The practical problem with teaching a large group of students is that you end up with a large pile of assignments to check, which means a large number of teaching assistants of various degrees of competence in reading and understanding proofs. Note that for programming assignments we didn’t have this problem because we could use automated random unit testing. Pedagogically, having inconsistent marking standards is not only irritating to students but potentially devastating in the final exam if TAs habitually accept wrong proofs as correct in the assignments. The final exam is marked by me, and I may not be as blind to mistakes.

One possibility is to use proof assistants such as Coq, Agda or Isabelle, but they are a bit too intricate for first year students who are just learning the basics of proofs, logic, recursion and induction. What we want is a proof checker tailored to the needs of the beginning student. These were our design principles:

  1. The syntax of production-level proof assistants aims for concision, elegance and expressiveness. Our aim was a syntax that matched as much as possible the informal mathematical vernacular that students are used to from pen-and-paper proofs.
  2. Production-level proof assistants have various levels of interaction and automation which are not only useless to the beginning student but actively get in the way of learning proof techniques because they may encourage a trial-and-error approach to proofs. Also, very simple fragments such as pure propositional may be entirely automated in such proof assistants.
  3. Even production-level proof assistants can be annoyingly clumsy when it comes to writing equational proofs. However, most of the proofs that we ask our students are equational. Doing congruence reasoning comes very easy to students, but doing it in proof assistants formally is a pain. This aspect is something we wanted automated.
  4. We also need a generally high level of user-friendliness.

The source code, documentation and a range of examples from the simplest to moderately complicated are available on Github. Here I am just going to give the proof for the very simple example above. If you find it appealing I recommend you read the full documentation on-line.

Signatures:
append : 'a list -> 'a list -> 'a list ;
Definitions:
[append nil]: forall xs:'a list.
              append [] xs = xs : 'a list ;
[append ys]:  forall xs:'a list. forall ys:'a list. forall y:'a.
              append (y::ys) xs = y :: append ys xs : 'a list ;
Theorem [append neutral]:
Statement: forall xs:'a list.
           append xs [] = xs :'a list 
Proof: by induction on list :
case []:
 we know [0]: append [] [] = [] :'a list
              because [append nil] with ([]) .
 by [0]
case (hd :: tl):
 [IH]: append tl [] = tl : 'a list .
 we know [1]: append (hd :: tl) [] = hd :: (append tl []) :'a list
              because [append ys] with ([], tl, hd) .
 we know [2]: append (hd :: tl) [] = hd :: tl : 'a list
              because equality on ([1], [IH]) .
 by [2]
QED.

A comparison with the Agda equivalent is perhaps a good illustration of our trading off succinctness for readability. Note especially the need for an explicit congruence principle in the Agda proof. The list data type and append (++) are pre-defined. (Coq is not really comparable because it is tactics-based.)

cong-∷ : {A : Set} → (x : A) → ∀ xs ys → xs ≡ ys → x ∷ xs ≡ x ∷ ys
cong-∷ x xs .xs refl = refl
unitr[] : {A : Set} → (xs : List A) → xs ++ [] ≡ xs
unitr[] [] = refl
unitr[] (x ∷ xs) = Goal where
 p : xs ++ [] ≡ xs
 p = unitr[] xs 
 Goal : x ∷ (xs ++ []) ≡ x ∷ xs
 Goal = cong-∷ x (xs ++ []) xs p

The author of the tool is my intern student Yu-Yang Lin, with essential supervision and help from Neel Krishnaswami. Funding for the project was provided by the College of Engineering and Physical Science, University of Birmingham.

Your feedback is most welcome! Even more welcome are more examples, bug reports and bug fixes. If you are looking to make a more substantial contribution, parsing errors could be vastly improved.

About Dan Ghica

Reader in Semantics of Programming Languages // University of Birmingham // https://twitter.com/danghica // https://www.facebook.com/dan.ghica
This entry was posted in General. Bookmark the permalink.

Leave a Reply

Your email address will not be published. Required fields are marked *

*

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>