X
トップページ⇒数学
1002コメント517KB
コラッツ予想がとけたらいいな
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
垢版 |
2012/10/14(日) 10:32:39.71
525 名前：１３２人目の素数さん[sage] 投稿日：2012/09/03(月) 18:24:27.22
http://d.hatena.ne.jp/righ1113/
コラッツ予想について、証明を考えてみました。
ご指摘ご意見ご感想など、ぜひよろしくお願いします。
0353righ1113 ◆OPKWA8uhcY
垢版 |
2016/05/14(土) 14:13:06.71ID:IrWcxE2T
>>350
僕のほうは>>323でコラッツ予想の証明を完成しています。
他に、別の方が、>>352で、コラッツ予想がLoopしない証明を載せています。
0355１３２人目の素数さん
垢版 |
2016/05/14(土) 18:02:52.16ID:kAt1eCb5
例えば、>>323の証明をCoqで検証するとかいうのはやってみる気ない？
素人の俺には証明に穴がないか検証するのは難しいが、
Coqで証明が検証されたとなれば信頼度がだいぶ変わってくる。

Coq
https://ja.wikipedia.org/wiki/Coq
0356righ1113 ◆OPKWA8uhcY
垢版 |
2016/05/15(日) 14:07:43.39ID:HMT90KXl
すごいことになってる。
しばらく考えさせて下さい。
0358righ1113 ◆OPKWA8uhcY
垢版 |
2016/05/16(月) 18:06:23.91ID:+2bpW1Z1
いえ、Coqで検証なんて、
思い付きもしなかったもんで。
0359１３２人目の素数さん
垢版 |
2016/05/16(月) 18:52:31.06ID:dTU5tRHR
Coqはめちゃくちゃ難しいぞ
まあ数板にスレがあるから行ってみれ
寂れてるけど
0373righ1113 ◆OPKWA8uhcY
垢版 |
2016/05/22(日) 16:19:17.83ID:As5SZbzk
手始めにコラッツ数列を計算する関数。

Require Import Coq.Program.Wf.
Require Import Omega.

Program Fixpoint collatz03 (x y : nat) {measure y} : list nat :=
match y with
| 0 => 0::nil
| _ => match x with
| 0 => 0::nil
| 1 => 1::nil
| _ => if Nat.odd x then (3*x+1) :: collatz03 (3*x+1) (y-1)
else (x/2) :: collatz03 (x/2) (y-1)
end
end.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.

ここまでで3日かかりました。www
0374righ1113 ◆OPKWA8uhcY
垢版 |
2016/05/22(日) 16:22:31.37ID:As5SZbzk
クエリで
Eval compute in collatz03 9 20
→
Result for command Eval compute in collatz03 9 20 . :
= (28
:: 14
:: 7
:: 22
:: 11
:: 34
:: 17
:: 52
:: 26
:: 13
:: 40
::
20
::
10
::
5
::
16
::
8
::
4
::
2 :: 1 :: 1 :: nil)%list
: list nat
0375１３２人目の素数さん
垢版 |
2016/05/22(日) 16:49:26.93ID:mkl5wCNj
頑張れ〜
もしCoqで証明が成功したらマジですごい。

Coqスレの1である片山博文MZも仲間に引き入れられれば
色々教えてもらえるかもね。
0376１３２人目の素数さん
垢版 |
2016/05/24(火) 02:04:08.25ID:xIwNaKmu
>>360
ところどころ何が言いたいかよくわからんが、とりあえず明確な間違いが一つ。

mod p^2 で
1 + p = n(l + kp)
より
nl = 1(mod p), nk = 1(mod p)

というところ。
nl = 1(mod p) は言えるが nk = 1(mod p) とは限らない。
例えば nl = p+1 の場合とか。
0377１３２人目の素数さん
垢版 |
2016/05/24(火) 10:35:07.76ID:WulNrhxx
流れぶったぎってすまんが
・ある自然数が100以下の素因数を持っていれば全て削る
・持ってなければ3n+1の操作を施す
みたいな問題から考えてくアプローチを思いついたんだけどこれって既出？
0378￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 10:50:07.49ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0380tai
垢版 |
2016/05/24(火) 21:39:24.40ID:374dBI4a
>>376

