How to prove this Haskell code using equational reasoning

Question

I found this exercise on equational reasoning and proofs in Haskell. The following code is given:

type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | ADD
deriving (Show)
--
-- Stack machine
--
exec :: Code -> Stack -> Stack
exec [ ] s = s
exec (PUSH n : c) s = exec c (n:s)
exec (ADD:c) (m:n:s) = exec c (n+m : s)
--
-- Interpeter
--
data Expr = Val Int | Add Expr Expr
deriving (Show)
eval :: Expr -> Int
eval (Val n) = n
eval (Add x y) = eval x+eval y
--
-- Compiler
--
comp :: Expr -> Code
comp (Val n) = [PUSH n]
comp (Add x y) = comp x ++ comp y ++ [ADD]

Now I have to prove that exec(comp e) s = eval e : s.

So I found this answer so far:

We have to prove that exec (comp e) s = eval e : s.

First case: Assume e = (Val n). Then comp (Val n) = [PUSH n], so we have to prove that exec ([PUSH n]) s = eval ([PUSH n] : s). We find that exec ([PUSH n]) s = exec [] (n:s) = (n:s) using the function definition of exec.

Now eval (Val n) : s = n : s. The first case is OK!

Second case: Assume e = (Add x y). Then comp (Add x y) = comp x ++ comp y ++ [ADD].

But now I'm struggling with this recursive use of comp. Should I be using some form of trees and induction on these trees to prove this? I'm not completely sure how to do that.

note that you are missing one line in exec _ [] = error "ADD applied to an empty or singleton stack" — epsilonhalbe
You will probably need a lemma about exec - in particular you have exec (a ++ b) s = exec b (exec a s). This would allow you write exec (comp x ++ comp y ++ [ADD]) as exec [ADD] (exec (comp y) (exec (comp x))) — user2407038

ErikR ErikR · Accepted Answer · 2016-05-31T14:47:26

When the first argument to exec is a list, the two possibilities are:

exec (PUSH n: codes)  -- #1
exec (ADD   : codes)  -- #2

In the induction step you get to assume that the proposition holds for codes, i.e. you may assume:

exec codes s = eval codes : s

for any value of s -- Keep this in mind - this is usually the key step in any induction proof.

Start by expanding #1 using the code you've written for exec:

exec (PUSH n: codes) s == exec codes (n:s)
                       == ...
                       == ...
                       == eval (PUSH n: codes) : s

Can you see a place to use the induction hypothesis?

How to prove this Haskell code using equational reasoning

1 Answers