Wed Sep 11 2019

具体的な型の等価の排中律 (Coq)

直観論理では排中律は成り立たないし, 特に一般の型について \[\forall a,b,~ a = b \lor a \ne b\] は成立しない.

けど、a b に具体的な型が与えられていて, それが普通日常で考える常識的なモノであれば, これは普通の成り立つ.

(*
  Excluded Middle Law (EML) of concrete types
*)

Theorem eml_bool : forall a b : bool, a = b \/ a <> b.
Proof.
  case; case; (by left) + (by right).
Qed.

Theorem eml_nat : forall a b : nat, a = b \/ a <> b.
Proof.
  induction a as [|a' IHa].
  case. by left. by right.
  case. by right.
  intro b'.
  move: (IHa b').
  case.
  - by left; apply f_equal.
  - by right; injection.
Qed.

Theorem eml_nat_list : forall (a b : list nat), a = b \/ a <> b.
Proof.
  induction a as [|x xs IH].
  case. by left. by right.
  case. by right.
  move => y ys.
  move: (IH ys); case => [E|E]; move: (eml_nat x y); case => [F|F];
      (rewrite E; rewrite F; by left) + (by right; injection).
Qed.