ありがとう

気づかなかった

間違いですね
0381￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 22:31:29.99ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0382１３２人目の素数さん
垢版 |
2016/05/24(火) 22:58:34.15ID:+Z6NkEEQ
>>379
や、まだ全然。多分簡単な問題から始めたら解決の糸口見つかるかなーと思ったけど
コラッツ問題の闇の深さを垣間見ることになっただけだった…
もし興味ある人いたら考えてみてくれ
0383￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 22:59:49.43ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0384￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:00:06.58ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0385￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:00:23.53ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0386￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:00:41.20ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0387￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:00:58.88ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0388￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:01:17.09ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0389￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:02:01.29ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0390￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:02:18.83ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0393tai
垢版 |
2016/05/24(火) 23:38:41.03ID:374dBI4a
一応直しておきました

まだ途中ですので

まちがっているかもしれません
0394￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:54:36.02ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0395￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:54:53.79ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0396￥ ◆2VB8wsVUoo
垢版 |
2016/05/24(火) 23:55:08.89ID:98ujCcPg
￥

>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0397righ1113 ◆OPKWA8uhcY
垢版 |
2016/05/25(水) 20:06:38.89ID:EB6pp118
まだCoq練習フェーズです。
Theorem m11_isnot_prime01:
forall (P Q R :Prop), (P->Q) -> (Q->R) -> (~R->~Q).
(* proof. *)
intros.
cbv.
intro.
cbv in H1.
apply H0 in H2.
apply H1 in H2.
apply H2.
Qed.
Theorem m11_isnot_prime01':
forall (P Q R :Prop), (P->Q) -> (Q->R) -> (~R->~Q).
(* proof. *)
intro.
intro.
intro.
intro.
auto.
Qed.

Theorem m11_isnot_prime02:
forall (Q R :Prop), (Q->R) -> (~R->~Q).
(* proof. *)
auto.
Qed.

Theorem m11_isnot_prime03:
forall (P Q R :Prop), (P=Q) -> (P->R) -> (Q->R).
(* proof. *)
intros.
rewrite H in H0.
apply H0 in H1.
apply H1.
Qed.
0398righ1113 ◆OPKWA8uhcY
垢版 |
2016/05/31(火) 13:18:55.66ID:MldWQZrV
やったーカリーのパラドックスが解けたよー

Lemma l1:
forall (X Y Z:Prop), (X->X->Y) -> X=(X->Y) -> X.
Proof.
intros.
rewrite H0.
intro.
apply H in H1.
apply H1.
apply H1.
Qed.

Theorem curry's_paradox:
forall (X Y:Prop), X=(X->Y) -> Y.
Proof.
intros.
assert(X->X).
auto.

pattern X at 2 in H0.
rewrite H in H0.
apply (l1 X Y) in H0.
pose H0.
rewrite H in x.
apply x in H0.
apply H0.
apply X.
apply H.
Qed.
0399righ1113 ◆OPKWA8uhcY
垢版 |
2016/05/31(火) 13:46:31.08ID:MldWQZrV
Zいらないっすね。

Lemma l1:
forall (X Y:Prop), (X->X->Y) -> X=(X->Y) -> X.
Proof.
intros.
rewrite H0.
intro.
apply H in H1.
apply H1.
apply H1.
Qed.

Theorem curry's_paradox:
forall (X Y:Prop), X=(X->Y) -> Y.
Proof.
intros.
assert(X->X).
auto.

