Idrisでrev_rev_id

rev_rev_idとは、リストに、逆順にする事を2回すると、元に戻る、というやつだ。

みょんみょんさんがIsabelleで、
いとうかつとしさんがAgdaで、実装動画を上げている。

ならば僕は、Idrisでやろう、と奮い立った。
（Idrisを起動するときは、> idris -XElabReflectionってやったら良い事があるかもしれない）
出来た物はこちら。

module rev_rev_id

%default total

a : List Nat
a = [1, 2, 3, 4]

snoc : List Nat -> Nat -> List Nat
snoc []      y = [y]
snoc (x::xs) y = x :: snoc xs y

myReverse : List Nat -> List Nat
myReverse []      = []
myReverse (x::xs) = snoc (myReverse xs) x

lemma : (xs:List Nat) -> (y:Nat) -> myReverse (snoc xs y) = y :: (myReverse xs)
lemma []      _ = Refl
lemma (x::xs) y = rewrite lemma xs y in Refl

theorem : (xs:List Nat) -> myReverse (myReverse xs) = xs
theorem []      = Refl
theorem (x::xs) = rewrite lemma (myReverse xs) x in
                  rewrite theorem xs in Refl

お二人と、ほぼ同じ形になった。
これでも苦労したのですよ、簡約されすぎたりして。

あと話は変わるけれど、Idrisのコマンドプロンプトはカラフルでかっこいい。

181020 追記　Reasoningを使った証明もやってみた。
libs/base/Syntax/PreorderReasoning.idr　にライブラリがある。

module rev_rev_id02

-- > idris -p base
import Syntax.PreorderReasoning

%default total
-- %language ElabReflection


snoc : List a -> a -> List a
snoc []      y = [y]
snoc (x::xs) y = x :: snoc xs y

myReverse : List a -> List a
myReverse []      = []
myReverse (x::xs) = snoc (myReverse xs) x

lemma : (xs:List a) -> (y:a) -> myReverse (snoc xs y) = y :: (myReverse xs)
lemma []      _ = Refl
lemma (x::xs) y = rewrite lemma xs y in Refl

theorem : (xs:List a) -> myReverse (myReverse xs) = xs
theorem []        = Refl
theorem (x :: xs) =
  (myReverse (myReverse (x::xs)))       ={ Refl                        }=
  (myReverse (snoc (myReverse xs) x))   ={ lemma (myReverse xs) x      }=
  (x :: (myReverse (myReverse xs)))     ={ cong {f=(x::)} (theorem xs) }=
  (x :: xs)                                QED