Skip to content

Commit 1605e24

Browse files
lengyijunlengyijun
committed
16 stmt => 15 stmt
E.0 is unreachable
1 parent a522b6d commit 1605e24

File tree

6 files changed

+11
-121
lines changed

6 files changed

+11
-121
lines changed

‎CollatzFunction/Tm8/Main.lean‎

Lines changed: 4 additions & 111 deletions
Original file line numberDiff line numberDiff line change
@@ -18,119 +18,15 @@ theorem G_collatz (n i: ℕ) (init_cfg: Cfg)
1818
:= by
1919
obtain ⟨l, h⟩ := h
2020
-- somehow surprise, the proof of `inl h` and `inr h` are the same
21-
cases h with
22-
| inl h => cases n with
21+
cases n with
2322
| zero => forward h
2423
forward h
25-
use (2+i)
26-
constructor
27-
any_goals omega
28-
use l
29-
left
30-
unfold collatz
31-
simp [h]
32-
simp! [Turing.ListBlank.mk]
33-
rw [Quotient.eq'']
34-
right
35-
use 1
36-
tauto
37-
| succ n => forward h
38-
cases n with
39-
| zero => simp at h
40-
forward h
41-
forward h
42-
forward h
43-
use (4+i)
44-
constructor
45-
any_goals omega
46-
use l
47-
right
48-
unfold collatz
49-
simp [h]
50-
| succ n => forward h
51-
unfold collatz
52-
split_ifs <;> rename_i g
53-
. rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
54-
apply B_even at h
55-
obtain ⟨j, _, h⟩ := h
56-
forward h
57-
rw [add_comm 1 (n/2)] at h
58-
rw [List.replicate_succ] at h
59-
simp at h
60-
forward h
61-
use (2+j)
62-
constructor
63-
any_goals omega
64-
use (List.replicate (n / 2) one ++ zero :: zero :: l)
65-
left
66-
simp [h]
67-
rw [← List.replicate_succ]
68-
apply congr
69-
any_goals rfl
70-
apply congr
71-
any_goals rfl
72-
apply congr
73-
any_goals rfl
74-
omega
75-
rw [← Nat.even_iff] at g
76-
obtain ⟨a, g⟩ := g
77-
cases a with
78-
| zero => omega
79-
| succ a => use a; omega
80-
. rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
81-
apply B_odd at h
82-
obtain ⟨j, _, h⟩ := h
83-
forward h
84-
cases n with
85-
| zero => omega
86-
| succ n =>
87-
ring_nf at h
88-
have g : (2+n)/2 = n/2 + 1:= by omega
89-
rw [g] at h
90-
rw [List.replicate_succ] at h
91-
simp at h
92-
rw [← List.replicate_succ] at h
93-
apply copy_half at h
94-
rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
95-
apply G_to_J at h
96-
forward h
97-
use (10 + j + n / 2 * 13 + (n / 2) ^ 2 * 4)
98-
constructor
99-
any_goals omega
100-
use l
101-
right
102-
simp [h]
103-
apply congr
104-
any_goals rfl
105-
rw [← List.replicate_one]
106-
rw [List.replicate_append_replicate]
107-
rw [← List.replicate_succ]
108-
apply congr
109-
any_goals rfl
110-
apply congr
111-
any_goals rfl
112-
omega
113-
have g : (n+2) % 2 = 1 := by omega
114-
rw [← Nat.odd_iff] at g
115-
obtain ⟨a, g⟩ := g
116-
cases a with
117-
| zero => omega
118-
| succ a => use a; omega
119-
| inr h => cases n with
120-
| zero => forward h
12124
forward h
122-
use (2+i)
123-
constructor
124-
any_goals omega
125-
use l
126-
left
25+
use (3+i)
12726
unfold collatz
27+
simp
28+
use (zero :: l)
12829
simp [h]
129-
simp! [Turing.ListBlank.mk]
130-
rw [Quotient.eq'']
131-
right
132-
use 1
133-
tauto
13430
| succ n => forward h
13531
cases n with
13632
| zero => simp at h
@@ -141,7 +37,6 @@ cases h with
14137
constructor
14238
any_goals omega
14339
use l
144-
right
14540
unfold collatz
14641
simp [h]
14742
| succ n => forward h
@@ -159,7 +54,6 @@ cases h with
15954
constructor
16055
any_goals omega
16156
use (List.replicate (n / 2) one ++ zero :: zero :: l)
162-
left
16357
simp [h]
16458
rw [← List.replicate_succ]
16559
apply congr
@@ -195,7 +89,6 @@ cases h with
19589
constructor
19690
any_goals omega
19791
use l
198-
right
19992
simp [h]
20093
apply congr
20194
any_goals rfl