pattern X at 2 in H0.
rewrite H in H0.
apply (l1 X Y) in H0.
pose H0.
rewrite H in x.
apply x in H0.
apply H0.
apply H.
Qed.
0400１３２人目の素数さん
垢版 |
2016/05/31(火) 16:43:04.58ID:Q9drQ/Ad
なかなか頑張ってますな。
正直すぐ投げ出すんじゃないかと侮っていたよ。
0401righ1113 ◆OPKWA8uhcY
垢版 |
2016/05/31(火) 23:37:09.87ID:5ZwDxW8h
証明で詰まると苦しいけど、
Coqで証明できると楽しいです。
0402righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/04(土) 21:52:45.29ID:1pZXMfoL
のんびりと、Coqでのコラッツ予想検証に取り掛かりたいと思います。
>>323の僕の証明の流れは、次のようになっています。

1.イントロダクション
2.コラッツパターンXsの定義
3.左端を伸ばすパターンYsの定義
4-1.コラッツパターンと左端を伸ばすパターンのずれを定義する
4-2.シミュレーションA−xsAを定義する
4-3.シミュレーションB−ysBを定義する
4-4.[log Xs] - [log Ys] <= [log(xsA * 2^pxs)] - [log(ysB * 2^pys)]
　　　　　を証明する　（この式の右辺が有限値なら、コラッツパターンと左端を伸ばすパターンのずれも有限値となる。）
5.ずれが有限という仮定で、コラッツ予想で4-2-1以外のLoopがない事を証明する
6.ずれが有限という仮定で、コラッツ予想で無限大に発散する数がない事を証明する
7.　4-4の右辺が有限値であることを、Haskellで証明する

「繰り上がりがあったりなかったりするから」とか、図から補題を証明していたりするので、
全てをCoqで検証・証明するのは難しいと考えています。

まずは4-4からやっていこうと思います。
0403righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/04(土) 22:01:11.07ID:1pZXMfoL
4-4その１
前提として、コラッツパターンXsよりシミュレーションAが大きい、というのがあります。
理由は、コラッツパターンの下位からの繰り上がりがあったりなかったりするのに対して、
シミュレーションAは、常に下位からの繰り上がりがあるからです。
なので、pxs=log Xs - bit + aが成り立つのですが、前述の理由によりa>=0です。
（これは>>323には書いてないです。Coqで証明するために変えました。）

という訳でCoqでの証明です。
Require Import Omega.

Theorem Xs_ge_xsA:
forall (Xs a bit pxs xsA: nat), 0<xsA -> 0<=pxs
-> Nat.log2 Xs +1 <= Nat.log2 Xs +1 +a
-> pxs = Nat.log2 Xs +1 -bit +a
-> bit = Nat.log2 xsA +1
-> Nat.log2 Xs +1 <= Nat.log2 (xsA*(2^pxs)) +1.
Proof.
intros.
rewrite (Nat.log2_mul_pow2 xsA pxs).

all: cycle 1.
apply H.
apply H0.

rewrite H2.
rewrite H3.
omega.
Qed.

これで、コラッツパターンよりシミュレーションAが大きいという事実のもとで、
[log Xs] <= [log xsA*(2^pxs)]が示せました。
0404righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/04(土) 22:03:58.52ID:1pZXMfoL
4-4その２
前提として、シミュレーションBより左端を伸ばすパターンが大きい、というのがあります。
理由は、左端を伸ばすパターンの下位からの繰り上がりがあったりなかったりするのに対して、
シミュレーションBは、常に下位からの繰り上がりがないからです。
なので、pys=log Ys - bit - aが成り立つのですが、前述の理由によりa>=0です。
（これは>>323には書いてないです。Coqで証明するために変えました。）

という訳でCoqでの証明です。こちらはZ_scopeで証明しています。
Require Import Omega.

Open Scope Z_scope.
Theorem ysB_ge_Ys:
forall (Ys a bit pys ysB:Z), 0<ysB -> 0<=pys
-> Z.log2 Ys +1 -a <= Z.log2 Ys +1
-> pys = Z.log2 Ys +1 -bit -a
-> bit = Z.log2 ysB +1
-> Z.log2 (ysB*(2^pys)) +1 <= Z.log2 Ys +1.
Proof.
intros.
rewrite (Z.log2_mul_pow2 ysB pys).

