rename

lengyijun · Nov 16, 2024 · d776c1e · d776c1e
1 parent 2328ce5
commit d776c1e
Show file tree

Hide file tree

Showing 11 changed files with 47 additions and 45 deletions.
diff --git a/GoldbachTm.lean b/GoldbachTm.lean
@@ -4,13 +4,13 @@ import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
 
-import GoldbachTm.Tm27.TuringMachine27
-import GoldbachTm.Tm27.Search0
-import GoldbachTm.Tm27.Transition
-import GoldbachTm.Tm27.Miscellaneous
-import GoldbachTm.Tm27.Prime
-import GoldbachTm.Tm27.PBP
-import GoldbachTm.Tm27.Content
+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.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Search0

diff --git a/GoldbachTm/Tm27/Content.lean → GoldbachTm/Tm26/Content.lean b/GoldbachTm/Tm27/Content.lean → GoldbachTm/Tm26/Content.lean
@@ -1,9 +1,9 @@
-import GoldbachTm.Tm27.TuringMachine27
-import GoldbachTm.Tm27.Search0
-import GoldbachTm.Tm27.PBP
+import GoldbachTm.Tm26.TuringMachine26
+import GoldbachTm.Tm26.Search0
+import GoldbachTm.Tm26.PBP
 import Mathlib.Data.Nat.Prime.Defs
 
-namespace Tm27
+namespace Tm26
 
 theorem lemma_22 (n : ℕ) (i : ℕ)
 (even_n : Even (n+2))
@@ -135,4 +135,4 @@ by_contra! g
 apply halt_lemma_rev' at g
 tauto
 
-end Tm27
+end Tm26
diff --git a/GoldbachTm/Tm27/Miscellaneous.lean → GoldbachTm/Tm26/Miscellaneous.lean b/GoldbachTm/Tm27/Miscellaneous.lean → GoldbachTm/Tm26/Miscellaneous.lean
@@ -1,9 +1,9 @@
 -- some lemmas tm31 doesn't contain
 
-import GoldbachTm.Tm27.TuringMachine27
-import GoldbachTm.Tm27.Transition
+import GoldbachTm.Tm26.TuringMachine26
+import GoldbachTm.Tm26.Transition
 
-namespace Tm27
+namespace Tm26
 
 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⟩⟩ →
@@ -111,4 +111,4 @@ cases r1 with simp_all
              simp [h]
              omega
 
-end Tm27
+end Tm26
diff --git a/GoldbachTm/Tm27/PBP.lean → GoldbachTm/Tm26/PBP.lean b/GoldbachTm/Tm27/PBP.lean → GoldbachTm/Tm26/PBP.lean
@@ -1,10 +1,10 @@
 -- PDP is short for "prime board prime"
-import GoldbachTm.Tm27.TuringMachine27
-import GoldbachTm.Tm27.Search0
-import GoldbachTm.Tm27.Prime
+import GoldbachTm.Tm26.TuringMachine26
+import GoldbachTm.Tm26.Search0
+import GoldbachTm.Tm26.Prime
 import Mathlib.Data.Nat.Prime.Defs
 
-namespace Tm27
+namespace Tm26
 
 -- l1 : count of 1 on the left
 -- r1 : count of 1 on the right
@@ -293,4 +293,4 @@ induction l1 with
       ring_nf
       tauto
 
-end Tm27
+end Tm26
diff --git a/GoldbachTm/Tm27/Prime.lean → GoldbachTm/Tm26/Prime.lean b/GoldbachTm/Tm27/Prime.lean → GoldbachTm/Tm26/Prime.lean
@@ -1,8 +1,8 @@
-import GoldbachTm.Tm27.TuringMachine27
-import GoldbachTm.Tm27.Transition
-import GoldbachTm.Tm27.Miscellaneous
+import GoldbachTm.Tm26.TuringMachine26
+import GoldbachTm.Tm26.Transition
+import GoldbachTm.Tm26.Miscellaneous
 
-namespace Tm27
+namespace Tm26
 
 -- c1++, c2++
 --    l 0 [la 11] 0  [lb 11] 0 [ra 11111] 0  [(rb+1) 1] 0 r
@@ -462,4 +462,4 @@ match r1 with
     rw [g] at h
     exact h
 
