reverse
関数型言語で reverse を書くときは
let rec reverse1 = function | [] -> [] | x::xs -> reverse1 xs @ [x]
ではなく
let reverse2 = let rec aux xs = function | [] -> xs | y::ys -> aux (y::xs) ys in aux []
と書け,という話はまぁよく例として聞く気がしますが,はじめての Coq なかんじでこの2つの reverse が等価,つまり reverse1 xs = reverse2 xs であることを証明してみた(たぶん).
Require Import List. Fixpoint reverse1 {A : Type} (xs : list A) := match xs with | nil => nil | x::xs => reverse1 xs ++ x::nil end. Fixpoint reverse2_aux {A : Type} (xs ys : list A) := match ys with | nil => xs | y::ys => reverse2_aux (y :: xs) ys end. Definition reverse2 {A : Type} (xs : list A) := reverse2_aux nil xs. Lemma app_assoc : forall (A : Type) (xs ys zs : list A), (xs ++ ys) ++ zs = xs ++ (ys ++ zs). Proof. induction xs. reflexivity. intros. simpl. f_equal. apply IHxs. Qed. Lemma rev2_app : forall (A : Type) (ys xs : list A), reverse2_aux xs ys = reverse2_aux nil ys ++ xs. Proof. induction ys. reflexivity. intros. simpl. rewrite IHys with (xs := a :: nil). rewrite app_assoc. simpl. apply IHys. Qed. Theorem reverse_eqv : forall (A : Type) (xs : list A), reverse1 xs = reverse2 xs. Proof. unfold reverse2. induction xs. reflexivity. simpl. rewrite IHxs. symmetry. apply rev2_app. Qed.