一発ネタかつフランツ・リストの超絶技巧練習曲のパロディです。
(** * 超絶技巧演習問題 - Coq *)
Require Import Coq.Init.Prelude Coq.Init.Nat.
Open Scope nat_scope.
Definition felmat
: forall n : nat, 2 < n -> ~ exists x y z, 0 < x /\ 0 < y /\ 0 < z /\ x ^ n + y ^ n = z ^ n.
Proof.
(* [Admitted] を [Qed] に取り換えて、この空欄を埋めよ *)
Admitted.
Definition catalanic a b x y := 1 < a /\ 1 < b /\ 1 < x /\ 1 < y /\ x ^ a = 1 + y ^ b.
Definition catalan
: forall a b x y, catalanic a b x y -> x = 3 /\ a = 2 /\ y = 2 /\ b = 3.
Proof.
(* [Admitted] を [Qed] に取り換えて、この空欄を埋めよ *)
Admitted.
Definition baudetic (P : nat -> bool) a b c n := forall p, p < n -> P (a + b * p) = c.
Definition baudet
: forall P, exists c, forall n, exists a b, baudetic P a b c n.
Proof.
(* [Admitted] を [Qed] に取り換えて、この空欄を埋めよ *)
Admitted.
Definition collatzic n := if even n then div2 n else n * 3 + 1.
Definition collatz
: forall n, n <> 0 -> exists p, iter p collatzic n = 1.
Proof.
(* [Admitted] を [Qed] に取り換えて、この空欄を埋めよ *)
Admitted.
解説
-
felmat,catalan- フェルマーの最終定理、カタラン予想と呼ばれる問題です。どちらもディオファントス方程式の形になっていて、こういう問題は簡単に書けるくせに難問だったりします。Coq でもCoq.Init.Preludeに足し算などがそろっているので簡単に記述することが出来ますが、冪はデフォルトで利用できずCoq.Init.Natをインポートしないといけないのでちょっと嵌りました。どちらも肯定的に解決していますが、その証明は非常に高度です。 -
baudet- 「自然数全体の集合を二つの集合に分けたとき、少なくとも一つの集合は任意の長さの等差数列を含む」。ちょっとマイナーですが、この予想に関する歴史はとても面白いです。詳細は参考文献を見てください。未解決です。 -
collatz- 「それが偶数だったら二で割り、それが基数だったら三を掛けて一を足す」という操作を考えます。このとき、ゼロではない全ての自然数に対して、その操作を繰り返していったとき、いつかは必ず一になるという問題です。計算してみると成り立ちそうなのですが、たまにたくさん繰り返さないと一にならない数があったりして言い切れません。未解決です。