たまにCoqを触りたくなることがあります。
0. 概要
Coq上で、選択公理からZornの補題を証明しました。証明の際には排中律を公理に追加しました。仕様の記述に20 行、 その証明に 150 行 という規模です。タワーを使った初等的な証明であり、超限帰納法も使わず、整礎集合の概念も使いません。
1. 何をやっているのか？
やっていることは、CIC という計算体系上に「選択公理と解釈できる型の証明項」を入力として「Zornの補題と解釈できる型の証明項」を導出することです。
これは、1階述語論理上のZFCという1階理論において、ある証明系を採用しZornの補題と解釈されうる論理式を定理として導出するのとは違います。
しかし、カリー＝ハワード対応により、CIC+排中律 の計算は ある形式的体系における導出と読むことができます。つまり、教科書に書かれている論証をそのままCoq上で展開できる ということです。実際、本稿の証明は、参考文献の論証とほぼ一致させることができます。
1.1 先行事例
Coqでの実装はあまり調査しませんでしたが、coq-community/zorns-lemma というそのものずばり、といったものがありました。本稿と比べても、規模間は同程度。証明方法は近いが違いもそこそこ。教科書での証明と対応がつけづらいので可読性に難。
数学の教科書として紙上で趙限帰納法を使わない証明として、以下がありそれぞれちょっとずつ証明方法が違います。
- AAU の教授による証明(PDF): https://people.math.aau.dk/~cornean/index.html/zornlemma.pdf
- Google で「zorn tower proof」 で検索して出てきた結果の中で一番分かりやすかったものです。本稿はおおむねこの論証を踏襲しますが、決定的な部分で違いがあります。
- 『超限帰納法抜きで選択公理から Zorn の補題を証明してみた』 (PDF) : https://www2u.biglobe.ne.jp/~nuida/m/doc/ACtoZorn_ja_v6.pdf
- Google で「zorn 証明」で出てきた中で、初等的証明として形式化しやすい形で論証しています。タワーの概念を経由しない（暗黙的には同等の概念を経由しているのですが……）ので、論証を追えたとしても「わかった！」という感触が得られないので、一度こちらで実装したのですが辞めたという経緯があります
1.2 Coq 実装上の注意
性質Pをもつ任意だが固定したa というようなものを扱うのが構成的な道具立てである Coq では苦手です。本稿でも以下のような場面でそのような概念を使います
- 選択関数: Fixpointとして構成できませんし、仕様を満たしていれば、外延すら自由度があります。論証のなかでは特定の集合に対する任意だが固定した選択関数を使って様々な性質を論じます
- sup(A): 鎖が与えられ時に、sup A はただ一つ存在することが証明できますが、Fixpointとして構成できません
任意だが固定したモノ を Coq の証明間をまたいで使う（例えば Definition で名前を付けてあげる) ために sigma type を使って実装しました。例えば選択公理は以下のように符号化しました:
Definition Choice := forall A (X:(A->Prop)->Prop),
(forall x, X x -> exists a, x a) -> { f | forall x, X x -> x (f x)}.
こうすることで proj1_sig で証明項から選択関数を抜き出せるので、定理間で同一の選択関数を使うことができます。
問題は、このように符号化することが正しいのか？そうしていいのか？ということですが、我々の非構成的で粗い立場では「・・・・が構成できる」を「・・・・が存在する」と常に 読むので、本稿の立場では問題ないと判断します。
CIC での選択公理は様々なバージョンがあり、標準ライブラリ で choice を検索するとでてきます。今回はその中での classicalchoice とは別の定式化となっています。
2. 概要
背理法による証明なので矛盾を証明することが目的になります。命題の否定を仮定し、以下の手順で論証します
-
鎖c が与えられたときにその有界sup(c) を返す関数に
gと名前を付けます。 -
選択関数によって得られる任意だが固定した後続関数に
nextと名前を付けます。これは任意の元 x に対してそれよりも真に大きい元を返す関数です。 -
台の部分集合 P にたいする性質 タワー性 というものを定義します。全てのタワー性をもつものの共通部分・つまり、最小のタワーに
Mという名前を付けます。 -
もし
Mが鎖なら、タワー性の定義より矛盾することが簡単に示せるので、Mが鎖であることの証明が目的になります。 -
Mに含まれる各元 x において定義される nextのギャップレス性, nextの直系性を定義します。 -
M上の全ての元でnextが直系ならギャップレスであり、M上の全ての元でnextがギャップレスならMは鎖であることが証明できます。要は「M上の全ての元でnextが直系である」を証明すれば矛盾を導けるわけですが、この証明も初等的に完遂できます。
3. 結果
証明できて排中律以外の仮定がないとCoq が教えてくれました。
Check ac_imply_zorn_impl: Choice -> forall A R H, Zorn A R H .
Print Assumptions ac_imply_zorn_impl.
(* Axioms: classic : forall P : Prop, P \/ ~ P *)
4. 仕様
Require Import Classical.
(* === spec ====*)
Record PO (A:Type) (R:A->A->Prop):= {
R_refl: forall a, R a a;
R_trans: forall a b c, R a b -> R b c -> R a c;
R_ant: forall a b, R a b -> R b a -> a = b
}.
Definition maximal {A} (R:A->A->Prop) (X:A->Prop) (a:A) :=
X a /\ (forall b, R a b -> a = b).
Definition chain {A} (R:A->A->Prop) (c:A->Prop) : Prop :=
forall (x y:A), c x -> c y -> (R x y \/ R y x).
Definition sup {A} (R:A->A->Prop) (X:A->Prop) a :=
(forall b, X b -> R b a) /\
(forall b, (forall c, X c -> R c b) -> R a b).
Record ZornSet A R := {
a0 : A; (*witness of non emptiness *)
po : PO A R;
zh : forall c, chain R c -> { u | sup R c u }
}.
Definition Zorn A R (H:ZornSet A R) :=exists a, maximal R (fun _:A => True) a.
Definition Choice := forall A (X:(A->Prop)->Prop),
(forall x, X x -> exists a, x a) -> { f | forall x, X x -> x (f x)}.
Definition ac_imply_zorn := Choice -> forall A R H, Zorn A R H.
5. 証明
(* === proof ====*)
(* This section aims to prove falsity under ~Zorn *)
Section Contradiction.
Variable A: Type.
Variable R: A->A->Prop.
Variable ZH: ZornSet A R.
Variable choice: Choice.
Variable Contra: forall a, exists b, R a b /\ a<> b. (*equivalent to ~Zorn*)
(* shortcuts for order facts *)
Definition refl := R_refl _ _ (po _ _ ZH).
Definition trans := R_trans _ _ (po _ _ ZH).
Definition ant := R_ant _ _ (po _ _ ZH).
(* sup(C) locater *)
Definition g:= fun c H => proj1_sig (zh _ _ ZH c H).
Lemma g_spec : forall c H, sup R c (g c H).
Proof. intros. pose proof (proj2_sig (zh _ _ ZH c H)). auto. Qed.
(* next (x): successor function defined via AC, not necesarily immideate successor *)
Definition U (c:A->Prop) (_: chain R c): A->Prop :=
fun u => forall a, c a -> (R a u /\ a <> u).
Lemma U_inh: forall c H, exists a, U c H a.
Proof. intros.
destruct (g_spec c H) as [H1 H2].
destruct (Contra (g c H)) as [y [Hy1 Hy2]].
exists y. intros z Hz. split.
eapply trans. 2:eassumption. now apply H1.
intros M; subst. apply Hy2. apply ant. auto. now apply H1. Qed.
Lemma choice_function: forall c H, { f | U c H (f (U c H))}.
Proof. intros.
remember (fun X=> exists c H, forall x, (U c H x <-> X x)) as V.
assert (HAC: forall x : A -> Prop, V x -> exists a : A, x a).
{ intros. rewrite HeqV in H0. destruct H0 as [c' [H']].
destruct (U_inh _ H') as [a Ha]. exists a. now apply H0. }
destruct (choice A V HAC) as [f Hf]. exists f.
apply Hf. rewrite HeqV. exists c. exists H. split;auto. Qed.
Lemma chain_single x : chain R (fun y => y = x).
Proof. intros ? ? ? ?. subst. left. apply refl. Qed.
Definition next (x:A) :A := proj1_sig (choice_function (fun y=> y=x) (chain_single x))
(U (fun y=> y=x) (chain_single x)).
Lemma next_spec : forall x, R x (next x) /\ x <> next x.
Proof. intros x.
pose proof (proj2_sig (choice_function (fun y=> y=x) (chain_single x))) as H.
simpl in H. destruct (H x); auto. Qed.
(* we name smallest tower as M *)
Definition tower (c:A->Prop): Prop :=
(forall x, c x -> c (next x)) /\
(forall (s:A->Prop) Hs, (forall x, s x -> c x) -> c (g s Hs)).
Definition M := fun x => forall Y, tower Y -> Y x.
Lemma M_tower : tower M.
Proof. split. intros x H Y HY. specialize (H _ HY). destruct HY. auto.
intros s Hs Hi Y Hc. pose proof Hc. destruct H.
apply H0. intros x Hx. specialize (Hi _ Hx).
apply (Hi _ Hc). Qed.
Lemma proof_tower: forall P, tower P -> forall x, M x -> P x.
Proof. intros. now apply (H0 _ H). Qed.
Lemma chain_M_False: chain R M -> False.
Proof. intros.
destruct (next_spec (g M H)).
apply H1. apply ant. auto.
assert (M (next (g M H))).
{ destruct M_tower as [P1 P2]. specialize (P2 _ H). auto. }
destruct (g_spec _ H) as [Hs1 _]. auto. Qed.
Definition gapless x := forall y, M y -> R y x \/ R (next x) y.
Definition good_succ x := forall y, M y -> (R y x /\ x<>y) -> R (next y) x.
Definition N x (H:M x) := fun y => M y /\ (R y x \/ R (next x) y).
Lemma gapless_chain: (forall x, M x ->gapless x) -> chain R M.
Proof. intros H x y Hx Hy. destruct (H _ Hx _ Hy) as [H1|H1]. auto.
left. apply trans with (next x);auto.
now destruct (next_spec x). Qed.
Lemma gsucc_gapless : forall x, M x -> good_succ x -> gapless x.
Proof. intros x Hx H. intros y Hy.
enough (tower (N _ Hx)).
{ pose proof (proof_tower _ H0 _ Hy). unfold N in H1. tauto. }
clear y Hy.
split. - intros y. intros [Hy1 Hy2]. split. now apply (M_tower).
destruct Hy2.
destruct (classic (x=y)). right; subst. now apply refl.
left. apply H;auto. right.
eapply trans. eassumption. apply next_spec.
- intros c Hc H1. split.
+ pose proof (g_spec _ Hc).
destruct (M_tower). apply H3.
intros y Hy. enough (N x Hx y). { now destruct H4. }
now apply H1.
+ destruct (classic (forall y, c y -> R y x)); [left|right].
destruct (g_spec _ Hc) as [Hu1 Hu2]. auto.
destruct (not_all_ex_not _ _ H0) as [z].
destruct (imply_to_and _ _ H2).
destruct (H1 _ H3).
destruct H6. contradiction.
eapply trans. eassumption.
destruct (g_spec c Hc). auto. Qed.
Lemma M_gsucc : forall x, M x -> good_succ x.
Proof. intros x Hx. enough (tower (fun y => M y /\ good_succ y)).
{ pose proof (proof_tower _ H _ Hx). simpl in *;tauto. }
clear x Hx.
split. - (* P1 *) intros x [Hx1 Hx2].
split;[now apply M_tower|].
intros y Hy [Hy1 Hy2].
destruct(gsucc_gapless _ Hx1 Hx2 _ Hy).
2:{ exfalso. apply Hy2. apply ant; auto. }
destruct (classic (x=y)). subst. apply refl.
apply trans with (b:=x).
now apply (Hx2 y).
pose proof (next_spec x). tauto.
- (* P2 *) intros c Hc ?. split.
destruct (M_tower) as [_ Hm].
apply Hm. intros x Hx. now destruct (H _ Hx).
intros y Hy1 [Hy2 Hy3].
destruct (g_spec c Hc) as [Hg1 Hg2] .
assert (~(forall x, c x -> R x y)).
{ intros X. specialize (Hg2 _ X). apply Hy3. apply ant; auto. }
destruct (not_all_ex_not _ _ H0) as [z Xz].
destruct (imply_to_and _ _ Xz).
destruct (H _ H1).
destruct (gsucc_gapless _ H3 H4 _ Hy1).
unfold good_succ in H4.
apply trans with z.
apply H4. auto. split;auto. intros X. subst. contradiction.
now apply Hg1.
exfalso. apply H2.
apply trans with (next z).
apply next_spec. auto. Qed.
Lemma falsity : False.
Proof. apply chain_M_False.
apply gapless_chain.
intros. apply gsucc_gapless. auto.
now apply M_gsucc. Qed.
End Contradiction.
Lemma ac_imply_zorn_impl : ac_imply_zorn.
Proof. intros choice A R ZH.
unfold Zorn, maximal. apply NNPP; intros X.
eapply falsity. eassumption. auto.
pose proof (not_ex_all_not _ _ X).
intros a.
destruct (not_and_or _ _ (H a)).
tauto.
destruct (not_all_ex_not _ _ H0).
destruct (imply_to_and _ _ H1).
now exists x. Qed.
Check ac_imply_zorn_impl: Choice -> forall A R H, Zorn A R H .
Print Assumptions ac_imply_zorn_impl.
(* Axioms: classic : forall P : Prop, P \/ ~ P *)