# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606985445 -32400
# Node ID b169617e42e5b2a0be66e22b086f5db74606e7a7
# Parent  e2071e2490a2c8093d6eb7dbf787fd5db9049fd4
...

diff -r e2071e2490a2 -r b169617e42e5 galois-prosym.ind
--- a/galois-prosym.ind	Thu Dec 03 15:52:48 2020 +0900
+++ b/galois-prosym.ind	Thu Dec 03 17:50:45 2020 +0900
@@ -219,6 +219,12 @@
 {\tt abc 0<3 0<4} は5つのFinのうち、a を b に、bをcに、cをaに置換する置換である。これが何回交換子を
 作っても残ってしまうことはアルティンの邦訳には以下のような証明が載っている。基本的にこれを証明することになる。
 
+abc 以外の二つの要素とかを Agda では具体的に指摘する必要があり、これが一般的に成立することも示す必要がある。
+Agda によれば
+
+    全部証明しろ
+
+ということになる。
 
 --Permutationに対応するデータ構造
 
@@ -243,11 +249,130 @@
 
 これは順列と1対1対応するので都合が良い。
 
---Permutationの数え上げ
+--PermutationとFL nの対応
+
+FL n が置換に対応することは証明する必要がある。ここでは順列の combinator を使う。
+
+    FL→perm   : {n : ℕ }  → FL n → Permutation n n 
+    FL→perm f0 = pid
+    FL→perm (x :: fl) = pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )
+
+    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) ) 
+
+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
+
+つまり、その位置の置換先が0でないと shrink は呼び出せない。pins/shrinkはBijection を構成するのでやや複雑。
+
+問題は、FL→perm と perm→FL が Bijection であることを示すことだが、
+
+    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
+
+が比較的簡単に示せるのでそれを使って証明できる。
 
 --実際の証明
 
+数え上げは FL n でおこなうのだが、
 
+   p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
+
+を示そうと思うとかなり面倒なことになる。しかし、ここで equalizer を使うと楽になる。
+置換は数字の列で表される。その列が等しければ、元の置換も等しいことが証明できる。
+
+   pleq  : {n  : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y
+
+これを使って
+
+   p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
+   p0id = pleq _ _ refl 
+
+という風に簡単に証明できる。plist0 x は具体的なλ項どうしの比較だから refl で良い。pleq の証明は
+plist0 の algorythm を二つの項 x, yで同時にたどって、入力 q : Fin n に対して (x ⟨$⟩ʳ q) ≡ (y ⟨$⟩ʳ q)
+を示していけばよい。
+
+3次では
+
+   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)
+
+になるのだが、これを3次対称群の要素全部に付いて確認する必要がある。
+
+   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) )
+   ... | s | (zero :: (zero :: (zero :: f0))) | se |  record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g)\
+ )
+   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } =
+        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
+   ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } =
+        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (suc zero) :: (suc zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } =
+        case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
+   ... | (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) )
+   ...
+
+というように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 : {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
+       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) ]
+
+これをすべての場所に付いて record を作成する。
+
+     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 }
+       ....
+
+これだけでは閉じてなくて、もう一種類必要になる。
+
+     dba-triple : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) → Triple i<3 j<4 (3rot  ∘ₚ 3rot )
+
+つまり、5次対称群の中で3次の置換は二種類にわかれて存在していて、それらが交互に交換子を生成するようになっている。
+
+     dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
+          → deriving n (abc i<3 j<4 )
+     dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
+          → deriving n (dba i<3 j<4 )
+
+この二つが相互参照している構造になっている。本の証明ではそれを気にする必要はないが、Agda は出目を気にするので必要である。
+
+このチェックにも時間はかかるが、3次対称群ほどではない。
+
+しかし、この方法では 4次対称群の可解性を示すのは厳しい。そこで、Sorted List である Fresh List を使う。
 
 --Fresh List
 
@@ -282,73 +407,162 @@
        ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
        []
 
-などとできる。
+などとできる。Sort されてないものを定義することはできない。
 
---Fresh List insert
+fresh は Set 、つまり命題を返す形なので、値が十分に決まらないと証明するものもわからない。
 
     fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1
 
-とできれば。
+とできれば良い。FLinsert は単なる線形挿入だが、fresh listを証明する必要がある。
 
-    FLinsert : {n : ℕ } → FL n → FList {n}  → FList {n}
+    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)
     FLinsert {zero} f0 y = f0 ∷# []
     FLinsert {suc n} x [] = x ∷# []
-    FLinsert {suc n} x (cons a y x₁) with total x a
-    ... | inj₁ (case1 eq) = cons a y x₁
-    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
-       ttf : (a : FL (suc n)) → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
-       ttf a [] fr = Level.lift tt
-       ttf a (cons a₁ y x1) (lift lt1 , _ ) = (Level.lift (ttf< {!!} )) , ttf a₁ y x1
-    ... | inj₂ (case1 eq) = cons a y x₁
-    ... | inj₂ (case2 lt) = cons a (cons x y {!!}) {!!}
+    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 )
+
+という形で、FLinsert と FLfresh で相互再帰していく。
+
+{\tt ⌊ _f<?_ ⌋} は{\tt  _f<?_}のままでは Set で扱いづらいので、それが真なのか偽なのかを表す data である。fromWitness や toWitness
+で変換する。中には不等号を表す data 構造が入る。fresh の base は ⊤ なので {\tt  Level.lift tt}が最後に来る。
+{\tt R a x × fresh a xs} はみづらいが、直積で不等号と、後に続く fresh の条件リストがある。
 
 --Permuation の数え上げ
 