all: cycle 1.
apply H.
apply H0.

rewrite H2.
rewrite H3.
omega.
Qed.
Open Scope nat_scope.

これで、シミュレーションBより左端を伸ばすパターンが大きいという事実のもとで、
[log ysB*(2^pys)] <= [log Ys]が示せました。
Ys<=Xsは自明なので、
よって[log Xs] - [log Ys] <= [log(xsA * 2^pxs)] - [log(ysB * 2^pys)]となります。
4-4は以上になります。
0405righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/05(日) 18:56:49.96ID:yXCfmuqW
次に7.をやろうと思います。>>232-241あたりです。
ビット数はbit=10です。
xsAの0ステップ目を1111111111、ysBの0ステップ目を0000000001として
（ずれが0で一番差が開いている数）ステップを重ねると、
xsAは115ステップ目が3ステップ目と一致して以後繰り返しになります。
xsBは93ステップ目が3ステップ目と一致して以後繰り返しになります。
その区間の最上位繰り上がりの可否を、大きい繰り返しになるまで調べます。
Haskellでやった時は、ずれの最大値は2でした。
Coqはこれからやります。
0406righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/07(火) 16:41:02.76ID:MtRwR70U
微妙にステップ数が違ってました。

xsAの0ステップ目を1111111111、ysBの0ステップ目を0000000001として　
（ずれが0で一番差が開いている数）ステップを重ねると、　
xsAは113ステップ目が2ステップ目と一致して以後繰り返しになります。　
xsBは91ステップ目が2ステップ目と一致して以後繰り返しになります。　
colPattAの第二要素でHaskellとCoqでdiffを取ったので大丈夫だと思います。
0407righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/07(火) 16:45:19.93ID:MtRwR70U
Coqですが、関数定義は省略します。Haskellのとそんなに変わらないです。

Theorem colPattA_2_eq_113:
last (iterate 2 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0))
= last (iterate 113 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0)).
Proof.
compute.
reflexivity.
Qed.

Theorem colPattB_2_eq_91:
last (iterate 2 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0))
= last (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)).
Proof.
compute.
reflexivity.
Qed.
これで小さい繰り返しはクリアできました。
0408righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/07(火) 20:12:15.58ID:MtRwR70U
なんかうまくいきません。
ずれが際限なく増えていきます。
0411righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/07(火) 22:06:33.54ID:MtRwR70U
なんとかできました。
colPattAは繰り返しの項数が111、colPattBは繰り返しの項数が89です。
colPattA*89=9879項、colPattB*111=9879項にして大きい繰り返しにします。
倍の19758項も用意しておきます。
これを初期ずれx=1、x+colPattA-colPattB < 定数　かを9879項、19758項調べるのですが、
途中colPattBが勝ってxが負になる可能性があるので、初期ずれx=2とします。

Definition colPattA2nd_1 : list nat :=
cycle 89 nil
(tail (tail (tail (map snd (iterate 113 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0)))))).
Definition colPattA2nd_2 : list nat :=
cycle (89*2) nil
(tail (tail (tail (map snd (iterate 113 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0)))))).

Definition colPattB2nd_1 : list nat :=
cycle 111 nil
(tail (tail (tail (map snd (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)))))).
Definition colPattB2nd_2 : list nat :=
cycle (111*2) nil
(tail (tail (tail (map snd (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)))))).
0413１３２人目の素数さん
垢版 |
2016/06/07(火) 23:18:10.94ID:KJBV85MD
逆に証明を突き詰めていったら反例がみつかったなんてこともあるかもね。
それならそれで面白いが。
0414righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/08(水) 00:37:23.48ID:JADn1FP5
>>232-241の通り、手計算ではうまくいくんです。
それをCoqに落とし込むのに手間取っています。
0415righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/08(水) 02:03:36.44ID:JADn1FP5
>>411は無しでお願いします。
>>237-238を見て、colPattA*5=555項、colPattB*6=534項にして大きい繰り返しにします。
この区間のずれの最大値が2、末項が1になったので、大きい繰り返しを何度繰り返しても、ずれは2以下です。

