Skip to content

Commit

Permalink
25 states is enough
Browse files Browse the repository at this point in the history 
no 16

merge 16 to 4
  • Loading branch information
@lengyijun
lengyijun committed Nov 17, 2024
1 parent b084c1a commit faef093
Show file tree
Hide file tree
Showing 14 changed files with 464 additions and 151 deletions.
240 changes: 240 additions & 0 deletions 26_to_25.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,240 @@
# How I reduce 26 states to 25 states

Notice 16.1 is unreachable.

So we need to find state X where X.0 is unreachable so that we can merge X and 16.


1. `lake exe sim26 > /tmp/log/26` to collect 100M logs.

2. I use this script to list all possible triples X-Y-Z where (X.0 -> Y OR X.1 -> Y) AND (Y.0 -> Z OR Y.1 -> Z)

```
import GoldbachTm.Tm26.TuringMachine26
import GoldbachTm.Basic
import Init.Data.List.Basic
open Tm26
unsafe def foo (cfg : Cfg) : IO Unit :=
match (step machine cfg) with
| some cfg => do
IO.println s!"{cfg}"
foo cfg
| none => IO.println s!"halt"
unsafe def bar : (zs: List (Fin 26 × Fin 26 × Fin 26 × Stmt)) -> IO Unit
| [] => pure ()
| ⟨a, b, c, _⟩ :: zs =>
if b < 10 then
if c < 10 then
do
IO.println s!"'rg --multiline -l \"{a}.*\\n {b}.*\\n {c}\"'"
bar zs
else
do
IO.println s!"'rg --multiline -l \"{a}.*\\n {b}.*\\n{c}\"'"
bar zs
else
if c < 10 then
do
IO.println s!"'rg --multiline -l \"{a}.*\\n{b}.*\\n {c}\"'"
bar zs
else
do
IO.println s!"'rg --multiline -l \"{a}.*\\n{b}.*\\n{c}\"'"
bar zs
unsafe def main : List String → IO Unit
| _ => let x : List (Fin 26) := [
⟨0, by omega⟩,
⟨1, by omega⟩,
⟨2, by omega⟩,
⟨3, by omega⟩,
⟨4, by omega⟩,
⟨5, by omega⟩,
⟨6, by omega⟩,
⟨7, by omega⟩,
⟨8, by omega⟩,
⟨9, by omega⟩,
⟨10, by omega⟩,
⟨11, by omega⟩,
⟨12, by omega⟩,
⟨13, by omega⟩,
⟨14, by omega⟩,
⟨15, by omega⟩,
⟨16, by omega⟩,
⟨17, by omega⟩,
⟨18, by omega⟩,
⟨19, by omega⟩,
⟨20, by omega⟩,
⟨21, by omega⟩,
⟨22, by omega⟩,
⟨23, by omega⟩,
⟨24, by omega⟩,
⟨25, by omega⟩,
]
let y := x.map (fun q => [
(machine q Γ.zero).map (fun ⟨a, b⟩ => (q, a)),
(machine q Γ.one).map (fun ⟨a, b⟩ => (q, a))
])
let z := y.flatten.reduceOption
let z := z.map (fun ⟨q1, q2⟩ => [
(machine q2 Γ.zero).map (fun c => (q1, q2, c)),
(machine q2 Γ.one).map (fun c => (q1, q2, c)),
])
let z := z.flatten.reduceOption
bar z
```

