AgdaによるGalois理論のプログラミング

+ +Menu + + +Menu + + +

+ +

motivation

+5次方程式が代数的に解けないことの復習 +

+数学書では省略されてても Agda は許してくれない +

+計算で示しても、それが証明になっているかどうかは別 +

+証明付きデータ構造を使う +

+計算と証明が「全部つながってる」 +

+　この計算、いったい、何を計算してるの? +

+それを型で示す +

+ +

Galois theory : 多項式方程式

+ +

+  (x - α)(x - β)(x - γ) = 0
+
+

+と因数分解されればαβγが解になる。 +

+ +

Galois theory : 解と置換群(対称群)

+αβγを入れ替えても良い(Symmetric Group))。これが +

+ +

+  (x - α)(x - β) = 0
+
+

+に帰着されるなら、αβ を入れ替えても良い。ならば、αβγ の置換で +

+ +

+   αβγ = βαγ
+
+

+にならないとおかしい。 +

+ +

Galois theory : 可解群

+ +

+   αβγ = βαγ
+   α⁻¹β⁻¹αβγγ⁻¹ = α⁻¹β⁻¹βαγγ⁻¹
+   α⁻¹β⁻¹αβ = e  (交換子 Commutator)
+
+

+なので、対称群のすべての要素を α⁻¹β⁻¹αβ の形にするのを繰り返して e になれば良い(可解群)。 +

+(もちろん、これは証明になってない。気分的な説明。本当は正規拡大体とか代数的拡大とか) +

+ここは今回は Agda で証明しません。 +

+あれ? 割と Agda の得意な分野なのでできるはず。やさしくはないだろうけど +

+Agdaは抽象的な証明が得意 +

+ +

5次方程式が代数的に解けないことの証明

+5次の対称群は可解でないことを示せばよい。2,3,4次は可解。教科書だと +

+ + +

+これは良い方で、岩波だと練習問題。 +

+ + +

+ +

数学の本の記述の特徴

+理解した後で読むとちゃんと書いてある +

+理解する前には何が書いてあるのかわからない +

+ +

Agda でちゃんとやろうぜ

+Curry Howard 対応に基づく定理証明支援系 +

+ +

+    依存型を持つ純関数型言語
+    依存型とは、型を値に持つ変数
+    命題そのものは Set という型を持つ
+
+

+構文的には Haskell とほぼ同じ。Coq と違い、何もしてくれない。全部、自分で証明を書く。(いさぎよい) +

+ +

Agda : lambda

+A → B の証明 +

+ +

+  →intro : {A B : Set } → A →  B → ( A → B )
+  →intro _ b = λ x → b
+     
+  →elim : {A B : Set } → A → ( A → B ) → B
+  →elim a f = f a 
+
+

+引数の値は、型の証明 +

+入力は∀が付いていると考える(∃はあとで) +

+ +

Agda : record

+A ∧ B の証明 +

+ +

+    record _∧_ (A B : Set) : Set where
+      field
+         proj1 : A
+         proj2 : B
+    ∧elim : {A B : Set} → ( A ∧ B ) → A 
+    ∧elim a∧b = proj1 a∧b 
+    ∧intro : {A B : Set} → A → B → ( A ∧ B ) 
+    ∧intro a b = record { proj1 = a ; proj2 = b }
+
+

+ +

Agda : data

+ +

+A ∨ B の証明 +

+ +

+    data _∨_ (A B : Set) : Set where
+      case1 : A → A ∨ B
+      case2 : B → A ∨ B
+    ∨intro : {A B : Set} → A → ( A ∨ B ) 
+    ∨intro a =  case1
+    ∨elim : {A B : Set} → ( A ∨ A ) → A 
+    ∨elim (case1 a) = a
+    ∨elim (case2 a) = a
+
+

+ +

Agda : negation

+ +

+    data ⊥ : Set where
+
+

