Skip to content

Commit 35b78c9

Browse files
lengyijunlengyijun
committed
F_collatz
listblank helper
1 parent e9a4490 commit 35b78c9

File tree

3 files changed

+240
-9
lines changed

3 files changed

+240
-9
lines changed

‎CollatzFunction/ListBlank.lean‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,3 +31,17 @@ match head_h : l.head with
3131
let _termination_proof : (l |> to_list_rev |> List.length) > (l.tail |> to_list_rev |> List.length):= by simp [h]
3232
1 + count1 l.tail
3333
termination_by (l |> to_list_rev |> List.length)
34+
35+
36+
37+
38+
open Γ
39+
40+
-- a more descriptive name for the theorem
41+
theorem ListBlank_empty_eq_single_zero: ∀ l, Turing.ListBlank.mk (l ++ [zero]) = Turing.ListBlank.mk l := by
42+
intros l
43+
simp! [Turing.ListBlank.mk]
44+
rw [Quotient.eq'']
45+
right
46+
use 1
47+
tauto

‎CollatzFunction/NonHalt/Main.lean‎

Lines changed: 220 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,234 @@
11
import CollatzFunction.NonHalt.TuringMachine9
22
import CollatzFunction.NonHalt.Even
33
import CollatzFunction.NonHalt.Odd
4+
import CollatzFunction.NonHalt.Search0
5+
import CollatzFunction.NonHalt.Search1
6+
import CollatzFunction.NonHalt.Miscellaneous
7+
import CollatzFunction.NonHalt.Transition
48
import CollatzFunction.Collatz
9+
import CollatzFunction.ListBlank
510

611
namespace NonHalt
712

813
open Lean Meta Elab Tactic Std Term TmState Γ
914

1015

