forall と -> : ゴールが２つ (1.4)

別の例をやってみたいと思います。Sコンビネータと呼ばれる定理です。

Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R.

いきなりexactで書いてもいいんですが、順を追ってやっていきましょう。

intros.

「ゴールにforallや->があったら、とりあえず何も考えずintrosする」というのはかなり成功率の高い戦略です。

略
H: P->Q->R
略
----------------------------------
R

こうなってると思うので、R を作るには apply H しましょう。他に R が仮定にないですし。これしかない。

さて、見慣れないことが起きました。右側に、"2 subgoals" と出ています。Hは二つ前件がある"ならば"なので（カリーハワード対応的にいうと、2引数の関数なので）、Hを使って"R"を示すには、"P"の証明と"Q"の証明の、二つの証明が必要です。というわけで、Coqさんからの要請として、「証明するものが２つになりましたよー」と言ってきているわけです。"P"と"Q"です。まずは(1/2)のゴールである"P"から片付けます。

  apply H0.
  apply H1.  (* exact H1. でも assumption. でも同じ *)

H0 が Q->P で、P を作るには H0 を使えばよい。あとは Q の証明が必要…と思ったら、H1 が Q そのものでした。おしまい。仮定にゴールそのものがあるときは、exactではなくてapplyでもいいです。何も前提条件のない"ならば"（0引数の関数）とみなしてapplyしている感覚です。

Pの証明が終わると自動的にもう一つのゴール"Q"に移るので

  assumption.
Qed.  

こちらも終わらせます。証明完了！

Print S.
==>
S = fun P Q R H H0 H1 => H (H0 H1) H1  (型情報略)