```
#!/bin/bash
# /tmp/b.sh
# List of commands
commands=(
'rg --multiline -l "0.*\n23.*\n24"'
'rg --multiline -l "0.*\n23.*\n23"'
'rg --multiline -l "0.*\n 1.*\n17"'
'rg --multiline -l "0.*\n 1.*\n 2"'
'rg --multiline -l "1.*\n17.*\n18"'
'rg --multiline -l "1.*\n17.*\n17"'
'rg --multiline -l "1.*\n 2.*\n21"'
'rg --multiline -l "1.*\n 2.*\n 3"'
'rg --multiline -l "2.*\n21.*\n24"'
'rg --multiline -l "2.*\n21.*\n21"'
'rg --multiline -l "2.*\n 3.*\n21"'
'rg --multiline -l "2.*\n 3.*\n 4"'
'rg --multiline -l "3.*\n21.*\n24"'
'rg --multiline -l "3.*\n21.*\n21"'
'rg --multiline -l "3.*\n 4.*\n 9"'
'rg --multiline -l "3.*\n 4.*\n 5"'
'rg --multiline -l "4.*\n 9.*\n10"'
'rg --multiline -l "4.*\n 9.*\n22"'
'rg --multiline -l "4.*\n 5.*\n 4"'
'rg --multiline -l "4.*\n 5.*\n 5"'
'rg --multiline -l "5.*\n 4.*\n 9"'
'rg --multiline -l "5.*\n 4.*\n 5"'
'rg --multiline -l "5.*\n 5.*\n 4"'
'rg --multiline -l "5.*\n 5.*\n 5"'
'rg --multiline -l "6.*\n 8.*\n 9"'
'rg --multiline -l "6.*\n 8.*\n 8"'
'rg --multiline -l "6.*\n 7.*\n 9"'
'rg --multiline -l "6.*\n 7.*\n 7"'
'rg --multiline -l "7.*\n 9.*\n10"'
'rg --multiline -l "7.*\n 9.*\n22"'
'rg --multiline -l "7.*\n 7.*\n 9"'
'rg --multiline -l "7.*\n 7.*\n 7"'
'rg --multiline -l "8.*\n 9.*\n10"'
'rg --multiline -l "8.*\n 9.*\n22"'
'rg --multiline -l "8.*\n 8.*\n 9"'
'rg --multiline -l "8.*\n 8.*\n 8"'
'rg --multiline -l "9.*\n10.*\n10"'
'rg --multiline -l "9.*\n10.*\n11"'
'rg --multiline -l "9.*\n22.*\n18"'
'rg --multiline -l "9.*\n22.*\n22"'
'rg --multiline -l "10.*\n10.*\n10"'
'rg --multiline -l "10.*\n10.*\n11"'
'rg --multiline -l "10.*\n11.*\n12"'
'rg --multiline -l "10.*\n11.*\n11"'
'rg --multiline -l "11.*\n12.*\n14"'
'rg --multiline -l "11.*\n12.*\n13"'
'rg --multiline -l "11.*\n11.*\n12"'
'rg --multiline -l "11.*\n11.*\n11"'
'rg --multiline -l "12.*\n14.*\n15"'
'rg --multiline -l "12.*\n14.*\n14"'
'rg --multiline -l "12.*\n13.*\n 6"'
'rg --multiline -l "12.*\n13.*\n13"'
'rg --multiline -l "13.*\n 6.*\n 8"'
'rg --multiline -l "13.*\n 6.*\n 7"'
'rg --multiline -l "13.*\n13.*\n 6"'
'rg --multiline -l "13.*\n13.*\n13"'
'rg --multiline -l "14.*\n15.*\n16"'
'rg --multiline -l "14.*\n15.*\n19"'
'rg --multiline -l "14.*\n14.*\n15"'
'rg --multiline -l "14.*\n14.*\n14"'
'rg --multiline -l "15.*\n16.*\n17"'
'rg --multiline -l "15.*\n19.*\n20"'
'rg --multiline -l "15.*\n19.*\n19"'
'rg --multiline -l "16.*\n17.*\n18"'
'rg --multiline -l "16.*\n17.*\n17"'
'rg --multiline -l "17.*\n18.*\n 9"'
'rg --multiline -l "17.*\n18.*\n25"'
'rg --multiline -l "17.*\n17.*\n18"'
'rg --multiline -l "17.*\n17.*\n17"'
'rg --multiline -l "18.*\n 9.*\n10"'
'rg --multiline -l "18.*\n 9.*\n22"'
'rg --multiline -l "18.*\n25.*\n24"'
'rg --multiline -l "19.*\n20.*\n 2"'
'rg --multiline -l "19.*\n20.*\n20"'
'rg --multiline -l "19.*\n19.*\n20"'
'rg --multiline -l "19.*\n19.*\n19"'
'rg --multiline -l "20.*\n 2.*\n21"'
'rg --multiline -l "20.*\n 2.*\n 3"'
'rg --multiline -l "20.*\n20.*\n 2"'
'rg --multiline -l "20.*\n20.*\n20"'
'rg --multiline -l "21.*\n24.*\n 0"'
'rg --multiline -l "21.*\n24.*\n24"'
'rg --multiline -l "21.*\n21.*\n24"'
'rg --multiline -l "21.*\n21.*\n21"'
'rg --multiline -l "22.*\n18.*\n 9"'
'rg --multiline -l "22.*\n18.*\n25"'
'rg --multiline -l "22.*\n22.*\n18"'
'rg --multiline -l "22.*\n22.*\n22"'
'rg --multiline -l "23.*\n24.*\n 0"'
'rg --multiline -l "23.*\n24.*\n24"'
'rg --multiline -l "23.*\n23.*\n24"'
'rg --multiline -l "23.*\n23.*\n23"'
'rg --multiline -l "24.*\n 0.*\n23"'
'rg --multiline -l "24.*\n 0.*\n 1"'
'rg --multiline -l "24.*\n24.*\n 0"'
'rg --multiline -l "24.*\n24.*\n24"'
'rg --multiline -l "25.*\n24.*\n 0"'
'rg --multiline -l "25.*\n24.*\n24"'
)
# Execute commands
for cmd in "${commands[@]}"; do
output=$(eval "$cmd")
if [ -z "$output" ]; then
echo "$cmd"
fi
done
```

