The Coq Proof Assistant A Tutorial (11) 排中律の証明 (完結編)

いまだに Coq をよくわかってませんが，いちおう証明はできたみたいです．

でも，いろいろ謎だらけです… 全然見当違いのことをしているのかもしれませんが…

$ ledit coqtop
Welcome to Coq 8.0pl3 (Jan 2006)

Coq < Section Minimal_Logic.

Coq < Variable P : Prop.
P is assumed

(* 二重否定除去規則 DN を仮定しておく *)

Coq < Hypothesis DN : forall P : Prop, ~~P -> P.
DN is assumed

(* 排中律 EM を証明 *)

Coq < Theorem EM : P \/ ~P.
1 subgoal

  P : Prop
  DN : forall P : Prop, ~ ~ P -> P
  ============================
   P \/ ~ P

EM < apply DN.
1 subgoal

  P : Prop
  DN : forall P : Prop, ~ ~ P -> P
  ============================
   ~ ~ (P \/ ~ P)

EM < intro.
1 subgoal

  P : Prop
  DN : forall P : Prop, ~ ~ P -> P
  H : ~ (P \/ ~ P)
  ============================
   False

EM < apply H.
1 subgoal

  P : Prop
  DN : forall P : Prop, ~ ~ P -> P
  H : ~ (P \/ ~ P)
  ============================
   P \/ ~ P

EM < right.
1 subgoal

  P : Prop
  DN : forall P : Prop, ~ ~ P -> P
  H : ~ (P \/ ~ P)
  ============================
   ~ P

EM < intro.
1 subgoal

  P : Prop
  DN : forall P : Prop, ~ ~ P -> P
  H : ~ (P \/ ~ P)
  H0 : P
  ============================
   False

EM < apply H.
1 subgoal

  P : Prop
  DN : forall P : Prop, ~ ~ P -> P
  H : ~ (P \/ ~ P)
  H0 : P
  ============================
   P \/ ~ P

EM < left.
1 subgoal

  P : Prop
  DN : forall P : Prop, ~ ~ P -> P
  H : ~ (P \/ ~ P)
  H0 : P
  ============================
   P

EM < apply H0.
Proof completed.

EM < Qed.
apply DN.
intro.
apply H.
right.
intro.
apply H.
left.
apply H0.
EM is defined

Coq < Check EM.
EM
     : P \/ ~ P

Coq < Print EM.
EM =
DN (P \/ ~ P)
  (fun H : ~ (P \/ ~ P) =>
   H (or_intror P (fun H0 : P => H (or_introl (~ P) H0))))
     : P \/ ~ P

いろいろあって，今日はもう体力の限界千代乃富士です… 続きはまた次回ということで．