CoqでFixを使って再帰関数を定義してみる

概要

Coqでは Fix という不動点オペレータを使って再帰関数を定義することができる。より複雑な再帰関数を定義したくなった場合に便利なことがある。

factorialの例

再帰関数といえば factorial 。階乗を計算する関数を考えてみる。

定義

Fact_definition.v

Definition fact (n: nat) : nat.
  refine (Fix (lt_wf) (fun _ => nat)
              (fun n F =>
                 match n as k return n=k -> nat with
                 | O => fun _ => 1
                 | S n' => fun _ => n * F n' _
                 end (eq_refl _)
              ) n).
  rewrite e. auto with arith.
Defined.

便利な補題

Fixpointで定義した場合に比べて、計算したいアルゴリズムと停止性のための処理がごちゃまぜになってしまっているため、以下のような補題があるとうれしい。

Fact_theory.v

Lemma fact_equation : forall n : nat, fact n = match n with
                                               | 0 => 1
                                               | S p => (S p) * fact p
                                               end.
Proof.
  intros n. unfold fact at 1. rewrite Fix_eq.
  - destruct n; reflexivity.
  - intros x f g F.
    destruct x; [reflexivity| now rewrite F].
Qed.

Lemma fact_ind :
  forall P : nat -> nat -> Prop,
    P 0 1 ->
    (forall n : nat,  P n (fact n) -> P (S n) (S n * fact n)) ->
    forall n : nat, P n (fact n).
Proof.
  intros P IH_0 IH_S n.
  apply (lt_wf_ind n (fun n => P n (fact n))). intros x H.
  destruct x.
  - assumption.
  - rewrite fact_equation. apply IH_S. apply H. now auto with arith.
Qed.