```
cd /tmp/log/26
bash /tmp/b.sh
```

We got thost unvisited triples :

```
rg --multiline -l "5.*\n 4.*\n 5"
rg --multiline -l "3.*\n 4.*\n 9"
rg --multiline -l "23.*\n24.*\n 0"
rg --multiline -l "25.*\n24.*\n24"
rg --multiline -l "4.*\n 9.*\n22"
rg --multiline -l "7.*\n 9.*\n22"
rg --multiline -l "18.*\n 9.*\n10"
rg --multiline -l "20.*\n 2.*\n21"
rg --multiline -l "4.*\n 5.*\n 4"
rg --multiline -l "6.*\n 8.*\n 9"
rg --multiline -l "12.*\n13.*\n 6"
rg --multiline -l "12.*\n14.*\n15"
rg --multiline -l "16.*\n17.*\n18"
rg --multiline -l "22.*\n18.*\n 9"
rg --multiline -l "19.*\n20.*\n 2"
rg --multiline -l "3.*\n21.*\n24"
rg --multiline -l "9.*\n22.*\n18"
```

We notice that state 4 maybe the optimizer.

14 changes: 7 additions & 7 deletions GoldbachTm.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,13 @@ import GoldbachTm.Basic
import GoldbachTm.Format
import GoldbachTm.ListBlank

import GoldbachTm.Tm26.TuringMachine26
import GoldbachTm.Tm26.Search0
import GoldbachTm.Tm26.Transition
import GoldbachTm.Tm26.Miscellaneous
import GoldbachTm.Tm26.Prime
import GoldbachTm.Tm26.PBP
import GoldbachTm.Tm26.Content
import GoldbachTm.Tm25.TuringMachine25
import GoldbachTm.Tm25.Search0
import GoldbachTm.Tm25.Transition
import GoldbachTm.Tm25.Miscellaneous
import GoldbachTm.Tm25.Prime
import GoldbachTm.Tm25.PBP
import GoldbachTm.Tm25.Content

import GoldbachTm.Tm31.TuringMachine31
import GoldbachTm.Tm31.Search0
Expand Down
2 changes: 1 addition & 1 deletion GoldbachTm/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ induction n with

