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

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

1階命題論理でresolutionが成り立つ事を示す

まずAかBかで場合を分けて、Aのときは¬AかCかで場合分けすればできる。Aと¬Aが同時に成り立つとなんでも証明できてしまうということを利用しよう。排中律は別に必要なく証明できる。

Proposition p09 :
  forall A B C, (A \/ B) /\ (~A \/ C) -> B \/ C.
Proof.
intros A B C H; elim H; intros.
elim H0.
 elim H1.
  intros H2 H3; elim H2.
    apply H3.
 intros H2 _; right; apply H2.
intro H2; left; apply H2.
Qed.