Agda の option

なんか、library が --without-k ってのを使ってるのは知ってたんですが、なんか最近、without-k 使ってないと文句言われたことがあって。

群論(S₅がS₃を含む)ってのも見直してたんですが、

　 [ dba , aec ] = (abd)(cea)(dba)(aec) = abc

が Altin に書いてあるやつなんだけど、作ってるのは abc だけど、元は dba とかで違うものじゃん。adb = dba⁻¹ だから、半分はわかる。

で、プロシンで発表した時は「全部の存在を示す」みたいな感じでやってたんですが、群でやれば良いんじゃないか? と思ったんですが、

　　交換子自体は積に閉じてない、なので、有限生成して群にする
　　なので、S₃から要素を取り出しても、交換子とは限らない

あだだ。でも、q が交換子なら、共役元 p ∙ q ∙ p⁻¹ は交換子になるってのを交換子群が正規部分群なことを示すのに使ってた。なので、
dba とか、abc の共役元で良いじゃん。で、次の一行で良いらしい。

　　 abc ≡ [ (dc)(abc ⁻¹　)(dc ⁻¹　)　, (eb)(abc) (eb ⁻¹　) ]

これで、abc の逆元と共役元から abc が作れるので、これが可解群 (いつか交換子群列は{ε}になる)の反例になる。簡単!

なんですが、

　　　チェックが全然終わらない。しかも、全部つながってるのだが、つなげると時間がかかる

　　% time agda　sym5h.agda
　　Checking sym5h (/home/teacher/kono/src/galois/src/sym5h.agda).
　　agda: Heap exhausted;
　　agda: Current maximum heap size is 3758096384 bytes (3584 MB).
　　agda sym5h.agda　1429.15s user 19.74s system 99% cpu 24:09.22 total

なので、もしかして、--without-k 使うと良いかと思って。なんだが、最近は、

　　{-# OPTIONS --cubical-compatible --safe #-}

と書くらしい。なんか、1 < x とかを展開するところで文句言われるので、かなりなおさないとだめらしい。で、

　　Dec p の展開で yes / no でも文句をいう

なので、何回いろいろ問題があるっぽい。たぶん、version 不整合とかかなぁ。