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.参考文献
