-title: Agda によるガロア理論

--All connected

数学の証明に計算機を使うのは既に古い歴史がある。Agda \cite{agda} は定理証明支援系だが、普通の関数型プログラミング言語でもあり、
群の要素の数え上げなどを直接に実行できる。この時に「正しく数え上げのか」ということが問題になる。4色問題が計算機を使って解かれた
時にも検算\cite{4color}が問題になった。

Agdaは Curry Howard 対応に基づく定理証明を行う。命題が型であり証明がλ項に対応する。つまり、Agdaは証明を変数の値として持ち歩くことが
できる。つまり、今計算している値だけでなく、その値の性質(5より小さいとか)、そして、その由来(何から作られたのか)を値として
持ち歩くことができる。
計算結果が、ちゃんと要求された証明につなかっていることを示すことが可能である。つまり計算だけなくて、証明としてちゃんとつながっていることになる。

ここでは、例題としてガロア理論の一部である可解群を使い、証明を含むデータ構造として、

   Data.Fin              有限な自然数
   FL                    順列に対応する減少列
   Data.List.Fresh       Sorted List

を使う。一部は、AgdaのLibrary でる。

証明付きのデータ構造は assert と異なり、それを作成する段階で証明を構成する必要がある。証明は型の整合性の検査なので、
実行時ではなく、プログラムコードの入力時に決まる。しかし、Dataの構成は実行に行われるので、群の要素の数え上げも
型検査の時に実行される。つまり、定理証明の時間が問題になる。

証明付きデータを使う方が10倍速いことがあり、また、証明自体も手で書く部分が少なくなるので楽になる。ただし、
List への挿入などは、証明を一緒に書くことになるのでやさしいとは言えない。

--ガロア理論

xの多項式f(x)が解を持てば因数定理により 

　 (x - α)(x - β)(x - γ)

の形に因数分解可能である。αβγは定数だが、この三つを置換しても式は同じになる。つまり展開すれば同じ式になる。
つまり、順列の群である対称群が対応することになある。f(x)因数定理による分解

　 f(x) => (x - α)(g x)

は、f(x)の対称群からg(x)の対称群への変換になる。具体的には三次の対称群から二次の対称群の変換がなければならない。
ここで二次式に帰着できれば変換があり、変換があれば三次式を二次式に変換できる。

三次の対称群、つまり三つの数の入れ替えは、αβγはγ..と.γ.と..γからなるが、
三次式を二次式に変換できるなら、αβγとβαγの二つの形にならないとおかしい。つまり、

　αγβ = αβγ

とγを移動できる必要がある。ということは、

　γβ=βγ

である必要がある。逆元をかけて

　 β⁻¹γ⁻¹βh = e

になれば良い。左辺がCommutator(交換子)と呼ぶ。ある群の二つの要素を取って交換子に変換したものを交換子群と呼ぶ。
これは群から群への関手になる。交換子群を繰り返し作り、単元だけの群になる場合をSolvable 可解と呼ぶ。
多項式に対応する対称群が可解であることがべき根を使って解けるための条件になる。

今回は可解と方程式がべき根で解ける部分には関与せず、2-5次の対称群が可解かどうかを計算で示す。

--Agdaによる Group の表現

群は階層的な構造をもっており、演算と同値関係を持つ Magma, 合同則を持つ Semigroup,結合則があるMonoid,そして逆元をもつるGroup
という順序で作成する。ここで作るのは対称群なので順列を要素にする。

Agda は Haskell と異なり、直積である record と Sum型である dataを区別する。record は field を持つオブジェクトに相当する。
IsGroup は別に定義されていて、そこに群の公理が記述されている。{\tt record { } } が record の構成子になる。

Agda の型には Level があり、基本型の後に自然数で指定する。⊔ はLevelの最大値演算子である。
: の前が名前で、後ろが型である。
Carrier は要素の型であり、関係と演算子が{\tt  Rel Carrier ℓ, Op₂ Carrier}と定義されているが、
これらは{\tt Carrier → Carrier → Set ℓ} と {\tt Carrier →　Carrier →　Carrier } のことである。

    record Group c ℓ : Set (suc (c ⊔ ℓ)) where
      field
        Carrier : Set c
        _≈_     : Rel Carrier ℓ
        _∙_     : Op₂ Carrier
        ε       : Carrier
        _⁻¹     : Op₁ Carrier
        isGroup : IsGroup _≈_ _∙_ ε _⁻¹
      open IsGroup isGroup public
      monoid : Monoid _ _
      monoid = record { isMonoid = isMonoid }
      open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)

群の構成要素は field で定義されているが、Monoid の公理 isMonoid などは module で定義されている。
これらの field を適切に埋めれば良い。

順列は Agda に

   Data.Fin.Permutation

というのがあるので、それを使う。これは Data.Fin の間の Bijection として4抽象的に定義されている。
中括弧は省略可能な引数である。

    -- Data.Fin.Permutation.id
    pid : {p : ℕ } → Permutation p p
    pid = permutation fid fid 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 }

    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 である。

    Symmetric : ℕ → Group  Level.zero Level.zero
    Symmetric p = record {
          Carrier        = Permutation p p
        ; _≈_            = _=p=_
        ; _∙_            = _∘ₚ_
        ; ε              = pid
        ; _⁻¹            = pinv
        ; 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} ))  
           ; ⁻¹-cong   = λ i=j → record { peq = λ q → p-inv i=j q }
          }
       } 

