Skip to content

Commit 395418f

Browse files
lengyijunlengyijun
committed
Halt
1 parent cb16e83 commit 395418f

File tree

13 files changed

+956
-1
lines changed

13 files changed

+956
-1
lines changed

‎CollatzFunction.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,13 @@ import CollatzFunction.NonHalt.Transition
1414
import CollatzFunction.NonHalt.Odd
1515
import CollatzFunction.NonHalt.Miscellaneous
1616
import CollatzFunction.NonHalt.Main
17+
18+
import CollatzFunction.Halt.TuringMachine10
19+
import CollatzFunction.Halt.Search0
20+
import CollatzFunction.Halt.Search1
21+
import CollatzFunction.Halt.BStep
22+
import CollatzFunction.Halt.Even
23+
import CollatzFunction.Halt.Transition
24+
import CollatzFunction.Halt.Odd
25+
import CollatzFunction.Halt.Miscellaneous
26+
import CollatzFunction.Halt.Main

‎CollatzFunction/Halt/BStep.lean‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
import CollatzFunction.Halt.TuringMachine10
2+
import CollatzFunction.Halt.Search0
3+
4+
namespace Halt
5+
6+
open Lean Meta Elab Tactic Std Term TmState Γ
7+
8+
lemma B_step (l r: List Γ) (n i: ℕ)
9+
(h : nth_cfg i = some ⟨B, ⟨one,
10+
Turing.ListBlank.mk (List.cons zero l),
11+
Turing.ListBlank.mk (List.replicate (2+n) one ++ zero :: r)⟩⟩)
12+
:
13+
nth_cfg (9 + i + n * 2) = some ⟨B, ⟨one,
14+
Turing.ListBlank.mk (zero :: one :: l),
15+
Turing.ListBlank.mk (List.replicate n one ++ zero :: one :: r)⟩⟩
16+
:= by
17+
apply recB at h
18+
forward h
19+
have g : 2 + n = n + 2 := by omega
20+
rw [g] at h
21+
forward h
22+
forward h
23+
apply recD at h
24+
forward h
25+
forward h
26+
rw [List.append_cons] at h
27+
rw [← List.replicate_one] at h
28+
rw [List.replicate_append_replicate] at h
29+
simp only [ne_eq, List.replicate_succ_ne_nil, not_false_eq_true, List.tail_append_of_ne_nil, List.tail_replicate, Nat.add_one_sub_one] at h
30+
rw [List.replicate_succ] at h
31+
simp at h
32+
rw [h]
33+
34+
lemma K_step (l r: List Γ) (n i: ℕ)
35+
(h : nth_cfg i = some ⟨K, ⟨one,
36+
Turing.ListBlank.mk (List.cons zero l),
37+
Turing.ListBlank.mk (List.replicate (2+n) one ++ zero :: r)⟩⟩)
38+
:
39+
nth_cfg (9 + i + n * 2) = some ⟨B, ⟨one,
40+
Turing.ListBlank.mk (zero :: one :: l),
41+
Turing.ListBlank.mk (List.replicate n one ++ zero :: one :: r)⟩⟩
42+
:= by
43+
forward h
44+
have k : 2+n = n+1+1 := by omega
45+
rw [k] at h
46+
rw [List.replicate_succ] at h
47+
simp at h
48+
apply recB at h
49+
forward h
50+
forward h
51+
rw [add_comm 1 n] at h
52+
rw [List.replicate_succ] at h
53+
simp at h
54+
rw [List.append_cons] at h
55+
rw [← List.replicate_one] at h
56+
rw [List.replicate_append_replicate] at h
57+
apply recD at h
58+
forward h
59+
forward h
60+
exact h
61+
62+
end Halt

