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.