Mercurial > hg > Papers > 2020 > kono-prosym

changeset 4:353edf5ef2d9

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 Sat, 09 Jan 2021 09:43:12 +0900
parents 57601db306e9
children 9027098a5b1d
files Galois1.mm fig/altin.jpg fig/fresh.graffle fig/fresh.svg fig/iwanami-gendai.jpg main.pdf presen.html presen.ind sigjouto.pdf
diffstat 9 files changed, 1756 insertions(+), 50 deletions(-) [+]
line wrap: on
line diff
--- a/Galois1.mm	Thu Jan 07 13:28:35 2021 +0900
+++ b/Galois1.mm	Sat Jan 09 09:43:12 2021 +0900
@@ -212,12 +212,15 @@
 </node>
 <node TEXT="solvable" ID="ID_178918488" CREATED="1609990354030" MODIFIED="1609990359075"/>
 </node>
-<node TEXT="symmetric group representation in agda" ID="ID_1083504702" CREATED="1609990379507" MODIFIED="1609990393339">
+<node TEXT="symmetric groupin agda" ID="ID_1083504702" CREATED="1609990379507" MODIFIED="1610005855100">
+<node TEXT="representation" ID="ID_319391779" CREATED="1610005856583" MODIFIED="1610005864458">
 <node TEXT="Data.Fin" ID="ID_1340949296" CREATED="1609990393883" MODIFIED="1609990404918"/>
 <node TEXT="Bijection" ID="ID_316860227" CREATED="1609990405535" MODIFIED="1609990409631"/>
 <node TEXT="List" ID="ID_1710126935" CREATED="1609990410154" MODIFIED="1609990413645"/>
 <node TEXT="FL" ID="ID_235104633" CREATED="1609990415278" MODIFIED="1609990419436"/>
 </node>
+<node TEXT="1 to 1" ID="ID_1677442759" CREATED="1610005903688" MODIFIED="1610005907592"/>
+</node>
 <node TEXT="proofs" ID="ID_1219242238" CREATED="1609992596012" MODIFIED="1609992600251">
 <node TEXT="2" OBJECT="java.lang.Long|2" ID="ID_514245484" CREATED="1609992600706" MODIFIED="1609992602407"/>
 <node TEXT="injection" ID="ID_1366306030" CREATED="1609992603682" MODIFIED="1609992607205">
@@ -232,6 +235,10 @@
 <node TEXT="a list contains everything" ID="ID_67235294" CREATED="1609990709190" MODIFIED="1609990733750">
 <node TEXT="sorted" ID="ID_73107613" CREATED="1609990734279" MODIFIED="1609990738112"/>
 <node TEXT="any" ID="ID_1569296473" CREATED="1609990738656" MODIFIED="1609990745411"/>
+<node TEXT="enumeration" ID="ID_992373663" CREATED="1610005876529" MODIFIED="1610005884864">
+<node TEXT="permutation" ID="ID_535994" CREATED="1610005972212" MODIFIED="1610005978496"/>
+<node TEXT="commutator" ID="ID_1725495702" CREATED="1610005979019" MODIFIED="1610005984240"/>
+</node>
 </node>
 <node TEXT="Fresh List" ID="ID_928929976" CREATED="1609990754285" MODIFIED="1609990759712">
 <node TEXT="Set valued function" ID="ID_1431257568" CREATED="1609990760342" MODIFIED="1609990767070"/>
@@ -242,6 +249,7 @@
 </node>
 <node TEXT="insert" ID="ID_1479901665" CREATED="1609990795810" MODIFIED="1609990799803"/>
 <node TEXT="insert / cons and Any" ID="ID_265930485" CREATED="1609990800355" MODIFIED="1609990813411"/>
+<node TEXT="enumeration of pair" ID="ID_622029876" CREATED="1610006179353" MODIFIED="1610006194627"/>
 </node>
 <node TEXT="proofs" ID="ID_71982613" CREATED="1609990838839" MODIFIED="1609990843748">
 <node TEXT="2" OBJECT="java.lang.Long|2" ID="ID_1357773799" CREATED="1609990844233" MODIFIED="1609990848197"/>