11-
lemma B_collatz (n: ℕ): ∀ (i: ℕ)(l r: List Γ),
12-
nth_cfg i = some ⟨B, ⟨one,
13-
Turing.ListBlank.mk (zero :: l),
14-
Turing.ListBlank.mk (List.replicate n one ++ zero :: r)⟩⟩ →
16+
/-
17+
-- if n >= 3, n -> collatz n
18+
lemma B_collatz (n: ℕ) (_ : n > 0) (i: ℕ)
19+
(h : nth_cfg i = some ⟨B, ⟨one,
20+
Turing.ListBlank.mk [],
21+
Turing.ListBlank.mk (List.replicate n one)⟩⟩) :
1522
∃ j>i, nth_cfg j = some ⟨B, ⟨one,
16-
Turing.ListBlank.mk (zero :: l),
17-
Turing.ListBlank.mk (List.replicate (collatz (n+2)) one ++ zero :: r)⟩⟩
23+
Turing.ListBlank.mk [],
24+
Turing.ListBlank.mk (List.replicate ((collatz (n+2))-2) one)⟩⟩
1825
:= by
19-
sorry
26+
unfold collatz
27+
split_ifs <;> rename_i g
28+
. rw [← ListBlank_empty_eq_single_zero []] at h
29+
simp at h
30+
rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
31+
apply B_even at h
32+
obtain ⟨j, _, h⟩ := h
33+
forward h
34+
rw [add_comm 1 (n/2)] at h
35+
rw [List.replicate_succ] at h
36+
simp at h
37+
rw [← (ListBlank_empty_eq_single_zero (List.replicate (n/2) one))] at h
38+
apply E_zeroing at h
39+
forward h
40+
apply recF at h
41+
forward h
42+
forward h
43+
use (6 + j + n / 2 * 2)
44+
simp [h]
45+
repeat any_goals apply And.intro
46+
. omega
47+
. cases n with
48+
| zero => omega
49+
| succ n => cases n with
50+
| zero => omega
51+
| succ n => ring_nf
52+
have h : (2+n)/2 = n/2 + 1:= by omega
53+
rw [h]
54+
rw [List.replicate_succ]
55+
simp
56+
. simp! [Turing.ListBlank.mk]
57+
rw [Quotient.eq'']
58+
right
59+
use (n/2+1+1+1+1)
60+
rw [← List.cons_append]
61+
rw [← List.cons_append]
62+
rw [← List.cons_append]
63+
rw [← List.replicate_succ]
64+
rw [← List.replicate_succ]
65+
rw [← List.replicate_succ]
66+
rw [List.append_cons]
67+
rw [← List.replicate_succ']
68+
simp
69+
tauto
70+
. rw [← Nat.even_iff] at g
71+
obtain ⟨a, g⟩ := g
72+
cases a with
73+
| zero => omega
74+
| succ a => use a; omega
75+
. rw [← ListBlank_empty_eq_single_zero []] at h
76+
simp at h
77+
rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
78+
apply B_odd at h
79+
obtain ⟨j, _, h⟩ := h
80+
forward h
81+
cases n with
82+
| zero => omega
83+
| succ n =>
84+
ring_nf at h
85+
have k : (2+n)/2 = n/2 + 1:= by omega
86+
rw [k] at h
87+
rw [List.replicate_succ] at h
88+
simp at h
89+
rw [← List.replicate_succ] at h
90+
apply copy_half at h
91+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
92+
apply lemma_G_to_H at h
93+
apply lemma_H_to_J at h
94+
forward h
95+
forward h
96+
forward h
97+
rw [← List.replicate_succ'] at h
98+
rw [List.replicate_succ] at h
99+
simp at h
100+
rw [← List.replicate_succ'] at h
101+
ring_nf at h
102+
use (12 + j + n / 2 * 13 + (n / 2) ^ 2 * 4)
103+
simp [h]
104+
repeat any_goals apply And.intro
105+
. omega
106+
. simp! [Turing.ListBlank.mk]
107+
rw [Quotient.eq'']
108+
right
109+
use 2
110+
tauto
111+
. ring_nf
112+
apply congr
113+
any_goals rfl
114+
apply congr
115+
any_goals rfl
116+
apply congr
117+
any_goals rfl
118+
omega
119+
. have g : (n+2) % 2 = 1 := by omega
120+
rw [← Nat.odd_iff] at g
121+
obtain ⟨a, g⟩ := g
122+
cases a with
123+
| zero => omega
124+
| succ a => use a; omega
125+
-/
126+
127+
-- if n ≥ 1, n -> collatz n
128+
lemma F_collatz (n: ℕ) (_ : n ≥ 1) (i: ℕ)
129+
(h : nth_cfg i = some ⟨F, ⟨one,
130+
Turing.ListBlank.mk [],
131+
Turing.ListBlank.mk (List.replicate (n-1) one)⟩⟩) :
132+
∃ j>i, nth_cfg j = some ⟨F, ⟨one,
133+
Turing.ListBlank.mk [],
134+
Turing.ListBlank.mk (List.replicate ((collatz n)-1) one)⟩⟩
135+
:= by
136+
cases n with
137+
| zero => omega
138+
| succ n => forward h
139+
cases n with
140+
| zero => simp
141+
forward h
142+
unfold collatz
143+
simp
144+
forward h
145+
forward h
146+
use (4+i)
147+
simp [h]
148+
simp! [Turing.ListBlank.mk]
149+
rw [Quotient.eq'']
150+
right
151+
use 1
152+
tauto
153+
| succ n =>
154+
rw [List.replicate_succ] at h
155+
simp at h
156+
unfold collatz
157+
split_ifs <;> rename_i g
158+
. rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
159+
apply B_even at h
160+
obtain ⟨j, _, h⟩ := h
161+
forward h
162+
rw [add_comm 1 (n/2)] at h
163+
rw [List.replicate_succ] at h
164+
simp at h
165+
rw [← (ListBlank_empty_eq_single_zero (List.replicate (n/2) one))] at h
166+
apply E_zeroing at h
167+
forward h
168+
apply recF at h
169+
forward h
170+
use (5 + j + n / 2 * 2)
171+
ring_nf at *
172+
simp [h]
173+
repeat any_goals apply And.intro
174+
. omega
175+
. rw [← List.replicate_succ']
176+
ring_nf
177+
simp! [Turing.ListBlank.mk]
178+
rw [Quotient.eq'']
179+
right
180+
use 3 + n/2
181+
rw [← List.replicate_succ]
182+
rw [← List.replicate_succ]
183+
simp
184+
ring_nf
185+
tauto
186+
. rw [← Nat.even_iff] at g
187+
obtain ⟨a, g⟩ := g
188+
cases a with
189+
| zero => omega
190+
| succ a => use a; omega
191+
. cases n with
192+
| zero => omega
193+
| succ n =>
194+
rw [← (ListBlank_empty_eq_single_zero (List.replicate (n+1) one))] at h
195+
apply B_odd at h
196+
obtain ⟨j, _, h⟩ := h
197+
forward h
198+
have k : (2+n)/2 = n/2 + 1:= by omega
199+
rw [k] at h
200+
rw [List.replicate_succ] at h
201+
simp at h
202+
rw [← List.replicate_succ] at h
203+
apply copy_half at h
204+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
205+
apply lemma_G_to_H at h
206+
apply lemma_H_to_J at h
207+
forward h
208+
forward h
209+
use (11 + j + n / 2 * 13 + (n / 2) ^ 2 * 4)
210+
simp [h]
211+
repeat any_goals apply And.intro
212+
. omega
213+
. simp! [Turing.ListBlank.mk]
214+
rw [Quotient.eq'']
215+
right
216+
use 1
217+
tauto
218+
. ring_nf
219+
apply congr
220+
any_goals rfl
221+
rw [← List.replicate_succ']
222+
apply congr
223+
any_goals rfl
224+
apply congr
225+
any_goals rfl
226+
omega
227+
. have g : (n+3) % 2 = 1 := by omega
228+
rw [← Nat.odd_iff] at g
229+
obtain ⟨a, g⟩ := g
230+
cases a with
231+
| zero => omega
232+
| succ a => use a; omega
20233

21234
end NonHalt

‎CollatzFunction/NonHalt/Miscellaneous.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,12 @@ namespace NonHalt
66
open Lean Meta Elab Tactic Std Term TmState
77

88
theorem E_zeroing (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
9-
nth_cfg i = some ⟨E, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
10-
nth_cfg (i + k + 1) = some ⟨E, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.zero ++ r)⟩⟩ := by
9+
nth_cfg i = some ⟨E, ⟨Γ.one,
10+
Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l),
11+
Turing.ListBlank.mk r⟩⟩ →
12+
nth_cfg (i + k + 1) = some ⟨E, ⟨Γ.zero,
13+
Turing.ListBlank.mk l,
14+
Turing.ListBlank.mk (List.replicate (k+1) Γ.zero ++ r)⟩⟩ := by
1115
induction k with intros i l r h
1216
| zero => forward h
1317
ring_nf at *

0 commit comments

Comments
 (0)