Skip to content

Commit 54f324b

Browse files
lengyijunlengyijun
committed
cases => match
1 parent 1326217 commit 54f324b

File tree

1 file changed

+100
-81
lines changed

1 file changed

+100
-81
lines changed

‎CollatzFunction/Tm8/Main.lean‎

Lines changed: 100 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ import CollatzFunction.Tm8.Transition
66
import CollatzFunction.Tm8.Representation
77
import CollatzFunction.Collatz
88
import CollatzFunction.ListBlank
9+
import Mathlib.Tactic.Zify
910

1011
namespace Tm8
1112

@@ -16,94 +17,112 @@ lemma G_even (n i: ℕ) (h_even: Even n) (init_cfg: Cfg)
1617
nth_cfg_is_n (i+(n^2+3*n)/2+3) (collatz n) init_cfg
1718
:= by
1819
obtain ⟨l, h⟩ := h
19-
cases n with
20-
| zero => unfold collatz nth_cfg_is_n
20+
match n with
21+
| 0 => unfold collatz nth_cfg_is_n
22+
simp
23+
forward h
24+
forward h
25+
forward h
26+
ring_nf at *
27+
simp [h]
28+
use (zero :: l)
29+
| 1 => tauto
30+
| Nat.succ (Nat.succ n) =>
31+
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+
forward h
39+
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
40+
apply B_even at h
41+
. forward h
42+
rw [add_comm 1] at h
43+
rw [List.replicate_succ] at h
44+
simp at h
45+
forward h
46+
ring_nf at *
47+
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
2148
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
49+
ring_nf
50+
calc
51+
_ = 3 + i + 5 + k * 7 + 2 * k ^ 2 := by omega
52+
_ = 8 + i + k ^ 2 * 2 + k * 7 := by ring_nf
53+
_ = _ := by omega
54+
rw [g]
55+
use (List.replicate k one ++ zero :: zero :: l)
56+
simp [h]
57+
simp [collatz]
58+
ring_nf
59+
simp
60+
rw [List.replicate_succ]
61+
. use k; omega
62+
5363

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

108127
-- n -> collatz n
109128
theorem G_collatz (n i: ℕ) (init_cfg: Cfg)

0 commit comments

Comments
 (0)