はどんなに頑張ってもだめだったので、 を試してみた。 すなわち match t1, t2, t3, t4, t5, t6, t7 with | Leaf, Leaf, Leaf, Leaf, Leaf, Leaf, Node s1 s2 => f_2 s1 s2 | s1, s2, s3, s4, s5, s6, s7 => Node s1 (Node s2 (Node s3 (Node s4 (Node s5 (N…

とにかく、デフォルトの場合にまとめられるところをまとめるという考えでいくと match t1, t2, t3, t4, t5, t6, t7 with | 特殊な場合 => | s1, s2, s3, s4, s5, s6, s7 => Node s1 (Node s2 (Node s3 (Node s4 (Node s5 (Node s6 s7))))) endとするのがよい…

最初の場合わけ match t1, t2, t3, t4, t5, t6, t7 with | Leaf, Leaf, Leaf, Leaf, Leaf, Leaf, s1 => f_1 s1 (* T *) | Leaf, Leaf, Leaf, Leaf, Leaf, (Node s1 s2), s3 => f_3 s1 s2 s3 (* T^3 *) | Leaf, Leaf, Leaf, Leaf, (Node s1 s2), s3, s4 => f_…

http://d.hatena.ne.jp/m-hiyama/20081031

Inductive Tree : Set := | Leaf | Node : Tree -> Tree -> Tree. Inductive Tree7 : Set := | T7 : Tree -> Tree -> Tree -> Tree -> Tree -> Tree -> Tree -> Tree7. Definition f (ts : Tree7) : Tree := match ts with | T7 Leaf Leaf Leaf Leaf Leaf Le…

Require Import ZArith. Open Scope Z_scope. Goal forall t:Z, t = 1 + t^2 -> t^7 = t. intros. ring [H].終わらない…

５分岐になった！難しかった

昨日頑張って考えてみた結果。 元のコードはmatchで完全に直和に分解してたので分岐が多かっただけで、圧縮してみたら８ぐらいになった。 その後色々考えてみたんだけど５にはならない…今のところ６分岐。

http://d.hatena.ne.jp/KeisukeNakano/20081024/1224806200には５種類に分類すればいいと書いてあるので、考えてみたのだがさっぱり分からない。その代わり考えるヒントが生まれた。 2〜6の場合に存在しないことを証明するために考えてたので、この問題を解…

http://d.hatena.ne.jp/m-hiyama/20081022/1224640248 http://d.hatena.ne.jp/ku-ma-me/20081023最近はやりの Seven Trees を解いてみた。 机上の計算ではできたっぽいのだが、やはり自信がない。 まめっちはいい加減にテストをしていたみたいだが、やはり総…

k.inabaさんが張ってたクロスワードで遊んでたら、Hardなのにとんでもなく難しいのがでてきた。 ■ 1 ■ 2 3 4 5 ■ 4 6 Ｘ 7 6 3 3 ■ 8 ■ 1 ■ 9 ■ ■ 10 ■ 11 12 5 11 13 12 1 14 10 13 4 4 ■ 15 ■ 2 ■ 12 ■ 15 ■ 5 ■ 5 3 14 10 11 6 16 16 2 3 3 ■ 17 ■ 10 ■ 9…