Reasoning with the HERMIT

Tool Support for Equational Reasoning on GHC Core Programs

Andrew Farmer - The University of Kansas
Neil Sculthorpe - Swansea University
Andy Gill - The University of Kansas


June 11, 2015

HERMIT

cabal update
cabal install hermit
image from http://www.angelfire.com/ks/larrycarter/LC/OldGuardCameron.html

Applications

HERMIT has previously been applied to a variety of transformational tasks:

What's New?

Previously, side- and pre-conditions were not captured.

Inductive reasoning was not supported.

Case Study: Proving Type-Class Laws

Type-class laws are properties expected to hold for class instances.

Example:

class Monad m where
  return :: a -> m a
  (>>=) :: m a -> (a -> m b) -> m b

The following three laws should hold for any instance of Monad:

return-left      return x >>= k == k x
return-right       k >>= return == k
bind-assoc      (j >>= k) >>= l == j >>= (\x -> k x >>= l)

If proven, these are typically proven by hand.

Case Study: Proving Type-Class Laws

As an example, prove the return-left law for lists using HERMIT.

Begin by creating a Haskell program containing the law as GHC rewrite rule.

module Laws where

main :: IO ()
main = return ()

{-# RULES "return-left" [~] forall k x. return x >>= k = k x #-}

Then invoke HERMIT on this file:

$ hermit Laws.hs

Case Study: Proving Type-Class Laws

The GHC rewrite rule can be turned into a HERMIT lemma.

Example Step 1

The monad type parameter can be instantiated to lists.

Example Step 2

Case Study: Proving Type-Class Laws

Begin the proof and instantiate the dictionary parameters.

Example Step 3

Rewrite return to a singleton list.

Example Step 4

Case Study: Proving Type-Class Laws

Appeal to two auxiliary lemmas to rewrite (>>=).

Auxilliary Lemmas 1

Example Step 5

Example Step 6

Case Study: Proving Type-Class Laws

Appeal to another auxiliary lemma to eliminate (++).

Auxilliary Lemmas 2

Example Step 7

Both sides are α-equivalent, so end the proof.

Example Step 8

Case Study: Proving Type-Class Laws

Comparing by-hand reasoning with the HERMIT script.

By-hand                             HERMIT
================================    =====================================================

                                    rule-to-lemma return-left
                                    copy-lemma return-left return-left-list
                                    inst-lemma return-left-list 'm [| [] |]
                                    prove-lemma return-left-list
                                    inst-dictionaries
  return x >>= k
    { definition of return }        { application-of 'return ; repeat (unfold <+ smash) }
= [x] >>= k
    { definition of >>= }           one-td (lemma-forward bind-left-cons)
= k x ++ ([] >>= k)
    { definition of >>= }           one-td (lemma-forward bind-left-nil)
= k x ++ []
    { xs ++ [] == xs }              one-td (lemma-forward append-right)
= k x

Case Study: Proving Type-Class Laws

Laws proven in the case study:

Type-class laws in study

Case Study: Proving Type-Class Laws

Length of proof scripts:

Length of proof scripts

Case Study: Proving Type-Class Laws

Case Study: Making a Century

pearls of functional algorithm design

Case Study: Making a Century

As an example, this property must be proved in the course of the study:

Lemma 6.2 Example Step 1

The proof begins by appealing to a more general lemma:

Filter Split Lemma

Lemma 6.2 Example Step 2

Case Study: Making a Century

Now unfold composition, and abstract the value x expression:

Lemma 6.2 Example Step 3

Lemma 6.2 Example Step 4

Case Study: Making a Century

Unfold both ok and good:

Lemma 6.2 Example Step 5

Case Study: Making a Century

Prove by cases (smash handles the undefined case):

Lemma 6.2 Example Step 6

Appeal to a lemma about integers from a library:

integer lemma

Lemma 6.2 Example Step 7

Case Study: Making a Century

Lemmas stated in textbook.