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

きくらげ観察日記

好きなことを、適当に。

Coqでデータ型に対して条件分岐を行う

Coq

証明中にデータ型に対して条件分岐を行うためには、case, case_eq, destruct等を使います。

とりあえず普通に条件分岐をする

caseは普通の条件分岐です。例えばb : boolに対してcase b.とすると、b = trueである場合とb = falseである場合の2つに分かれ、それぞれの場合に対して証明を行うことで証明終了となります。

(* negb は bool の not *)
Goal forall b : bool, negb (negb b) = b.
Proof.
  intros b.
  case b. (* b についての場合分けを行う。 *)
  - (* b = true の場合 *)
    reflexivity.
  - (* b = false の場合 *)
    reflexivity.
Qed.

フィールドを持つ値の場合は、フィールドの名前はCoqが勝手に決めてくれます。

Require Import Coq.Init.Datatypes.

Inductive singleton : Type := single : singleton.

Definition option_to_sum (T : Type) (opt : option T) : sum T singleton :=
  match opt with
    | Some x => inl x
    | None => inr single
  end.

Definition sum_to_option (T : Type) (s : sum T singleton) : option T :=
  match s with
    | inl x => Some x
    | inr single => None
  end.

Theorem option_to_sum_iso:
  forall (T : Type) (x : option T),
    sum_to_option T (option_to_sum T x) = x.
Proof.
  intros T x.
  case x.
  - (* x = Some t *)
    (* Goal: forall t : T, sum_to_option T (option_to_sum (Some t)) = Some t *)
    (* Some t の t は Coq によって勝手に命名された *)
    intros t.
    reflexivity.
  - (* x = None *)
    (* Goal: sum_to_option T (option_to_sum T None) = None *)
    reflexivity.
Qed.

フィールド名を自分で指定して条件分岐をする。

destructタクティックを使用すると、先ほどの証明に出てきた"Some t"の"t"の部分に、自分で好きなように名前をつけることができます。
destructタクティックの使い方は以下の通りです。

Inductive hoge : Type :=
| foo : hoge -> hoge
| bar : hoge -> hoge -> hoge
| baz : hoge.

(* 上のような型 hoge の値 h に対して destruct したい場合 *)
  destruct h as [x | a b |].
  - (* h = foo x *)
    ...
  - (* h = bar a b *)
    ...
  - (* h = baz *)

as以下で指定している"|"で区切られた名前の列がフィールド名になります。
先ほどのoption_to_sum_isoをdestructを使って書きなおしてみると、以下のようになります。

Theorem option_to_sum_iso2:
  forall (T : Type) (x : option T),
    sum_to_option T (option_to_sum T x) = x.
Proof.
  intros T x.
  destruct x as [x' |].
  - (* x = Some x' *)
    reflexivity.
  - (* x = None *)
    reflexivity.
Qed.

場合分けの等式を前提に追加する

前提の部分にない複雑な式などについて場合分けを行いたい場合、場合分けの式(先ほどの例で言えばx = Some x', x = None等)が前提に入ってくれると嬉しいことがあります。
そういった場合にはcase_eqを使います。これはcaseとほとんど同じですが、場合分けの式を前提に追加してくれることだけが異なります。

Require Import Coq.Arith.EqNat.

Goal forall n m : nat,
       n = m \/ n <> m.
Proof.
  intros n m.
  (* beq_nat n m = true | false で場合分けを行えば証明できそう *)
  case_eq (beq_nat n m).
  - (* beq_nat n m = true *)
    intros H. (* H : beq_nat n m = true *)
    apply beq_nat_true in H. (* beq_nat_true: beq_nat n m = true -> n = m *)
    left.
    apply H.
  - (* beq_nat n m = false *)
    intros H. (* H : beq_nat n m = false *)
    apply beq_nat_false in H. (* beq_nat_false: beq_nat n m = false -> n <> m *)
    right.
    apply H.
Qed.