読者です 読者をやめる 読者になる 読者になる

きくらげ観察日記

好きなことを、適当に。

Coqのsplit, left, rightについてもう少し詳しく

Coq

inkar-us-i.hatenablog.com

上の記事でandを証明するためにsplit, orを証明するためにleft, rightを使えばいいと書きましたが、実はこれらのタクティックはもう少し一般的に作られています。

split

splitはandのみではなく、コンストラクタがC : X1 -> X2 -> .. -> Xn -> Pという形の任意のゴールPに対して扱うことができ、X1, X2, .., Xnの証明を与えることでPを証明してくれます。

Inductive and3 (A B C : Prop) : Prop :=
  conj3 : A -> B -> C -> and3 A B C.

Goal forall P Q R : Prop,
       P -> Q -> R -> and3 P Q R.
Proof.
  intros P Q R HP HQ HR.
  split. (* ここでサブゴールが P Q R の3つに分かれる *)
  - apply HP.
  - apply HQ.
  - apply HR.
Qed.

left, right

left, rightはorのみではなく、2つのコンストラクタC : X1 -> X2 -> .. -> Xn -> PとD : Y1 -> Y2 -> .. -> Ym -> Pからなる任意のゴールPに対して扱うことができ、leftの場合は1つめのコンストラクタ、rightの場合は2つめのコンストラクタのすべての引数について証明を行うことで、ゴールPを証明できます。

(* (A and B) or (C and D) *)
Inductive and_or (A B C D : Prop) : Prop :=
| and_or_introl : A -> B -> and_or A B C D
| and_or_intror : C -> D -> and_or A B C D.

Goal forall A B C D : Prop,
       C -> D -> and_or A B C D.
Proof.
  intros A B C D HC HD.
  right. (* ここで C D の証明に移る *)
  - apply HC.
  - apply HD.
Qed.