Mercurial > hg > Papers > 2020 > kono-prosym

changeset 2:72ec93c67ab2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 04 Dec 2020 07:07:19 +0900
parents b169617e42e5
children 57601db306e9
files fig/fresh.graffle galois-prosym.ind main.tex
diffstat 3 files changed, 173 insertions(+), 149 deletions(-) [+]
line wrap: on
line diff
Binary file fig/fresh.graffle has changed
--- a/galois-prosym.ind	Thu Dec 03 17:50:45 2020 +0900
+++ b/galois-prosym.ind	Fri Dec 04 07:07:19 2020 +0900
@@ -1,6 +1,6 @@
 -title: Agda によるガロア理論
 
---All connected
+--All connected 
 
 数学の証明に計算機を使うのは既に古い歴史がある。Agda \cite{agda} は定理証明支援系だが、普通の関数型プログラミング言語でもあり、
 群の要素の数え上げなどを直接に実行できる。この時に「正しく数え上げのか」ということが問題になる。4色問題が計算機を使って解かれた
@@ -12,11 +12,9 @@
 計算結果が、ちゃんと要求された証明につなかっていることを示すことが可能である。つまり計算だけなくて、証明としてちゃんとつながっていることになる。
 
 ここでは、例題としてガロア理論の一部である可解群を使い、証明を含むデータ構造として、
-
    Data.Fin              有限な自然数
    FL                    順列に対応する減少列
    Data.List.Fresh       Sorted List
-
 を使う。一部は、AgdaのLibrary でる。
 
 証明付きのデータ構造は assert と異なり、それを作成する段階で証明を構成する必要がある。証明は型の整合性の検査なので、
@@ -29,35 +27,26 @@
 --ガロア理論
 
 xの多項式f(x)が解を持てば因数定理により 
-
-　 (x - α)(x - β)(x - γ)
-
+   (x - α)(x - β)(x - γ)
 の形に因数分解可能である。αβγは定数だが、この三つを置換しても式は同じになる。つまり展開すれば同じ式になる。
 つまり、順列の群である対称群が対応することになある。f(x)因数定理による分解
-
-　 f(x) => (x - α)(g x)
-
+   f(x) => (x - α)(g x)
 は、f(x)の対称群からg(x)の対称群への変換になる。具体的には三次の対称群から二次の対称群の変換がなければならない。
 ここで二次式に帰着できれば変換があり、変換があれば三次式を二次式に変換できる。
 
 三次の対称群、つまり三つの数の入れ替えは、αβγはγ..と.γ.と..γからなるが、
 三次式を二次式に変換できるなら、αβγとβαγの二つの形にならないとおかしい。つまり、
-
-　αγβ = αβγ
-
+  αγβ = αβγ
 とγを移動できる必要がある。ということは、
-
-　γβ=βγ
-
+  γβ=βγ
 である必要がある。逆元をかけて
-
-　 β⁻¹γ⁻¹βh = e
+  e=β⁻¹γ⁻¹βγ  
+になれば良い(これは正確な話ではない)。左辺をCommutator(交換子)と呼び [β,γ]と書く。
 
-になれば良い。左辺がCommutator(交換子)と呼ぶ。ある群の二つの要素を取って交換子に変換したものを交換子群と呼ぶ。
+ある群の二つの要素を取って交換子に変換したものを交換子群と呼ぶ。
 これは群から群への関手になる。交換子群を繰り返し作り、単元だけの群になる場合をSolvable 可解と呼ぶ。
-多項式に対応する対称群が可解であることがべき根を使って解けるための条件になる。
-
-今回は可解と方程式がべき根で解ける部分には関与せず、2-5次の対称群が可解かどうかを計算で示す。
+多項式に対応する対称群が可解であることがべき根を使って解けるための条件になるとされている。
+今回は対称群が可解であることがが方程式がべき根で解ける条件であることには関与せず、2-5次の対称群が可解かどうかを計算で示す。
 
 --Agdaによる Group の表現
 
@@ -70,7 +59,8 @@
 Agda の型には Level があり、基本型の後に自然数で指定する。⊔ はLevelの最大値演算子である。
 : の前が名前で、後ろが型である。
 Carrier は要素の型であり、関係と演算子が{\tt  Rel Carrier ℓ, Op₂ Carrier}と定義されているが、
