Как доказать этот код на Haskell с помощью эквациональных рассуждений

Question

Я нашел это упражнение на уравнительных рассуждениях и доказательствах в Хаскеле. Дан следующий код:

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]

Теперь я должен доказать, что exec(comp e) s = eval e : s,

Так что я нашел этот ответ до сих пор:

Мы должны доказать это exec (comp e) s = eval e : s,

Первый случай: предположим e = (Val n), затем comp (Val n) = [PUSH n]Таким образом, мы должны доказать, что exec ([PUSH n]) s = eval ([PUSH n] : s), Мы находим, что exec ([PUSH n]) s = exec [] (n:s) = (n:s) используя определение функции exec.

Сейчас eval (Val n) : s = n : s, Первый случай в порядке!

Второй случай: предположим e = (Add x y), затем comp (Add x y) = comp x ++ comp y ++ [ADD],

Но сейчас я борюсь с этим рекурсивным использованием комп. Должен ли я использовать какую-то форму деревьев и индукцию на этих деревьях, чтобы доказать это? Я не совсем уверен, как это сделать.

Answer 1

Когда первый аргумент exec это список, две возможности:

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

На шаге индукции вы предполагаете, что предложение верно для codes, то есть вы можете предположить:

exec codes s = eval codes : s

для любого значения s - имейте это в виду - обычно это ключевой шаг в любом доказательстве индукции.

Начните с расширения #1, используя код, который вы написали для exec:

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

Можете ли вы увидеть место, чтобы использовать гипотезу индукции?