finish tm 31

GoldbachTm/Basic.lean

@@ -18,3 +18,52 @@ structure Stmt where
   write : Γ
 
 def goldbach (n : ℕ) := ∃ (x y: ℕ), x + y = n /\ Nat.Prime x /\ Nat.Prime y
+
+theorem unlimitedQ (Q : ℕ → Prop)
+               (base : ℕ) (hbase : Q base)
+               (hq : ∀ x, Q x → ∃ y > x, Q y) :
+               ∀ n, ∃ m > n, Q m := by
+intros n
+induction n with
+| zero => cases base with
+          | zero => apply hq at hbase
+                    tauto
+          | succ base => use (base+1)
+                         constructor
+                         . omega
+                         . tauto
+| succ n => rename_i h
+            obtain ⟨m, _, _⟩ := h
+            by_cases hm: m = n + 1
+            . subst m
+              apply hq
+              tauto
+            . use m
+              constructor
+              . omega
+              . assumption
+
+
+/-
+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 []⟩⟩
+-/
+theorem jiting (P : ℕ → Prop) (Q : ℕ → ℕ → Prop)
+               (base : ℕ) (hbase : Q base 0)
+               (hq : ∀ i n, Q i n → ∃ j > i, Q j (n+1))
+               (pq : ∀ i n, Q i n → ∀ j ≤ i, P j)
+: ∀ j, P j := by
+intro j
+have h := unlimitedQ (fun i => ∃ n, Q i n) base ⟨0, hbase⟩
+simp at h
+refine (?_ ∘ h) ?_
+. intros g
+  obtain ⟨i, hi, n, hqin⟩ := g j
+  apply pq i n hqin
+  omega
+. intros i m hqim
+  obtain ⟨j, _, _⟩ := hq i m hqim
+  use j
+  constructor
+  . omega
+  . use (m+1)

GoldbachTm/Tm31/Content.lean

@@ -38,17 +38,9 @@ lemma never_halt_step (n : ℕ) :
  := by
 induction n with
 | zero =>
-have h : nth_cfg 0 = init [] := by simp!
-simp [init, Turing.Tape.mk₁, Turing.Tape.mk₂, Turing.Tape.mk'] at h
-forward h h 0
-forward h h 1
-forward h h 2
-forward h h 3
-forward h h 4
-forward h h 5
 intros _
 use 6
-simp [h]
+simp [cfg6]
 tauto
 | succ n =>
 rename_i induction_step
@@ -87,14 +79,35 @@ refine (?_ ∘ g) ?_
   tauto
 
 
-theorem halt_lemma :
-(∃ (n x y: ℕ), Even n /\ n > 2 /\ x + y = n /\ Nat.Prime x /\ Nat.Prime y) →
-∃ i, nth_cfg i = none
-:= by
-sorry
+theorem halt_lemma_rev' (h : ∀ n, goldbach (2*n+4)) :
+∀ i, nth_cfg i ≠ none := by
+apply jiting (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩) 6
+. simp [cfg6]; tauto
+. intros i n g
+  apply (lemma_25 (2*n)) at g
+  specialize g (h _)
+  obtain ⟨j, g⟩ := g
+  use (i+j)
+  simp! [g]
+. 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 x y: ℕ), Even n /\ n > 2 /\ x + y = n /\ Nat.Prime x /\ Nat.Prime y)
+(∃ i, nth_cfg i = none) → (∃ n, ¬ goldbach (2*n+4))
 := by
-sorry
+intros h
+by_contra! g
+apply halt_lemma_rev' at g
+tauto

GoldbachTm/Tm31/TuringMachine31.lean

@@ -115,3 +115,15 @@ try ring_nf at h
 clear $g1
 rename_i $g2
 ))
+
+theorem cfg6 : nth_cfg 6 = some ⟨25,
+        { head := default, left := Turing.ListBlank.mk (List.replicate 4 Γ.one), right := Turing.ListBlank.mk [] } ⟩ := by
+have h : nth_cfg 0 = init [] := by simp!
+simp [init, Turing.Tape.mk₁, Turing.Tape.mk₂, Turing.Tape.mk'] at h
+forward h h 0
+forward h h 1
+forward h h 2
+forward h h 3
+forward h h 4
+forward h h 5
+assumption