compiler correctness for addition language

Comp.agda

module Comp where

open import Data.List
  using (List; []; _∷_; _++_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)
open import Data.Nat
  using (ℕ; _+_)
open import Data.List.Properties
  using (++-assoc; ++-identityʳ)
open import Data.Nat.Properties
  using (+-comm)

data Expr : Set where
  Val : ℕ -> Expr
  Add : Expr -> Expr -> Expr

data Instr : Set where
  PUSH : ℕ -> Instr
  ADD  : Instr

eval : Expr -> ℕ
eval (Val n) = n
eval (Add e1 e2) = (eval e1) + (eval e2)

stack : Set
stack = List ℕ

compile : Expr -> List Instr
compile (Val n) = PUSH n ∷ []
compile (Add e1 e2) = compile e1 ++ compile e2 ++ (ADD ∷ [])

exec : List Instr -> stack -> stack
exec (PUSH x ∷ ls) s = exec ls (x ∷ s)
exec (ADD ∷ ls) (s1 ∷ s2 ∷ s) = exec ls (s1 + s2 ∷ s)
exec l s = s

compile-hom
  : ∀ (e : Expr) (is : List Instr) (st : stack)
  → exec (compile e ++ is) st ≡ exec is (eval e ∷ st)
compile-hom (Val n) is st = refl
compile-hom (Add e1 e2) is st 
  rewrite ++-assoc (compile e1) (compile e2 ++ ADD ∷ []) is
  with compile-hom e1 ((compile e2 ++ ADD ∷ []) ++ is) st 
... | c-e1 rewrite c-e1
  rewrite ++-assoc (compile e2) (ADD ∷ []) is 
  with compile-hom e2 (ADD ∷ is) (eval e1 ∷ st)
... | c-e2 rewrite c-e2 | +-comm (eval e2) (eval e1) = refl

comp-correctness : ∀ (e : Expr) -> exec (compile e) [] ≡ eval e ∷ []
comp-correctness e 
  with compile-hom e [] []
... | ind rewrite ++-identityʳ (compile e) = ind