Zorn の補題の Agda での証明完了

いや、3月くらいからやってて、かなり難航したんですができました。詳細はプロシンで話すので興味のある方はどうぞ。

　　record SUP ( A B : HOD )　: Set (Level.suc n) where
　　　 field
　　　　　sup : HOD
　　　　　ax : odef A x
　　　　　x≤sup　 : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -- B is Total, use positive

　　record Maximal ( A : HOD )　: Set (Level.suc n) where
　　　 field
　　　　　maximal : HOD
　　　　　as : A ∋ maximal
　　　　　¬maximal<x : {x : HOD} → A ∋ x　→ ¬ maximal < x　　　 -- A is Partial, use negative

　　Zorn-lemma : { A : HOD }
　　　　→ o∅ o< & A
　　　　→ ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B　 ) -- SUP condition
　　　　→ Maximal A

定理自体はこれだけ。HODってのが、今回使ってる Agda で実装した ZF 集合論の集合。遺伝的順序数定義可能集合(Heritic Ordinal Definable Set)ですね。

Kunen と田中先生の本には載ってるけど、ちょっとずれてる。ってことは、別な集合論の公理をAgda用に作ったわけ。

A上の単調増加関数 f x と、その閉包 FClosure A f x を与える上界関数列 supf x 、そして、それが定義するAの全順序部分集合列 UnionCF A f supf x
と、それらの性質を表す record である ZChain で、

　　全部で 1800行

nvim 上でチェックにかかる時間は5分。agda command だと6秒。なんなの。メモリは7GB。なんだが、ソースコードを工夫したら3GBに。

時間がかかった理由はいろいろあるが、最小上界でなくてもできると思ったのが間違いで、さらに、≤ な関数で fixpoint を示せると
思ったのが間違いで、まぁ、それではだめなのに気づくのに試行錯誤しまくったのがだめだったみたい。

その辺の証明を正確に追うことも可能なんですが、あんまり Agda っぽくないしな。整列集合の切片とかのあれですね。

でも、まぁ、証明自体は岩波現代数学概説に沿っているはずです。

これで、Generic Filter の存在とか、チコノフの定理とかが示せるはずです。