tm27 finish

GoldbachTm.lean

@@ -4,6 +4,13 @@ import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
 import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Search0
+import GoldbachTm.Tm27.Prime
+import GoldbachTm.Tm27.PBP
+import GoldbachTm.Tm27.Content
+import GoldbachTm.Tm27.Transition
+import GoldbachTm.Tm27.Miscellaneous
+
 import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Search0
 import GoldbachTm.Tm31.Content

GoldbachTm/Tm27/Content.lean

@@ -0,0 +1,126 @@
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Search0
+import GoldbachTm.Tm27.PBP
+import Mathlib.Data.Nat.Prime.Defs
+
+namespace Tm27
+
+theorem lemma_26 (n : ℕ) (i : ℕ)
+(even_n : Even (n+2))
+(g :
+nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
+( hpp : goldbach (n+4)) :
+∃ j>i, nth_cfg j = some ⟨⟨26, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
+:= by
+forward g g i
+repeat rw [← List.replicate_succ] at g
+apply (leap_18 _ _ 0) at g
+any_goals omega
+any_goals assumption
+refine (?_ ∘ g) ?_
+. intros g
+  obtain ⟨k, _, h⟩ := g
+  use k
+  constructor
+  . omega
+  . simp [h]
+. obtain ⟨x, y, _, hx, hy⟩ := hpp
+  by_cases x ≤ y
+  . use! x, y
+    repeat any_goals apply And.intro
+    any_goals assumption
+    apply Nat.Prime.two_le at hx
+    omega
+  . use! y, x
+    repeat any_goals apply And.intro
+    any_goals assumption
+    any_goals omega
+    apply Nat.Prime.two_le at hy
+    omega
+
+lemma never_halt_step (n : ℕ) :
+(∀ i < n, goldbach (2*i+4)) ->
+∃ j, nth_cfg j = some ⟨⟨26, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+ := by
+induction n with
+| zero =>
+intros _
+use 45
+simp [cfg45]
+tauto
+| succ n =>
+rename_i induction_step
+intros h
+refine (?_ ∘ induction_step) ?_
+. intros g
+  obtain ⟨j, g⟩ := g
+  specialize h n (by omega)
+  apply lemma_26 at g
+  . specialize g h
+    obtain ⟨k, g⟩ := g
+    use k
+    simp [g]
+    ring_nf
+  . use (n+1)
+    ring_nf
+. intros i hi
+  apply h i (by omega)
+
+theorem never_halt (never_none : ∀ i, nth_cfg i ≠ none) (n : ℕ):
+goldbach (2*n + 4)
+:= by
+induction' n using Nat.strongRecOn with n IH
+apply never_halt_step at IH
+obtain ⟨j, g⟩ := IH
+by_contra! h
+forward g g j
+repeat rw [← List.replicate_succ] at g
+apply (leap_18_halt _ _ 0) at g
+any_goals omega
+refine (?_ ∘ g) ?_
+. intros h
+  obtain ⟨k, h⟩ := h
+  apply never_none _ h
+. intros x y _
+  apply h ⟨x, y, ?_⟩
+  ring_nf at *
+  tauto
+
+
+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 ⟨⟨26, 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_26 (2*n)) at g
+  . specialize g (h _)
+    obtain ⟨j, g⟩ := g
+    use j
+    simp! [g]
+  . use (n+1)
+    ring_nf
+. intros i n g j hij _
+  have h₂ : ∀ k, nth_cfg (j+k) = none := by
+    intro k
+    induction k with
+    | zero => tauto
+    | succ k => rename_i h₁
+                forward h₁ h₁ (j+k)
+                rw [← h₁]
+                ring_nf
+  specialize h₂ (i-j)
+  have h₃ : j + (i-j) = i := by omega
+  rw [h₃] at h₂
+  rw [h₂] at g
+  tauto
+
+theorem halt_lemma_rev :
+(∃ i, nth_cfg i = none) → (∃ n, ¬ goldbach (2*n+4))
+:= by
+intros h
+by_contra! g
+apply halt_lemma_rev' at g
+tauto
+
+
+end Tm27

GoldbachTm/Tm27/Miscellaneous.lean

@@ -0,0 +1,116 @@
+-- some lemmas tm31 doesn't contain
+
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Transition
+
+namespace Tm27
+
+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⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨7, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.zero ++ r)⟩⟩ := by
+induction k with (intros i l r h; simp_all)
+| zero => forward h h i
+          rw [← h]
+          ring_nf
+| succ k => forward h h i
+            rename_i induction_step
+            apply induction_step at h
+            ring_nf at *
+            simp! [h]
+            rw [List.append_cons]
+            rw [← List.replicate_succ']
+            ring_nf
+
+theorem lemma8 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨8, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 2) = some ⟨⟨9, 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 => forward h h i
+          forward h h (1+i)
+          rw [← h]
+          ring_nf
+| succ k => forward h h i
+            rename_i induction_step
+            apply induction_step at h
+            ring_nf at *
+            simp! [h]
+            rw [List.append_cons]
+            rw [← List.replicate_succ']
+            ring_nf
+
+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
+induction k with (intros i l r h; simp_all)
+| zero => forward h h i
+          forward h h (1+i)
+          rw [← h]
+          ring_nf
+| succ k => forward h h i
+            rename_i induction_step
+            apply induction_step at h
+            ring_nf at *
+            simp! [h]
+            rw [List.append_cons]
+            rw [← List.replicate_succ']
+            ring_nf
+
+theorem lemma10 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.zero ++ List.cons Γ.one r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨10, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
+induction k with (intros i l r h; simp_all)
+| zero => forward h h i
+          rw [← h]
+          ring_nf
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) (List.cons Γ.one l) r
+            have g : i + (k+1) +1 = i + 1 + k + 1 := by omega
+            rw [g, induction_step]
+            . simp [List.replicate_succ' (k+1)]
+            . simp! [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+
+theorem lemma_6_to_7 (i : ℕ) (l1: ℕ) (l r : List Γ)
+(h :
+nth_cfg i = some ⟨⟨6, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate l1 Γ.one ++ List.cons Γ.zero l),
+  Turing.ListBlank.mk r,
+  ⟩⟩) :
+∃ j>i, nth_cfg j = some ⟨⟨7, by omega⟩, ⟨Γ.zero,
+    Turing.ListBlank.mk l,
+    Turing.ListBlank.mk (List.replicate (l1+1) Γ.zero ++ r),
+    ⟩⟩
+:= by
+forward h h i
+cases l1 with
+| zero => use (1+i)
+          simp [h]
+| succ l1 => simp! at h
+             apply lemma7 at h
+             use (1+i+l1 + 1)
+             simp [h]
+             constructor
+             . omega
+             . rw [List.append_cons, ← List.replicate_succ']
+
+theorem lemma_9_to_10 (i : ℕ) (r1: ℕ) (l r : List Γ)
+(h :
+nth_cfg i = some ⟨⟨9, by omega⟩, ⟨Γ.zero,
+  Turing.ListBlank.mk l,
+  Turing.ListBlank.mk (List.replicate r1 Γ.zero ++ List.cons Γ.one r),
+  ⟩⟩) :
+∃ j>i, nth_cfg j = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+    Turing.ListBlank.mk (List.replicate r1 Γ.one ++ Γ.zero :: l),
+    Turing.ListBlank.mk r,
+    ⟩⟩
+:= by
+forward h h i
+cases r1 with simp_all
+| zero => use (1+i)
+          simp [h]
+| succ l1 => simp! at h
+             apply lemma10 at h
+             use (1+i+l1 + 1)
+             simp [h]
+             omega
+
+end Tm27