Definition colPattA2nd : list nat :=
cycle 5 nil
(tail (tail (tail (map snd (iterate 113 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0)))))).

Definition colPattB2nd_1 : list nat :=
cycle 1 nil
(tail (tail (tail (map snd (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)))))).
Definition colPattB2nd_2 : list nat :=
cycle 6 nil
(tail (tail (tail (map snd (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)))))).

Theorem p_misalignment_first:
misalignment_max_last 1 1 colPattA2nd colPattB2nd_1 = (2, 1).
Proof.
compute.
reflexivity.
Qed.
Theorem p_misalignment_second:
misalignment_max_last 1 1 colPattA2nd colPattB2nd_2 = (2, 1).
Proof.
compute.
reflexivity.
Qed.
7.もできました。
0416righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/08(水) 09:39:08.70ID:JADn1FP5
やっぱりうまくいってないみたいです。
>>237-238の手計算も間違っていました。
ビット数を増やすという切り札があるので、それをやってみます。

Coqはウソつかないんですねー
0417413
垢版 |
2016/06/08(水) 21:39:10.48ID:lYAR2M8u
俺は>>1が>>1証明のほころびからコラッツ予想の反例を見つけるというストーリーを期待しているｗ
0418１３２人目の素数さん
垢版 |
2016/06/08(水) 22:23:08.13ID:WkHIclqp
ブールピタゴラス問題も真っ青の反例ループのサイズが200TB超えとかを希望w
0419righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/08(水) 23:36:44.69ID:aPj7A/ik
ビット数を増やしても、ずれが際限なく増えていく〜〜
0420１３２人目の素数さん
垢版 |
2016/06/09(木) 02:17:55.30ID:Z2BPqjfW
ずれの計算では上手く行くわけがないって、ずっと前に指摘されてたじゃん。
何をいまさら。こんなやり方でコラッツの予想が解けるわけがない。
0421１３２人目の素数さん
垢版 |
2016/06/09(木) 19:53:16.16ID:OutW5kLL
仮にずれの計算でうまくいかなかったとしても>>1は修正してくるだろう。
Coqがあれば間違った証明は通らないだろうしいくらでも頑張れる環境がある。
コラッツの予想が解けるのは時間の問題だな。
0422righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/10(金) 05:50:42.64ID:oOXw5TlH
まだ思いつきのレベルなんであれですが……
5bitで考えて、さらに命題を一つ考えます。
（★）「下位からの繰り上がりは、2ステップ連続では起こらない」
これでcollatzPatternA2とBを計算すると、Loopが両方とも7項で4繰り上がりになって、
いくら繰り返してもずれは増大しません。

