Egisonでも出来たので報告します。
関数fifteenで、1..9のうち、和が15になる三数を選びます。
関数fifTripleで、fifteenから、任意の三要素（{{1 5 9} {1 6 8} {2 4 9}}とか）の組み合わせを得ます。
関数makeMagicで、fifTripleのから、縦と斜めの和が15になるものをパターンマッチします。
数字が重複するものもはじきます。
実行に15分ぐらいかかります。
メモリも3GBぐらい食います。
Haskellと同様に、解は8個出力されます。
3つconsするmatcherを作って、書き直しました。
実行時間8分、消費メモリ250MBまで削減できました。
これは、matcherの効果というよりも、fifteenをunique/mで絞ったのが大きいです。
.
.
YouTubeで3*3魔方陣は1種類しか存在しないことをやっていた。
これをプログラムでやったらどうなるだろう。
最初はEgisonでやっていたけれど、計算が終わらないのでやめた。
ソースだけ貼っておきます。
Haskellでやることにする。
リスト[1..9]に対して順列を出力する関数permutationsをかまして、
後は縦・横・斜めの和が15になるものをフィルタリングすれば良いだろう。
（一列の和が15というのは分かっているものとします）
*MagicSquare> answer1 [[2,9,4,7,5,3,6,1,8],[2,7,6,9,5,1,4,3,8],[8,3,4,1,5,9,6,7,2],[8,1,6,3,5,7,4,9,2],[4,9,2,3,5,7,8,1,6],[4,3,8,9,5,1,2,7,6],[6,7,2,1,5,9,8,3,4],[6,1,8,7,5,3,2,9,4]]
8個出力された。
魔方陣の回転と鏡映を同一視する。
これは二面体群D4になるのかな？ 位数が8なので計算結果とも一致している。
9要素タプルをnewtypeする。
回転と鏡映を考慮した、Eqクラスのインスタンスにする。
そして、先頭要素D4 (2, 9, 4, 7, 5, 3, 6, 1, 8)と残りを比較する。
*MagicSquare> answer2 [True,True,True,True,True,True,True]
これで、3*3魔方陣は1種類しか存在しないことが証明できた。
.
.
Idrisでもやってみたいが、どうやるのだろう。
ラムゼーの時もそうだったけれど、
組み合わせ系は、定理証明支援系は苦手なのかもしれない。
IdrisでもHaskellと同じように「計算」すればいいかな、とも思ったけど、
それでは意味がないな、と考える。
.
.
Twitterで「各桁の和が3の倍数な整数は3の倍数、定理証明の練習に良さそう」
というのがあったので、チャレンジしてみる。
sumDigitは各桁の和を求める関数だが、
ここで一つズルをする。
直接、各桁の和を求めるのではなく、再帰した時の関係性を書くのだ。
| n | sumDigit n | sumDigit (n-3)を引く |
|---|---|---|
| 9 | 9 | 3 |
| 10 | 1 | -6 |
| 19 | 10 | 3 |
| 20 | 2 | -6 |
| 99 | 18 | 3 |
| 100 | 1 | -6-9 |
普段は3だが、繰り上がりのところで-6になる。
そして100で-9追加、1000で-9-9追加になる。
これは、繰り上がりがある所では、
sumDigit (S (S (S n))) = -3a + sumDigit n
と置けそうだ。
こうすることによって、3の倍数か調べる時に、aを落とせる訳だ。
（190223追記）
Leanで関数内のif文は、
by_casestacticと、
rw if_posで突破できた。
.
.
Idris版もやってみる。
……まぁ すぐに詰んでやろう
Idrisのif文はwith (式) proof pで突破できるし、
簡約もバッチリだ。
.
.
rev_rev_idとは、リストを2回逆順にすると元に戻る、というやつだ。
Leanで挑戦してみた。
バイナリがあるから、それを持ってくるだけ。
本格的にやりたい方は
https://righ1113.hatenablog.com/entry/2020/06/06/101151
をどうぞ。
#checkで型の確認ができる。#reduceで値の評価ができる。まだやっていない。
calcでおこなうみたい。
Reasoningの中でrewrite（rw）できるのは大きいかも。
例によってsnocを使う方法でやってみた。
みょんみょんさんの実装を参考にした。
.
.
無限長のリストであるStreamは、
Idrisではlibs/prelude/Prelude/Stream.idrで以下のように定義されている。
||| An infinite stream data Stream : Type -> Type where (::) : (value : elem) -> Inf (Stream elem) -> Stream elem
これは以下と同等だそうだ。
codata Stream : Type -> Type where (::) : (value : elem) -> Stream elem -> Stream elem
codataである。余帰納である。
ところで以下のコードを見て欲しい。
無条件に（xs -> Q xsの間の条件無しに）Q xsが言えている。
すごくね？
これが余帰納の力か……
（何に使えるのか分からないけど）
.
.
.
foldrで挿入ソートを実装できることを知った。
insert : Nat -> List Nat -> List Nat insert x [] = [x] insert x (y::ys) = if lte x y then x :: y :: ys else y :: insert x ys -- 挿入ソート isort : List Nat -> List Nat isort = foldr insert [] *Isort> isort [9, 3, 7, 1, 4, 1] [1, 1, 3, 4, 7, 9] : List Nat
.
.
よし、この挿入ソートの正当性を証明しよう。
ソートの正当性を言う為には、ソートされている事の他に、
要素が変わっていない事（元リストのPermutationであること）
も言わないといけないですが、スキップします。
.
.
sorted (foldr insert [] zs) = True
foldrに関数をかぶせているので、何か定理がないかな～と探したら、
『foldrのfusion則』
というのがあるらしい。
.
.
これは、
f undefined = undefined（今回は手で確認する） f a = b ∀x,y f (g x y) = h x (f y)
の3条件の元で、
f . foldr g a = foldr h b
が成立するというもの。
参考記事：
.
.
『foldrのfusion則』を使ってsortedを証明したものがこちら。
Idrisのテクとして、if (expr) then a else bを証明したい時、
with (expr) proof pで場合分けすると、
exprにTrueとFalseを設定することができる。
（今回はdecideLTEを使っても良かったけど）
それと、fusion則を一般化した形で書きたかったけどな～
.
.