Binary file fig/altin.jpg has changed
Binary file fig/fresh.graffle has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/fig/fresh.svg	Sat Jan 09 09:43:12 2021 +0900
@@ -0,0 +1,97 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<svg xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns="http://www.w3.org/2000/svg" viewBox="183.22286 263 458.1275 78.90935" width="458.1275" height="78.90935">
+  <defs>
+    <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black">
+      <g>
+        <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
+      </g>
+    </marker>
+    <font-face font-family="Hiragino Sans" font-size="14" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300">
+      <font-face-src>
+        <font-face-name name="HiraginoSans-W3"/>
+      </font-face-src>
+    </font-face>
+  </defs>
+  <metadata> Produced by OmniGraffle 7.18\n2021-01-08 02:22:07 +0000</metadata>
+  <g id="Canvas_1" stroke-dasharray="none" fill-opacity="1" fill="none" stroke="none" stroke-opacity="1">
+    <title>Canvas 1</title>
+    <rect fill="white" x="183.22286" y="263" width="458.1275" height="78.90935"/>
+    <g id="Canvas_1_Layer_1">
+      <title>Layer 1</title>
+      <g id="Line_14">
+        <path d="M 188.22289 322.40935 C 188.22289 322.40935 206.7649 298.61305 227.12523 291.33123 C 247.48556 284.0494 245.4722 285.8769 260.09007 296.70623 C 266.41293 301.39036 270.75205 308.1683 273.64056 314.3524" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/>
+      </g>
+      <g id="Line_15">
+        <path d="M 195.79042 327.57326 C 209.39587 322.3717 243.40837 309.5726 272.2229 300.40935 C 309.1942 288.6522 297.0605 288.14154 320.2229 288.40935 C 343.3853 288.67716 340.5237 289.5975 353.9807 301.35466 C 358.5137 305.3151 361.55214 309.84744 363.5885 314.11703" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/>
+      </g>
+      <g id="Line_17">
+        <path d="M 198.34832 326.59766 C 198.34832 326.59766 278.14717 312.945 332.2229 302.40935 C 386.2986 291.8737 357.84464 290.57312 389.2229 289.40935 C 420.60113 288.2456 423.8576 287.12603 442.9807 298.30152 C 453.16225 304.2516 456.3976 312.5272 457.19713 318.96533" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/>
+      </g>
+      <g id="Line_18">
+        <path d="M 196.16473 329.03786 C 225.74445 325.03864 350.34712 308.2198 426.2229 298.40935 C 512.77257 287.2188 464.19767 289.26728 495.2229 290.40935 C 526.2481 291.55143 521.4277 291.25005 535.7346 302.4406 C 540.191 305.9263 542.8403 309.90566 544.3759 313.7329" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/>
+      </g>
+      <g id="Line_19">
+        <path d="M 196.19472 329.3015 C 232.02956 325.93584 407.9802 309.4123 504.2229 300.40935 C 611.7371 290.35203 534.30333 295.00652 569.2229 294.40937 C 604.14244 293.8122 608.7826 284.9862 627.4807 298.30152 C 639.3752 306.77184 639.2697 321.9099 637.61815 331.8049" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/>
+      </g>
+      <g id="Graphic_2">
+        <circle cx="189.72289" cy="329.90935" r="6.50001038636234" fill="black"/>
+      </g>
+      <g id="Graphic_3">
+        <circle cx="278.7229" cy="329.55614" r="6.1585124580284" fill="black"/>
+      </g>
+      <g id="Graphic_4">
+        <circle cx="367.7229" cy="329.90935" r="6.50001038636232" fill="black"/>
+      </g>
+      <g id="Graphic_5">
+        <circle cx="456.7229" cy="329.90935" r="6.50001038636232" fill="black"/>
+      </g>
+      <g id="Graphic_6">
+        <circle cx="545.7229" cy="329.90935" r="6.50001038636234" fill="black"/>
+      </g>
+      <g id="Graphic_7">
+        <circle cx="634.7229" cy="329.90935" r="6.50001038636233" fill="black"/>
+      </g>
+      <g id="Line_8">
+        <line x1="196.22287" y1="329.88356" x2="262.66448" y2="329.61987" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_9">
+        <line x1="284.88136" y1="329.5806" x2="351.323" y2="329.84427" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_10">
+        <line x1="374.2229" y1="329.90935" x2="440.32286" y2="329.90935" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_11">
+        <line x1="463.2229" y1="329.90935" x2="529.32286" y2="329.90935" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_12">
+        <line x1="552.2229" y1="329.90935" x2="618.32286" y2="329.90935" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Graphic_23">
+        <text transform="translate(231.1296 268.17145) rotate(2)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">＞</tspan>
+        </text>
+      </g>
+      <g id="Graphic_24">
+        <text transform="translate(322.9956 268.17145) rotate(2)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">＞</tspan>
+        </text>
+      </g>
+      <g id="Graphic_25">
+        <text transform="translate(414.8616 268.17145) rotate(2)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">＞</tspan>
+        </text>
+      </g>
+      <g id="Graphic_26">
+        <text transform="translate(515.0936 268.17145) rotate(2)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">＞</tspan>
+        </text>
+      </g>
+      <g id="Graphic_27">
+        <text transform="translate(598.5936 272.17145) rotate(2)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">＞</tspan>
+        </text>
+      </g>
+    </g>
+  </g>
+</svg>
Binary file fig/iwanami-gendai.jpg has changed
Binary file main.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presen.html	Sat Jan 09 09:43:12 2021 +0900
@@ -0,0 +1,987 @@
+<html>
+<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=UTF-8">
+<head>
+<STYLE type="text/css">
+.main { width:100%; }
+.side { top:0px; width:0%; position:fixed; left:80%; display:none}
+</STYLE>
+<script type="text/javascript">
+function showElement(layer){
+    var myLayer = document.getElementById(layer);
+    var main = document.getElementById('mmm');
+    if(myLayer.style.display=="none"){
+        myLayer.style.width="20%";
+        main.style.width="80%";
+        myLayer.style.display="block";
+        myLayer.backgroundPosition="top";
+    } else { 
+        myLayer.style.width="0%";
+        main.style.width="100%";
+        myLayer.style.display="none";
+    }
+}
+</script>
+<title>AgdaによるGalois理論のプログラミング</title>
+</head>
+<body>
+<div class="main" id="mmm">
+<h1>AgdaによるGalois理論のプログラミング</h1>
+<a href="#" right="0px" onclick="javascript:showElement('menu')">
+<span>Menu</span>
+</a>
+<a href="#" left="0px" onclick="javascript:showElement('menu')">
+<span>Menu</span>
+</a>
+
+<p>
+
+<hr/>
+<h2><a name="content000">motivation </a></h2>
+5次方程式が代数的に解けないことの復習
+<p>
+数学書では省略されてても Agda は許してくれない
+<p>
+計算で示しても、それが証明になっているかどうかは別
+<p>
+証明付きデータ構造を使う
+<p>
+計算と証明が「全部つながってる」
+<p>
+　この計算、いったい、何を計算してるの?
+<p>
+それを型で示す
+<p>
+
+<hr/>
+<h2><a name="content001">Galois theory :  多項式方程式</a></h2>
+
+<pre>
+  (x - α)(x - β)(x - γ) = 0
+
+</pre>
+と因数分解されればαβγが解になる。
+<p>
+
+<hr/>
+<h2><a name="content002">Galois theory :  解と置換群(対称群)</a></h2>
+αβγを入れ替えても良い(Symmetric Group))。これが
+<p>
+
+<pre>
+  (x - α)(x - β) = 0
+
+</pre>
+に帰着されるなら、αβ を入れ替えても良い。ならば、αβγ の置換で
+<p>
+
+<pre>
+   αβγ = βαγ
+
+</pre>
+にならないとおかしい。
+<p>
+
+<hr/>
+<h2><a name="content003">Galois theory :  可解群</a></h2>
+
+<pre>
+   αβγ = βαγ
+   α⁻¹β⁻¹αβγγ⁻¹ = α⁻¹β⁻¹βαγγ⁻¹
+   α⁻¹β⁻¹αβ = e  (交換子 Commutator)
+
+</pre>
+なので、対称群のすべての要素を α⁻¹β⁻¹αβ の形にするのを繰り返して e になれば良い(可解群)。
+<p>
+(もちろん、これは証明になってない。気分的な説明。本当は正規拡大体とか代数的拡大とか)
+<p>
+ここは今回は Agda で証明しません。
+<p>
+あれ? 割と Agda の得意な分野なのでできるはず。やさしくはないだろうけど
+<p>
+Agdaは抽象的な証明が得意
+<p>
+
+<hr/>
+<h2><a name="content004">5次方程式が代数的に解けないことの証明</a></h2>
+5次の対称群は可解でないことを示せばよい。2,3,4次は可解。教科書だと
+<p>
+<img src="fig/altin.jpg" height="600">
+
+<p>
+これは良い方で、岩波だと練習問題。
+<p>
+<img src="fig/iwanami-gendai.jpg" height="600">
+
+<p>
+
+<hr/>
+<h2><a name="content005">数学の本の記述の特徴</a></h2>
+理解した後で読むとちゃんと書いてある
+<p>
+理解する前には何が書いてあるのかわからない
+<p>
+
+<hr/>
+<h2><a name="content006">Agda でちゃんとやろうぜ</a></h2>
+Curry Howard 対応に基づく定理証明支援系
+<p>
+
+<pre>
+    依存型を持つ純関数型言語
+    依存型とは、型を値に持つ変数
+    命題そのものは Set という型を持つ
+
+</pre>
+構文的には Haskell とほぼ同じ。Coq と違い、何もしてくれない。全部、自分で証明を書く。(いさぎよい)
+<p>
+
+<hr/>
+<h2><a name="content007">Agda :            lambda</a></h2>
+A → B の証明
+<p>
+
+<pre>
+  →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 
+
+</pre>
+引数の値は、型の証明
+<p>
+入力は∀が付いていると考える(∃はあとで)
+<p>
+
+<hr/>
+<h2><a name="content008">Agda :            record</a></h2>
+A ∧ B の証明
+<p>
+
+<pre>
+    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 }
+
+</pre>
+
+<hr/>
+<h2><a name="content009">Agda :            data</a></h2>
+
+<p>
+A ∨ B の証明
+<p>
+
+<pre>
+    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
+
+</pre>
+
+<hr/>
+<h2><a name="content010">Agda :            negation</a></h2>
+
+<p>
+
+<pre>
+    data ⊥ : Set where
+
+</pre>
+constructor のないデータ構造(偽
+<p>
+
+<pre>
+    ⊥-elim : {A : Set } -&gt; ⊥ -&gt; A
+    ⊥-elim ()
+
+</pre>
+起きない入力は () 。λ () とも書ける
+<p>
+
+<pre>
+    data ⊤ : Set where
+       tt : ⊤
+
+</pre>
+要素が一つしかない型(真
+<p>
+
+<hr/>
+<h2><a name="content011">Agda :            unification</a></h2>
+
+<pre>
+    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
+
+</pre>
+項(正規化された)として等しい。変数はどうするの? 十分に instanciation されない場合は黄色くなる。
+<p>
+その他、細かい問題が... internal parametricity... inspect...
+<p>
+でも、これで全部。さぁ、Agda を書こう。
+<p>
+
+<hr/>
+<h2><a name="content012">Galois theory i nAgda :        Commutator</a></h2>
+
+<pre>
+    [_,_] :  Carrier   → Carrier   → Carrier  
+    [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h 
+
+</pre>
+こんな風に数学の教科書通りに Unicode を使って書けるところが Agda の良いところ
+<p>
+
+<pre>
+    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
+
+</pre>
+Set を返してるのはなに? Set は何かの命題、 つまり真偽として扱って良い。したがって
+<p>
+　　P : Carrier → Set
+<p>
+これは Carrier の部分集合を指定する命題となる。 (Carrier は群の要素の型)
+<p>
+交換子 Commutator p は述語 f p で限定された p : Carrier が [ g , h ] という形で生成されることを示している。
+<p>
+deriving i は、Carrier の部分集合で、Commutator を再帰的に繰り返して得られたもの
+<p>
+
+<hr/>
+<h2><a name="content013">Galois theory in Agda :        Solvable</a></h2>
+
+<pre>
+    record solvable : Set (Level.suc n ⊔ m) where
+      field 
+         dervied-length : ℕ
+         end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε  
+
+</pre>
+存在∃は record で書く。ある dervied-length : ℕ があって、その回数のderive の繰り返しで  x ≈ ε になる
+<p>
+この record を構成できれば、その群は可解ということになる。これで問題は定義できた
+<p>
+
+<hr/>
+<h2><a name="content014">Galois theory in Agda :        Symmetric group </a></h2>
+対称群の要素は置換だが、Agdaの標準ライブラリだと有限な数のBijectionとして定義される
+<p>
+
+<pre>
+   Permutation p p
+
+</pre>
+定義は複雑だが二つの写像 _⟨$⟩ˡ_  _⟨$⟩ʳ_ と  y ⟨$⟩ˡ (y ⟨$⟩ʳ x) ≡ x と  y ⟨$⟩ʳ (y ⟨$⟩ˡ x) ≡ x からなる record 
+<p>
+残念ながら扱いにくい。同等性とか。単純に x ≡ y を証明できない(Agdaの制約 1)
+<p>
+しかし群であることを示すのは簡単
+<p>
+
+<hr/>
+<h2><a name="content015">Permutation :        Data.Fin</a></h2>
+有限な数
+<p>
+
+<pre>
+   data Fin : ℕ → Set where
+     zero : {n : ℕ} → Fin (suc n)
+     suc  : {n : ℕ} (i : Fin n) → Fin (suc n)
+
+</pre>
+x : Fin 3 のように使う
+<p>
+Fin 0 の値は存在しない
+<p>
+
+<pre>
+     _⟨$⟩ˡ_ : Fin p →  Fin p
+
+</pre>
+
+<hr/>
+<h2><a name="content016">Permutation :        List</a></h2>
+
+<p>
+置換は List ℕ で表されるので、それで良いのだが、List  ℕ が全部置換になるわけではない
+<p>
+そこで減少列 FL とその大小関係を定義する
+<p>
+
+<pre>
+    data  FL : (n : ℕ )→ Set where
+       f0 :  FL 0 
+       _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
+    data _f&lt;_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  where
+       f&lt;n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.&lt; yn →   (xn :: xt) f&lt; ( yn :: yt )
+       f&lt;t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f&lt; yt →   (xn :: xt) f&lt; ( xn :: yt )
+
+</pre>
+すると、これは置換と 1 to 1 になる。しかし  1 to 1 の証明は煩雑。しかし、簡単な方法があるかも。
+<p>
+煩雑でも証明できてしまえば問題ないので、簡単にする motivation はあまりでない。
+<p>
+でも簡単にしておくと、次に使えるかも。
+<p>
+
+<hr/>
+<h2><a name="content017">Proofs : 2</a></h2>
+これで道具立てはそろったので証明に行く
+<p>
+まず、二次対称群から
+<p>
+
+<pre>
+   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  }
+
+</pre>
+となるのだが、g と h が何かわからないので FL 2 に変換する
+<p>
+FL 2 は
+<p>
+
+<pre>
+   zero :: (zero :: f0)
+
+</pre>
+というものなので、これが pid つまり恒等置換であることは証明してあるのだが
+<p>
+
+<pre>
+   FL-inject : {n : ℕ }  → {g h : Permutation n n }  → perm→FL g ≡  perm→FL h → g =p= h
+
+</pre>
+を証明して使う。ところが、
+<p>
+
+<pre>
+  pleq  : {n  : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y
+
+</pre>
+を使うと
+<p>
+
+<pre>
+   p0 :  FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid
+   p0 = pleq _ _ refl
+
+</pre>
+とできる。Injection は圏論でいう Equalizaer で写像した先で等しいなら手元でも等しいという性質
+<p>
+
+<hr/>
+<h2><a name="content018">Proofs : 3</a></h2>
+2でこれなので 3 は絶望的に煩雑になる
+<p>
+たぶん、ガロアはそれを手で計算したはず
+<p>
+
+<hr/>
+<h2><a name="content019">Proofs : 5</a></h2>
+5は、solvable が存在しない、つまり否定を示せばよいsolvable から矛盾 counter-example を作る
+<p>
+
+<pre>
+    ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
+    ¬sym5solvable sol = counter-example (end5 (abc 0&lt;3 0&lt;4 ) (dervie-any-3rot0 (dervied-length sol) 0&lt;3 0&lt;4 ) ) where
+
+</pre>
+3次の対称群を含むことを示せばよいのだが、それが dervie-any-3rot0 実は dervie-any-3rot0 と dervie-any-3rot1 がいる
+<p>
+教科書だと「要素三つがとれるよね」と書いてあるが、Agda だと具体的に取ってくる必要がある。「あとは同じだよね」と書いてあっても、それを示す必要がある。
+<p>
+
+<hr/>
+<h2><a name="content020">もっと簡単にできるでしょ</a></h2>
+derving は簡単に計算できるので、それで証明した方が良いんじゃないの?
+<p>
+確かにその通り
+<p>
+計算は簡単だが、それを証明にするにはどうすれば良いの?
+<p>
+
+<pre>
+    すべての交換子の組み合せを計算している
+
+</pre>
+を証明すればよい
+<p>
+つまり sort された List に、全部の要素が含まれている (どんな要素でも入っている) any
+ことを Agda で書く
+<p>
+それには Fresh List というのを使う
+<p>
+
+<hr/>
+<h2><a name="content021">Fresh List</a></h2>
+(A : Set )と (R : A → A → Set) に対して
+<p>
+
+<pre>
+      data List# : Set 
+        []   : List#
+        cons : (a : A) (as : List#) → fresh a as → List#
+
+</pre>
+という List を定義する
+<p>
+
+<pre>
+      fresh : (a : A) (as : List#) → Set 
+      fresh a []        = ⊤
+      fresh a (cons x xs _) = R a ∧ fresh a xs
+
+</pre>
+普通の∷ (cons)の代わりに _∷#_ を使う
+<p>
+
+<pre>
+      infixr 5 _∷#_
+      pattern _∷#_ x xs = cons x xs _
+
+</pre>
+これも Set を値にしている。Fresh List の最後とそうでないもので fresh の中身が違う
+<p>
+List の要素毎に、fresh が存在するので、結構でかいものになる(O(2^n))。
+<p>
+<img src="fig/fresh.svg" width="80%" height="600">
+
+<p>
+
+<pre>
+    FList : (n : ℕ ) → Set
+    FList n = List# (FL n) ⌊ _f&lt;?_ ⌋
+    fr1 : FList 3
+    fr1 =
+       ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+       ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+       ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+       ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
+       ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
+       []
+
+</pre>
+と定義できる。これで FList 3 が sort されていることが「証明されている」。⌊ _f&lt;?_ ⌋ が不思議だが...
+<p>
+
+<hr/>
+<h2><a name="content022">Fresh List :        Any</a></h2>
+
+<pre>
+  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)
+
+</pre>
+ここにあったら here、先にあるなら there
+<p>
+
+<hr/>
+<h2><a name="content023">Fresh List :        Insert</a></h2>
+普通の insert と変わらないけど、fresh を作る必要がある
+<p>
+
+<pre>
+    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; 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&gt; ¬a ¬b lt  = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
+    FLinsert {suc n} x (cons a y yr)  | tri&gt; ¬a ¬b a&lt;x = cons a (FLinsert x y) (FLfresh a x y a&lt;x yr )
+
+</pre>
+
+<hr/>
+<h2><a name="content024">Fresh List :        Property on Insert / Cons </a></h2>
+
+<p>
+
+<pre>
+    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&lt;?_ ⌋ 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)
+
+</pre>
+あたりがあると便利
+<p>
+
+<hr/>
+<h2><a name="content025">Fresh List :        Any on Pair</a></h2>
+Commutator (それを作っていたのだった) は任意の pair なので
+<p>
+
+<pre>
+    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
+
+</pre>
+つまり二つの FList から、組を全部生成する必要がある。(fpq は ∧  の方が良かったか?)
+<p>
+
+<pre>
+    (p,q)   (p,qn) ....           (p,q0)
+    pn,q       
+    :        AnyComm FL0 FL0 P  Q
+    p0,q       
+
+</pre>
+こんな風に再帰で作れる(やさしくない
+<p>
+
+<hr/>
+<h2><a name="content026">Fresh List :        Solved using Fresh List</a></h2>
+まず全部の FL が入ってる FList
+<p>
+
+<pre>
+    record AnyFL (n : ℕ) : Set where
+       field
+         allFL : FList n
+         anyP : (x : FL n) → Any (x ≡_ ) allFL 
+
+</pre>
+これは AnyComm から作れる (やさしくない
+<p>
+次に Commutator 
+<p>
+
+<pre>
+    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 ] ))
+
+</pre>
+そして、Commutator がちゃんと全部入っていることを示す(やさしい
+<p>
+
+<pre>
+    CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i)
+
+</pre>
+すると
+<p>
+
+<pre>
+    CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
+
+</pre>
+という形で可解を定義できる。
+<p>
+
+<hr/>
+<h2><a name="content027">Proofs :        2</a></h2>
+以下のように極めて簡単になった(やった!
+<p>
+
+<pre>
+   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
+
+</pre>
+このまま 3, 4を証明可能
+<p>
+
+<hr/>
+<h2><a name="content028">Proofs :        5</a></h2>
+e 以外を含む stage 3 が stage 4 と同じことを示すだけで可解でないことを示せる
+<p>
+しかし5を計算すると停まらない(きっと停まるが遅すぎる
+<p>
+メモリは食わない (FList 5 自体は計算できて、それで抑えられる)
+<p>
+単に計算が遅い
+<p>
+
+<hr/>
+<h2><a name="content029">時間</a></h2>
+
+<pre>
+    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
+
+</pre>
+
+<hr/>
+<h2><a name="content030">しかし、Agda には compiler が!</a></h2>
+
+<p>
+コンパイルすれば計算可能
+<p>
+
+<pre>
+    ./sym5n  0.00s user 0.01s system 37% cpu 0.044 total
+
+</pre>
+ただし、それは証明には接続できない
+<p>
+型検査時に compile して計算する機能はない
+<p>
+
+<hr/>
+<h2><a name="content031">Analysis :        overhead of proof carrying data structure</a></h2>
+Fin, Commutator, FL, Fresh , Any, FList は、すべて証明付きデータ構造
+<p>
+証明は実行時ではなく型検査時に行われるので実行時のオーバヘッドは理論的にはない
+<p>
+Any や fresh は実行されない型しか計算しないコードになる
+<p>
+しかし、Fresh は Product を含んでいるので実際に heapを食うのでオーバーヘッドがあるように見える
+<p>
+ところが、それは使われないので実行時には明示的に触らない限り生成されない(遅延評価
+<p>
+なので、普通に高速に計算される
+<p>
+
+<hr/>
+<h2><a name="content032">Analysis        connection of computation and type</a></h2>
+普通は何を計算したのかは計算機は知らない
+<p>
+まして作った人以外はさっぱりわからない
+<p>
+しかし、証明付きデータならば、そこに何を計算したのかが書いてある
+<p>
+ただ
+<p>
+　　プログラミングは、めっちゃ面倒
+<p>
+でも、それができるならプログラミングの信頼性は上がる
+<p>
+しかし、それでも完全に正しいとは...
+<p>
+
+<hr/>
+<h2><a name="content033">Appendix : ZF fix</a></h2>
+証明があっても正しいとは限らない
+<p>
+去年のZFには間違いがあって
+<p>
+
+<pre>
+    record OD : Set (suc n ) where
+      field
+        def : (x : Ordinal  ) → Set n
+
+</pre>
+OD ⇔ Ordinal を要求すると矛盾になる
+<p>
+
+<pre>
+    ¬OD-order : ( &amp; : OD  → Ordinal ) → ( * : Ordinal  → OD ) → ( { x y : OD  }  → def y ( &amp; x ) → &amp; x o&lt; &amp; y) → ⊥
+    ¬OD-order &amp; * c&lt;→o&lt; = osuc-&lt; &lt;-osuc (c&lt;→o&lt; {Ords} OneObj )
+
+</pre>
+なので最大値を付けてやると良い
+<p>
+
+<pre>
+    record HOD : Set (suc n) where
+      field
+        od : OD
+        odmax : Ordinal
+        &lt;odmax : {y : Ordinal} → def od y → y o&lt; odmax
+
+</pre>
+つまり証明が合ってても仮定が間違ってたらダメ
+<p>
+これは (集合論の用語での) Set と Class の区別になっている。つまり OD が Class で、最大値があれば集合になる。
+<p>
+
+<hr/>
+<h2><a name="content034">Appendix : Topology</a></h2>
+今年は
+<p>
+
+<pre>
+    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)
+
+</pre>
+やっても良いかも。 Tychonovの定理の証明とか(やさしくなさそう
+<p>
+あるいは ZF の cohen model とか
+<p>
+
+<pre>
+    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)
+
+</pre>
+Topology と Filter は似てることがわかる
+<p>
+
+<hr/>
+<h2><a name="content035">Permutation :        等号</a></h2>
+
+<pre>
+    record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
+        field
+           peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
+
+</pre>
+を統合して使う   
+<p>
+
+<pre>
+    x  ≡ y → x =p y
+
+</pre>
+は言えるが
+<p>
+
+<pre>
+    x =p y → x  ≡ y
+
+</pre>
+は仮定するしかない。(Functional Extentionality)
+<p>
+
+<hr/>
+<h2><a name="content036">Permutation :        Data.Fin と Data.Nat</a></h2>
+suc と zero が自然数と重なっていて扱いを気をつける必要がある
+<p>
+
+<pre>
+   data ℕ : Set where
+     zero : ℕ
+     suc  : ℕ  → ℕ
+
+</pre>
+x ∧ x &lt; n で不等号を持ち歩く方法でも良いのだが...
+<p>
+x &lt; n も 
+<p>
+
+<pre>
+    data _≤_ : Rel ℕ 0ℓ where
+      z≤n : ∀ {n}                 → zero  ≤ n
+      s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
+
+</pre>
+と再帰的データ構造なので二重に持ち歩くことになるので美しくない
+<p>
+
+<hr/>
+<h2><a name="content037">Permutation :        FL と Permutation の対応の証明</a></h2>
+Permutation の combinator 表現を使う
+<p>
+
+<pre>
+    pprep  先頭に一つ置換を増やす
+    pswap  先頭の二つを入れ替える
+
+</pre>
+これだけで任意の置換を構成できる
+<p>
+これから pins という任意の置換に任意の位置に 0(の位置の要素) を入れる関数を作る
+<p>
+そして、pins の逆を
+<p>
+
+<pre>
+    pshrink 置換を一つ減らす
+
+</pre>
+を作って構成する
+<p>
+極めて煩雑な証明になる
+<p>
+
+<hr/>
+<h2><a name="content038">Fresh List : witness</a></h2>
+⌊ _f&lt;?_ ⌋ は witness と呼ばれるもので、 
+<p>
+
+<pre>
+    data Dec : {R : FL → FL → Set} : Set where
+        yes :   R → Dec R
+        no  : ¬ R → Dec R
+    x f&lt;? y with FLcmp x y
+    ... | tri&lt; a ¬b ¬c = yes a
+    ... | tri≈ ¬a refl ¬c = no ( ¬a )
+    ... | tri&gt; ¬a ¬b c = no ( ¬a )
+
+</pre>
+
+<hr/>
+<h2><a name="content039">sym5</a></h2>
+
+<p>
+abc が反例。これが常に残ることを示す
+<p>
+
+<pre>
+     counter-example :  ¬ (abc 0&lt;3 0&lt;4  =p= pid )
+     counter-example eq with ←pleq _ _ eq
+     ...  | ()
+
+</pre>
+二つ余地を確保する
+<p>
+
+<pre>
+     ins2 : {i j : ℕ }  → Permutation 3 3  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     ins2 abc i&lt;3 j&lt;4 = (save2 i&lt;3 j&lt;4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i&lt;3 j&lt;4 ) 
+
+</pre>
+abc と dba を作る
+<p>
+
+<pre>
+     abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     abc i&lt;3 j&lt;4 = ins2 3rot i&lt;3 j&lt;4
+     dba : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
+     dba i&lt;3 j&lt;4 = ins2 (3rot ∘ₚ 3rot) i&lt;3 j&lt;4
+
+</pre>
+abc が derive されることを示す
+<p>
+
+<pre>
+     dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ }  → (i&lt;3 : i ≤ 3 ) → (j&lt;4 : j ≤ 4 )
+          → deriving n (abc i&lt;3 j&lt;4 ) 
+     dervie-any-3rot0 0 i&lt;3 j&lt;4 = lift tt 
+     dervie-any-3rot0 (suc i) i&lt;3 j&lt;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
+
+</pre>
+df と dg が前に derive されたもの
+<p>
+
+<pre>
+        df =  dervie-any-3rot1 i  (fin≤n {3} (dba0&lt;3 tc)) (fin≤n {4} (dba1&lt;4 tc))
+        dg =  dervie-any-3rot1 i  (fin≤n {3} (aec0&lt;3 tc)) (fin≤n {4} (aec1&lt;4 tc)) 
+
+</pre>
+それは、再帰的に作れるのだが種(dbaとaec)を二つ計算する必要がある
+<p>
+それは右回転と左回転があって、 dervie-any-3rot0 と dervie-any-3rot1 で交互に作られる
+<p>
+そのつくり方だが...
+<p>
+
+<pre>
+        tc = triple i&lt;3 j&lt;4
+        dba0 = dba (fin≤n {3} (dba0&lt;3 tc)) (fin≤n {4} (dba1&lt;4 tc))
+        aec0 = dba (fin≤n {3} (aec0&lt;3 tc)) (fin≤n {4} (aec1&lt;4 tc))
+        ceq : abc i&lt;3 j&lt;4  =p=  [ dba0 , aec0 ]  
+        ceq = record { peq = peq (abc= tc) }
+
+</pre>
+dba と aec を作るのだが
+<p>
+
+<pre>
+     record Triple {i j : ℕ } (i&lt;3 : i ≤ 3) (j&lt;4 : j ≤ 4) (rot : Permutation 3 3) : Set where
+       field 
+         dba0&lt;3 : Fin 4
+         dba1&lt;4 : Fin 5
+         aec0&lt;3 : Fin 4
+         aec1&lt;4 : Fin 5
+         abc= : ins2 rot i&lt;3 j&lt;4 =p= [ ins2 (rot ∘ₚ rot)  (fin≤n {3} dba0&lt;3) (fin≤n {4} dba1&lt;4)  , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0&lt;3) (fin≤n {4} aec1&lt;4) ]
+     open Triple
+     triple : {i j : ℕ } → (i&lt;3 : i ≤ 3) (j&lt;4 : j ≤ 4) → Triple i&lt;3 j&lt;4 3rot
+     triple z≤n z≤n =                               record { dba0&lt;3 = # 0 ; dba1&lt;4 = # 4 ; aec0&lt;3 = # 2 ; aec1&lt;4 = # 0 ; abc= = pleq _ _ refl }
+     triple z≤n (s≤s z≤n) =                         record { dba0&lt;3 = # 0 ; dba1&lt;4 = # 4 ; aec0&lt;3 = # 2 ; aec1&lt;4 = # 0 ; abc= = pleq _ _ refl }
+       ....
+
+</pre>
+と自分でうまく2つの余地を選択する必要がある
+<p>
+もちろん、計算することは可能だが...
+<p>
+</div>
+<ol class="side" id="menu">
+AgdaによるGalois理論のプログラミング
+<li><a href="#content000">  motivation </a>
+<li><a href="#content001">  Galois theory :  多項式方程式</a>
+<li><a href="#content002">  Galois theory :  解と置換群(対称群)</a>
+<li><a href="#content003">  Galois theory :  可解群</a>
+<li><a href="#content004">  5次方程式が代数的に解けないことの証明</a>
+<li><a href="#content005">  数学の本の記述の特徴</a>
+<li><a href="#content006">  Agda でちゃんとやろうぜ</a>
+<li><a href="#content007">  Agda :            lambda</a>
+<li><a href="#content008">  Agda :            record</a>
+<li><a href="#content009">  Agda :            data</a>
+<li><a href="#content010">  Agda :            negation</a>
+<li><a href="#content011">  Agda :            unification</a>
+<li><a href="#content012">  Galois theory i nAgda :        Commutator</a>
+<li><a href="#content013">  Galois theory in Agda :        Solvable</a>
+<li><a href="#content014">  Galois theory in Agda :        Symmetric group </a>
+<li><a href="#content015">  Permutation :        Data.Fin</a>
+<li><a href="#content016">  Permutation :        List</a>
+<li><a href="#content017">  Proofs : 2</a>
+<li><a href="#content018">  Proofs : 3</a>
+<li><a href="#content019">  Proofs : 5</a>
+<li><a href="#content020">  もっと簡単にできるでしょ</a>
+<li><a href="#content021">  Fresh List</a>
+<li><a href="#content022">  Fresh List :        Any</a>
+<li><a href="#content023">  Fresh List :        Insert</a>
+<li><a href="#content024">  Fresh List :        Property on Insert / Cons </a>
+<li><a href="#content025">  Fresh List :        Any on Pair</a>
+<li><a href="#content026">  Fresh List :        Solved using Fresh List</a>
+<li><a href="#content027">  Proofs :        2</a>
+<li><a href="#content028">  Proofs :        5</a>
+<li><a href="#content029">  時間</a>
+<li><a href="#content030">  しかし、Agda には compiler が!</a>
+<li><a href="#content031">  Analysis :        overhead of proof carrying data structure</a>
+<li><a href="#content032">  Analysis        connection of computation and type</a>
+<li><a href="#content033">  Appendix : ZF fix</a>
+<li><a href="#content034">  Appendix : Topology</a>
+<li><a href="#content035">  Permutation :        等号</a>
+<li><a href="#content036">  Permutation :        Data.Fin と Data.Nat</a>
+<li><a href="#content037">  Permutation :        FL と Permutation の対応の証明</a>
+<li><a href="#content038">  Fresh List : witness</a>
+<li><a href="#content039">  sym5</a>
+</ol>
+
+<hr/> Shinji KONO <kono@ie.u-ryukyu.ac.jp> /  Fri Jan  8 15:30:18 2021
+</body></html>
--- a/presen.ind	Thu Jan 07 13:28:35 2021 +0900
+++ b/presen.ind	Sat Jan 09 09:43:12 2021 +0900
@@ -1,74 +1,688 @@
--title:    AgdaによるGalois理論のプログラミング 
+-title:    AgdaによるGalois理論のプログラミング
+
+--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次は可解。教科書だと
+
+<center><img src="fig/altin.jpg"></center>
+
+これは良い方で、岩波だと練習問題。
+
+<center><img src="fig/iwanami-gendai.jpg"></center>
+
+--数学の本の記述の特徴
+
+理解した後で読むとちゃんと書いてある
+
+理解する前には何が書いてあるのかわからない
+
+--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 : ⊤
 
---motivation
-        agda say prove all of it
-        proof carrying data structure
---all connected
-            not only the result
-            the result is proved to be correct
---What are you computing?
---Galois theory
---Galois theory :        polynominal equation
---Galois theory :        symmetric group on solutions
---Galois theory :        group mapping
---Galois theory :        commutator
---Galois theory :        commutator group
---Galois theory :        solvable
---proof in math text book
---formalization in agda
---Agda :            lambda
---Agda :            data
---Agda :            record
+要素が一つしかない型(真
+
 --Agda :            unification
-                equation
+
+    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
---Galois theory in Agda :            Set valued function
+
+    [_,_] :  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
---Permutation :        Bijection
+
+有限な数
+
+   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
---Permutation :        FL
+
+置換は 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
---Proofs : Injection
+
+これで道具立てはそろったので証明に行く
+
+まず、二次対称群から
+
+   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
 
---A list contains everything
-        sorted
-        any
+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
-        Set valued function
-        proof carrying data structure
+
+(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))。
+
+<center><img src="fig/fresh.svg"></center>
+
+    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
-            here
-            there
+
+  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 
 
-Any
+    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
---Proofs :        3
---Proofs :        5
-            two sym 3
---Proofs :        4
+
+以下のように極めて簡単になった(やった!
+
+   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
-            compilation
---Analysis
+
+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
-              type
-              heap
-                  product
-              type check
-              compiled
+
+Fin, Commutator, FL, Fresh , Any, FList は、すべて証明付きデータ構造
+
+証明は実行時ではなく型検査時に行われるので実行時のオーバヘッドは理論的にはない
+
+Any や fresh は実行されない型しか計算しないコードになる
+
+しかし、Fresh は Product を含んでいるので実際に heapを食うのでオーバーヘッドがあるように見える
+
+ところが、それは使われないので実行時には明示的に触らない限り生成されない(遅延評価
+
+なので、普通に高速に計算される
+
 --Analysis        connection of computation and type
 
+普通は何を計算したのかは計算機は知らない
+
+まして作った人以外はさっぱりわからない
+
+しかし、証明付きデータならば、そこに何を計算したのかが書いてある
+
+ただ
+
+　　プログラミングは、めっちゃ面倒
+
+でも、それができるならプログラミングの信頼性は上がる
+
+しかし、それでも完全に正しいとは...
+
 --Appendix : ZF fix
-            od max
-            Set and Class
+
+証明があっても正しいとは限らない
+
+去年の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
-    Tychonov
+
+今年は
+
+    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
 
---Appendix : ZF 
-   cohen model
+⌊ _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つの余地を選択する必要がある
+
+もちろん、計算することは可能だが...
+
Binary file sigjouto.pdf has changed