Coq 帰納法と余帰納法

前回、iterateとtakeを定義した。

Require Import List.
Require Import Coq.Lists.Streams.

Section MyStreams.
  Variable A : Type.

  CoFixpoint iterate (f : A -> A) (x : A) : Stream A :=
    Cons x (iterate f (f x)).

  Fixpoint take (n : nat) (s : Stream A) : list A :=
    match n with
      | O => nil
      | S n1 => (hd s) :: take n1 (tl s)
    end.

加えて次の関数を定義する。

Streamを生成するunfold。unfoldはanamorphismというものらしい。

  CoFixpoint unfold (B : Type) (f : B -> A * B) (b : B) : Stream A :=
    let (a, b') := f b in
      Cons a (unfold B f b').

Streamの先頭にlistを連結するapp。

  Fixpoint app (l : list A) (s : Stream A) : Stream A :=
    match l with
      | nil => s
      | a :: l1 => Cons a (app l1 s)
    end.

Streamの先頭n要素を捨てるdrop。

  Fixpoint drop (n : nat) (s : Stream A) : Stream A :=
    match n with
      | O => s
      | S n1 =>
        match s with
          | Cons _ s1 => drop n1 s1
        end
    end.

今日はこれらの関数に対して証明を書いてみようと思う。

Streamからtakeしてから、dropした残りのStreamにappすると元のストリームに戻ることの証明。

Stream同士が等しいことは、 eq ではなく余帰納的に定義された述語 EqSt を使って記述する。

  Theorem app_take : forall (n : nat) (s : Stream A),
    EqSt (app (take n s) (drop n s)) s.
  Proof.
    intros n.
    induction n as [|n' IH].

      apply EqSt_reflex.

      intros s.
      case s; intros a s'.
      simpl.
      apply eqst.

        reflexivity.

        apply IH.
  Qed.

listをStreamにappしてからtakeすると元のlistが得られることの証明。

  Theorem take_app : forall (l : list A) (s : Stream A),
    (take (length l) (app l s)) = l.
  Proof.
    induction l as [|a l' IH].

      reflexivity.

      intros s.
      case s; intros a0 s0.
      simpl.
      apply f_equal.
      apply IH.
  Qed.

iterate id a が const a に等しいことの証明。これは余帰納法を使わないといけない。Stream A型を返す関数で、余再帰的に定義されているconstやiterateを簡約するには、simplを使う前に補題 unfold_Stream を使って書き換えておく必要があった。

  Theorem iterate_id : forall (a : A),
    EqSt (iterate id a) (const a).
  Proof.
    intros a.
    cofix iterate_id.
    rewrite (unfold_Stream (iterate id a)).
    rewrite (unfold_Stream (const a)).
    simpl.
    apply eqst.

      reflexivity.

      apply iterate_id.
  Qed.

End MyStreams.

参考文献