# HG changeset patch # User Shinji KONO # Date 1609993715 -32400 # Node ID 57601db306e98c84aedcf98e1722e580458c821d # Parent 72ec93c67ab27fe71d8448396aea9283034e5d41 ... diff -r 72ec93c67ab2 -r 57601db306e9 Galois.mm --- a/Galois.mm Fri Dec 04 07:07:19 2020 +0900 +++ b/Galois.mm Thu Jan 07 13:28:35 2021 +0900 @@ -27,7 +27,7 @@ - + @@ -50,7 +50,7 @@ - + @@ -117,7 +117,7 @@ - + diff -r 72ec93c67ab2 -r 57601db306e9 Galois1.mm --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Galois1.mm Thu Jan 07 13:28:35 2021 +0900 @@ -0,0 +1,415 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r 72ec93c67ab2 -r 57601db306e9 galois-prosym.ind --- a/galois-prosym.ind Fri Dec 04 07:07:19 2020 +0900 +++ b/galois-prosym.ind Thu Jan 07 13:28:35 2021 +0900 @@ -1,4 +1,4 @@ --title: Agda によるガロア理論 +-title: AgdaによるGalois理論のプログラミング --All connected @@ -6,7 +6,7 @@ 群の要素の数え上げなどを直接に実行できる。この時に「正しく数え上げのか」ということが問題になる。4色問題が計算機を使って解かれた時にも検算\cite{4color}が問題になった。 -Agdaは Curry Howard 対応に基づく定理証明を行う。命題が型であり証明がλ項に対応する。つまり、Agdaは証明を変数の値として持ち歩くことが +Agda\cite{AgdaWiki}は Curry Howard 対応に基づく定理証明を行う。命題が型であり証明がλ項に対応する。つまり、Agdaは証明を変数の値として持ち歩くことができる。つまり、今計算している値だけでなく、その値の性質(5より小さいとか)、そして、その由来(何から作られたのか)を値として持ち歩くことができる。計算結果が、ちゃんと要求された証明につなかっていることを示すことが可能である。つまり計算だけなくて、証明としてちゃんとつながっていることになる。 @@ -335,10 +335,15 @@ --5次対称群 -abc はpinsなどで定義できる。5次の中の3次なので二つ空き場所がある。それを不等式で指定する。不等式なのはFinを指定するのに便利だからである。 +abc はpinsなどで定義できる。 + + --- 1 ∷ 2 ∷ 0 ∷ [] abc + 3rot : Permutation 3 3 + 3rot = pid {3} ∘ₚ pins (n≤ 2) + +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 ]} なのだが、場所を正確に指定する必要がある。 @@ -353,23 +358,44 @@ [ 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 を作成する。これがすべての組み合せについて記述される。10行程度である。 +これをすべての場所に付いて record を作成する。これがすべての組み合せについて記述される。図\ref{fig:3s}の10行程度である中の値は自分で計算する必要がある。 +\begin{figure*}[tb] + 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 } - .... + 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 (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = + record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } +\caption{5次対称群のめんどくさい計算の半分} +\label{fig:5s} +\end{figure*} -これだけでは閉じてなくて、もう一種類必要になる。 +これだけでは閉じてなくて、もう一種類必要になる。3次の置換には右回転と左回転があり、右回転は左回転の交換子で作るためである。 +この対称性は置換のレベルでもFL nのレベルでも自明には見えない。なので、別々に手計算する必要がある。 - dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot ) + dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) + → Triple i<3 j<4 (3rot ∘ₚ 3rot ) -つまり、5次対称群の中で3次の置換は二種類にわかれて存在していて、それらが交互に交換子を生成するようになっている。 +5次対称群の中で3次の置換は二種類にわかれて存在していて、それらが交互に交換子を生成するようになっている。 dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 ) @@ -380,32 +406,38 @@ このチェックにも時間はかかるが、3次対称群ほどではない。 -しかし、この方法では 4次対称群の可解性を示すのは厳しい。そこで、Sorted List である Fresh List を使う。 +しかし、この方法では 4次対称群の可解性を示すのは厳しい。そこで、Sorted List である Fresh List \cite{Coquand2002}を使う。 + +

--Fresh List 各要素の大小関係がすべて入っている sort された List 。これを使うと重複要素を排除できる。 -

+ module _ {a} (A : Set a) (R : Rel A r) where - data List# : Set (a ⊔ r) - fresh : (a : A) (as : List#) → Set r + data List# : Set (a ⊔ r) + fresh : (a : A) (as : List#) → Set r - data List# where - [] : List# - cons : (a : A) (as : List#) → fresh a as → List# + data List# where + [] : List# + cons : (a : A) (as : List#) → fresh a as → List# - infixr 5 _∷#_ - pattern _∷#_ x xs = cons x xs _ + infixr 5 _∷#_ + pattern _∷#_ x xs = cons x xs _ - fresh a [] = ⊤ - fresh a (x ∷# xs) = R a x × fresh a xs + fresh a [] = ⊤ + fresh a (x ∷# xs) = R a x × fresh a xs + +% もう少し説明するこれを使うと FList : {n : ℕ } → Set FList {n} = List# (FL n) ⌊ _f