-これらは{\tt Carrier → Carrier → Set ℓ} と {\tt Carrier →　Carrier →　Carrier } のことである。
+これらは{\tt Carrier → Carrier → Set ℓ} と {\tt Carrier →  Carrier →  Carrier } のことである。
+Agda は Haskell と同じく indent で構文のブロックを表している。
 
     record Group c ℓ : Set (suc (c ⊔ ℓ)) where
       field
@@ -83,33 +73,37 @@
       open IsGroup isGroup public
       monoid : Monoid _ _
       monoid = record { isMonoid = isMonoid }
-      open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)
-
+      open Monoid monoid public 
+         using (rawMagma; magma; semigroup; rawMonoid)
 群の構成要素は field で定義されているが、Monoid の公理 isMonoid などは module で定義されている。
-これらの field を適切に埋めれば良い。
+群を定義するにはこれらの field を適切に埋めれば良い。
 
 順列は Agda に
 
    Data.Fin.Permutation
-
 というのがあるので、それを使う。これは Data.Fin の間の Bijection として4抽象的に定義されている。
 中括弧は省略可能な引数である。
+置換 p には二つの写像が中置演算子\verb+ ⟨$⟩,⟨$⟩ʳ+として定義されている。record の中にはBijectionの性質が入っている。
 
     -- Data.Fin.Permutation.id
     pid : {p : ℕ } → Permutation p p
-    pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
+    pid = permutation ( λ x → x)( λ x → x) record 
+       { left-inverse-of = λ x → refl 
+       ; right-inverse-of = λ x → refl }
 
     -- Data.Fin.Permutation.flip
     pinv : {p : ℕ } → Permutation p p → Permutation p p
-    pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
+    pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record 
+      { left-inverse-of = λ x → inverseʳ P 
+      ; right-inverse-of = λ x → inverseˡ P }
+という感じで簡単に逆元と単位元が求まる。  refl は data である {\tt x ≡ x} を生成する constructor である。
+
+置換の同値性は写像が等しければよい。これを record で定義する。
 
     record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
         field
            peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
-
-という感じで簡単に逆元と単位元が求まる。Bijection の field は詳しく説明しないが二つの写像とBijectionの公理を表している。
-
-identity の refl は data である {\tt x ≡ x} を生成する constructor である。
+これらを使って置換の群を以下のように定義できる。(prespとpassocなどはここでは記述していない)
 
     Symmetric : ℕ → Group  Level.zero Level.zero
     Symmetric p = record {
@@ -118,15 +112,20 @@
         ; _∙_            = _∘ₚ_
         ; ε              = pid
         ; _⁻¹            = pinv
-        ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-           isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym }
+        ; isGroup = record { isMonoid  = record { 
+           isSemigroup = record { isMagma = record {
+            isEquivalence = record {refl = prefl 
+               ; trans = ptrans ; sym = psym }
            ; ∙-cong = presp }
            ; assoc = passoc }
-           ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } ))  }
-           ; inverse   = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} ))  
+           ; identity = ( (λ q → record { peq = λ q → refl } ) 
+                , (λ q → record { peq = λ q → refl } ))  }
+           ; inverse   = ( (λ x → record { peq = λ q → inverseʳ x} ) 
+                , (λ x → record { peq = λ q → inverseˡ x} ))  
            ; ⁻¹-cong   = λ i=j → record { peq = λ q → p-inv i=j q }
           }
        } 
+例えば identity は (ε ∙ x) =p= x だが、これは x ⟨$⟩ʳ q ≡ x ⟨$⟩ʳ q なので、refl で生成できる。
 
 --Data.Fin
 
@@ -136,10 +135,9 @@
    data Fin : ℕ → Set where
      zero : {n : ℕ} → Fin (suc n)
      suc  : {n : ℕ} (i : Fin n) → Fin (suc n)
-
 zero と suc はNatと重なっているので Monomorphic な Agda では注意が必要である。このデータ構造は基本的には Nat と
