coqのandとorを含む命題

これまでの記事

前々回: https://zenn.dev/emma_e_evans/articles/de3c743845c2cf2dd42d
前回: https://zenn.dev/emma_e_evans/articles/3ac81ac25d3a650618a7

andを含む命題の証明

andはcoqでは/(スラッシュとバックスラッシュ)と書きます。
仮定にandが含まれている場合とゴールにandが含まれている場合に分けてそれぞれ見ていきましょう。

andが仮定に含まれている場合

命題「forall (A B:Prop), A /\ B -> B.」を証明する場合，

Example prop3: forall (A B:Prop), A /\ B -> B.
Proof.
intros.
apply H.
Qed.

で終わりです。簡単ですね。

andがゴールに含まれている場合

命題「forall (A B:Prop), A -> B -> A /\ B.」を証明する場合，

Example prop4: forall (A B:Prop), A -> B -> A /\ B.
Proof.
intros.
split.
apply H.
apply H0.
Qed.

です。ここで，splitというのは，ゴールであるA /\ BをAとBに分割して個別に証明するというタクティクスです。

orを含む命題の証明

orはcoqでは/と書きます。こちらも同様に場合わけをして見ていきましょう。

orが仮定に含まれている場合

命題「forall (A B:Prop), A / B -> (~ A) -> B.」を証明する場合，

Example prop5: forall (A B:Prop), A \/ B -> (~ A) -> B.
Proof.
intros. (* A \/ B と ~ A を仮定に追加して，Bを証明する *)
destruct H. (* A \/ B をAが真のときとBが真のときとで場合分け *)
(* Aが真のとき *)
contradiction. (* Aと~Aの2つの仮定が矛盾しているので何でも導ける*)
(* Bが真のとき *)
apply H. (* 自明 *)
Qed.

となります。このように仮定に対する場合分けはdestructタクティクスを使います。ちなみにInductiveで定義されたものにdestructを適用すると，構成子ごとに場合分けしてくれます。

orがゴールに含まれている場合

命題「forall (A B:Prop), A -> A / B.」を証明する場合，

Example prop6: forall (A B:Prop), A -> A \/ B.
Proof.
intros. (* 仮定にAを追加して，A\/Bを証明する *)
left. (* A \/ Bを証明する代わりに左側のAだけに絞って証明する *)
apply H. (* 仮定AをゴールAに適用して終わり *)
Qed.

とします。コメントでも書いていますが，A / Bというゴールに対してはleft, rightタクティクスでゴールを絞ることができます。