andとorとnot: コンストラクタ (2.3)

ここまでの内容をまとめると、

• ゴールが A∧B の形なら ∧の公理(コンストラクタ)を使う
  • つまり apply conj.
• ゴールが A∨B の形なら ∨の公理(コンストラクタ)を使う
  • つまり apply or_introl.
  • または apply or_intror.
  • どっちがいいかは人間が頑張って考える。

です。

これはこれでいいんですけど、「∧のコンストラクタの名前ってなんだったけ…」「∨のコンストラクタって…」って毎回思い出したり、リファレンス引いたりするのは面倒ですよね。

この辺は、自動化してくれる tactic があります。

Lemma De_Morgan:
  forall A B: Prop, ~(A \/ B) -> (~A /\ ~B).
Proof.
  unfold not.
  intros.
  constructor.  (* apply conj. の代わり *)

constructor. と打つと、名前忘れたけどコンストラクタ使うぜ！という意味になって、Coqさんが上手いことやってくれます。
orの場合はコンストラクタが2つあるので…

  intros.
  apply H.
  constructor 1. (* apply or_introl. の代わり *)
  exact H0.

  intros.
  apply H.
  constructor 2. (* apply or_intror. の代わり *)
  exact H0.
Qed.

どっちのコンストラクタなのか、「1番目のやつ！」「2番目のやつ！」と指定してあげましょう。番号指定しないと、コンストラクタを先頭から順にapplyしてみて成功した最初の結果を返すみたいです。

実は、さらにさらに、短く書く略記tacticも用意されています。

constructor.

ゴール命題の、コンストラクタをapply。(複数ある場合は最初にマッチした物)

constructor n.

ゴール命題の、n番目のコンストラクタをapply

split.

1つしかコンストラクタがないゴールに。そのコンストラクタをapply

left.

丁度2つコンストラクタがあるゴールに。constructor 1 と同じ

right.

丁度2つコンストラクタがあるゴールに。constructor 2 と同じ

splitは「"A∧B"を証明」というゴールを「Aを証明」と「Bを証明」に分ける(split)感覚で、leftは「"A∨B"を証明」というゴールを「Aを証明」に左(left)だけ残して変える感覚ですかね。rightは右。constructorのただの別名なので、splitもleftもrightも、andやor以外にも使えます（かえって意味がわかりにくくなったりするかもしれませんが…）。