‎CollatzFunction/Halt/Even.lean‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
import CollatzFunction.Halt.TuringMachine10
2+
import CollatzFunction.Halt.BStep
3+
4+
namespace Halt
5+
6+
open Lean Meta Elab Tactic Std Term TmState Γ
7+
8+
lemma B_even (n: ℕ) (h_even : Even n): ∀ (i: ℕ)(l r: List Γ),
9+
nth_cfg i = some ⟨B, ⟨one,
10+
Turing.ListBlank.mk (zero :: l),
11+
Turing.ListBlank.mk (List.replicate n one ++ zero :: r)⟩⟩ →
12+
∃ j>i, nth_cfg j = some ⟨A, ⟨zero,
13+
Turing.ListBlank.mk (List.replicate (1+n/2) one ++ l),
14+
Turing.ListBlank.mk (List.replicate (1+n/2) one ++ r)⟩⟩
15+
:= by
16+
induction' n using Nat.strongRecOn with n IH
17+
intros i l r h
18+
cases n with
19+
| zero => simp
20+
forward h
21+
forward h
22+
forward h
23+
forward h
24+
use (4+i)
25+
simp [h]
26+
| succ n => cases n with
27+
| zero => tauto
28+
| succ n => ring_nf at h
29+
apply B_step at h
30+
specialize IH n (by omega)
31+
apply IH at h
32+
. obtain ⟨j, _, h⟩ := h
33+
use j
34+
constructor
35+
any_goals omega
36+
simp [h]
37+
ring_nf
38+
have h : (2+n)/2 = n/2+1 := by omega
39+
rw [h]
40+
ring_nf
41+
rw [List.append_cons]
42+
rw [← List.replicate_one]
43+
rw [List.replicate_append_replicate]
44+
ring_nf
45+
rw [List.append_cons]
46+
rw [← List.replicate_one]
47+
rw [List.replicate_append_replicate]
48+
ring_nf
49+
tauto
50+
. obtain ⟨k, h_even⟩ := h_even
51+
cases k with
52+
| zero => omega
53+
| succ k => use k; omega
54+
55+
lemma K_even (n: ℕ) (h_even : Even n) (i: ℕ) (l r: List Γ):
56+
nth_cfg i = some ⟨K, ⟨one,
57+
Turing.ListBlank.mk (zero :: l),
58+
Turing.ListBlank.mk (List.replicate n one ++ zero :: r)⟩⟩ →
59+
∃ j>i, nth_cfg j = some ⟨A, ⟨zero,
60+
Turing.ListBlank.mk (List.replicate (1+n/2) one ++ l),
61+
Turing.ListBlank.mk (List.replicate (1+n/2) one ++ r)⟩⟩
62+
:= by
63+
intros h
64+
cases n with
65+
| zero => forward h
66+
forward h
67+
forward h
68+
forward h
69+
use (4+i)
70+
simp [h]
71+
| succ n => forward h
72+
apply recB at h
73+
forward h
74+
forward h
75+
rw [List.append_cons] at h
76+
rw [← List.replicate_one] at h
77+
rw [List.replicate_append_replicate] at h
78+
apply recD at h
79+
forward h
80+
forward h
81+
cases n with
82+
| zero => simp at h_even
83+
| succ n => rw [List.replicate_succ] at h
84+
simp at h
85+
apply B_even at h
86+
. obtain ⟨j, _, h⟩ := h
87+
use j
88+
simp [h]
89+
repeat any_goals apply And.intro
90+
. omega
91+
. rw [List.append_cons]
92+
rw [← List.replicate_one]
93+
rw [List.replicate_append_replicate]
94+
have g : (1 + n / 2 + 1) = (1 + (n + 1 + 1) / 2) := by omega
95+
rw [g]
96+
. rw [List.append_cons]
97+
rw [← List.replicate_one]
98+
rw [List.replicate_append_replicate]
99+
have g : (1 + n / 2 + 1) = (1 + (n + 1 + 1) / 2) := by omega
100+
rw [g]
101+
. obtain ⟨a, _⟩ := h_even
102+
cases a with
103+
| zero => omega
104+
| succ a => use a; omega
105+
106+
107+
end Halt

