Skip to content

Commit bdccd18

Browse files
lengyijunlengyijun
committed
cases => match
1 parent b54620b commit bdccd18

File tree

1 file changed

+99
-81
lines changed

1 file changed

+99
-81
lines changed

‎CollatzFunction/Tm8/Main.lean‎

Lines changed: 99 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -16,94 +16,112 @@ lemma G_even (n i: ℕ) (h_even: Even n) (init_cfg: Cfg)
1616
nth_cfg_is_n (i+(n^2+3*n)/2+3) (collatz n) init_cfg
1717
:= by
1818
obtain ⟨l, h⟩ := h
19-
cases n with
20-
| zero => unfold collatz nth_cfg_is_n
19+
match n with
20+
| 0 => use (zero :: l)
21+
unfold collatz
22+
simp
23+
forward h
24+
forward h
25+
forward h
26+
ring_nf at *
27+
simp [h]
28+
| 1 => tauto
29+
| Nat.succ (Nat.succ n) =>
30+
obtain ⟨k, h_even⟩ := h_even
31+
cases k with
32+
| zero => omega
33+
| succ k =>
34+
have h_even : n = 2 * k := by omega
35+
subst n
36+
forward h
37+
forward h
38+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
39+
apply B_even at h
40+
. forward h
41+
rw [add_comm 1] at h
42+
rw [List.replicate_succ] at h
43+
simp at h
44+
forward h
45+
ring_nf at *
46+
have g : 3 + i + ((k * 2).succ.succ * 3 + (k * 2).succ.succ ^ 2) / 2 = 8 + i + k ^ 2 * 4 / 2 + k * 14 / 2 := by
2147
simp
22-
forward h
23-
forward h
24-
forward h
25-
ring_nf at *
26-
simp [h]
27-
use (zero :: l)
28-
| succ n => forward h
29-
cases n with
30-
| zero => ring_nf at *; tauto
31-
| succ n => obtain ⟨k, h_even⟩ := h_even
32-
cases k with
33-
| zero => omega
34-
| succ k =>
35-
have h_even : n = 2 * k := by omega
36-
subst n
37-
forward h
38-
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
39-
apply B_even at h
40-
. forward h
41-
rw [add_comm 1] at h
42-
rw [List.replicate_succ] at h
43-
simp at h
44-
forward h
45-
ring_nf at *
46-
have g :(3 + i + (10 + k * 14 + k ^ 2 * 4) / 2) = (8 + i + k ^ 2 * 4 / 2 + k * 14 / 2) := by omega
47-
rw [g]
48-
use (List.replicate k one ++ zero :: zero :: l)
49-
simp [h]
50-
simp [collatz]
51-
rw [List.replicate_succ]
52-
. use k; omega
48+
ring_nf
49+
calc
50+
_ = 3 + i + 5 + k * 7 + 2 * k ^ 2 := by omega
51+
_ = 8 + i + k ^ 2 * 2 + k * 7 := by ring_nf
52+
_ = _ := by omega
53+
rw [g]
54+
use (List.replicate k one ++ zero :: zero :: l)
55+
simp [h]
56+
simp [collatz]
57+
ring_nf
58+
simp
59+
rw [List.replicate_succ]
60+
. use k; omega
61+
5362

5463
lemma G_odd (n i: ℕ) (h_odd: Odd n) (init_cfg: Cfg)
5564
(h: nth_cfg_is_n i n init_cfg) :
5665
nth_cfg_is_n (i+(3 * n^2+4*n+1)/2) (collatz n) init_cfg
5766
:= by
5867
obtain ⟨l, h⟩ := h
59-
cases n with
60-
| zero => ring_nf at *; tauto
61-
| succ n => forward h
62-
cases n with
63-
| zero => ring_nf at *
64-
forward h
65-
forward h
66-
forward h
67-
use l
68-
simp [h]
69-
simp [collatz]
70-
| succ n => obtain ⟨k, h_odd⟩ := h_odd
71-
cases k with
72-
| zero => omega
73-
| succ k =>
74-
have h_odd : n = 2 * k+1 := by omega
75-
subst n
76-
forward h
77-
rw [← List.replicate_succ] at h
78-
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
79-
apply B_odd at h
80-
. forward h
81-
have g : (2 +k*2) /2 = k + 1:= by omega
82-
rw [g] at h
83-
rw [List.replicate_succ] at h
84-
simp at h
85-
rw [← List.replicate_succ] at h
86-
apply copy_half at h
87-
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
88-
apply G_to_J at h
89-
forward h
90-
ring_nf at *
91-
have g : (i + (40 + k * 44 + k ^ 2 * 12) / 2) = (16 + i + k * 13 + k ^ 2 * 4 + (8 + k * 18 + k ^ 2 * 4) / 2) := by omega
92-
rw [g]
93-
use l
94-
simp [h]
95-
simp [collatz]
96-
rw [← List.replicate_one]
97-
rw [List.replicate_append_replicate]
98-
rw [← List.replicate_succ]
99-
apply congr
100-
any_goals rfl
101-
apply congr
102-
any_goals rfl
103-
apply congr
104-
any_goals rfl
105-
omega
106-
. use k; omega
68+
match n with
69+
| 0 => tauto
70+
| 1 => forward h
71+
ring_nf at *
72+
forward h
73+
forward h
74+
forward h
75+
use l
76+
simp [h]
77+
simp [collatz]
78+
| Nat.succ (Nat.succ n) =>
79+
forward h
80+
obtain ⟨k, h_odd⟩ := h_odd
81+
cases k with
82+
| zero => omega
83+
| succ k =>
84+
have h_odd : n = 2 * k+1 := by omega
85+
subst n
86+
forward h
87+
rw [← List.replicate_succ] at h
88+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
89+
apply B_odd at h
90+
. forward h
91+
have g : (2 +k*2) /2 = k + 1:= by omega
92+
rw [g] at h
93+
rw [List.replicate_succ] at h
94+
simp at h
95+
rw [← List.replicate_succ] at h
96+
apply copy_half at h
97+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
98+
apply G_to_J at h
99+
forward h
100+
ring_nf at *
101+
have g : i + (1 + (1 + k * 2).succ.succ * 4 + (1 + k * 2).succ.succ ^ 2 * 3) / 2 = 16 + i + k * 13 + k ^ 2 * 4 + (8 + k * 18 + k ^ 2 * 4) / 2 := by
102+
simp
103+
ring_nf
104+
calc
105+
_ = i + 20 + 22 * k + 6 * k^2 := by omega
106+
_ = 16 + i + k * 13 + k ^ 2 * 4 + 4 + k * 9 + k ^ 2 * 2 := by ring_nf
107+
_ = _ := by omega
108+
rw [g]
109+
use l
110+
simp [h]
111+
simp [collatz]
112+
ring_nf
113+
simp
114+
rw [← List.replicate_one]
115+
rw [List.replicate_append_replicate]
116+
rw [← List.replicate_succ]
117+
apply congr
118+
any_goals rfl
119+
apply congr
120+
any_goals rfl
121+
apply congr
122+
any_goals rfl
123+
omega
124+
. use k; omega
107125

108126
-- n -> collatz n
109127
theorem G_collatz (n i: ℕ) (init_cfg: Cfg)

0 commit comments

Comments
 (0)