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

きくらげ観察日記

好きなことを、適当に。

Coqで「任意のxについて…」「あるxが存在して…」を扱う

Coq

Coqで「任意のxについて…」を表すforall xは、xを受け取って残りの命題の証明を返す関数となっています。

Definition prop_1 : forall (x : nat), x = x :=
  fun x => eq_refl x.

また、「あるxが存在して…」を表すexists xは、以下のようなデータ型として定義されています。

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex (A:=A) P.

結論がforall x, ...である命題を証明する

introsタクティックを使うと、forallの部分が外れます。

Goal forall x : nat, x = x.
Proof.
  intros x. (* x : nat, Goal: x = x *)
  reflexivity.
Qed.

前提のforallを具体的な値に変換する

specializeタクティックを使うと、forall x, ...のxを具体的な値で置き換えることができます。

Goal forall P : nat -> Prop,
       (forall x, P x) -> P 5.
Proof.
  intros P H. (* H : forall x : nat, P x *)
  specialize (H 5). (* H : P 5 *)
  assumption.
Qed.

結論がexists x, ...である命題を証明する

一番基本的な方法は、上のコンストラクタex_introをそのまま使うことです。

Goal exists (x : nat), x = 0.
Proof.
  (* ex_intro : forall x : A, P x -> ex (A := A) P のxに0を与える *)
  apply ex_intro with (x := 0).
  (* Goal: 0 = 0 *)
  apply eq_refl.
Qed.

これと同等なことを行うためのタクティックとして、existsというものが存在します。

Goal exists (x : nat), 1 + 1 = x.
Proof.
  (* 「あるx」の「x」は2だよ、ということを教える *)
  exists 2.
  reflexivity.
Qed.

前提のexists x, ...からxの値を取り出す

existsはただのデータ構造なので、destructを使うと変数を取り出すことができるようになります。

Goal forall (x : nat) (P : nat -> nat -> Prop),
       (forall a b : nat, P a b -> P b a) ->
       (exists y : nat, P x y) ->
       (exists z : nat, P z x).
Proof.
  intros x P H0 H1.
  (* H0 : forall a b : nat, P a b -> P b a *)
  (* H1 : exists y : nat, P x y *)
  (* Goal: exists z : nat, P z x *)
  destruct H1.
  (*
   *  H が具体化されて、
   * x0 : nat, H : P x x0
   * の2つになる
   *)
  specialize (H0 x x0).
  (* H0 : P x x0 -> P x0 x *)
  apply H0 in H.
  (* H : P x0 x *)
  exists x0.
  (* Goal : P x0 x *)
  assumption.
Qed.