Skip to content

Commit c827678

Browse files
lengyijunlengyijun
committed
G_even, G_odd
1 parent ceb6998 commit c827678

File tree

1 file changed

+109
-87
lines changed

1 file changed

+109
-87
lines changed

‎CollatzFunction/Tm8/Main.lean‎

Lines changed: 109 additions & 87 deletions
Original file line numberDiff line numberDiff line change
@@ -11,97 +11,119 @@ namespace Tm8
1111

1212
open Lean Meta Elab Tactic Std Term TmState Γ
1313

14+
lemma G_even (n i: ℕ) (h_even: Even n) (init_cfg: Cfg)
15+
(h: nth_cfg_is_n i n init_cfg) :
16+
nth_cfg_is_n (i+(n^2+3*n)/2+3) (collatz n) init_cfg
17+
:= by
18+
obtain ⟨l, h⟩ := h
19+
cases n with
20+
| zero => unfold collatz nth_cfg_is_n
21+
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
53+
54+
lemma G_odd (n i: ℕ) (h_odd: Odd n) (init_cfg: Cfg)
55+
(h: nth_cfg_is_n i n init_cfg) :
56+
nth_cfg_is_n (i+(3 * n^2+4*n+1)/2) (collatz n) init_cfg
57+
:= by
58+
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
107+
14108
-- n -> collatz n
15109
theorem G_collatz (n i: ℕ) (init_cfg: Cfg)
16110
(h: nth_cfg_is_n i n init_cfg) :
17111
∃ j>i, nth_cfg_is_n j (collatz n) init_cfg
18112
:= by
19-
obtain ⟨l, h⟩ := h
20-
cases n with
21-
| zero => forward h
22-
forward h
23-
forward h
24-
use (3+i)
25-
unfold collatz
26-
simp
27-
use (zero :: l)
28-
simp [h]
29-
| succ n => forward h
30-
cases n with
31-
| zero => simp at h
32-
forward h
33-
forward h
34-
forward h
35-
use (4+i)
36-
constructor
37-
any_goals omega
38-
use l
39-
unfold collatz
40-
simp [h]
41-
| succ n => forward h
42-
unfold collatz
43-
split_ifs <;> rename_i g
44-
. rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
45-
apply B_even at h
46-
forward h
47-
rw [add_comm 1 (n/2)] at h
48-
rw [List.replicate_succ] at h
49-
simp at h
50-
forward h
51-
use (8 + i + n ^ 2 / 2 + n * 7 / 2)
52-
constructor
53-
any_goals omega
54-
use (List.replicate (n / 2) one ++ zero :: zero :: l)
55-
simp [h]
56-
rw [← List.replicate_succ]
57-
apply congr
58-
any_goals rfl
59-
apply congr
60-
any_goals rfl
61-
apply congr
62-
any_goals rfl
63-
omega
64-
rw [← Nat.even_iff] at g
65-
obtain ⟨a, g⟩ := g
66-
cases a with
67-
| zero => omega
68-
| succ a => use a; omega
69-
. rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
70-
apply B_odd at h
71-
forward h
72-
cases n with
73-
| zero => omega
74-
| succ n =>
75-
ring_nf at h
76-
have g : (2+n)/2 = n/2 + 1:= by omega
77-
rw [g] at h
78-
rw [List.replicate_succ] at h
79-
simp at h
80-
rw [← List.replicate_succ] at h
81-
apply copy_half at h
82-
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
83-
apply G_to_J at h
84-
forward h
85-
use (16 + i + (8 + n * 9 + n ^ 2) / 2 + n / 2 * 13 + (n / 2) ^ 2 * 4)
86-
constructor
87-
any_goals omega
88-
use l
89-
simp [h]
90-
apply congr
91-
any_goals rfl
92-
rw [← List.replicate_one]
93-
rw [List.replicate_append_replicate]
94-
rw [← List.replicate_succ]
95-
apply congr
96-
any_goals rfl
97-
apply congr
98-
any_goals rfl
99-
omega
100-
have g : (n+2) % 2 = 1 := by omega
101-
rw [← Nat.odd_iff] at g
102-
obtain ⟨a, g⟩ := g
103-
cases a with
104-
| zero => omega
105-
| succ a => use a; omega
113+
cases (Nat.even_or_odd n) with
114+
| inl _ => apply G_even at h
115+
any_goals assumption
116+
use (i + (n ^ 2 + 3 * n) / 2 + 3)
117+
constructor
118+
. omega
119+
. simp [h]
120+
| inr _ => apply G_odd at h
121+
any_goals assumption
122+
use (i + (3 * n ^ 2 + 4 * n + 1) / 2)
123+
constructor
124+
. cases n with
125+
| zero => tauto
126+
| succ n => omega
127+
. simp [h]
106128

107129
end Tm8

0 commit comments

Comments
 (0)