Mercurial > hg > Papers > 2020 > kono-prosym
comparison galois-prosym.ind @ 1:b169617e42e5
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 03 Dec 2020 17:50:45 +0900 |
parents | e2071e2490a2 |
children | 72ec93c67ab2 |
comparison
equal
deleted
inserted
replaced
0:e2071e2490a2 | 1:b169617e42e5 |
---|---|
217 | 217 |
218 ここで {\tt ¬ A = A → ⊥} であり、⊥ は生成子のない data である。sol には仮定した solvable が来る。 | 218 ここで {\tt ¬ A = A → ⊥} であり、⊥ は生成子のない data である。sol には仮定した solvable が来る。 |
219 {\tt abc 0<3 0<4} は5つのFinのうち、a を b に、bをcに、cをaに置換する置換である。これが何回交換子を | 219 {\tt abc 0<3 0<4} は5つのFinのうち、a を b に、bをcに、cをaに置換する置換である。これが何回交換子を |
220 作っても残ってしまうことはアルティンの邦訳には以下のような証明が載っている。基本的にこれを証明することになる。 | 220 作っても残ってしまうことはアルティンの邦訳には以下のような証明が載っている。基本的にこれを証明することになる。 |
221 | 221 |
222 abc 以外の二つの要素とかを Agda では具体的に指摘する必要があり、これが一般的に成立することも示す必要がある。 | |
223 Agda によれば | |
224 | |
225 全部証明しろ | |
226 | |
227 ということになる。 | |
222 | 228 |
223 --Permutationに対応するデータ構造 | 229 --Permutationに対応するデータ構造 |
224 | 230 |
225 有限な自然数 Fin の一対一対応 Bijection が Permutation だが 関数なので見えない。 | 231 有限な自然数 Fin の一対一対応 Bijection が Permutation だが 関数なので見えない。 |
226 これを数え上げる必要があるので、もっと具体的なものが望ましい。 | 232 これを数え上げる必要があるので、もっと具体的なものが望ましい。 |
241 f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn → (xn :: xt) f< ( yn :: yt ) | 247 f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn → (xn :: xt) f< ( yn :: yt ) |
242 f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt → (xn :: xt) f< ( xn :: yt ) | 248 f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt → (xn :: xt) f< ( xn :: yt ) |
243 | 249 |
244 これは順列と1対1対応するので都合が良い。 | 250 これは順列と1対1対応するので都合が良い。 |
245 | 251 |
246 --Permutationの数え上げ | 252 --PermutationとFL nの対応 |
253 | |
254 FL n が置換に対応することは証明する必要がある。ここでは順列の combinator を使う。 | |
255 | |
256 FL→perm : {n : ℕ } → FL n → Permutation n n | |
257 FL→perm f0 = pid | |
258 FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x ) | |
259 | |
260 perm→FL : {n : ℕ } → Permutation n n → FL n | |
261 perm→FL {zero} perm = f0 | |
262 perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) | |
263 | |
264 pprep は先頭に 0 を付加する。{\tt 0 ∷ 1 ∷ 2 ∷ []} が{0 ∷ 1 ∷ 2 ∷ 3 ∷ []}になる。 | |
265 pins は 0 を指定した位置に挿入する。{\tt 0 ∷ 1 ∷ 2 ∷ 3 ∷ []} が {\tt 1 ∷ 2 ∷ 0 ∷ 3 ∷ []}にするような順列に対する演算である。 | |
266 shirink は pins の逆演算で 0 の位置を指定する p=0 を使っている。 | |
267 | |
268 shrink : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n | |
269 | |
270 つまり、その位置の置換先が0でないと shrink は呼び出せない。pins/shrinkはBijection を構成するのでやや複雑。 | |
271 | |
272 問題は、FL→perm と perm→FL が Bijection であることを示すことだが、 | |
273 | |
274 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm) refl =p= perm | |
275 shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} | |
276 → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0) → pprep (shrink perm p=0) =p= perm | |
277 | |
278 が比較的簡単に示せるのでそれを使って証明できる。 | |
247 | 279 |
248 --実際の証明 | 280 --実際の証明 |
249 | 281 |
250 | 282 数え上げは FL n でおこなうのだが、 |
283 | |
284 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid | |
285 | |
286 を示そうと思うとかなり面倒なことになる。しかし、ここで equalizer を使うと楽になる。 | |
287 置換は数字の列で表される。その列が等しければ、元の置換も等しいことが証明できる。 | |
288 | |
289 pleq : {n : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y | |
290 | |
291 これを使って | |
292 | |
293 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid | |
294 p0id = pleq _ _ refl | |
295 | |
296 という風に簡単に証明できる。plist0 x は具体的なλ項どうしの比較だから refl で良い。pleq の証明は | |
297 plist0 の algorythm を二つの項 x, yで同時にたどって、入力 q : Fin n に対して (x ⟨$⟩ʳ q) ≡ (y ⟨$⟩ʳ q) | |
298 を示していけばよい。 | |
299 | |
300 3次では | |
301 | |
302 p3 = FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) | |
303 p4 = FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) | |
304 st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4) | |
305 | |
306 になるのだが、これを3次対称群の要素全部に付いて確認する必要がある。 | |
307 | |
308 st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4) | |
309 st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h | |
310 ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) ) | |
311 ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g)\ | |
312 ) | |
313 ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = | |
314 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) | |
315 ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = | |
316 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) | |
317 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = | |
318 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) | |
319 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = | |
320 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) | |
321 ... | |
322 | |
323 というように50行程度書く必要がある。この証明チェックには数分かかる。 | |
324 | |
325 --5次対称群 | |
326 | |
327 abc は以下のようにpinsなどで定義できる。 | |
328 | |
329 --- 1 ∷ 2 ∷ 0 ∷ [] abc | |
330 3rot : Permutation 3 3 | |
331 3rot = pid {3} ∘ₚ pins (n≤ 2) | |
332 | |
333 save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 | |
334 save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) | |
335 | |
336 ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 | |
337 ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) | |
338 | |
339 abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 | |
340 abc i<3 j<4 = ins2 3rot i<3 j<4 | |
341 | |
342 これを交換子から生成してやればよい。{\tt [ dba , aec ]} なのだが、場所を正確に指定する必要がある。 | |
343 | |
344 record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where | |
345 field | |
346 dba0<3 : Fin 4 | |
347 dba1<4 : Fin 5 | |
348 aec0<3 : Fin 4 | |
349 aec1<4 : Fin 5 | |
350 abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) | |
351 , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] | |
352 | |
353 これをすべての場所に付いて record を作成する。 | |
354 | |
355 triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot | |
356 triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
357 triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
358 .... | |
359 | |
360 これだけでは閉じてなくて、もう一種類必要になる。 | |
361 | |
362 dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot ) | |
363 | |
364 つまり、5次対称群の中で3次の置換は二種類にわかれて存在していて、それらが交互に交換子を生成するようになっている。 | |
365 | |
366 dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) | |
367 → deriving n (abc i<3 j<4 ) | |
368 dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) | |
369 → deriving n (dba i<3 j<4 ) | |
370 | |
371 この二つが相互参照している構造になっている。本の証明ではそれを気にする必要はないが、Agda は出目を気にするので必要である。 | |
372 | |
373 このチェックにも時間はかかるが、3次対称群ほどではない。 | |
374 | |
375 しかし、この方法では 4次対称群の可解性を示すのは厳しい。そこで、Sorted List である Fresh List を使う。 | |
251 | 376 |
252 --Fresh List | 377 --Fresh List |
253 | 378 |
254 各要素の大小関係がすべて入っている sort された List 。これを使うと重複要素を排除できる。 | 379 各要素の大小関係がすべて入っている sort された List 。これを使うと重複要素を排除できる。 |
255 | 380 |
280 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# | 405 ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# |
281 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# | 406 ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# |
282 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# | 407 ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# |
283 [] | 408 [] |
284 | 409 |
285 などとできる。 | 410 などとできる。Sort されてないものを定義することはできない。 |
286 | 411 |
287 --Fresh List insert | 412 fresh は Set 、つまり命題を返す形なので、値が十分に決まらないと証明するものもわからない。 |
288 | 413 |
289 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 | 414 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 |
290 | 415 |
291 とできれば。 | 416 とできれば良い。FLinsert は単なる線形挿入だが、fresh listを証明する必要がある。 |
292 | 417 |
293 FLinsert : {n : ℕ } → FL n → FList {n} → FList {n} | 418 FLinsert : {n : ℕ } → FL n → FList n → FList n |
419 FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x | |
420 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y) | |
294 FLinsert {zero} f0 y = f0 ∷# [] | 421 FLinsert {zero} f0 y = f0 ∷# [] |
295 FLinsert {suc n} x [] = x ∷# [] | 422 FLinsert {suc n} x [] = x ∷# [] |
296 FLinsert {suc n} x (cons a y x₁) with total x a | 423 FLinsert {suc n} x (cons a y x₁) with FLcmp x a |
297 ... | inj₁ (case1 eq) = cons a y x₁ | 424 ... | tri≈ ¬a b ¬c = cons a y x₁ |
298 FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (ttf< lt ) , ttf a y x₁) where | 425 ... | tri< lt ¬b ¬c = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁) |
299 ttf : (a : FL (suc n)) → (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y | 426 FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) |
300 ttf a [] fr = Level.lift tt | 427 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 ) |
301 ttf a (cons a₁ y x1) (lift lt1 , _ ) = (Level.lift (ttf< {!!} )) , ttf a₁ y x1 | 428 |
302 ... | inj₂ (case1 eq) = cons a y x₁ | 429 という形で、FLinsert と FLfresh で相互再帰していく。 |
303 ... | inj₂ (case2 lt) = cons a (cons x y {!!}) {!!} | 430 |
431 {\tt ⌊ _f<?_ ⌋} は{\tt _f<?_}のままでは Set で扱いづらいので、それが真なのか偽なのかを表す data である。fromWitness や toWitness | |
432 で変換する。中には不等号を表す data 構造が入る。fresh の base は ⊤ なので {\tt Level.lift tt}が最後に来る。 | |
433 {\tt R a x × fresh a xs} はみづらいが、直積で不等号と、後に続く fresh の条件リストがある。 | |
304 | 434 |
305 --Permuation の数え上げ | 435 --Permuation の数え上げ |
306 | 436 |
307 全部のPermutationをListにする。全部入っていることをデータ構造として表す | 437 全部のPermutationをFresh Listにする。全部入っていることをデータ構造として表すには以下の data を使う。 |
308 | 438 |
309 data Any : List# A R → Set (p ⊔ a ⊔ r) where | 439 data Any : List# A R → Set (p ⊔ a ⊔ r) where |
310 here : ∀ {x xs pr} → P x → Any (cons x xs pr) | 440 here : ∀ {x xs pr} → P x → Any (cons x xs pr) |
311 there : ∀ {x xs pr} → Any xs → Any (cons x xs pr) | 441 there : ∀ {x xs pr} → Any xs → Any (cons x xs pr) |
312 | 442 |
313 ここにある、あそこにあるみたいな感じ。 | 443 ここにある、あそこにあるみたいな感じである。 |
314 | 444 |
315 AnyFList : (n : ℕ ) → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax) | 445 AnyFList : (n : ℕ ) → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax) |
316 | 446 |
317 が示せれば、∀Flist fmax に全部の FL n が入っていることがわかる。 | 447 が示せれば、∀Flist fmax に全部の FL n が入っていることがわかる。 |
318 | 448 |
449 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n) → Any (x ≡_ ) (FLinsert x xs) | |
450 insAny : {n : ℕ} → {x h : FL n } → (xs : FList n) → Any (x ≡_ ) xs → Any (x ≡_ ) (FLinsert h xs) | |
451 | |
452 などが証明できるのでこれを使う。 | |
453 | |
319 --数え上げの方法 | 454 --数え上げの方法 |
320 | 455 |
321 Flist1 : {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n) | 456 FL n は一つ小さいリストの前に、0からnまでを付け加えることで数え上げられる。 |
322 Flist1 zero i<n [] _ = [] | 457 この方法だと fresh を作るのに相互再帰は必要ない。しかし、このままでは Agda が停止条件を見つけられなので、 |
323 Flist1 zero i<n (a ∷# x ) z = FLinsert ( zero :: a ) (Flist1 zero i<n x z ) | 458 \verb+{-# TERMINATING #-}+を付けている。 |
324 Flist1 (suc i) (s≤s i<n) [] z = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z | 459 |
325 Flist1 (suc i) i<n (a ∷# x ) z = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z ) | 460 |
326 | 461 {-# TERMINATING #-} |
327 ∀Flist : {n : ℕ } → FL n → FList n | 462 AnyFList : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax) |
328 ∀Flist {zero} f0 = f0 ∷# [] | 463 AnyFList {zero} f0 = here refl |
329 ∀Flist {suc n} (x :: y) = Flist1 n a<sa (∀Flist y) (∀Flist y) | 464 AnyFList {suc zero} (zero :: f0) = here refl |
330 | 465 AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any (_≡_ (k :: y)) (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) )) |
331 しかし、Any を示しにくい。あと、もう少しだが... | 466 (fromℕ<-toℕ _ _) ( AnyFList1 (suc n) (toℕ x) a<sa (∀Flist fmax) (∀Flist fmax) fin<n fin<n (AnyFList y) (AnyFList y)) where |
332 | 467 AnyFList1 : (i x : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → (x<n : x < suc (suc n) ) → x < suc i |
333 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n | 468 → Any (y ≡_ ) L → Any (y ≡_ ) L1 |
334 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where | 469 → Any (((fromℕ< x<n) :: y) ≡_ ) (Flist i i<n L L1) |
335 fsuc1 : suc (toℕ x) < n | 470 AnyFList1 = ? |
336 fsuc1 = Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) ) | 471 |
337 fsuc (x :: y) (f<t lt) = x :: fsuc y lt | 472 以下の部分で |
338 | 473 |
339 この時に、x f< fsuc x が成立する。 | 474 AnyFList1 (suc i) x (s≤s i<n) (cons a (cons a₁ L x₂) x₁) L1 x<n (s≤s x<i) (there wh) any with FLcmp a a₁ |
340 | 475 ... | tri< a₂ ¬b ¬c = insAny _ (AnyFList1 (suc i) x (s≤s i<n) (cons a₁ L x₂) L1 x<n (s≤s x<i) wh any ) |
341 ∀Flist' : (n : ℕ ) → FList n | 476 |
342 ∀Flist' n = ∀Flist0' n n FL0 {!!} where | 477 {\tt (cons a (cons a₁ L x₂) x₁)} は {\tt (cons a₁ L x₂)} と小さくなってるのだが、Agda はそれを認識してくれない。 |
343 ∀Flist0' : (i j : ℕ) → (x : FL n) → x f< fmax → FList n | 478 |
344 ∀Flist0' zero zero x _ = [] | 479 --Commutator の数え上げの方法 |
345 ∀Flist0' zero (suc j) x lt = ∀Flist0' j j fmax {!!} | 480 |
346 ∀Flist0' (suc i) j x lt = cons (fsuc x lt) (∀Flist0' i j (fsuc x lt) {!!} ) {!!} | 481 さらに、交換子の生成を数え上げる必要がある。差分リストを使えば |
347 | 482 |
348 なのだが、fsuc は最大を越えないことを示す必要がある。めんどい。 | 483 tl3 : (FL n) → ( z : FList n) → FList n → FList n |
484 tl3 h [] w = w | |
485 tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w ) | |
486 tl2 : ( x z : FList n) → FList n → FList n | |
487 tl2 [] _ x = x | |
488 tl2 (h ∷# x) z w = tl2 x z (tl3 h z w) | |
489 | |
490 CommFList : FList n → FList n | |
491 CommFList x = tl2 x x [] | |
492 | |
493 CommFListN : ℕ → FList n | |
494 CommFListN 0 = ∀Flist fmax | |
495 CommFListN (suc i) = CommFList (CommFListN i) | |
496 | |
497 数え上げ自体は簡単で、すべての組の交換子を作ってFLinsertすればよい。そのために FLinsert を作ったのだった。 | |
498 | |
499 それが正しく、すべての組み合せを含んでいるかを示す必要がある。 | |
500 | |
501 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i ) | |
502 | |
503 つまり、deriving i x ならば、それは CommFListN i に含まれているというわけである。これを示すには、 | |
504 CommFListNを i にそって deriving i x と一緒に分解していく。あとは、 tl2 と tl3 が特定の組み合せを含むことを | |
505 調べに行く。 | |
506 | |
507 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x) | |
508 CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) [] where | |
509 G = perm→FL g | |
510 H = perm→FL h | |
511 -- tl2 case | |
512 comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → (L3 : FList n) → Any (perm→FL [ g , h ] ≡_) (tl2 L L1 L3) | |
513 comm2 = ? | |
514 -- tl3 case | |
515 commc : (L3 L1 : FList n) → Any (_≡_ (perm→FL [ FL→perm G , FL→perm H ])) L3 | |
516 → Any (_≡_ (perm→FL [ FL→perm G , FL→perm H ])) (tl3 G L1 L3) | |
517 commc = ? | |
518 | |
519 この時に、 | |
520 | |
521 comm8 : (L L4 L2 : FList n) → (a : FL n) | |
522 → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) | |
523 → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L L2)) | |
524 comm8← : (L L4 L2 : FList n) → (a : FL n) → ¬ ( a ≡ perm→FL g ) | |
525 → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L L2)) | |
526 → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) | |
527 | |
528 などの交換法則が必要になる。つまり、g が a と関係なければ {\tt (tl3 a L L2)} を移動して良い。 | |
529 | |
530 このアルゴリズムだと、一度、tl2 のそこまで潜らないと戻り値が確定しない。なので、交換則をつかって行きつ戻りつする必要がある。 | |
531 | |
532 おそらく、CommFListN と CommStage→ を同時に生成する見通しの良い方法があると思われる。 | |
533 | |
534 --Fresh List を使った可解の検査 | |
535 | |
536 結局、 {\tt Any (perm→FL x ≡_) y → x =p= pid }を調べるには FList n が {\tt FL0 ∷# []} であることを確認すればよい。 | |
537 | |
538 CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) | |
539 → Any (perm→FL x ≡_) y → x =p= pid | |
540 CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0 | |
541 | |
542 stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt) | |
543 stage3FList = refl | |
544 | |
545 solved1 : (x : Permutation 3 3) → deriving 2 x → x =p= pid | |
546 solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where | |
547 solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 ) | |
548 solved2 = CommStage→ 3 2 x dr | |
549 | |
550 と簡単に記述することができる。 | |
551 | |
349 | 552 |
350 --実行時間 | 553 --実行時間 |
554 | |
555 Fresh List を使う方法だと、3次の場合でも10秒でチェックされる。4次でも10秒である。 | |
556 5次も高速化される可能性がある。 | |
557 | |
558 agda sym3.agda 258.01s user 2.95s system 98% cpu 4:23.68 total | |
559 agda sym3n.agda 9.18s user 0.45s system 95% cpu 10.089 total | |
560 agda sym2n.agda 9.09s user 0.35s system 99% cpu 9.454 total | |
561 agda sym2.agda 9.34s user 0.50s system 94% cpu 10.448 total | |
562 agda sym4.agda 9.38s user 0.37s system 99% cpu 9.784 total | |
563 agda sym5.agda 9.04s user 0.34s system 99% cpu 9.427 total | |
564 | |
351 | 565 |
352 --Agdaの証明 | 566 --Agdaの証明 |
353 | 567 |
354 静的と動的 | 568 静的と動的 |
355 | 569 |