読者です 読者をやめる 読者になる 読者になる

きくらげ観察日記

好きなことを、適当に。

Coqで数学的帰納法を行う

数学的帰納法を行いたい場合は、基本的にelimかinductionのどちらかのタクティックを利用します。

elim

こちらが最も基本的な帰納法です。elim x.とすることで、xについての帰納法を行うことができます。
例えば、以下のコードでは直接to_zero n = 0を示すのではなく、ゴールをto_zero 0 = 0と、
forall n0, to_zero n0 = 0 -> to_zero (S n0) = 0の2つのサブゴールに分割してそれぞれ証明しています。

Fixpoint to_zero (n : nat) : nat :=
  match n with
    | O => O
    | S n' => to_zero n'
  end.

Theorem to_zero_n_is_zero:
  forall n : nat, to_zero n = 0.
Proof.
  intros n.
  elim n.
  - (* Goal: to_zero 0 = 0 *)
    reflexivity.
  - (* Goal: forall n0 : nat, to_zero n0 = 0 -> to_zero (S n0) = 0 *)
    intros n0 H. (* H : to_zero n0 = 0 *)
    (* Goal: to_zero (S n0) = 0 *)
    simpl.
    (* Goal: to_zero n0 = 0 *)
    apply H.
Qed.

induction

inductionはもう少し高機能な帰納法です。こちらはもう少し通常の証明で使うような方法で数学的帰納法を扱えます。
induction xを行うとxについて場合分けが行われ、フィールドを持つ値の場合は帰納法の仮定がIHhoge(hogeは変数名)の形で追加されます。

Theorem to_zero_n_is_zero2:
  forall n : nat, to_zero n = 0.
Proof.
  intros n.
  induction n as [| n']. (* destruct と同様の構文で変数名を指定する *)
  - (* n = O の場合 *)
    (* Goal: to_zero 0 = 0 *)
    reflexivity.
  - (* n = S n' の場合 *)
    (* IHn' : to_zero n' = 0 *)
    (* Goal: to_zero (S n') = 0 *)
    simpl.
    (* Goal: to_zero n' = 0 *)
    apply IHn'.
Qed.

ちなみに、場合分けの頭についている"-"は単なる見やすさのためだけの構文なので、別に無くてもかまいません。
"-"の他に"+", "*", "{ .. }"が使えます。

自然数以外のデータ型についての数学的帰納法

自然数以外でも、機能的に定義されたデータ構造に対しては数学的帰納法を行うことができます。
例えばlistについて以下のような定理を証明してみましょう。

Require Import Coq.Init.Datatypes.

Theorem list_length:
  forall (T : Type) (xs ys : list T),
    length (xs ++ ys) = length xs + length ys.
Proof.
  intros T xs ys.
  induction xs as [| x' xs'].
  - (* xs = nil *)
    reflexivity.
  - (* xs = x' :: xs' *)
    (* IHxs': length (xs' ++ ys) = length xs' + length ys *)
    simpl.
    (* Goal: S (length xs' ++ ys) = S (length xs' + length ys) *)
    rewrite -> IHxs'.
    reflexivity.
Qed.