‎CollatzFunction/Halt/Main.lean‎

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
import CollatzFunction.Halt.TuringMachine10
2+
import CollatzFunction.Halt.Even
3+
import CollatzFunction.Halt.Odd
4+
import CollatzFunction.Halt.Search0
5+
import CollatzFunction.Halt.Search1
6+
import CollatzFunction.Halt.Miscellaneous
7+
import CollatzFunction.Halt.Transition
8+
import CollatzFunction.Collatz
9+
import CollatzFunction.ListBlank
10+
11+
namespace Halt
12+
13+
open Lean Meta Elab Tactic Std Term TmState Γ
14+
15+
-- if n ≥ 2, n -> collatz n
16+
theorem F_collatz (n: ℕ) (_ : n ≥ 2) (i: ℕ)
17+
(h : nth_cfg i = some ⟨F, ⟨one,
18+
Turing.ListBlank.mk [],
19+
Turing.ListBlank.mk (List.replicate (n-1) one)⟩⟩) :
20+
∃ j>i, nth_cfg j = some ⟨F, ⟨one,
21+
Turing.ListBlank.mk [],
22+
Turing.ListBlank.mk (List.replicate ((collatz n)-1) one)⟩⟩
23+
:= by
24+
cases n with
25+
| zero => omega
26+
| succ n => forward h
27+
cases n with
28+
| zero => omega
29+
| succ n => cases n with
30+
| zero => simp
31+
forward h
32+
unfold collatz
33+
simp
34+
forward h
35+
forward h
36+
forward h
37+
forward h
38+
forward h
39+
forward h
40+
forward h
41+
forward h
42+
use (10+i)
43+
simp [h]
44+
simp! [Turing.ListBlank.mk]
45+
rw [Quotient.eq'']
46+
right
47+
use 3
48+
tauto
49+
| succ n =>
50+
rw [List.replicate_succ] at h
51+
simp at h
52+
unfold collatz
53+
split_ifs <;> rename_i g
54+
. rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
55+
apply K_even at h
56+
obtain ⟨j, _, h⟩ := h
57+
forward h
58+
rw [add_comm 1 ((1+n)/2)] at h
59+
rw [List.replicate_succ] at h
60+
simp at h
61+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
62+
apply E_zeroing at h
63+
forward h
64+
apply recF at h
65+
forward h
66+
use (5 + j + (1+n) / 2 * 2)
67+
ring_nf at *
68+
simp [h]
69+
repeat any_goals apply And.intro
70+
. omega
71+
. rw [← List.replicate_succ']
72+
ring_nf
73+
simp! [Turing.ListBlank.mk]
74+
rw [Quotient.eq'']
75+
right
76+
use 3 + (1+n)/2
77+
rw [← List.replicate_succ]
78+
rw [← List.replicate_succ]
79+
simp
80+
ring_nf
81+
tauto
82+
. apply congr
83+
any_goals rfl
84+
apply congr
85+
any_goals rfl
86+
apply congr
87+
any_goals rfl
88+
omega
89+
. rw [← Nat.even_iff] at g
90+
obtain ⟨a, g⟩ := g
91+
cases a with
92+
| zero => omega
93+
| succ a => use a; omega
94+
. rw [← (ListBlank_empty_eq_single_zero (List.replicate (n+1) one))] at h
95+
apply K_odd at h
96+
obtain ⟨j, _, h⟩ := h
97+
forward h
98+
have k : (2+n)/2 = n/2 + 1:= by omega
99+
rw [k] at h
100+
rw [List.replicate_succ] at h
101+
simp at h
102+
rw [← List.replicate_succ] at h
103+
apply copy_half at h
104+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
105+
apply lemma_G_to_H at h
106+
apply lemma_H_to_J at h
107+
forward h
108+
forward h
109+
use (11 + j + n / 2 * 13 + (n / 2) ^ 2 * 4)
110+
simp [h]
111+
repeat any_goals apply And.intro
112+
. omega
113+
. simp! [Turing.ListBlank.mk]
114+
rw [Quotient.eq'']
115+
right
116+
use 1
117+
tauto
118+
. apply congr
119+
any_goals rfl
120+
rw [← List.replicate_succ']
121+
apply congr
122+
any_goals rfl
123+
apply congr
124+
any_goals rfl
125+
omega
126+
. have g : (n+3) % 2 = 1 := by omega
127+
rw [← Nat.odd_iff] at g
128+
obtain ⟨a, g⟩ := g
129+
cases a with
130+
| zero => omega
131+
| succ a => use a; omega
132+
133+
end Halt

0 commit comments

Comments
 (0)