-同じだが、{\tt Fin zero }は作れない。{\tt # 1} と書く記法が用意されているが、{\tt n}が決まるように記述する必要が
-ある。つまり、{\tt # 1} でも n が異なると別物になる。{\tt toℕ} で自然数を取り出すことができる。{\tt Fin n}を
+同じだが、{\tt Fin zero }は作れない。\verb+# 1+ と書く記法が用意されているが、{\tt n}が決まるように記述する必要が
+ある。つまり、\verb+# 1+ でも n が異なると別物になる。{\tt toℕ} で自然数を取り出すことができる。{\tt Fin n}を
 作るためには、それが n よりも小さい証明が必要である。\verb+{n : ℕ}+ 省略可能で型推論により自動的に決まる。
 決まらなければ Agda が黄色で instantiation が足りないと警告される。証明では黄色を全部消す必要がある。
 計算自体は値が決まってなくても計算可能なところまで進む。これは関数型言語の特徴である。
@@ -164,7 +162,8 @@
 
 この形で生成されるものを繰り返し生成したい。そのための生成演算子を以下のように定義する。
 
-    data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
+    data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) 
+            : (f : Carrier) → Set (Level.suc n ⊔ m) 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
 
@@ -179,7 +178,8 @@
 という定義を持つ。交換子は積に付いて閉じてないので、交換子群を作る場合には以下の生成子も必要になる。しかし、
 今回は単位元だけになるかどうかを知りたいだけなので、これは使わない。
 
-      gen   : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙  g  )
+      gen   : {f g : Carrier} → Commutator P f → Commutator P g 
+           → Commutator P ( f ∙  g  )
 
 交換子の生成を繰り返すのが次の述語 deriving である。。これも Set (Level.suc n ⊔ m) を返してる。つまり証明するべき命題を返すような関数になっている。
 証明はもちろん、Commutator で作られるλ項であり、⊤の構成子 tt で終わる。
@@ -209,7 +209,8 @@
     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
     counter-example = ?
 
-     end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →  x =p= pid  
+     end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x 
+        →  x =p= pid  
      end5 = ?
 
     ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
@@ -244,8 +245,10 @@
 このListに大小関係を入れる。
 
     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 )
+       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対1対応するので都合が良い。
 
@@ -259,19 +262,22 @@
 
     perm→FL   : {n : ℕ }  → Permutation n n → FL n
     perm→FL {zero} perm = f0
-    perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) 
+    perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (
+        shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) 
 
 pprep は先頭に 0 を付加する。{\tt 0 ∷ 1 ∷ 2 ∷ []} が{0 ∷ 1 ∷ 2 ∷ 3 ∷ []}になる。
 pins は 0 を指定した位置に挿入する。{\tt 0 ∷ 1 ∷ 2 ∷ 3 ∷ []} が {\tt 1 ∷ 2 ∷ 0 ∷ 3 ∷ []}にするような順列に対する演算である。
 shirink は pins  の逆演算で 0 の位置を指定する p=0 を使っている。
 
-    shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
+    shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) 
+          → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
 
 つまり、その位置の置換先が0でないと shrink は呼び出せない。pins/shrinkはBijection を構成するのでやや複雑。
 
 問題は、FL→perm と perm→FL が Bijection であることを示すことだが、
 
-    shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm)  refl =p=  perm
+    shrink-iso : { n : ℕ } → {perm : Permutation n n} 
+         → shrink (pprep perm)  refl =p=  perm
     shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} 
        → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0)  → pprep (shrink perm p=0) =p= perm
 
@@ -301,10 +307,13 @@
 
    p3 =  FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0)))
    p4 =  FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0)))
-   st02 :  ( g h : Permutation 3 3) →  ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
+   st02 :  ( g h : Permutation 3 3) →  
+      ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
 
 になるのだが、これを3次対称群の要素全部に付いて確認する必要がある。
+図\ref{fig:3s}というように50行程度書く必要がある。この証明チェックには数分かかる。
 
+\begin{figure*}[tb]
    st02 :  ( g h : Permutation 3 3) →  ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
    st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
    ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
@@ -319,42 +328,41 @@
    ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
    ...
+\caption{3次対称群のめんどくさい計算}
+\label{fig:3s}
+\end{figure*}
 
-というように50行程度書く必要がある。この証明チェックには数分かかる。
 
 --5次対称群
 
-abc は以下のようにpinsなどで定義できる。
-
-     --- 1 ∷ 2 ∷ 0 ∷ []      abc
-     3rot : Permutation 3 3
-     3rot = pid {3} ∘ₚ pins (n≤ 2)
-
-     save2 : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) →  Permutation  5 5
-     save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4)
-
-     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 はpinsなどで定義できる。5次の中の3次なので二つ空き場所がある。それを不等式で指定する。不等式なのはFinを指定するのに便利だからである。
 
      abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
      abc i<3 j<4 = ins2 3rot i<3 j<4
 
 これを交換子から生成してやればよい。{\tt [ dba , aec ]} なのだが、場所を正確に指定する必要がある。
 