-end Tm27
+end Tm26
diff --git a/GoldbachTm/Tm27/Search0.lean → GoldbachTm/Tm26/Search0.lean b/GoldbachTm/Tm27/Search0.lean → GoldbachTm/Tm26/Search0.lean
@@ -1,8 +1,8 @@
 -- theorem of recursive states
 -- all these states' usage is to search 0
-import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm26.TuringMachine26
 
-namespace Tm27
+namespace Tm26
 
 -- left
 theorem rec13 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
@@ -126,4 +126,4 @@ induction k with intros i l r h
             . simp [List.replicate_succ' (k+1)]
             . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
 
-end Tm27
+end Tm26
diff --git a/GoldbachTm/Tm27/Sim27.lean → GoldbachTm/Tm26/Sim26.lean b/GoldbachTm/Tm27/Sim27.lean → GoldbachTm/Tm26/Sim26.lean
@@ -1,7 +1,7 @@
-import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm26.TuringMachine26
 import GoldbachTm.Basic
 
-open Tm27
+open Tm26
 
 unsafe def foo (cfg : Cfg) : IO Unit :=
 match (step machine cfg) with

diff --git a/GoldbachTm/Tm27/Transition.lean → GoldbachTm/Tm26/Transition.lean b/GoldbachTm/Tm27/Transition.lean → GoldbachTm/Tm26/Transition.lean
@@ -1,7 +1,7 @@
-import GoldbachTm.Tm27.TuringMachine27
-import GoldbachTm.Tm27.Search0
+import GoldbachTm.Tm26.TuringMachine26
+import GoldbachTm.Tm26.Search0
 
-namespace Tm27
+namespace Tm26
 
 theorem lemma_10_to_11 (i : ℕ) (r1: ℕ) (l r : List Γ)
 (h :
@@ -42,4 +42,4 @@ cases l1 with simp! [*, -nth_cfg] at h
               rw [List.append_cons, ← List.replicate_succ']
               ring_nf
 
-end Tm27
+end Tm26
diff --git a/GoldbachTm/Tm27/TuringMachine27.lean → GoldbachTm/Tm26/TuringMachine26.lean b/GoldbachTm/Tm27/TuringMachine27.lean → GoldbachTm/Tm26/TuringMachine26.lean
@@ -5,7 +5,7 @@ import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
 
-namespace Tm27
+namespace Tm26
 
 open Lean Meta Elab Tactic Std Term
 
@@ -140,4 +140,4 @@ constructor
   tauto
 
 
-end Tm27
+end Tm26
diff --git a/README.md b/README.md
@@ -1,22 +1,24 @@
-# goldbach_tm27
+# goldbach_tm26
 
 https://gist.github.com/anonymous/a64213f391339236c2fe31f8749a0df6
 give a 27-state Turing machine which halts if, and only if, Goldbach's conjecture is false,
 
-This repo verifies the 27-state and 31-state Turing mahcine formally in lean4
+Actually, it's a 26-state Turing machine : 22 and 24 are same state.
+
+This repo verifies the 26-state and 31-state Turing mahcine formally in lean4
 
 ## Verify the proof
 
 ```
-# main results at `GoldbachTm/Tm27/Content.lean`
+# main results at `GoldbachTm/Tm26/Content.lean`
 lake build
 ```
 
 
 ## Run simulator
 
 ```
-lake exe sim27
+lake exe sim26
 lake exe sim31
 ```
 
@@ -28,11 +30,11 @@ lake exe sim31
 
 Now it should be modified to 
 
->  A 43-state Turing machine has been constructed that halts if, and only if, Goldbach's conjecture is false, and a 27-state machine for that conjecture has been proposed and **verified in lean4**.
+>  A 43-state Turing machine has been constructed that halts if, and only if, Goldbach's conjecture is false, and a **26-state** machine for that conjecture has been proposed and **verified in lean4**.
 
 ## Note
 
 This repo doesn't 
 - solve Goldbach's conjecture
-- help solve Goldbach's conjecture, because understanding 27-state turing machine is more difficult than Goldbach's conjecture
+- help solve Goldbach's conjecture, because understanding 26-state turing machine is more difficult than Goldbach's conjecture
 
diff --git a/lakefile.lean b/lakefile.lean
@@ -17,5 +17,5 @@ lean_lib «GoldbachTm» where
 lean_exe «sim31» where
   root := `GoldbachTm.Tm31.Sim31
 
-lean_exe «sim27» where
-  root := `GoldbachTm.Tm27.Sim27
+lean_exe «sim26» where
+  root := `GoldbachTm.Tm26.Sim26