Skip to content

Commit 6dd20cc

Browse files
lengyijunlengyijun
committed
style
1 parent 8e9507e commit 6dd20cc

File tree

1 file changed

+103
-114
lines changed

1 file changed

+103
-114
lines changed

‎CollatzFunction/NonHalt/Main.lean‎

Lines changed: 103 additions & 114 deletions
Original file line numberDiff line numberDiff line change
@@ -19,72 +19,64 @@ lemma F_odd (n i: ℕ) (h_odd: Odd n) (init_cfg: Cfg)
1919
nth_cfg init_cfg (i+(3 * n^2+4*n+1)/2) = ⟨F, ⟨one,
2020
Turing.ListBlank.mk [],
2121
Turing.ListBlank.mk (List.replicate ((collatz n)-1) one)⟩⟩
22-
:= by
23-
cases n with
24-
| zero => ring_nf at *; tauto
25-
| succ n => forward h
26-
cases n with
27-
| zero => ring_nf at *
28-
forward h
29-
forward h
30-
forward h
31-
simp [h]
32-
simp [collatz]
33-
simp! [Turing.ListBlank.mk]
34-
rw [Quotient.eq'']
35-
right
36-
use 1
37-
tauto
38-
| succ n => obtain ⟨k, h_odd⟩ := h_odd
39-
cases k with
40-
| zero => omega
41-
| succ k =>
42-
have h_odd : n = 2 * k+1 := by omega
43-
subst n
44-
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
45-
apply B_odd at h
46-
. ring_nf at *
47-
forward h
48-
have g : (1 +(2+k*2-1)) /2 = k + 1:= by omega
49-
rw [g] at h
50-
rw [List.replicate_succ] at h
51-
simp at h
52-
rw [← List.replicate_succ] at h
53-
apply copy_half at h
54-
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
55-
apply G_to_J at h
56-
forward h
57-
forward h
58-
simp [collatz]
59-
ring_nf at *
60-
have g : i + (40 + k * 44 + k ^ 2 * 12) / 2 = 20 + 22 * k + 6 * k ^ 2 + i := by omega
61-
rw [g]
62-
have g : 2+k*2-1 = k*2 +1 := by omega
63-
rw [g] at h
64-
have g : (k * 2 + 1) ^ 2 = 4 * k + 4 * k ^ 2 + 1 := by ring_nf
65-
have g : ((k * 2 + 1) * 7 + (k * 2 + 1) ^ 2) / 2 = 4 + 9 * k + 2 * k ^ 2 := by omega
66-
have g : 16 + i + k * 13 + k ^ 2 * 4 + ((k * 2 + 1) * 7 + (k * 2 + 1) ^ 2) / 2 = 20 + 22 * k + 6 * k ^ 2 + i := by omega
67-
rw [← g]
68-
simp [h]
69-
constructor
70-
. simp! [Turing.ListBlank.mk]
71-
rw [Quotient.eq'']
72-
right
73-
use 1
74-
tauto
75-
. rw [← List.replicate_one]
76-
rw [List.replicate_append_replicate]
77-
apply congr
78-
any_goals rfl
79-
apply congr
80-
any_goals rfl
81-
apply congr
82-
any_goals rfl
83-
omega
84-
. use k; omega
85-
22+
:= match n with
23+
| 0 => by ring_nf at *; tauto
24+
| 1 => by forward h
25+
ring_nf at *
26+
forward h
27+
forward h
28+
forward h
29+
simp [h]
30+
simp [collatz]
31+
simp! [Turing.ListBlank.mk]
32+
rw [Quotient.eq'']
33+
right
34+
use 1
35+
tauto
36+
| Nat.succ (Nat.succ n) => by
37+
forward h
38+
obtain ⟨k, h_odd⟩ := h_odd
39+
cases k with
40+
| zero => omega
41+
| succ k =>
42+
have h_odd : n = 2 * k+1 := by omega
43+
subst n
44+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
45+
apply B_odd at h
46+
. ring_nf at *
47+
forward h
48+
rw [← List.replicate_succ] at h
49+
rw [← List.replicate_succ] at h
50+
apply copy_half at h
51+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
52+
apply G_to_J at h
53+
forward h
54+
forward h
55+
simp [collatz]
56+
ring_nf at *
57+
have g : i + (40 + k * 44 + k ^ 2 * 12) / 2 = 20 + 22 * k + 6 * k ^ 2 + i := by omega
58+
rw [g]
59+
have g : (8 + k * 18 + k ^ 2 * 4) / 2 = 4 + k * 9 + k ^ 2 * 2 := by omega
60+
rw [g] at h
61+
ring_nf at *
62+
simp [h]
63+
constructor
64+
. simp! [Turing.ListBlank.mk]
65+
rw [Quotient.eq'']
66+
right
67+
use 1
68+
tauto
69+
. rw [← List.replicate_one]
70+
rw [List.replicate_append_replicate]
71+
apply congr
72+
any_goals rfl
73+
apply congr
74+
any_goals rfl
75+
apply congr
76+
any_goals rfl
77+
omega
78+
. use k
8679