-     record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
+     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) ]
+         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) ]
 
-これをすべての場所に付いて record を作成する。
+これをすべての場所に付いて record を作成する。これがすべての組み合せについて記述される。10行程度である。
+中の値は自分で計算する必要がある。
 
      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 }
+     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 }
        ....
 
 これだけでは閉じてなくて、もう一種類必要になる。
@@ -378,7 +386,7 @@
 
 各要素の大小関係がすべて入っている sort された List 。これを使うと重複要素を排除できる。
 
-<center><img src="fig/fresh.svg"></center>
+<center><img src="fig/fresh.pdf"></center>
 
   data List# : Set (a ⊔ r)
   fresh : (a : A) (as : List#) → Set r
@@ -395,8 +403,8 @@
 
 これを使うと
 
-FList : {n : ℕ } → Set
-FList {n} = List# (FL n) ⌊ _f<?_ ⌋
+     FList : {n : ℕ } → Set
+     FList {n} = List# (FL n) ⌊ _f<?_ ⌋
 
     fr1 : FList
     fr1 =
@@ -417,18 +425,22 @@
 
     FLinsert : {n : ℕ } → FL n → FList n  → FList n
     FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x
-         → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
+         → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y 
+         → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
     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 )
+    ... | 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 )
 
-という形で、FLinsert と FLfresh で相互再帰していく。
+という形で、FLinsert と FLfresh で相互再帰していく。FLfresh は省略している。
 
-{\tt ⌊ _f<?_ ⌋} は{\tt  _f<?_}のままでは Set で扱いづらいので、それが真なのか偽なのかを表す data である。fromWitness や toWitness
+\verb+⌊ _f<?_ ⌋+ は{\tt  \_f<?\_}のままでは Set で扱いづらいので、それが真なのか偽なのかを表す data である。fromWitness や toWitness
 で変換する。中には不等号を表す data 構造が入る。fresh の base は ⊤ なので {\tt  Level.lift tt}が最後に来る。
 {\tt R a x × fresh a xs} はみづらいが、直積で不等号と、後に続く fresh の条件リストがある。
 
@@ -446,8 +458,10 @@
 
 が示せれば、∀Flist fmax に全部の FL n が入っていることがわかる。
 
-    x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
-    insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  → Any (x ≡_ ) xs → Any (x ≡_ ) (FLinsert h xs)
+    x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  
+         → Any (x ≡_ ) (FLinsert x xs)
+    insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  
+         → Any (x ≡_ ) xs → Any (x ≡_ ) (FLinsert h xs)
 
 などが証明できるのでこれを使う。
 
@@ -462,17 +476,22 @@
     AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
     AnyFList {zero} f0 = here refl
     AnyFList {suc zero} (zero :: f0) = here refl
-    AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any (_≡_ (k :: y)) (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) ))
-             (fromℕ<-toℕ _ _) ( AnyFList1 (suc n) (toℕ x) a<sa (∀Flist fmax) (∀Flist fmax) fin<n fin<n (AnyFList y) (AnyFList y)) where
-       AnyFList1 :  (i x : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → (x<n : x < suc (suc n) ) → x < suc i
+    AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any (_≡_ (k :: y)) 
+         (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) ))
+             (fromℕ<-toℕ _ _) ( AnyFList1 (suc n) (toℕ x) a<sa (∀Flist fmax) 
+                  (∀Flist fmax) fin<n fin<n (AnyFList y) (AnyFList y)) where
+       AnyFList1 :  (i x : ℕ) → (i<n : i < suc (suc n) ) → 
+          (L L1 : FList (suc n) ) → (x<n : x < suc (suc n) ) → x < suc i
             → Any (y ≡_ ) L → Any (y ≡_ ) L1
             → Any (((fromℕ< x<n) :: y) ≡_ ) (Flist i i<n L L1)
        AnyFList1 = ?
 
 以下の部分で
 
-       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₁
-       ... | 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 )
+       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₁
+       ... | 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 )
 
 {\tt (cons a (cons a₁ L x₂) x₁)} は {\tt (cons a₁ L x₂)} と小さくなってるのだが、Agda はそれを認識してくれない。
 