--Data.Fin

Agda は単なる自然数ではなく、有限な自然数をSum型として data 表されている。これが証明を持つデータ構造の最初の例
になっている。

   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}を
作るためには、それが n よりも小さい証明が必要である。\verb+{n : ℕ}+ 省略可能で型推論により自動的に決まる。
決まらなければ Agda が黄色で instantiation が足りないと警告される。証明では黄色を全部消す必要がある。
計算自体は値が決まってなくても計算可能なところまで進む。これは関数型言語の特徴である。

Fin は n よりも小さいという性質をデータ構造として持っているので、それを証明により取り出すことができる。

    -- toℕ≤n
    fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
    fin≤n {_} zero = z≤n
    fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f)

ここで、{\tt s≤s}と{\tt z≤n}は不等式をを表す data である。つまり、この証明は Fin から ≤ へのデータ構造の変換になっている。

--交換子

対称群が定義できたので交換子を定義する。

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

このように、Unicode っでほぼ数式として定義できるところが Agda の特徴である。Coq\cite{Coq}と異なる部分でもある。

この形で生成されるものを繰り返し生成したい。そのための生成演算子を以下のように定義する。

    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

: の前の引数 {\tt (P : Carrier → Set (Level.suc n ⊔ m))} は前回生成した時の条件である。ここに前の{\tt Commutator}を入れる。
: の後の引数はこのdataの出力であり、生成された要素になる。これは comm で作成した時に作らている。
ccong がないと、Commutator の等式が処理できない。
条件がない時には{\tt ⊤}を用いる。これは唯一つの生成演算子を持つData.Unit つまり Singleton である。

    data ⊤ : Set where
       tt : ⊤ 

という定義を持つ。交換子は積に付いて閉じてないので、交換子群を作る場合には以下の生成子も必要になる。しかし、
今回は単位元だけになるかどうかを知りたいだけなので、これは使わない。

      gen   : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙  g  )

交換子の生成を繰り返すのが次の述語 deriving である。。これも Set (Level.suc n ⊔ m) を返してる。つまり証明するべき命題を返すような関数になっている。
証明はもちろん、Commutator で作られるλ項であり、⊤の構成子 tt で終わる。

    deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
    deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
    deriving (suc i) x = Commutator (deriving i) x 

これを dervied-length 回繰り返すと、単位元のみになるというのは以下の record で表される。これが可解の定義になる。

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

dervied-length 回繰り返すと、単位元のみになるという数学的構造である。この時に、{\tt dervied-length : ℕ} は存在記号が付いていると
思って良い。

record を定義する以下のような記法で Symmetric 2 が solvable であることを表す。

    sym2solvable : solvable (Symmetric 2)
    solvable.dervied-length sym2solvable = 1
    solvable.end sym2solvable x d = ?

この ? を埋めるのが今回の仕事になる。5次対称群は可解でないので、以下を証明する。

    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 = ?

    ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
    ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) ? )

ここで {\tt ¬ A = A → ⊥} であり、⊥ は生成子のない data である。sol には仮定した solvable が来る。
{\tt abc 0<3 0<4} は5つのFinのうち、a を b に、bをcに、cをaに置換する置換である。これが何回交換子を
作っても残ってしまうことはアルティンの邦訳には以下のような証明が載っている。基本的にこれを証明することになる。


--Permutationに対応するデータ構造

有限な自然数 Fin の一対一対応 Bijection が Permutation だが 関数なので見えない。
これを数え上げる必要があるので、もっと具体的なものが望ましい。
単なるリストでも良いのだが、長さが決まらなかったり、同じ数字が入ったり、数字が足りなかったりで都合が悪い。
そこで Permutation を以下の data 構造に対応させる。

    data  FL : (n : ℕ )→ Set where
       f0 :  FL 0 
       _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)

Fin の減少列になる。最初の挿入の選択肢はゼロ、次は一つ、次は二つなどとなる。

       ((# 3) :: ((# 1) :: ((# 0 ) :: f0))) 

この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 )

これは順列と1対1対応するので都合が良い。

--Permutationの数え上げ

--実際の証明



--Fresh List

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

<center><img src="fig/fresh.svg"></center>

  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#

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

  fresh a []        = ⊤
  fresh a (x ∷# xs) = R a x × fresh a xs

これを使うと

FList : {n : ℕ } → Set
FList {n} = List# (FL n) ⌊ _f<?_ ⌋

    fr1 : FList
    fr1 =
       ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
       ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
       ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
       ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
       ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
       []

などとできる。

--Fresh List insert

    fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1

とできれば。

    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 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 {!!}) {!!}

--Permuation の数え上げ

全部のPermutationをListにする。全部入っていることをデータ構造として表す

  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 が入っていることがわかる。

--数え上げの方法

    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 )

    ∀Flist : {n : ℕ } → FL n → FList n
    ∀Flist {zero} f0 = f0 ∷# [] 
    ∀Flist {suc n} (x :: y)  = Flist1 n a<sa (∀Flist y) (∀Flist y)   

しかし、Any を示しにくい。あと、もう少しだが...

    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

この時に、x f< fsuc x が成立する。

    ∀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) {!!} ) {!!}

なのだが、fsuc は最大を越えないことを示す必要がある。めんどい。

--実行時間

--Agdaの証明

静的と動的

抽象的と具体的

証明を持つデータ型

--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 = {!!}

良くわからん。