87-
variable {a b c : ℕ}
8880

8981
lemma F_even (n i: ℕ) (_ : n ≥ 1) (h_even: Even n) (init_cfg: Cfg)
9082
(h : nth_cfg init_cfg i = ⟨F, ⟨one,
@@ -93,55 +85,52 @@ lemma F_even (n i: ℕ) (_ : n ≥ 1) (h_even: Even n) (init_cfg: Cfg)
9385
nth_cfg init_cfg (i+(n^2+5*n)/2+3) = ⟨F, ⟨one,
9486
Turing.ListBlank.mk [],
9587
Turing.ListBlank.mk (List.replicate ((collatz n)-1) one)⟩⟩
96-
:= by
97-
cases n with
98-
| zero => omega
99-
| succ n => cases n with
100-
| zero => tauto
101-
| succ n => obtain ⟨k, h_even⟩ := h_even
102-
cases k with
103-
| zero => omega
104-
| succ k =>
105-
have h_even : n = 2 * k := by omega
106-
subst n
107-
forward h
108-
rw [add_comm 1 (k*2)] at h
109-
rw [List.replicate_succ] at h
110-
simp at h
111-
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
112-
apply B_even at h
113-
. forward h
114-
rw [add_comm 1 k] at h
115-
rw [List.replicate_succ] at h
116-
simp at h
117-
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
118-
apply E_zeroing at h
119-
forward h
120-
apply recF at h
121-
forward h
122-
simp [collatz]
123-
ring_nf at *
124-
simp
125-
have g : k * 14 / 2 = k * 7 := by omega
126-
rw [g] at h
127-
have g : (14 + k * 18 + k ^ 2 * 4) / 2 = 7 + k * 9 + k ^ 2 * 2 := by omega
128-
rw [g]
129-
have g : k ^ 2 * 4 / 2 = k ^ 2 * 2 := by omega
130-
rw [g] at h
131-
ring_nf at *
132-
simp [h]
133-
simp! [Turing.ListBlank.mk]
134-
rw [Quotient.eq'']
135-
right
136-
use (3+k)
137-
simp
138-
rw [← List.replicate_one]
139-
rw [List.replicate_append_replicate]
140-
rw [← List.replicate_succ]
141-
rw [← List.replicate_succ]
142-
ring_nf
143-
tauto
144-
. use k; omega
88+
:= match n with
89+
| 0 => by omega
90+
| 1 => by tauto
91+
| Nat.succ (Nat.succ n) => by
92+
obtain ⟨k, h_even⟩ := h_even
93+
cases k with
94+
| zero => omega
95+
| succ k =>
96+
have h_even : n = 2 * k := by omega
97+
subst n
98+
forward h
99+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
100+
apply B_even at h
101+
. forward h
102+
rw [add_comm 1 k] at h
103+
rw [List.replicate_succ] at h
104+
simp at h
105+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
106+
apply E_zeroing at h
107+
forward h
108+
apply recF at h
109+
forward h
110+
simp [collatz]
111+
ring_nf at *
112+
simp
113+
have g : k * 14 / 2 = k * 7 := by omega
114+
rw [g] at h
115+
have g : (14 + k * 18 + k ^ 2 * 4) / 2 = 7 + k * 9 + k ^ 2 * 2 := by omega
116+
rw [g]
117+
have g : k ^ 2 * 4 / 2 = k ^ 2 * 2 := by omega
118+
rw [g] at h
119+
ring_nf at *
120+
simp [h]
121+
simp! [Turing.ListBlank.mk]
122+
rw [Quotient.eq'']
123+
right
124+
use (3+k)
125+
simp
126+
rw [← List.replicate_one]
127+
rw [List.replicate_append_replicate]
128+
rw [← List.replicate_succ]
129+
rw [← List.replicate_succ]
130+
ring_nf
131+
tauto
132+
. use k; omega
133+
145134

146135
-- if n ≥ 1, n -> collatz n
147136
theorem F_collatz (n: ℕ) (_ : n ≥ 1) (i: ℕ) (init_cfg: Cfg)

0 commit comments

Comments
 (0)