-全部のPermutationをListにする。全部入っていることをデータ構造として表す
+全部のPermutationをFresh Listにする。全部入っていることをデータ構造として表すには以下の data を使う。
 
   data Any : List# A R → Set (p ⊔ a ⊔ r) where
     here  : ∀ {x xs pr} → P x → Any (cons x xs pr)
     there : ∀ {x xs pr} → Any xs → Any (cons x xs pr)
 
-ここにある、あそこにあるみたいな感じ。
+ここにある、あそこにあるみたいな感じである。
 
     AnyFList : (n : ℕ )  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
 
 が示せれば、∀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)
+
+などが証明できるのでこれを使う。
+
 --数え上げの方法
 
-    Flist1 :  {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
-    Flist1 zero i<n [] _ = []
-    Flist1 zero i<n (a ∷# x ) z  = FLinsert ( zero :: a ) (Flist1 zero i<n x z )
-    Flist1 (suc i) (s≤s i<n) [] z  = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z 
-    Flist1 (suc i) i<n (a ∷# x ) z  = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z )
+FL n は一つ小さいリストの前に、0からnまでを付け加えることで数え上げられる。
+この方法だと fresh を作るのに相互再帰は必要ない。しかし、このままでは Agda が停止条件を見つけられなので、
+\verb+{-# TERMINATING #-}+を付けている。
+
+
+    {-# TERMINATING #-}
+    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
+            → 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 )
+
+{\tt (cons a (cons a₁ L x₂) x₁)} は {\tt (cons a₁ L x₂)} と小さくなってるのだが、Agda はそれを認識してくれない。
 
-    ∀Flist : {n : ℕ } → FL n → FList n
-    ∀Flist {zero} f0 = f0 ∷# [] 
-    ∀Flist {suc n} (x :: y)  = Flist1 n a<sa (∀Flist y) (∀Flist y)   
+--Commutator の数え上げの方法
+
+さらに、交換子の生成を数え上げる必要がある。差分リストを使えば
+
+    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 )
+    tl2 : ( x z : FList n) → FList n →  FList n
+    tl2 [] _ x = x
+    tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
 
-しかし、Any を示しにくい。あと、もう少しだが...
+    CommFList  :  FList n →  FList n
+    CommFList x =  tl2 x x []
+
+    CommFListN  : ℕ  →  FList n
+    CommFListN  0 = ∀Flist fmax
+    CommFListN  (suc i) = CommFList (CommFListN i)
+
+数え上げ自体は簡単で、すべての組の交換子を作ってFLinsertすればよい。そのために FLinsert を作ったのだった。
+
+それが正しく、すべての組み合せを含んでいるかを示す必要がある。
+
+    CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )
 
-    fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n 
-    fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
-        fsuc1 : suc (toℕ x) < n
-        fsuc1 =  Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
-    fsuc (x :: y) (f<t lt) = x :: fsuc y lt
+つまり、deriving i x ならば、それは  CommFListN i に含まれているというわけである。これを示すには、
+CommFListNを i にそって deriving i x と一緒に分解していく。あとは、 tl2　と tl3  が特定の組み合せを含むことを
+調べに行く。
 
-この時に、x f< fsuc x が成立する。
+    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
+       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  = ?
+       -- 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 = ?
+
+この時に、
+
+       comm8 : (L L4 L2 : FList n) → (a : FL n)
+            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2)
+            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L L2))
+       comm8← : (L L4 L2 : FList n) → (a : FL n)  → ¬ ( a ≡ perm→FL g )
+           →  Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L L2))
+           →  Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2)
 
-    ∀Flist' : (n : ℕ ) → FList n
-    ∀Flist' n = ∀Flist0' n n FL0 {!!} where
-       ∀Flist0' : (i j : ℕ) → (x : FL n) → x f< fmax → FList n
-       ∀Flist0' zero zero x _ = []
-       ∀Flist0' zero (suc j) x lt = ∀Flist0' j j fmax {!!}
-       ∀Flist0' (suc i) j x lt = cons (fsuc x lt) (∀Flist0' i j (fsuc x lt) {!!} ) {!!}
+などの交換法則が必要になる。つまり、g が a と関係なければ {\tt (tl3 a L L2)} を移動して良い。
+
+このアルゴリズムだと、一度、tl2 のそこまで潜らないと戻り値が確定しない。なので、交換則をつかって行きつ戻りつする必要がある。
+
+おそらく、CommFListN と CommStage→ を同時に生成する見通しの良い方法があると思われる。
+
+--Fresh List を使った可解の検査
+
+結局、 {\tt Any (perm→FL x ≡_) y → x =p= pid }を調べるには FList n が {\tt FL0 ∷# []} であることを確認すればよい。
 
-なのだが、fsuc は最大を越えないことを示す必要がある。めんどい。
+   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 = refl
+
+   solved1 :  (x : Permutation 3 3) → deriving 2 x → x =p= pid
+   solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where
+      solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 )
+      solved2 = CommStage→ 3 2 x dr
+
+と簡単に記述することができる。
+
 
 --実行時間
 
+Fresh List を使う方法だと、3次の場合でも10秒でチェックされる。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の証明
 
 静的と動的