@@ -482,7 +501,8 @@
 
     tl3 : (FL n) → ( z : FList n) → FList n → FList n
     tl3 h [] w = w
-    tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
+    tl3 h (x ∷# z) w = tl3 h z 
+       (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
     tl2 : ( x z : FList n) → FList n →  FList n
     tl2 [] _ x = x
     tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
@@ -498,22 +518,28 @@
 
 それが正しく、すべての組み合せを含んでいるかを示す必要がある。
 
-    CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )
+    CommStage→ : (i : ℕ) → (x : Permutation n n ) 
+       → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )
 
 つまり、deriving i x ならば、それは  CommFListN i に含まれているというわけである。これを示すには、
-CommFListNを i にそって deriving i x と一緒に分解していく。あとは、 tl2　と tl3  が特定の組み合せを含むことを
+CommFListNを i にそって deriving i x と一緒に分解していく。あとは、 tl2  と tl3  が特定の組み合せを含むことを
 調べに行く。
 
     CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x)
-    CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) [] where
+    CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = 
+     comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) 
+          (CommStage→ i h q) [] where
        G = perm→FL g
        H = perm→FL h
        -- tl2 case
-       comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → (L3 : FList n) → Any (perm→FL [ g , h ]  ≡_) (tl2 L L1 L3)
+       comm2 : (L L1 : FList n) → Any (G ≡_) L 
+            → Any (H ≡_) L1 → (L3 : FList n) 
+            → Any (perm→FL [ g , h ]  ≡_) (tl2 L L1 L3)
        comm2  = ?
        -- tl3 case
-       commc :  (L3 L1 : FList n) →  Any (_≡_ (perm→FL [  FL→perm G , FL→perm H ])) L3
-               →  Any (_≡_ (perm→FL [ FL→perm G , FL→perm H ])) (tl3 G L1 L3)
+       commc :  (L3 L1 : FList n) 
+          →  Any (_≡_ (perm→FL [  FL→perm G , FL→perm H ])) L3
+          →  Any (_≡_ (perm→FL [ FL→perm G , FL→perm H ])) (tl3 G L1 L3)
        commc = ?
 
 この時に、
@@ -533,13 +559,15 @@
 
 --Fresh List を使った可解の検査
 
-結局、 {\tt Any (perm→FL x ≡_) y → x =p= pid }を調べるには FList n が {\tt FL0 ∷# []} であることを確認すればよい。
+結局、 {\tt Any (perm→FL x ≡\_) y → x =p= pid }を調べるには FList n が {\tt FL0 ∷\# []} であることを確認すればよい。
 
-   CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) 
+   CommSolved : (x : Permutation n n) → (y : FList n) 
+      → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) 
       → Any (perm→FL x ≡_) y → x =p= pid
    CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0
 
-   stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt)
+   stage3FList : CommFListN 3 2 ≡ 
+       cons (zero :: zero :: zero :: f0) [] (Level.lift tt)
    stage3FList = refl
 
    solved1 :  (x : Permutation 3 3) → deriving 2 x → x =p= pid
@@ -552,38 +580,67 @@
 
 --実行時間
 
-Fresh List を使う方法だと、3次の場合でも10秒でチェックされる。4次でも10秒である。
+Fresh List を使う方法だと、3次の場合でも10秒(sym3n)でチェックされる。4次でも10秒である。
 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 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の証明
+--Agdaの証明付きコード
+
+Agda はHaskellに近い構文を持つ、Haskell で実装された定理証明系であり、純関数型プログラミング言語でもある。
+Agda から実行コードを生成することもできる。証明に特化した Coq よりはプログラマにとって近いしいものかも知れない。
 
-静的と動的
+さまざまな計算が「いったい何を計算しているのか」をちゃんと把握することは重要だし、{\tt すべてのバグはつまらないバグ}
+なので、さまざまな理由でバグが混入する。そこで、計算しているものの仕様を記述して、それを証明するのは回り道であるが有効かも知れない。
+
+一方で、実行時に証明のコードはまったくの無駄とも言える。一方で実行時に型検査する必要はないはずなので、オーバヘッドは存在しない。
+しかし、Fresh List は {\tt Level.lift tt} を持つので、それは生成される。
 