+constructor のないデータ構造(偽 +

+ +

+    ⊥-elim : {A : Set } -> ⊥ -> A
+    ⊥-elim ()
+
+

+起きない入力は () 。λ () とも書ける +

+ +

+    data ⊤ : Set where
+       tt : ⊤
+
+

+要素が一つしかない型(真 +

+ +

Agda : unification

+ +

+    data _≡_ {A : Set } : A → A → Set where
+       refl :  {x : A} → x ≡ x
+    ≡intro : {A : Set} {x : A } → x ≡ x
+    ≡intro  = refl
+    ≡elim : {A : Set} {x y : A } → x ≡ y → y ≡ x
+    ≡elim refl = refl
+
+

+項(正規化された)として等しい。変数はどうするの? 十分に instanciation されない場合は黄色くなる。 +

+その他、細かい問題が... internal parametricity... inspect... +

+でも、これで全部。さぁ、Agda を書こう。 +

+ +

Galois theory i nAgda : Commutator

+ +

+    [_,_] :  Carrier   → Carrier   → Carrier  
+    [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h 
+
+

+こんな風に数学の教科書通りに Unicode を使って書けるところが Agda の良いところ +

+ +

+    data Commutator (P : Carrier → Set ) : (f : Carrier) → Set  where
+      comm  : {g h : Carrier} → P g → P h  → Commutator P [ g , h ] 
+      ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g
+    deriving : ( i : ℕ ) → Carrier → Set 
+    deriving 0 x = ⊤
+    deriving (suc i) x = Commutator (deriving i) x
+
+

+Set を返してるのはなに? Set は何かの命題、つまり真偽として扱って良い。したがって +

+　　P : Carrier → Set +

+これは Carrier の部分集合を指定する命題となる。 (Carrier は群の要素の型) +

+交換子 Commutator p は述語 f p で限定された p : Carrier が [ g , h ] という形で生成されることを示している。 +

+deriving i は、Carrier の部分集合で、Commutator を再帰的に繰り返して得られたもの +

+ +

Galois theory in Agda : Solvable

+ +

+    record solvable : Set (Level.suc n ⊔ m) where
+      field 
+         dervied-length : ℕ
+         end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε  
+
+

+存在∃は record で書く。ある dervied-length : ℕ があって、その回数のderive の繰り返しで x ≈ ε になる +

+この record を構成できれば、その群は可解ということになる。これで問題は定義できた +

+ +

Galois theory in Agda : Symmetric group

+対称群の要素は置換だが、Agdaの標準ライブラリだと有限な数のBijectionとして定義される +

+ +

+   Permutation p p
+
+

+定義は複雑だが二つの写像 _⟨$⟩ˡ_ _⟨$⟩ʳ_ と y ⟨$⟩ˡ (y ⟨$⟩ʳ x) ≡ x と y ⟨$⟩ʳ (y ⟨$⟩ˡ x) ≡ x からなる record +

+残念ながら扱いにくい。同等性とか。単純に x ≡ y を証明できない(Agdaの制約 1) +

+しかし群であることを示すのは簡単 +

+ +

Permutation : Data.Fin

+有限な数 +

+ +

+   data Fin : ℕ → Set where
+     zero : {n : ℕ} → Fin (suc n)
+     suc  : {n : ℕ} (i : Fin n) → Fin (suc n)
+
+

+x : Fin 3 のように使う +

+Fin 0 の値は存在しない +

+ +

+     _⟨$⟩ˡ_ : Fin p →  Fin p
+
+

+ +

Permutation : List

+ +

+置換は List ℕ で表されるので、それで良いのだが、List ℕ が全部置換になるわけではない +

+そこで減少列 FL とその大小関係を定義する +

+ +

+    data  FL : (n : ℕ )→ Set where
+       f0 :  FL 0 
+       _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
+    data _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  where
+       f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn →   (xn :: xt) f< ( yn :: yt )
+       f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt →   (xn :: xt) f< ( xn :: yt )
+
+

+すると、これは置換と 1 to 1 になる。しかし 1 to 1 の証明は煩雑。しかし、簡単な方法があるかも。 +

+煩雑でも証明できてしまえば問題ないので、簡単にする motivation はあまりでない。 +

+でも簡単にしておくと、次に使えるかも。 +

+ +

Proofs : 2

+これで道具立てはそろったので証明に行く +

+まず、二次対称群から +

+ +

+   sym2lem0 :  ( g h : Permutation 2 2 ) → (q : Fin 2)  → ([ g , h ]  ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
+   sym2lem0 = ?
+   solved :  (x : Permutation 2 2) → Commutator  (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
+   solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h  }
+
+

+となるのだが、g と h が何かわからないので FL 2 に変換する +

+FL 2 は +

+ +

+   zero :: (zero :: f0)
+
+

+というものなので、これが pid つまり恒等置換であることは証明してあるのだが +

+ +

+   FL-inject : {n : ℕ }  → {g h : Permutation n n }  → perm→FL g ≡  perm→FL h → g =p= h
+
+

+を証明して使う。ところが、 +

+ +

+  pleq  : {n  : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y
+
+

+を使うと +

+ +

+   p0 :  FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid
+   p0 = pleq _ _ refl
+
+

+とできる。Injection は圏論でいう Equalizaer で写像した先で等しいなら手元でも等しいという性質 +

+ +

Proofs : 3

+2でこれなので 3 は絶望的に煩雑になる +

+たぶん、ガロアはそれを手で計算したはず +

+ +

Proofs : 5

+5は、solvable が存在しない、つまり否定を示せばよいsolvable から矛盾 counter-example を作る +

+ +

+    ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
+    ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where
+
+

+3次の対称群を含むことを示せばよいのだが、それが dervie-any-3rot0 実は dervie-any-3rot0 と dervie-any-3rot1 がいる +

+教科書だと「要素三つがとれるよね」と書いてあるが、Agda だと具体的に取ってくる必要がある。「あとは同じだよね」と書いてあっても、それを示す必要がある。 +

+ +

もっと簡単にできるでしょ

+derving は簡単に計算できるので、それで証明した方が良いんじゃないの? +

+確かにその通り +

+計算は簡単だが、それを証明にするにはどうすれば良いの? +

+ +

+    すべての交換子の組み合せを計算している
+
+

+を証明すればよい +

+つまり sort された List に、全部の要素が含まれている (どんな要素でも入っている) any +ことを Agda で書く +

+それには Fresh List というのを使う +

+ +

Fresh List

+(A : Set )と (R : A → A → Set) に対して +

+ +

+      data List# : Set 
+        []   : List#
+        cons : (a : A) (as : List#) → fresh a as → List#
+
+

+という List を定義する +

+ +

+      fresh : (a : A) (as : List#) → Set 
+      fresh a []        = ⊤
+      fresh a (cons x xs _) = R a ∧ fresh a xs
+
+

+普通の∷ (cons)の代わりに _∷#_ を使う +

+ +

+      infixr 5 _∷#_
+      pattern _∷#_ x xs = cons x xs _
+
+

+これも Set を値にしている。Fresh List の最後とそうでないもので fresh の中身が違う +

+List の要素毎に、fresh が存在するので、結構でかいものになる(O(2^n))。 +

+ + +

+ +

+    FList : (n : ℕ ) → Set
+    FList n = List# (FL n) ⌊ _f<?_ ⌋
+    fr1 : FList 3
+    fr1 =
+       ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+       ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+       ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+       ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+       ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+       []
+
+

+と定義できる。これで FList 3 が sort されていることが「証明されている」。⌊ _f<?_ ⌋ が不思議だが... +

+ +

Fresh List : Any

+ +

+  data Any : List# A R → Set  where
+    here  : ∀ {x xs pr} → P x → Any (cons x xs pr)
+    there : ∀ {x xs pr} → Any xs → Any (cons x xs pr)
+
+

+ここにあったら here、先にあるなら there +

+ +

Fresh List : Insert

+普通の insert と変わらないけど、fresh を作る必要がある +

+ +

+    FLinsert : {n : ℕ } → FL n → FList n  → FList n 
+    FLinsert {zero} f0 y = f0 ∷# []
+    FLinsert {suc n} x [] = x ∷# []
+    FLinsert {suc n} x (cons a y x₁) with FLcmp x a
+    ... | tri≈ ¬a b ¬c  = cons a y x₁
+    ... | tri< lt ¬b ¬c  = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁) 
+    FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt  = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
+    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 )
+
+

+ +

Fresh List : Property on Insert / Cons

+ +

+    x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_) (FLinsert x xs)
+    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 )
+    insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs)
+
+

+あたりがあると便利 +

+ +

Fresh List : Any on Pair

+Commutator (それを作っていたのだった) は任意の pair なので +

+ +

+    record AnyComm {n m l : ℕ}  (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where
+       field
+         commList : FList l
+         commAny : (p : FL n) (q : FL m)
+             → Any ( p ≡_ ) P →  Any ( q ≡_ ) Q
+             → Any (fpq p q ≡_) commList
+
+

+つまり二つの FList から、組を全部生成する必要がある。(fpq は ∧ の方が良かったか?) +

+ +

+    (p,q)   (p,qn) ....           (p,q0)
+    pn,q       
+    :        AnyComm FL0 FL0 P  Q
+    p0,q       
+
+

+こんな風に再帰で作れる(やさしくない +

+ +

Fresh List : Solved using Fresh List

+まず全部の FL が入ってる FList +

+ +

+    record AnyFL (n : ℕ) : Set where
+       field
+         allFL : FList n
+         anyP : (x : FL n) → Any (x ≡_ ) allFL 
+
+

+これは AnyComm から作れる (やさしくない +

+次に Commutator +

+ +

+    CommFListN  : ℕ →  FList n
+    CommFListN  zero = allFL (anyFL n)
+    CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))
+
+

+そして、Commutator がちゃんと全部入っていることを示す(やさしい +

+ +

+    CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i)
+
+

+すると +

+ +

+    CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
+
+

+という形で可解を定義できる。 +

+ +

Proofs : 2

+以下のように極めて簡単になった(やった! +

+ +

+   stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt)
+   stage2FList = refl
+   solved1 :  (x : Permutation 2 2) → deriving 1 x → x =p= pid
+   solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList p0id solved0 where
+      solved0 : Any (perm→FL x ≡_) ( CommFListN 2 1 )
+      solved0 = CommStage→ 2 1 x dr
+
+

+このまま 3, 4を証明可能 +

+ +

Proofs : 5

+e 以外を含む stage 3 が stage 4 と同じことを示すだけで可解でないことを示せる +

+しかし5を計算すると停まらない(きっと停まるが遅すぎる +

+メモリは食わない (FList 5 自体は計算できて、それで抑えられる) +

+単に計算が遅い +

+ +

時間

+ +

+    agda sym3.agda  258.01s user 2.95s system 98% cpu 4:23.68 total
+    agda sym3n.agda  9.18s user 0.45s system 95% cpu 10.089 total
+    agda sym2n.agda  9.09s user 0.35s system 99% cpu 9.454 total
+    agda sym2.agda  9.34s user 0.50s system 94% cpu 10.448 total
+    agda sym4.agda  9.38s user 0.37s system 99% cpu 9.784 total
+    agda sym5.agda  9.04s user 0.34s system 99% cpu 9.427 total
+
+

+ +

しかし、Agda には compiler が!

+ +

+コンパイルすれば計算可能 +

+ +

+    ./sym5n  0.00s user 0.01s system 37% cpu 0.044 total
+
+

+ただし、それは証明には接続できない +

+型検査時に compile して計算する機能はない +

+ +

Analysis : overhead of proof carrying data structure

+Fin, Commutator, FL, Fresh , Any, FList は、すべて証明付きデータ構造 +

+証明は実行時ではなく型検査時に行われるので実行時のオーバヘッドは理論的にはない +

+Any や fresh は実行されない型しか計算しないコードになる +

+しかし、Fresh は Product を含んでいるので実際に heapを食うのでオーバーヘッドがあるように見える +

+ところが、それは使われないので実行時には明示的に触らない限り生成されない(遅延評価 +

+なので、普通に高速に計算される +

+ +

Analysis connection of computation and type

+普通は何を計算したのかは計算機は知らない +

+まして作った人以外はさっぱりわからない +

+しかし、証明付きデータならば、そこに何を計算したのかが書いてある +

+ただ +

+　　プログラミングは、めっちゃ面倒 +

+でも、それができるならプログラミングの信頼性は上がる +

+しかし、それでも完全に正しいとは... +

+ +

Appendix : ZF fix

+証明があっても正しいとは限らない +

+去年のZFには間違いがあって +

+ +

+    record OD : Set (suc n ) where
+      field
+        def : (x : Ordinal  ) → Set n
+
+

+OD ⇔ Ordinal を要求すると矛盾になる +

+ +

+    ¬OD-order : ( & : OD  → Ordinal ) → ( * : Ordinal  → OD ) → ( { x y : OD  }  → def y ( & x ) → & x o< & y) → ⊥
+    ¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
+
+

+なので最大値を付けてやると良い +

+ +

+    record HOD : Set (suc n) where
+      field
+        od : OD
+        odmax : Ordinal
+        <odmax : {y : Ordinal} → def od y → y o< odmax
+
+

+つまり証明が合ってても仮定が間違ってたらダメ +

+これは (集合論の用語での) Set と Class の区別になっている。つまり OD が Class で、最大値があれば集合になる。 +

+ +

Appendix : Topology

+今年は +

+ +

+    record Toplogy  ( L : HOD ) : Set (suc n) where
+       field
+           OS    : HOD
+           OS⊆PL :  OS ⊆ Power L 
+           o∪ : { P : HOD }  →  P  ⊆ OS           → OS ∋ Union P
+           o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q  → OS ∋ (p ∩ q)
+
+

+やっても良いかも。 Tychonovの定理の証明とか(やさしくなさそう +

+あるいは ZF の cohen model とか +

+ +

+    record Filter  ( L : HOD  ) : Set (suc n) where
+       field
+           filter : HOD   
+           f⊆PL :  filter ⊆ Power L 
+           filter1 : { p q : HOD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
+           filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
+
+

+Topology と Filter は似てることがわかる +

+ +

Permutation : 等号

+ +

+    record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
+        field
+           peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
+
+

+を統合して使う +

+ +

+    x  ≡ y → x =p y
+
+

+は言えるが +

+ +

+    x =p y → x  ≡ y
+
+

+は仮定するしかない。(Functional Extentionality) +

+ +

Permutation : Data.Fin と Data.Nat

+suc と zero が自然数と重なっていて扱いを気をつける必要がある +

+ +

+   data ℕ : Set where
+     zero : ℕ
+     suc  : ℕ  → ℕ
+
+

+x ∧ x < n で不等号を持ち歩く方法でも良いのだが... +

+x < n も +

+ +

+    data _≤_ : Rel ℕ 0ℓ where
+      z≤n : ∀ {n}                 → zero  ≤ n
+      s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
+
+

+と再帰的データ構造なので二重に持ち歩くことになるので美しくない +

+ +

Permutation : FL と Permutation の対応の証明

+Permutation の combinator 表現を使う +

+ +

+    pprep  先頭に一つ置換を増やす
+    pswap  先頭の二つを入れ替える
+
+

+これだけで任意の置換を構成できる +

+これから pins という任意の置換に任意の位置に 0(の位置の要素) を入れる関数を作る +

+そして、pins の逆を +

+ +

+    pshrink 置換を一つ減らす
+
+

+を作って構成する +

+極めて煩雑な証明になる +

+ +

Fresh List : witness

+⌊ _f<?_ ⌋ は witness と呼ばれるもので、 +

+ +

+    data Dec : {R : FL → FL → Set} : Set where
+        yes :   R → Dec R
+        no  : ¬ R → Dec R
+    x f<? y with FLcmp x y
+    ... | tri< a ¬b ¬c = yes a
+    ... | tri≈ ¬a refl ¬c = no ( ¬a )
+    ... | tri> ¬a ¬b c = no ( ¬a )
+
+

+ +

sym5

+ +

+abc が反例。これが常に残ることを示す +

+ +

+     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
+     counter-example eq with ←pleq _ _ eq
+     ...  | ()
+
+

+二つ余地を確保する +

+ +

+     ins2 : {i j : ℕ }  → Permutation 3 3  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) 
+
+

+abc と dba を作る +

+ +

+     abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     abc i<3 j<4 = ins2 3rot i<3 j<4
+     dba : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4
+
+

+abc が derive されることを示す +

+ +

+     dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
+          → deriving n (abc i<3 j<4 ) 
+     dervie-any-3rot0 0 i<3 j<4 = lift tt 
+     dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where
+        commd : {n : ℕ } → (f g : Permutation 5 5)
+               →  deriving n f
+               →  deriving n g
+               → Commutator (deriving n) [ f , g ]
+        commd {n} f g df dg =  comm {deriving n} {f} {g} df dg
+
+

+df と dg が前に derive されたもの +

+ +

+        df =  dervie-any-3rot1 i  (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
+        dg =  dervie-any-3rot1 i  (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) 
+
+

+それは、再帰的に作れるのだが種(dbaとaec)を二つ計算する必要がある +

+それは右回転と左回転があって、 dervie-any-3rot0 と dervie-any-3rot1 で交互に作られる +

+そのつくり方だが... +

+ +

+        tc = triple i<3 j<4
+        dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
+        aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
+        ceq : abc i<3 j<4  =p=  [ dba0 , aec0 ]  
+        ceq = record { peq = peq (abc= tc) }
+
+

+dba と aec を作るのだが +

+ +

+     record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
+       field 
+         dba0<3 : Fin 4
+         dba1<4 : Fin 5
+         aec0<3 : Fin 4
+         aec1<4 : Fin 5
+         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) ]
+     open Triple
+     triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot
+     triple z≤n z≤n =                               record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
+     triple z≤n (s≤s z≤n) =                         record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
+       ....
+
+

+と自分でうまく2つの余地を選択する必要がある +

+もちろん、計算することは可能だが... +