Isabelle prog-proveのExercise 2.4の解答

ハマったのでメモ

問題

Exercise 2.4 Define a recursive function snoc :: 'a list => 'a => 'a list that appends an element to the end of a list. With the help of snoc define a recursive function reverse :: 'a list => 'a list that reverses a list. Prove reverse (reverse xs) = xs

reverse関数をappend無しで定義しよう、という問題。

snocの定義

ハマりどころその1。snoc xs aをx1 # x2 # ... # xn # [a]に展開していくイメージで書く。

fun snoc :: "'a list => 'a => 'a list" where
"snoc [] a = [a]" |
"snoc (x # xs) a = x # (snoc xs a)"

reverseの定義

こちらは簡単。

fun reverse :: "'a list => 'a list" where
"reverse [] = []" |
"reverse (x # xs) = snoc (reverse xs) x"

reverse (reverse xs) = xsの証明

2つ目のハマりどころにして一番難しいところ。素直にinductionからのautoのコンボを使ってみる:

theorem rev_rev: "reverse (reverse xs) = xs"
  apply(induction xs)
  apply(auto)
done

これは数学的帰納法の2つ目の証明が失敗してしまう。 という訳でここに補題を付け加えるわけだが、それを見つけるのが難しい。

以下のような補題を上の証明の前に入れる:

lemma snoc_rev_sim [simp]: "reverse (snoc xs x) = x # (reverse xs)"
  apply(induction xs)
  apply(auto)
done

この命題はConsとsnocの対称性を表している。 Consを#、snocを*と書いてみると分かりやすい:

reverse (x # xs) = (reverse xs) * x （reverseの定義）
reverse (xs * x) = x # (reverse xs) （さっき証明した補題）

こうしてみるとConsとsnocは項の順番を置き換えることで交換できることがわかる。