*CollatzPatt> collatzPatternA2 繰り上がりなし、あり、なし、あり、……
[([1,1,1,1,1],0,0),([1,1,1,0,1],1,1),([1,0,0,0,1],1,0),([1,0,0,1,1],0,1),([1,1,0,0,1],1,0),([0,0,1,1,1],0,1),([1,0,1,0,1],1,0),([1,1,1,1,1],0,1)]
*CollatzPatt> map snd3 collatzPatternA2
[0,#1,1,0,1,0,1,0]

*CollatzPatt> collatzPatternB
[([0,0,0,0,1],0),([0,0,0,1,1],0),([0,1,0,0,1],1),([1,1,0,1,1],0),([0,0,1,0,1],1),([0,1,1,1,1],0),([0,1,1,0,1],1),([0,0,0,0,1],1)]
*CollatzPatt> map snd collatzPatternB
[0,#0,1,0,1,0,1,1]
まだHaskellなのはご容赦を。
0424righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/11(土) 03:48:47.75ID:6GM2rdQN
単純に僕のCoq歴が3週間、Haskell歴が5年くらいだからだと思います。
0425１３２人目の素数さん
垢版 |
2016/06/11(土) 18:00:38.27ID:p56I7Lto
Haskell　5年もやってんのか凄いな。
5年間で何行くらいHaskellでコード書いたの？
0426righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/11(土) 20:46:46.40ID:6GM2rdQN
Haskellはコード量が短くすむこともあって、
5年間で2000〜3000行ぐらいじゃないでしょうか。
0427１３２人目の素数さん
垢版 |
2016/06/11(土) 20:59:42.80ID:p56I7Lto
100行のプログラム20〜30本書いてるってことか
なかなか大したもんだ。
0428righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/13(月) 02:40:18.56ID:6i9eMAsV
大幅に証明を変えます。
左端を伸ばすパターンYs=x0(3/2)^sに対して、Zs=2^p(3/2)^sを考えます。
ここで2^pは、x0と右端を揃えるものです。
例えば、2進数でx0=11001なら、2^p=00001となります。
2^p < x0なので、Zs < Ysが言えます。

Ys <= コラッツパターンXsは自明です。

x0=11001なら、y0B=11111で、pysはx0と右端を揃えるものです。
X0とy0Bは1ずれた状態からスタートします。
ysBの繰り返しは8bitでおこなって[1,1,#0,1,0,1,1,0,1,0,1,0,1,1]です。12ステップ中7個が1です。
Xsの先頭2ステップは最大で1,1ですから、2ステップ目でX2とy2Bのずれは1以上です。
次に、Xsを12ステップで区切った時、8個以上1が入る事はありません。(※)
よってXsはysB*2^(pys+1)を超えないので、Xs < ysB*2^(pys+1)です。

（初期値11111） < （初期値000001）
ysB*2^(pys+1) < 2^(p+2)(3/2)^sが言えます。図参照。
http://cdn-ak.f.st-hatena.com/images/fotolife/r/righ1113/20160613/20160613021641.jpg
2^(p+2)(3/2)^s < 2*2^(p+2)(3/2)^sなので、ysB*2^(pys+2) < 8Zsです。
まとめると、Zs < Ys <= Xs < ysB*2^(pys+1) < 8Zsとなります。

Zsと8Zsのずれは3で、これがずっと変わらないです。
よって、YsとXsのずれも3以下に押さえられる事になります。

(※)は後で書きます。
0429righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/13(月) 05:34:28.73ID:6i9eMAsV
×　（初期値11111）　<　（初期値000001）
○　（初期値011111） < （初期値0000001）
0430righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/13(月) 09:53:52.64ID:6i9eMAsV
Xsを12ステップで区切った時、8個以上1が入る事はありません。(※)
まずは補題から。

・2連続の0は無い。　0.585+0.585=1.135より、必ず1繰り上がるから
・3連続の1は無い。
・1,1,0,1,1パターンは無い。
1つ前　　　　　　　　1,　　　　　1,　　　　　　0,　　　　　　　1,　　　　　　　1
.415~.999 .000~584
　　　　　　　　.000~414は脱落
.830~.999 .415~584 .000~.169 .585~.754 .170~.339 全部脱落
　　　　　　　　　　　　　　　　　　　　　　　　　（↑3連続の1は無い事も分かる）
0431righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/13(月) 09:57:29.37ID:6i9eMAsV
次に、8個1/12ステップの[0,0,0,0,1,1,1,1,1,1,1,1]の全ての順列に対して、上3つを除外します。
またもやHaskellですwww

import Data.List (permutations, nub)

cycleN :: Int -> [Int] -> [Int] -> [Int]
cycleN 0 la _ = la
cycleN x la lb = cycleN (x-1) (la++lb) lb

remove_0_0 :: [Int] -> Bool
remove_0_0 [_] = True
remove_0_0 (0:0:xs) = False
remove_0_0 (_:x1:xs) = remove_0_0 (x1:xs)

remove_1_1_1 :: [Int] -> Bool
remove_1_1_1 [_,_] = True
remove_1_1_1 (1:1:1:xs) = False
remove_1_1_1 (_:x1:x2:xs) = remove_1_1_1 (x1:x2:xs)

remove_1_1_0_1_1 :: [Int] -> Bool
remove_1_1_0_1_1 [_,_,_,_] = True
remove_1_1_0_1_1 (1:1:0:1:1:xs) = False
remove_1_1_0_1_1 (_:x1:x2:x3:x4:xs) = remove_1_1_0_1_1 (x1:x2:x3:x4:xs)

*CollatzPatt> let multi=filter remove_1_1_1 $ filter remove_0_0 $
nub $ permutations [0,0,0,0,1,1,1,1,1,1,1,1]　←1時間ぐらいかかる
*CollatzPatt> filter remove_1_1_0_1_1 $ filter remove_1_1_1 $ map (cycleN 2 []) multi
[]
空リストになったので、(※)が証明できました。
0432righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/14(火) 09:36:32.33ID:GDyexPn/
Xsを12ステップで区切った時、8個以上1が入る事はありません。(※)
Coq版できました。
ただnub permutationsの部分がCoqでは12時間計算しても終わらなかったので、
そこだけHaskellで495行出力して（それでも1時間かかる）、permu.vに書いています。

permu.v
Require Import List.

Definition nub_permu: list (list nat) :=
((0::0::0::0::1::1::1::1::1::1::1::1::nil)::
(1::0::0::0::0::1::1::1::1::1::1::1::nil)::
---略---
(1::1::1::1::1::0::1::0::0::1::1::0::nil)::
(1::1::1::1::1::1::0::0::0::1::1::0::nil)::nil).
0433righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/14(火) 09:41:24.87ID:GDyexPn/
collatz06.v
Require Import Omega.
Require Import List.
Require Import Coq.Program.Wf.
Require Import permu.

Fixpoint cycle{A} (n:nat) (la:list A) (lb:list A) :list A :=
match n with
| 0 => la
| S m => cycle m (app la lb) lb
end.

Fixpoint remove_0_0 (l:list nat): bool :=
match l with
| nil => true
| _::nil => true
| 0::0::_ => false
| l1::ls => remove_0_0 ls
end.

Fixpoint remove_1_1_1 (l:list nat): bool :=
match l with
| nil => true
| _::nil => true
| _::_::nil => true
| 1::1::1::_ => false
| l1::ls => remove_1_1_1 ls
end.

Fixpoint remove_1_1_0_1_1 (l:list nat): bool :=
match l with
| nil => true
| _::nil => true
| _::_::nil => true
| _::_::_::nil => true
| _::_::_::_::nil => true
| 1::1::0::1::1::_ => false
| l1::ls => remove_1_1_0_1_1 ls
end.
0434righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/14(火) 09:46:24.20ID:GDyexPn/
Fixpoint beq_list (l:list nat) (m:list nat): bool :=
match l,m with
| nil, nil => true
| nil, _ => false
| _, nil => false
| l1::ls, m1::ms => if beq_nat l1 m1 then beq_list ls ms else false
end.
Fixpoint elem (x:list nat) (l:list (list nat)): bool :=
match l with
| nil => false
| l1::ls => if beq_list x l1 then true else elem x ls
end.
Fixpoint nub (l:list (list nat)): list (list nat) :=
match l with
| nil => nil
| l1::ls => (if elem l1 ls then nil else (l1::nil)) ++ (nub ls)
end.

Definition bnt_nat (x:nat) (y:nat): bool :=
if beq_nat x y then false else true.
Fixpoint concatMap (f:nat->list (list nat)) (l:list nat): list (list nat) :=
match l with
| nil => nil
| l1::ls => (f l1) ++ concatMap f ls
end.
Fixpoint replace (x y:nat) (l m:list nat): list nat :=
match m with
| nil => l
| m1::ms => if beq_nat x m1 then replace x y (y::l) ms else replace x y (m1::l) ms
end.
Program Fixpoint permutations (l:list nat) (cnt:nat) {measure cnt}: (list (list nat)) :=
match cnt with
| 0 => ((nil)::nil)
| _ =>
match l with
| nil => ((nil)::nil)
| ls => concatMap (fun x => (map (fun y => x::y) (permutations (filter (bnt_nat x) ls) (cnt-1)))) ls
end
end.
Next Obligation.
omega.
Qed.
0435righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/14(火) 09:49:36.01ID:GDyexPn/
Definition multi1: list (list nat) :=
filter remove_1_1_1
(filter remove_0_0
(* (nub (map (replace 2 0 nil)
(map (replace 3 0 nil)
(map (replace 4 0 nil)
(map (replace 5 1 nil)
(map (replace 6 1 nil)
(map (replace 7 1 nil)
(map (replace 8 1 nil)
(map (replace 9 1 nil)
(map (replace 10 1 nil)
(map (replace 11 1 nil)
(permutations (0::1::2::3::4::5::6::7::8::9::10::11::nil) 12)))))))))))) *)
nub_permu).
Definition multi2: list (list nat) :=
filter remove_1_1_0_1_1 (filter remove_1_1_1 (map (cycle 2 (nil)) multi1)).

Theorem multi2_is_nil:
multi2 = nil.
Proof.
compute.
reflexivity.
Qed.

やっぱQed.が通ると気持ちが良いですね。
0440１３２人目の素数さん
垢版 |
2016/06/19(日) 05:13:52.50ID:R9PbWXF5
>>1
コラッツパターンとかライトエッジパターンとかよくわからん。
もし余力があればideoneにプログラム上げてくれんか？
好きな数を入力してそれに対してそのパターンを出力してほしい。

http://ideone.com/

haskellも選べるからたぶんもうすでに書いたものがあるだろ？
0443１３２人目の素数さん
垢版 |
2016/06/19(日) 08:36:15.00ID:R9PbWXF5
エクセルマクロはうごきました。
サンクス。

左端がどう決まってるのかいまいち分かってないんだけど
２で割れた回数とかだよね？
>>439のは英語だったからいまいち自信がもてない。
0444righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/19(日) 12:31:44.57ID:o4I0V/Mj
コラッツパターンの左側は、
コラッツ操作で＜2で割った回数-1＞を蓄積しているものです。
>>173にもあります。
（マクロやpdfでは0を書いてないけど）
0445１３２人目の素数さん
垢版 |
2016/06/20(月) 20:49:50.82ID:AO/P2Y9A
左端を伸ばすパターンの説明で

3. Becomes the next x from the left end of the 1 to 1 on the right.

てのがあるんだけど、どう訳せばいいのかよくわからんｗ
教えて〜
0446righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/20(月) 22:36:36.36ID:IBPpfU1W
「次のxとして、左端の1から右端の1までを取る」という意味です。
_111111001　=x0が
1011110111　=x1になった時、
x1は左端の1から右端の1までを取るね、という事です。

実は英語は苦手で、いつも赤点でしたwww
0449１３２人目の素数さん
垢版 |
2016/06/21(火) 20:10:09.84ID:shTmSKB6
まだ理解できてないが左端を伸ばすパターンもエクセルマクロあるの？
あるならオクレ。
0450righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/21(火) 20:18:58.92ID:w+gnd+8K
左端を伸ばすパターンは数が左に伸びるのと、
ステップが無限に続くので、作れてないです。すみません。
0452１３２人目の素数さん
垢版 |
2016/06/21(火) 21:05:09.09ID:shTmSKB6
んー左に伸ばすパターンって出力のサイズを制限したらプログラム書ける？
制限しても難しい？
■ このスレッドは過去ログ倉庫に格納されています
ニューススポーツなんでも実況