Coqの演習問題、あるいはifとapplyについて

Logical Foundationsを進めがてら、基礎固め的に簡単な命題論理の命題を証明してみたいと思ってググったらこんなスレに遭遇した：

coq.discourse.group

このうちの最初の問題が簡単ながらもいくつか面白い点があったのでメモ。

証明する命題：

Lemma a1 : forall (A B C D : Prop),
    (A -> B) -> (A -> C) -> (B -> C -> D) -> (A -> D).

まずは命題と仮定を導入しておく：

Proof.
  intros A B C D.
  intros Hab Hac Hbcd Ha.

この時点での仮定とゴールは以下のようになっている：

  A, B, C, D : Prop
  Hab : A -> B
  Hac : A -> C
  Hbcd : B -> C -> D
  Ha : A
  ============================
  D

解１

ここで一番スッキリした解法は

  apply Hbcd.
  - apply Hab. apply Ha.
  - apply Hac. apply Ha.
Qed.

になると思う。

• B -> C -> Dという仮定を適用してゴールDを二つのサブゴールBとCに変換
• サブゴールBは仮定A -> BとAで証明
• サブゴールCは仮定A -> CとAで証明

となる。

ここで個人的に面白いポイントは

apply Hbcd（仮定B -> C -> D）でゴールDがB -> Cになるのではなく、BとCという独立したサブゴールになること。

よく考えたらB -> Cになってしまっては意味がおかしくなってしまうのだが、この「二つのサブゴールを導入する」挙動は最初何が起きたのかわからず混乱した。

B -> C -> Dは(B /\ C) -> Dと等価なので、まずB /\ Cに変換してからsplitしていると考えればいい。

解２と仮定の複製

別解を考えてみたいので、命題と仮定をintrosで導入した時点まで戻る：

Proof.
  intros A B C D.
  intros Hab Hac Hbcd Ha.

  A, B, C, D : Prop
  Hab : A -> B
  Hac : A -> C
  Hbcd : B -> C -> D
  Ha : A
  ============================
  D

ここで個人的には：

• 仮定にAとA -> BがあるからB
• 仮定にAとA -> CがあるからC
• B、CとB -> C -> DだからD

という流れで証明した方が自然に思える。Coqでそう証明する場合は：

  assert (Ha' := Ha).
  apply Hab in Ha.
  apply Hac in Ha'.
  apply Hbcd in Ha.
  - apply Ha.
  - apply Ha'.
Qed.

のようになる。

ここで面白いのはassert (Ha' := Ha)の部分で、仮定Ha : AをHa' : Aという別の仮定として複製している。

というのもこれを省略して単にapply Hab in HaでAにA -> Bを適用してしまうと、その適用された仮定Aがなくなってしまい、A -> Cを適用するためのAがなくなってしまうためだ。複製しておけばHa'が残っているのでそちらにA -> Cを適用できるから大丈夫。

複製する方法はStack Overflowから：

stackoverflow.com

ただ、上記の回答でも言及されている通り、「仮定を複製しないといけない」ような証明の仕方はCoqらしくない。仮定をいじり続けてゴールに到達するのではなく、ゴールを変換していく形がCoqとしては自然だ（とLogical Foundationsにも書いてある）。

解３

またしても命題と仮定をintrosで導入した時点まで戻る：

Proof.
  intros A B C D.
  intros Hab Hac Hbcd Ha.

  A, B, C, D : Prop
  Hab : A -> B
  Hac : A -> C
  Hbcd : B -> C -> D
  Ha : A
  ============================
  D

ここでapply Hbcd in Habあるいはapply Hbcd in Hacという手もある。

一般的にH1 : W -> YとH2 : X -> Y -> Zという仮定があってapply H2 in H1した場合、H1 : Zと片方の仮定が変換された上でサブゴールとしてWとXが追加される。

それを利用すればこんな感じで：

  apply Hbcd in Hac.
  - apply Hac.
  - apply Hab. apply Ha.
  - apply Ha.
Qed.

D、B、そしてAというサブゴールを個別で証明して終わり。

仮定に仮定を適用するとサブゴールが作成される、というのはちょっと非直感的な印象だった。

あとHbcd : B -> C -> DでもHbcd : C -> B -> Dでも大丈夫なのに、Hbcd : (B /\ C) -> Dだとapply Hbcd in Hacできない、というのは注意点。そういう意味では->で記述されている方が使い勝手がいいようだ。

雑感

Logical Foundationsの演習問題はinductionやらdestructやらが入り混じることが多く、ガチャガチャやっていたらなんだか証明できてしまった「俺たちは雰囲気で証明している」感があった。

なのでこういう簡単な演習問題で->を含む命題がapplyで使われるとどういう挙動を見せるのか試せてよかった。命題論理をいろいろいじり倒すのも勉強になりそう。