-抽象的と具体的
+    cons (zero :: zero :: zero :: f0)
+    (cons (suc zero :: suc zero :: zero :: f0)
+     (cons (suc (suc zero) :: zero :: zero :: f0) [] (Level.lift tt))
+     (Level.lift tt , Level.lift tt))
+    (Level.lift tt , Level.lift tt , Level.lift tt)
 
-証明を持つデータ型
+のような形になる。これは実行時に生成されてしまう。 これはオーバヘッドになる。
 
---coinduction?
+証明自体は線形挿入でもかなりめんどうでプログラミングの手間に見合うとは思えない。しかし、ライブラリは重要なので、その手間に見合う可能性も
+ある。また、証明自体は大半の証明は簡単なので機械学習が使える可能性が高い。
 
-   record  CFresh {n : ℕ } (i : Size) : Set  where
-      coinductive
-      field
-         δ : ∀{j : Size< i} → (y : FL n) → CFresh {n} j 
-         -- δ : ∀{j : Size< i} → (y : FL n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ y x) → CFresh {n} j (cons y x xr)
-   
-   open CFresh
-   ∀CF : ∀{i} {n : ℕ } → FL n → CFresh {n} i ?
-   δ (∀CF x) y fr = {!!}
+置換の表現としてのBijectionの扱いは面倒で、同値を調べるには、すべての要素に付いて写像が等しいことを調べる必要がある。
+一方で、入力を固定すれば、それは単なる定数関数となる。つまり、抽象的なものを具体的なものに置き換えられれば、話は簡単になる。
+あらゆる抽象的なものはゲーデル的な意味で具体的な構造物を持つはずなので、一般的にそういうことが可能かも知れない。
+
+Agda での同値性は、三つの表現方法がある。一つは refl つまり、Agdaのλ項として等しいことである。これは圏論の言葉で言う small に相当する。
+プログラミングで出てくるもののほんどは、この形ですむ。もう一つは dataを使って Sum型として表す方法がある。例えば、
+具体的な有限グラフはこの方法が適している。この方法だとエッジの不存在を簡単に証明できる。三つ目としてrecordを持ちても良い。
+置換の結果が等しいとかはこの方式である。いずれの方式でも問題になるのはλ項の単一化(Unification)である。
+
+Agdaは自然演繹なので推論規則自体は理解しやすい。難しさは単一化にあり、さまざまな問題が生じる。しかも、それはプログラミング上、証明上
+良く見えない。巨大な変数を含む項が生成されて、計算時間を消費する。現在の Agda はファイル単位での差分実行はあるが、一つのファイル内での
+差分実行はないので、重い証明が存在する。単一化の計算量は指数計算量で予測は難しい。
 
-良くわからん。
+もう一つは停止性の問題である。停止性は無視することもできるが、もう少し制御したい。制御の方法は不明だが、必要なのは deduction つまり、
+減少列を明確にすることなので、外付けがそれを付加できると良い。
+
+Any は任意の要素 x が L : Fresh List に入っていることを示す。これは L が x集合の Initial Object つまり、L → x となる関数を
+すべて持っているということになっている。 CommStage→ を示す時に使った可換性は Any が自然変換であることを意味している。この部分は
+証明なので実際の計算には関係ない。しかし、その部分では圏論的なアプローチが有効かも知れない。
+
+--終わりに
+
+Agda による対称群の可解性についての証明を行った。手計算では入力と検査時間がかかるが、Fresh List のような証明付きデータ構造を
+用いることにより検査時間を短縮し、記述も短くすることができた。一方で、リストへの挿入などのコードが複雑になってしまう。
+しかし、それにより Any のように、Fresh List に必要なものが全部入っていることを確認することができ、それをそのまま証明に使う
+ことがきる。これにより、計算結果を直接に証明で使うことができるようになる。
+
+この例はプログラムの正しさを直接に証明としてコードに埋め込んだ例になっている。
 
 
 
@@ -592,35 +649,3 @@
 
 
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/main.tex	Thu Dec 03 17:50:45 2020 +0900
+++ b/main.tex	Fri Dec 04 07:07:19 2020 +0900
@@ -20,9 +20,8 @@
 \input usepackage.tex
 \begin{document}
 \setmainfont{STIX Math}%
-\setmonofont{STIXGeneralBol}[
-  Scale=MatchLowercase
-] % or whatever font you prefer
+\setmonofont{STIXGeneralBol}
+%[Scale=MatchLowercase] % or whatever font you prefer
 
 \ltjsetparameter{jacharrange={-3}}