/-
P i => nth_cfg i ≠ none
Q i n => nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
Q i n => nth_cfg i = some ⟨⟨24, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
-/
theorem propagating_induction (P : ℕ → Prop) (Q : ℕ → ℕ → Prop)
(base : ℕ) (hbase : Q base 0)
Expand Down
30 changes: 15 additions & 15 deletions GoldbachTm/Tm26/Content.lean → GoldbachTm/Tm25/Content.lean
View file
Original file line number Diff line number Diff line change
@@ -1,20 +1,20 @@
import GoldbachTm.Tm26.TuringMachine26
import GoldbachTm.Tm26.Search0
import GoldbachTm.Tm26.PBP
import GoldbachTm.Tm25.TuringMachine25
import GoldbachTm.Tm25.Search0
import GoldbachTm.Tm25.PBP
import Mathlib.Data.Nat.Prime.Defs

namespace Tm26
namespace Tm25

theorem lemma_22 (n : ℕ) (i : ℕ)
theorem lemma_21 (n : ℕ) (i : ℕ)
(even_n : Even (n+2))
(g :
nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
( hpp : Goldbach (n+4)) :
∃ j>i, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
∃ j>i, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
:= by
forward g
repeat rw [← List.replicate_succ] at g
apply (leap_18 _ _ 0) at g
apply (leap_17 _ _ 0) at g
any_goals omega
any_goals assumption
refine (?_ ∘ g) ?_
Expand All @@ -40,7 +40,7 @@ refine (?_ ∘ g) ?_

lemma never_halt_step (n : ℕ) :
(∀ i < n, Goldbach (2*i+4)) ->
∃ j, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
∃ j, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
:= by
induction n with
| zero =>
Expand All @@ -54,7 +54,7 @@ refine (?_ ∘ induction_step) ?_
. intros g
obtain ⟨j, g⟩ := g
specialize h n (by omega)
apply lemma_22 at g
apply lemma_21 at g
. specialize g h
obtain ⟨k, g⟩ := g
use k
Expand All @@ -73,7 +73,7 @@ apply never_halt_step at IH
obtain ⟨j, g⟩ := IH
forward g
repeat rw [← List.replicate_succ] at g
apply (leap_18_halt _ _ 0) at g
apply (leap_17_halt _ _ 0) at g
any_goals omega
by_contra! h
refine (?_ ∘ g) ?_
Expand All @@ -88,10 +88,10 @@ refine (?_ ∘ g) ?_

theorem halt_lemma_rev' (h : ∀ n, Goldbach (2*n+4)) :
∀ i, nth_cfg i ≠ none := by
apply propagating_induction (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩) 45
apply propagating_induction (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩) 45
. simp [cfg45]; tauto
. intros i n g
apply (lemma_22 (2*n)) at g
apply (lemma_21 (2*n)) at g
. specialize g (h _)
obtain ⟨j, g⟩ := g
use j
Expand Down Expand Up @@ -120,7 +120,7 @@ by rw [← Mathlib.Tactic.PushNeg.not_not_eq (Goldbach (2*i+4))]
)
forward hj
repeat rw [← List.replicate_succ] at hj
apply (leap_18_halt _ _ 0) at hj
apply (leap_17_halt _ _ 0) at hj
any_goals omega
apply hj
intros x y _
Expand All @@ -135,4 +135,4 @@ by_contra! g
apply halt_lemma_rev' at g
tauto

end Tm26
end Tm25
10 changes: 5 additions & 5 deletions GoldbachTm/Tm26/Miscellaneous.lean → GoldbachTm/Tm25/Miscellaneous.lean
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
-- some lemmas tm31 doesn't contain

import GoldbachTm.Tm26.TuringMachine26
import GoldbachTm.Tm26.Transition
import GoldbachTm.Tm25.TuringMachine25
import GoldbachTm.Tm25.Transition

namespace Tm26
namespace Tm25

theorem lemma7 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨7, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
Expand Down Expand Up @@ -39,7 +39,7 @@ induction k with (intros i l r h; simp_all)

theorem lemma5 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨5, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
nth_cfg (i + k + 2) = some ⟨⟨4, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
nth_cfg (i + k + 2) = some ⟨⟨7, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
induction k with (intros i l r h; simp_all)
| zero => iterate 2 forward h
rw [← h]
Expand Down Expand Up @@ -111,4 +111,4 @@ cases r1 with simp_all
simp [h]
omega

end Tm26
end Tm25
Loading

0 comments on commit faef093

Please sign in to comment.