More than 5 years have passed since last update.
一発ネタかつフランツ・リストの超絶技巧練習曲のパロディです。
(** * 超絶技巧演習問題 - Coq *)RequireImportCoq.Init.PreludeCoq.Init.Nat.OpenScopenat_scope.Definitionfelmat:foralln:nat,2<n->~existsxyz,0<x/\0<y/\0<z/\x^n+y^n=z^n.Proof.(* [Admitted] を [Qed] に取り換えて、この空欄を埋めよ *)Admitted.Definitioncatalanicabxy:=1<a/\1<b/\1<x/\1<y/\x^a=1+y^b.Definitioncatalan:forallabxy,catalanicabxy->x=3/\a=2/\y=2/\b=3.Proof.(* [Admitted] を [Qed] に取り換えて、この空欄を埋めよ *)Admitted.Definitionbaudetic(P:nat->bool)abcn:=forallp,p<n->P(a+b*p)=c.Definitionbaudet:forallP,existsc,foralln,existsab,baudeticPabcn.Proof.(* [Admitted] を [Qed] に取り換えて、この空欄を埋めよ *)Admitted.Definitioncollatzicn:=ifevennthendiv2nelsen*3+1.Definitioncollatz:foralln,n<>0->existsp,iterpcollatzicn=1.Proof.(* [Admitted] を [Qed] に取り換えて、この空欄を埋めよ *)Admitted.解説
-
felmat,catalan- フェルマーの最終定理、カタラン予想と呼ばれる問題です。どちらもディオファントス方程式の形になっていて、こういう問題は簡単に書けるくせに難問だったりします。Coq でもCoq.Init.Preludeに足し算などがそろっているので簡単に記述することが出来ますが、冪はデフォルトで利用できずCoq.Init.Natをインポートしないといけないのでちょっと嵌りました。どちらも肯定的に解決していますが、その証明は非常に高度です。 -
baudet- 「自然数全体の集合を二つの集合に分けたとき、少なくとも一つの集合は任意の長さの等差数列を含む」。ちょっとマイナーですが、この予想に関する歴史はとても面白いです。詳細は参考文献を見てください。未解決です。 -
collatz- 「それが偶数だったら二で割り、それが基数だったら三を掛けて一を足す」という操作を考えます。このとき、ゼロではない全ての自然数に対して、その操作を繰り返していったとき、いつかは必ず一になるという問題です。計算してみると成り立ちそうなのですが、たまにたくさん繰り返さないと一にならない数があったりして言い切れません。未解決です。
参考文献
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme