Falseの証明（その2）

Coqで、次の述語を考えてみます。

Inductive is0P : nat -> Prop := is0P_0 : is0P 0.

is0Pは、「自然数が0である」という意味の述語になります。

is0P 1 -> Falseの証明

is0P 1は成り立たないのですが、not (is0P 1)すなわちis0P 1 -> Falseを証明してみましょう。

通常の方法で証明すると次のようになります。

Example not01 : is0P 1 -> False.
Proof.
  intros. inversion H.
Qed.

証明項を直接作ろうとすると次のようになります。

fun H : is0P 1 =>
  match H in (is0P n)
    return
      match n with
        | 0 => True
        | S _ => False
      end 
    with
      | is0P_0 => I
  end
    : is0P 1 -> False

なぜこれで証明ができるのかを、私の理解している範囲で説明します。matchは次の順番で処理されているようです。

1. match H ...となっているのでHの型から対応するInductiveを割り出し、コンストラクタを思い出す
2. 1.で思い出したコンストラクタのすべてがwithの後に来ていることを確認。Hの型はis0P 1なのでコンストラクタはis0P_0のみ。
3. コンストラクタ毎に指定された式を分岐と呼ぶ。この場合はIのみ。
4. それぞれの分岐がin ... return ...で指定された型になっているかを確認する。inとreturnを使って分岐の型を確認する方法は後述する。ここではIがin ... return ...で指定された型になっている。
5. Hの型とin ...を見比べてreturn ...に出てくるnを求める。この場合、Hの型はis0P 1で、inで指定されているのはis0P nなのでこれらを見比べるとnは1となる。
6. 5.で求めたnをreturn ...に当てはめて、このmatch式の型とする。今回は、returnで指定された部分のnを1とすることで、型はmatch 1 with | 0 => True | S _ => False endとなる。これはCheckコマンド等ではFalseと表示される式である。

上記の手順で使っている「分岐の型の確認方法」は次の通り。

1. 分岐に対応するパターンの型とin ...を見比べる。今回は、パターンはis0P_0でその型はis0P 0である。また、inにはis0P nが指定されているのでnは0となる。
2. 1.で求めたnをreturn ...に当てはめて、分岐の型とする。この場合は、match 0 with | 0 => True | S _ => False endとなる。
3. 2.で求めた型を分岐が持っているかを確かめる。この場合はIがmatch 0 with | 0 => True | S _ => False endという型かを調べ、OKということになる。

return ...で指定する式は変数nを含んでいて、分岐の型を確認する際には分岐毎にnの値を変えながら確認するというのがポイントのようです。