ひとり勉強会

ひとり楽しく勉強会

forall と -> : 仮定側の変形 (1.5)

Coq

ここまでに紹介した apply と intro(s) は、どちらも、証明のゴールを変形する tactic でした。なのですが、これってあまり直感的ではない気がするのですよね。私見ですが。

  • 「A と B と C を仮定して Z を証明して下さい！」

って言われたときに

  • 「Cが使えるから、Zを言うためにはYを証明すれば言えるな。」てことは、「AとBとCを仮定して、Yを証明」すれば終了だ

という考え方は、勿論しないことはないですけど、自分の場合それよりはむしろ

  • 「AとB からは、D が言えるな。」てことは「AとBとCとD から、Zを証明」できればOKだ
    • 「あ、CとDからE も示せる。」つまり「AとBとCとDとE から、Z」が言えれば…

と、仮定の方をどんどんリッチにしていって、そのうちZが出てくる、と考えることが多いです。というわけで、仮定の方を変形する証明スタイルをやってみます。お題はさっきの S コンビネータで。

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

introsは仕方ないので何も考えず脊髄反射でintros。そうすると、ゴールはこうなります。

H : P -> Q -> R
H0 : Q -> P
H1 : Q
-------------------
R

H0: "QならばP" と H1: "Q" があるから、これを使って、まず "P" が証明できますよね。H0 に H1 を適用すれば証明できる。

  assert (Proof_of_P := H0 H1).

assert (X := t)
証明tによって証明された命題を、名前Xの仮定として追加

すると、Proof_of_P: "P" と、H1: "Q" と H: "Pならば(QならばR)" が仮定にあるのだから、"R" が証明できますね。

  assert (PrR := H Proof_of_P H1).

おや、いつの間にやら仮定に R があって、ゴールも R です。証明完了ですね。

  exact PrR.
Qed.

Print S.
==>
S = fun P Q R H H0 H1 =>
  let Proof_of_P := H0 H1           in
  let PrR        := H Proof_of_P H1 in
     PrR.                                (* 型情報略 *)

証明項をPrintしてみると、このスタイルの証明は、こんな風な、let を使ったプログラムになります。

その他の仮定側変形tactic

さきほどは、H0: Q->P で H1: Q のときに、この２つから P が証明できるよね、と、assert を使ってPを出しました。違うtacticを使う方法もあります。

specialize (A B)
仮定Aを、A B に置き換え

Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R.
Proof.
  intros.
  specialize (H0 H1).

こうすると、さっきまで "H0: Q->P" だったのが "H0: P" に変化します。assertと違って、

  • 仮定の名前 X := を書かなくていいので楽
  • その代わり、もとあった仮定 Q->P が消えてしまう。複数回 Q->P を使いたい場合は specialize してはいけない
  • 逆に考えると、もう二度と使わない仮定なら消えた方が画面が広くて綺麗なので、specialize しちゃってよい

その名の通り、H0という"ならば"型の仮定を、H1 という特殊な場合に限定(specialize)して使うよ、という方針をCoqさんに伝えるのが、このtacticです。

さて、今の仮定は H:P->Q->R、H0:P、H1:Q です。ここから R が出せますね。もう一つ、別の仮定変形があります。

apply A in B
仮定Bを、A B に置き換え

Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R.
Proof.
  intros.
  specialize (H0 H1).
  apply (H H1) in H0.

こうすると、さっきまで "H0: P" だったのが "H H1: Q->R" を適用(apply)されて、"H0: R" に変化します。specializeは適用する"ならば"仮定の方を消してしまうのに対し、こちらのapply〜inは、適用される側を消して新しい結果で上書きします。これも、消される仮定が後で要るか要らないかよく考えてから使いましょう。