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