‎CollatzFunction/Tm8/Representation.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ open Lean Meta Elab Tactic Std Term TmState Γ
1313
-- `nth_cfg i cfg` represent `n`
1414
def nth_cfg_is_n (i n: Nat) (init_cfg : Cfg) :=
1515
∃ l,
16-
nth_cfg init_cfg i = ⟨E, ⟨zero, Turing.ListBlank.mk (zero :: l), Turing.ListBlank.mk (List.replicate n one)⟩⟩ \/
1716
nth_cfg init_cfg i = ⟨G, ⟨zero, Turing.ListBlank.mk (zero :: l), Turing.ListBlank.mk (List.replicate n one)⟩⟩
1817

1918
end Tm8

‎CollatzFunction/Tm8/TuringMachine8.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ instance : ToString Cfg where
5252
s!"{q} {s}"
5353

5454
/-- The initial configuration. -/
55-
def init (l : List Γ) : Cfg := ⟨TmState.E, Turing.Tape.mk₁ l⟩
55+
def init (l : List Γ) : Cfg := ⟨TmState.G, Turing.Tape.mk₁ l⟩
5656

5757
/-- Execution semantics of the Turing machine. -/
5858
def step (M : Machine) : Cfg → Cfg :=
@@ -71,8 +71,8 @@ def machine : Machine
7171
| C, Γ.one => ⟨D, ⟨Turing.Dir.left, Γ.zero⟩⟩
7272
| D, Γ.zero => ⟨A, ⟨Turing.Dir.right, Γ.one⟩⟩
7373
| D, Γ.one => ⟨D, ⟨Turing.Dir.left, Γ.one⟩⟩
74-
| E, Γ.zero => ⟨A, ⟨Turing.Dir.right, Γ.zero⟩⟩
75-
| E, Γ.one => ⟨E, ⟨Turing.Dir.right, Γ.zero⟩⟩
74+
| E, Γ.zero => ⟨G, ⟨Turing.Dir.right, Γ.zero⟩⟩ -- only used in `collatz 0`
75+
| E, Γ.one => ⟨G, ⟨Turing.Dir.right, Γ.zero⟩⟩
7676
| G, Γ.zero => ⟨A, ⟨Turing.Dir.right, Γ.zero⟩⟩
7777
| G, Γ.one => ⟨H, ⟨Turing.Dir.right, Γ.zero⟩⟩
7878
| H, Γ.zero => ⟨J, ⟨Turing.Dir.left, Γ.one⟩⟩

‎README.md‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,17 +18,13 @@ A B C D E G H J are 8 states.
1818
- 1 states (E) for even cases
1919
- 3 states (G, H, J) for odd cases
2020

21-
`000 (0F) 000` denotes 0
22-
2321
`000 (0G) 000` denotes 0
2422

25-
`000 (0F)1^n 000` denotes n
26-
2723
`000 (0G)1^n 000` denotes n
2824

2925
let b = collatz n
3026

31-
`000 (0F)1^n 000` -> `000 (0F)1^b 000` or `000 (0G)1^b 000`
27+
`000 (0G)1^n 000` -> `000 (0G)1^b 000`
3228

3329
## Comparsion to previous results
3430

‎table.pdf‎

133 Bytes
Binary file not shown.

‎table.tex‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@
6666
\hline
6767
$D$ & 1R$A$ & 1L$D$ \\
6868
\hline
69-
$E$ & 0R$A$ & 0R$E$ \\
69+
$E$ & --- & 0R$G$ \\
7070
\hline
7171
$G$ & 0R$A$ & 0R$H$ \\
7272
\hline
@@ -77,6 +77,8 @@
7777
\end{tabular}
7878
\end{center}
7979

80+
--- means unreachable: any write, move and states is ok
81+
8082
\begin{thebibliography}{99}
8183
\bibitem{Ba98} C.\ Baiocchi, 3N+1, UTM e Tag-systems (Italian),
8284
Dipartimento di Matematica dell'Universit\`a ``La Sapienza'' di Roma {\bf 98/38}, 1998.

0 commit comments

Comments
 (0)