Supervisor

Suitable for

Abstract

What?

The purpose of this project would be to implement an interactive system to support the discovery (and pretty presentation) of equational proofs by a combination of “automatic choice” and human guidance. Richard Bird, acknowledging Mike Spivey’s unpublished work, sketched an implementation of the simplest form of such a “proof assistant” in Haskell in his most excellent book: Thinking Functionally with Haskell. The project would start by implementing a similar assistant with a convenient interactive workflow for discovering, recording, and checking proofs.

The tool should also support the use of appropriate induction rules derived automatically from data declarations.

An interesting challenge will be the provision of convenient methods for providing human guidance for the application of algebraic laws (such as associativity, commutativity, distributivity) at appropriate points in a proof. Although now somewhat long in the tooth, the Jape generic proof editor still provides (in its functional programming example theory) a working concrete example of the sort of guidance that could be used here, and a user interface by which such guidance can be communicated. Our slogan while building Jape (and many of its example theories) was “Proof by Pointing”. The Jape GitHub repository is here.

Equational Proofs

Many Haskell proofs take the form of straightforward equational rewriting using definitions or derived laws left-to-right as rules. Typically the discovery of a proof of

    lhs = rhs

will take the form

     lhs
    = { rule name
     lhs1
    = { rule name
     lhs2
    .
     lhsn
    = { rule name}
    crux        

followed by

     rhs
    = { rule name
     rhs1
    = { rule name
     rhs2
    ...
     rhsm
    = { rule name
    crux

Where crux is the common term to which both sides can be reduced. This style of presentation relies implicitly on the transitivity of equality.

Aside: it is annoying that some authors obfuscate these sensible discovery steps by a linearised presentation “as if” the post-crux proof had been discovered by using rules ``right to left’’

    ...
    crux
    = { rule name
     rhsm
    = { rule name
    ...
     rhs2
    = { rule name
     rhs1
    = { rule name
     rhs

In our experience such presentations can be pedagogically harmful.

Sometimes the choice of rule at each stage is almost automatic: “pretend you are the Haskell interpreter”. At other times firm human guidance (and/or the invention of lemmas) is needed. For example, a proof of

    (rev * rev) . swap . (rev * rev) . swap
   =
   ...
   =
   id

in the presence of laws/definitions

    rev . rev     = id
    swap(y,z)     = (z,y)
    (f * g)(y, z) = (f x, g y)

can use the lemmas

    swap . (f*g) . swap = g*f
    (f * g) . (h *j) = (f . h) * (g . j)

as well as timely invocation of the associativity of composition.