Mercurial > hg > Papers > 2020 > kono-prosym
comparison presen.ind @ 4:353edf5ef2d9
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 09 Jan 2021 09:43:12 +0900 |
parents | 57601db306e9 |
children | 9027098a5b1d |
comparison
equal
deleted
inserted
replaced
3:57601db306e9 | 4:353edf5ef2d9 |
---|---|
1 -title: AgdaによるGalois理論のプログラミング | 1 -title: AgdaによるGalois理論のプログラミング |
2 | 2 |
3 --motivation | 3 --motivation |
4 agda say prove all of it | 4 |
5 proof carrying data structure | 5 5次方程式が代数的に解けないことの復習 |
6 --all connected | 6 |
7 not only the result | 7 数学書では省略されてても Agda は許してくれない |
8 the result is proved to be correct | 8 |
9 --What are you computing? | 9 計算で示しても、それが証明になっているかどうかは別 |
10 --Galois theory | 10 |
11 --Galois theory : polynominal equation | 11 証明付きデータ構造を使う |
12 --Galois theory : symmetric group on solutions | 12 |
13 --Galois theory : group mapping | 13 計算と証明が「全部つながってる」 |
14 --Galois theory : commutator | 14 |
15 --Galois theory : commutator group | 15 この計算、いったい、何を計算してるの? |
16 --Galois theory : solvable | 16 |
17 --proof in math text book | 17 それを型で示す |
18 --formalization in agda | 18 |
19 --Galois theory : 多項式方程式 | |
20 | |
21 (x - α)(x - β)(x - γ) = 0 | |
22 | |
23 と因数分解されればαβγが解になる。 | |
24 | |
25 --Galois theory : 解と置換群(対称群) | |
26 | |
27 αβγを入れ替えても良い(Symmetric Group))。これが | |
28 | |
29 (x - α)(x - β) = 0 | |
30 | |
31 に帰着されるなら、αβ を入れ替えても良い。ならば、αβγ の置換で | |
32 | |
33 αβγ = βαγ | |
34 | |
35 にならないとおかしい。 | |
36 | |
37 --Galois theory : 可解群 | |
38 | |
39 αβγ = βαγ | |
40 α⁻¹β⁻¹αβγγ⁻¹ = α⁻¹β⁻¹βαγγ⁻¹ | |
41 α⁻¹β⁻¹αβ = e (交換子 Commutator) | |
42 | |
43 なので、対称群のすべての要素を α⁻¹β⁻¹αβ の形にするのを繰り返して e になれば良い(可解群)。 | |
44 | |
45 (もちろん、これは証明になってない。気分的な説明。本当は正規拡大体とか代数的拡大とか) | |
46 | |
47 ここは今回は Agda で証明しません。 | |
48 | |
49 あれ? 割と Agda の得意な分野なのでできるはず。やさしくはないだろうけど | |
50 | |
51 Agdaは抽象的な証明が得意 | |
52 | |
53 --5次方程式が代数的に解けないことの証明 | |
54 | |
55 5次の対称群は可解でないことを示せばよい。2,3,4次は可解。教科書だと | |
56 | |
57 <center><img src="fig/altin.jpg"></center> | |
58 | |
59 これは良い方で、岩波だと練習問題。 | |
60 | |
61 <center><img src="fig/iwanami-gendai.jpg"></center> | |
62 | |
63 --数学の本の記述の特徴 | |
64 | |
65 理解した後で読むとちゃんと書いてある | |
66 | |
67 理解する前には何が書いてあるのかわからない | |
68 | |
69 --Agda でちゃんとやろうぜ | |
70 | |
71 Curry Howard 対応に基づく定理証明支援系 | |
72 | |
73 依存型を持つ純関数型言語 | |
74 | |
75 依存型とは、型を値に持つ変数 | |
76 | |
77 命題そのものは Set という型を持つ | |
78 | |
79 構文的には Haskell とほぼ同じ。Coq と違い、何もしてくれない。全部、自分で証明を書く。(いさぎよい) | |
80 | |
19 --Agda : lambda | 81 --Agda : lambda |
82 | |
83 A → B の証明 | |
84 | |
85 →intro : {A B : Set } → A → B → ( A → B ) | |
86 →intro _ b = λ x → b | |
87 | |
88 →elim : {A B : Set } → A → ( A → B ) → B | |
89 →elim a f = f a | |
90 | |
91 引数の値は、型の証明 | |
92 | |
93 入力は∀が付いていると考える(∃はあとで) | |
94 | |
95 --Agda : record | |
96 | |
97 A ∧ B の証明 | |
98 | |
99 record _∧_ (A B : Set) : Set where | |
100 field | |
101 proj1 : A | |
102 proj2 : B | |
103 | |
104 ∧elim : {A B : Set} → ( A ∧ B ) → A | |
105 ∧elim a∧b = proj1 a∧b | |
106 | |
107 ∧intro : {A B : Set} → A → B → ( A ∧ B ) | |
108 ∧intro a b = record { proj1 = a ; proj2 = b } | |
109 | |
20 --Agda : data | 110 --Agda : data |
21 --Agda : record | 111 |
112 A ∨ B の証明 | |
113 | |
114 data _∨_ (A B : Set) : Set where | |
115 case1 : A → A ∨ B | |
116 case2 : B → A ∨ B | |
117 | |
118 ∨intro : {A B : Set} → A → ( A ∨ B ) | |
119 ∨intro a = case1 | |
120 | |
121 ∨elim : {A B : Set} → ( A ∨ A ) → A | |
122 ∨elim (case1 a) = a | |
123 ∨elim (case2 a) = a | |
124 | |
125 --Agda : negation | |
126 | |
127 data ⊥ : Set where | |
128 | |
129 constructor のないデータ構造(偽 | |
130 | |
131 ⊥-elim : {A : Set } -> ⊥ -> A | |
132 ⊥-elim () | |
133 | |
134 起きない入力は () 。λ () とも書ける | |
135 | |
136 data ⊤ : Set where | |
137 tt : ⊤ | |
138 | |
139 要素が一つしかない型(真 | |
140 | |
22 --Agda : unification | 141 --Agda : unification |
23 equation | 142 |
143 data _≡_ {A : Set } : A → A → Set where | |
144 refl : {x : A} → x ≡ x | |
145 | |
146 ≡intro : {A : Set} {x : A } → x ≡ x | |
147 ≡intro = refl | |
148 | |
149 ≡elim : {A : Set} {x y : A } → x ≡ y → y ≡ x | |
150 ≡elim refl = refl | |
151 | |
152 項(正規化された)として等しい。変数はどうするの? 十分に instanciation されない場合は黄色くなる。 | |
153 | |
154 その他、細かい問題が... internal parametricity... inspect... | |
155 | |
156 でも、これで全部。さぁ、Agda を書こう。 | |
157 | |
24 --Galois theory i nAgda : Commutator | 158 --Galois theory i nAgda : Commutator |
25 --Galois theory in Agda : Set valued function | 159 |
160 [_,_] : Carrier → Carrier → Carrier | |
161 [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h | |
162 | |
163 こんな風に数学の教科書通りに Unicode を使って書けるところが Agda の良いところ | |
164 | |
165 data Commutator (P : Carrier → Set ) : (f : Carrier) → Set where | |
166 comm : {g h : Carrier} → P g → P h → Commutator P [ g , h ] | |
167 ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g | |
168 | |
169 deriving : ( i : ℕ ) → Carrier → Set | |
170 deriving 0 x = ⊤ | |
171 deriving (suc i) x = Commutator (deriving i) x | |
172 | |
173 Set を返してるのはなに? Set は何かの命題、 つまり真偽として扱って良い。したがって | |
174 | |
175 P : Carrier → Set | |
176 | |
177 これは Carrier の部分集合を指定する命題となる。 (Carrier は群の要素の型) | |
178 | |
179 交換子 Commutator p は述語 f p で限定された p : Carrier が [ g , h ] という形で生成されることを示している。 | |
180 | |
181 deriving i は、Carrier の部分集合で、Commutator を再帰的に繰り返して得られたもの | |
182 | |
26 --Galois theory in Agda : Solvable | 183 --Galois theory in Agda : Solvable |
184 | |
185 record solvable : Set (Level.suc n ⊔ m) where | |
186 field | |
187 dervied-length : ℕ | |
188 end : (x : Carrier ) → deriving dervied-length x → x ≈ ε | |
189 | |
190 存在∃は record で書く。ある dervied-length : ℕ があって、その回数のderive の繰り返しで x ≈ ε になる | |
191 | |
192 この record を構成できれば、その群は可解ということになる。これで問題は定義できた | |
193 | |
27 --Galois theory in Agda : Symmetric group | 194 --Galois theory in Agda : Symmetric group |
195 | |
196 対称群の要素は置換だが、Agdaの標準ライブラリだと有限な数のBijectionとして定義される | |
197 | |
198 Permutation p p | |
199 | |
200 定義は複雑だが二つの写像 _⟨$⟩ˡ_ _⟨$⟩ʳ_ と y ⟨$⟩ˡ (y ⟨$⟩ʳ x) ≡ x と y ⟨$⟩ʳ (y ⟨$⟩ˡ x) ≡ x からなる record | |
201 | |
202 残念ながら扱いにくい。同等性とか。単純に x ≡ y を証明できない(Agdaの制約 1) | |
203 | |
204 しかし群であることを示すのは簡単 | |
205 | |
28 --Permutation : Data.Fin | 206 --Permutation : Data.Fin |
29 --Permutation : Bijection | 207 |
208 有限な数 | |
209 | |
210 data Fin : ℕ → Set where | |
211 zero : {n : ℕ} → Fin (suc n) | |
212 suc : {n : ℕ} (i : Fin n) → Fin (suc n) | |
213 | |
214 x : Fin 3 のように使う | |
215 | |
216 Fin 0 の値は存在しない | |
217 | |
218 _⟨$⟩ˡ_ : Fin p → Fin p | |
219 | |
30 --Permutation : List | 220 --Permutation : List |
31 --Permutation : FL | 221 |
222 置換は List ℕ で表されるので、それで良いのだが、List ℕ が全部置換になるわけではない | |
223 | |
224 そこで減少列 FL とその大小関係を定義する | |
225 | |
226 data FL : (n : ℕ )→ Set where | |
227 f0 : FL 0 | |
228 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n) | |
229 | |
230 data _f<_ : {n : ℕ } (x : FL n ) (y : FL n) → Set where | |
231 f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn → (xn :: xt) f< ( yn :: yt ) | |
232 f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt → (xn :: xt) f< ( xn :: yt ) | |
233 | |
234 すると、これは置換と 1 to 1 になる。しかし 1 to 1 の証明は煩雑。しかし、簡単な方法があるかも。 | |
235 | |
236 煩雑でも証明できてしまえば問題ないので、簡単にする motivation はあまりでない。 | |
237 | |
238 でも簡単にしておくと、次に使えるかも。 | |
239 | |
32 --Proofs : 2 | 240 --Proofs : 2 |
33 --Proofs : Injection | 241 |
242 これで道具立てはそろったので証明に行く | |
243 | |
244 まず、二次対称群から | |
245 | |
246 sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) | |
247 sym2lem0 = ? | |
248 solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid | |
249 solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h } | |
250 | |
251 となるのだが、g と h が何かわからないので FL 2 に変換する | |
252 | |
253 FL 2 は | |
254 | |
255 zero :: (zero :: f0) | |
256 | |
257 というものなので、これが pid つまり恒等置換であることは証明してあるのだが | |
258 | |
259 FL-inject : {n : ℕ } → {g h : Permutation n n } → perm→FL g ≡ perm→FL h → g =p= h | |
260 | |
261 を証明して使う。ところが、 | |
262 | |
263 pleq : {n : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y | |
264 | |
265 を使うと | |
266 | |
267 p0 : FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid | |
268 p0 = pleq _ _ refl | |
269 | |
270 とできる。Injection は圏論でいう Equalizaer で写像した先で等しいなら手元でも等しいという性質 | |
271 | |
34 --Proofs : 3 | 272 --Proofs : 3 |
273 | |
274 2でこれなので 3 は絶望的に煩雑になる | |
275 | |
276 たぶん、ガロアはそれを手で計算したはず | |
277 | |
35 --Proofs : 5 | 278 --Proofs : 5 |
36 | 279 |
37 --A list contains everything | 280 5は、solvable が存在しない、つまり否定を示せばよい |
38 sorted | 281 solvable から矛盾 counter-example を作る |
39 any | 282 |
283 ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) | |
284 ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where | |
285 | |
286 3次の対称群を含むことを示せばよいのだが、それが dervie-any-3rot0 | |
287 実は dervie-any-3rot0 と dervie-any-3rot1 がいる | |
288 | |
289 教科書だと「要素三つがとれるよね」と書いてあるが、Agda だと具体的に取ってくる必要がある。「あとは同じだよね」 | |
290 と書いてあっても、それを示す必要がある。 | |
291 | |
292 --もっと簡単にできるでしょ | |
293 | |
294 derving は簡単に計算できるので、それで証明した方が良いんじゃないの? | |
295 | |
296 確かにその通り | |
297 | |
298 計算は簡単だが、それを証明にするにはどうすれば良いの? | |
299 | |
300 すべての交換子の組み合せを計算している | |
301 | |
302 を証明すればよい | |
303 | |
304 つまり sort された List に、全部の要素が含まれている (どんな要素でも入っている) any | |
305 ことを Agda で書く | |
306 | |
307 それには Fresh List というのを使う | |
308 | |
40 --Fresh List | 309 --Fresh List |
41 Set valued function | 310 |
42 proof carrying data structure | 311 (A : Set )と (R : A → A → Set) に対して |
312 | |
313 data List# : Set | |
314 [] : List# | |
315 cons : (a : A) (as : List#) → fresh a as → List# | |
316 | |
317 という List を定義する | |
318 | |
319 fresh : (a : A) (as : List#) → Set | |
320 fresh a [] = ⊤ | |
321 fresh a (cons x xs _) = R a ∧ fresh a xs | |
322 | |
323 普通の∷ (cons)の代わりに _∷#_ を使う | |
324 | |
325 infixr 5 _∷#_ | |
326 pattern _∷#_ x xs = cons x xs _ | |
327 | |
328 これも Set を値にしている。Fresh List の最後とそうでないもので fresh の中身が違う | |
329 | |
330 List の要素毎に、fresh が存在するので、結構でかいものになる(O(2^n))。 | |
331 | |
332 <center><img src="fig/fresh.svg"></center> | |
333 | |
334 FList : (n : ℕ ) → Set | |
335 FList n = List# (FL n) ⌊ _f<?_ ⌋ | |
336 | |
337 fr1 : FList 3 | |
338 fr1 = | |
339 ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# | |
340 ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# | |
341 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# | |
342 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# | |
343 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# | |
344 [] | |
345 | |
346 と定義できる。これで FList 3 が sort されていることが「証明されている」。 | |
347 ⌊ _f<?_ ⌋ が不思議だが... | |
348 | |
43 --Fresh List : Any | 349 --Fresh List : Any |
44 here | 350 |
45 there | 351 data Any : List# A R → Set where |
352 here : ∀ {x xs pr} → P x → Any (cons x xs pr) | |
353 there : ∀ {x xs pr} → Any xs → Any (cons x xs pr) | |
354 | |
355 ここにあったら here、先にあるなら there | |
356 | |
46 --Fresh List : Insert | 357 --Fresh List : Insert |
358 | |
359 普通の insert と変わらないけど、fresh を作る必要がある | |
360 | |
361 FLinsert : {n : ℕ } → FL n → FList n → FList n | |
362 FLinsert {zero} f0 y = f0 ∷# [] | |
363 FLinsert {suc n} x [] = x ∷# [] | |
364 FLinsert {suc n} x (cons a y x₁) with FLcmp x a | |
365 ... | tri≈ ¬a b ¬c = cons a y x₁ | |
366 ... | tri< lt ¬b ¬c = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁) | |
367 FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) | |
368 FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr ) | |
369 | |
47 --Fresh List : Property on Insert / Cons | 370 --Fresh List : Property on Insert / Cons |
48 | 371 |
49 Any | 372 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_) (FLinsert x xs) |
373 nextAny : {n : ℕ} → {x h : FL n } → {L : FList n} → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_) L → Any (x ≡_) (cons h L hr ) | |
374 insAny : {n : ℕ} → {x h : FL n } → (xs : FList n) → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs) | |
375 | |
376 あたりがあると便利 | |
377 | |
378 --Fresh List : Any on Pair | |
379 | |
380 Commutator (それを作っていたのだった) は任意の pair なので | |
381 | |
382 record AnyComm {n m l : ℕ} (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where | |
383 field | |
384 commList : FList l | |
385 commAny : (p : FL n) (q : FL m) | |
386 → Any ( p ≡_ ) P → Any ( q ≡_ ) Q | |
387 → Any (fpq p q ≡_) commList | |
388 | |
389 つまり二つの FList から、組を全部生成する必要がある。(fpq は ∧ の方が良かったか?) | |
390 | |
391 (p,q) (p,qn) .... (p,q0) | |
392 pn,q | |
393 : AnyComm FL0 FL0 P Q | |
394 p0,q | |
395 | |
396 こんな風に再帰で作れる(やさしくない | |
397 | |
398 --Fresh List : Solved using Fresh List | |
399 | |
400 まず全部の FL が入ってる FList | |
401 | |
402 record AnyFL (n : ℕ) : Set where | |
403 field | |
404 allFL : FList n | |
405 anyP : (x : FL n) → Any (x ≡_ ) allFL | |
406 | |
407 これは AnyComm から作れる (やさしくない | |
408 | |
409 次に Commutator | |
410 | |
411 CommFListN : ℕ → FList n | |
412 CommFListN zero = allFL (anyFL n) | |
413 CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q → perm→FL [ FL→perm p , FL→perm q ] )) | |
414 | |
415 そして、Commutator がちゃんと全部入っていることを示す(やさしい | |
416 | |
417 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i) | |
418 | |
419 すると | |
420 | |
421 CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid | |
422 | |
423 という形で可解を定義できる。 | |
50 | 424 |
51 --Proofs : 2 | 425 --Proofs : 2 |
52 --Proofs : 3 | 426 |
427 以下のように極めて簡単になった(やった! | |
428 | |
429 stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt) | |
430 stage2FList = refl | |
431 | |
432 solved1 : (x : Permutation 2 2) → deriving 1 x → x =p= pid | |
433 solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList p0id solved0 where | |
434 solved0 : Any (perm→FL x ≡_) ( CommFListN 2 1 ) | |
435 solved0 = CommStage→ 2 1 x dr | |
436 | |
437 このまま 3, 4を証明可能 | |
438 | |
53 --Proofs : 5 | 439 --Proofs : 5 |
54 two sym 3 | 440 |
55 --Proofs : 4 | 441 e 以外を含む stage 3 が stage 4 と同じことを示すだけで可解でないことを示せる |
56 --Proofs : 5 | 442 |
57 compilation | 443 しかし5を計算すると停まらない(きっと停まるが遅すぎる |
58 --Analysis | 444 |
445 メモリは食わない (FList 5 自体は計算できて、それで抑えられる) | |
446 | |
447 単に計算が遅い | |
448 | |
449 --時間 | |
450 | |
451 agda sym3.agda 258.01s user 2.95s system 98% cpu 4:23.68 total | |
452 agda sym3n.agda 9.18s user 0.45s system 95% cpu 10.089 total | |
453 agda sym2n.agda 9.09s user 0.35s system 99% cpu 9.454 total | |
454 agda sym2.agda 9.34s user 0.50s system 94% cpu 10.448 total | |
455 agda sym4.agda 9.38s user 0.37s system 99% cpu 9.784 total | |
456 agda sym5.agda 9.04s user 0.34s system 99% cpu 9.427 total | |
457 | |
458 | |
459 --しかし、Agda には compiler が! | |
460 | |
461 コンパイルすれば計算可能 | |
462 | |
463 ./sym5n 0.00s user 0.01s system 37% cpu 0.044 total | |
464 | |
465 | |
466 ただし、それは証明には接続できない | |
467 | |
468 型検査時に compile して計算する機能はない | |
469 | |
470 | |
59 --Analysis : overhead of proof carrying data structure | 471 --Analysis : overhead of proof carrying data structure |
60 type | 472 |
61 heap | 473 Fin, Commutator, FL, Fresh , Any, FList は、すべて証明付きデータ構造 |
62 product | 474 |
63 type check | 475 証明は実行時ではなく型検査時に行われるので実行時のオーバヘッドは理論的にはない |
64 compiled | 476 |
477 Any や fresh は実行されない型しか計算しないコードになる | |
478 | |
479 しかし、Fresh は Product を含んでいるので実際に heapを食うのでオーバーヘッドがあるように見える | |
480 | |
481 ところが、それは使われないので実行時には明示的に触らない限り生成されない(遅延評価 | |
482 | |
483 なので、普通に高速に計算される | |
484 | |
65 --Analysis connection of computation and type | 485 --Analysis connection of computation and type |
66 | 486 |
487 普通は何を計算したのかは計算機は知らない | |
488 | |
489 まして作った人以外はさっぱりわからない | |
490 | |
491 しかし、証明付きデータならば、そこに何を計算したのかが書いてある | |
492 | |
493 ただ | |
494 | |
495 プログラミングは、めっちゃ面倒 | |
496 | |
497 でも、それができるならプログラミングの信頼性は上がる | |
498 | |
499 しかし、それでも完全に正しいとは... | |
500 | |
67 --Appendix : ZF fix | 501 --Appendix : ZF fix |
68 od max | 502 |
69 Set and Class | 503 証明があっても正しいとは限らない |
504 | |
505 去年のZFには間違いがあって | |
506 | |
507 record OD : Set (suc n ) where | |
508 field | |
509 def : (x : Ordinal ) → Set n | |
510 | |
511 OD ⇔ Ordinal を要求すると矛盾になる | |
512 | |
513 ¬OD-order : ( & : OD → Ordinal ) → ( * : Ordinal → OD ) → ( { x y : OD } → def y ( & x ) → & x o< & y) → ⊥ | |
514 ¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj ) | |
515 | |
516 なので最大値を付けてやると良い | |
517 | |
518 record HOD : Set (suc n) where | |
519 field | |
520 od : OD | |
521 odmax : Ordinal | |
522 <odmax : {y : Ordinal} → def od y → y o< odmax | |
523 | |
524 つまり証明が合ってても仮定が間違ってたらダメ | |
525 | |
526 これは (集合論の用語での) Set と Class の区別になっている。つまり OD が Class で、最大値があれば集合になる。 | |
527 | |
70 --Appendix : Topology | 528 --Appendix : Topology |
71 Tychonov | 529 |
72 | 530 今年は |
73 --Appendix : ZF | 531 |
74 cohen model | 532 record Toplogy ( L : HOD ) : Set (suc n) where |
533 field | |
534 OS : HOD | |
535 OS⊆PL : OS ⊆ Power L | |
536 o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P | |
537 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) | |
538 | |
539 やっても良いかも。 Tychonovの定理の証明とか(やさしくなさそう | |
540 | |
541 あるいは ZF の cohen model とか | |
542 | |
543 record Filter ( L : HOD ) : Set (suc n) where | |
544 field | |
545 filter : HOD | |
546 f⊆PL : filter ⊆ Power L | |
547 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q | |
548 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) | |
549 | |
550 Topology と Filter は似てることがわかる | |
551 | |
552 --Permutation : 等号 | |
553 | |
554 record _=p=_ {p : ℕ } ( x y : Permutation p p ) : Set where | |
555 field | |
556 peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q | |
557 | |
558 を統合して使う | |
559 | |
560 x ≡ y → x =p y | |
561 | |
562 は言えるが | |
563 | |
564 x =p y → x ≡ y | |
565 | |
566 は仮定するしかない。(Functional Extentionality) | |
567 | |
568 --Permutation : Data.Fin と Data.Nat | |
569 | |
570 suc と zero が自然数と重なっていて扱いを気をつける必要がある | |
571 | |
572 data ℕ : Set where | |
573 zero : ℕ | |
574 suc : ℕ → ℕ | |
575 | |
576 x ∧ x < n で不等号を持ち歩く方法でも良いのだが... | |
577 | |
578 x < n も | |
579 | |
580 data _≤_ : Rel ℕ 0ℓ where | |
581 z≤n : ∀ {n} → zero ≤ n | |
582 s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n | |
583 | |
584 と再帰的データ構造なので二重に持ち歩くことになるので美しくない | |
585 | |
586 --Permutation : FL と Permutation の対応の証明 | |
587 | |
588 Permutation の combinator 表現を使う | |
589 | |
590 pprep 先頭に一つ置換を増やす | |
591 pswap 先頭の二つを入れ替える | |
592 | |
593 これだけで任意の置換を構成できる | |
594 | |
595 これから pins という任意の置換に任意の位置に 0(の位置の要素) を入れる関数を作る | |
596 | |
597 そして、pins の逆を | |
598 | |
599 pshrink 置換を一つ減らす | |
600 | |
601 を作って構成する | |
602 | |
603 極めて煩雑な証明になる | |
604 | |
605 | |
606 --Fresh List : witness | |
607 | |
608 ⌊ _f<?_ ⌋ は witness と呼ばれるもので、 | |
609 | |
610 data Dec : {R : FL → FL → Set} : Set where | |
611 yes : R → Dec R | |
612 no : ¬ R → Dec R | |
613 | |
614 x f<? y with FLcmp x y | |
615 ... | tri< a ¬b ¬c = yes a | |
616 ... | tri≈ ¬a refl ¬c = no ( ¬a ) | |
617 ... | tri> ¬a ¬b c = no ( ¬a ) | |
618 | |
619 | |
620 --sym5 | |
621 | |
622 abc が反例。これが常に残ることを示す | |
623 | |
624 counter-example : ¬ (abc 0<3 0<4 =p= pid ) | |
625 counter-example eq with ←pleq _ _ eq | |
626 ... | () | |
627 | |
628 二つ余地を確保する | |
629 | |
630 ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 | |
631 ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) | |
632 | |
633 abc と dba を作る | |
634 | |
635 abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 | |
636 abc i<3 j<4 = ins2 3rot i<3 j<4 | |
637 dba : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 | |
638 dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4 | |
639 | |
640 abc が derive されることを示す | |
641 | |
642 dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) | |
643 → deriving n (abc i<3 j<4 ) | |
644 dervie-any-3rot0 0 i<3 j<4 = lift tt | |
645 dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where | |
646 commd : {n : ℕ } → (f g : Permutation 5 5) | |
647 → deriving n f | |
648 → deriving n g | |
649 → Commutator (deriving n) [ f , g ] | |
650 commd {n} f g df dg = comm {deriving n} {f} {g} df dg | |
651 | |
652 df と dg が前に derive されたもの | |
653 | |
654 df = dervie-any-3rot1 i (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) | |
655 dg = dervie-any-3rot1 i (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) | |
656 | |
657 それは、再帰的に作れるのだが種(dbaとaec)を二つ計算する必要がある | |
658 | |
659 それは右回転と左回転があって、 dervie-any-3rot0 と dervie-any-3rot1 で交互に作られる | |
660 | |
661 そのつくり方だが... | |
662 | |
663 tc = triple i<3 j<4 | |
664 dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) | |
665 aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) | |
666 ceq : abc i<3 j<4 =p= [ dba0 , aec0 ] | |
667 ceq = record { peq = peq (abc= tc) } | |
668 | |
669 dba と aec を作るのだが | |
670 | |
671 record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where | |
672 field | |
673 dba0<3 : Fin 4 | |
674 dba1<4 : Fin 5 | |
675 aec0<3 : Fin 4 | |
676 aec1<4 : Fin 5 | |
677 abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] | |
678 | |
679 open Triple | |
680 triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot | |
681 triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
682 triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
683 .... | |
684 | |
685 と自分でうまく2つの余地を選択する必要がある | |
686 | |
687 もちろん、計算することは可能だが... | |
688 |