wip

GoldbachTm.lean

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

GoldbachTm/Tm27/Content.lean

@@ -0,0 +1,16 @@
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Search0
+import Mathlib.Data.Nat.Prime.Defs
+
+namespace Tm27
+
+theorem lemma_26 (n : ℕ) (i : ℕ)
+(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
+sorry
+
+
+end Tm27

GoldbachTm/Tm27/Prime.lean

@@ -0,0 +1,118 @@
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Transition
+
+namespace Tm27
+
+-- c1++, c2++
+--    l 0 [la 11] 0  [lb 11] 0 [ra 11111] 0  [(rb+1) 1] 0 r
+--                c1         ^            c2
+--
+--    l 0 [la' 1] 0  [lb' 1] 0 [(ra+1) 1] 0  [rb 11111] 0 r
+--                c1         ^            c2
+private lemma step_10_pointer (i la lb ra rb: ℕ) (l r : List Γ) :
+nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate lb Γ.one ++ List.cons Γ.zero (List.replicate la Γ.one ++ List.cons Γ.zero l)),
+  Turing.ListBlank.mk (List.replicate ra Γ.one ++ List.cons Γ.zero (List.replicate (rb+1) Γ.one ++ List.cons Γ.zero r))⟩⟩ →
+  (ra + 2) ≡ (la + 1) [MOD (la + lb + 1)] →
+∃ j>i, ∃ la' lb', nth_cfg j = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk (List.replicate lb' Γ.one ++ List.cons Γ.zero (List.replicate la' Γ.one ++ List.cons Γ.zero l)),
+  Turing.ListBlank.mk (List.replicate (ra+1) Γ.one ++ List.cons Γ.zero (List.replicate rb Γ.one ++ List.cons Γ.zero r))⟩⟩
+  /\ (ra + 3) ≡ (la' + 1) [MOD (la + lb + 1)]
+  /\ la + lb = la' + lb'
+:= by
+intros g hm
+apply lemma_10_to_11 at g
+obtain ⟨j, g⟩ := g
+forward g g (j+i)
+forward g g (1+j+i)
+apply rec13 at g
+forward g g (2+j+i+ra+1)
+cases lb with simp_all
+| zero => forward g g (4+j+i+ra)
+          cases la with simp_all
+          | zero => forward g g (5+j+i+ra)
+                    forward g g (6+j+i+ra)
+                    use (7+j+i+ra)
+                    constructor
+                    . omega
+                    . simp [g]
+                      use! 0, 0
+                      simp!
+                      apply Nat.modEq_one
+          | succ la => simp! at g
+                       sorry
+| succ lb => sorry
+
+-- not sure
+theorem prime_21 (i r1: ℕ) (l r : List Γ)
+(g :
+nth_cfg i = some ⟨⟨0, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩)
+(p : Nat.Prime (r1+1)) :
+∃ j, nth_cfg (i+j) = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
+match h : r1 with
+| Nat.zero => by subst r1
+                 exfalso
+                 apply Nat.not_prime_one p
+| Nat.succ Nat.zero => by
+  subst r1
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  forward g g (3+i)
+  forward g g (4+i)
+  use 5
+  ring_nf at *
+  simp [g]
+| Nat.succ (Nat.succ Nat.zero) => by
+  subst r1
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  forward g g (3+i)
+  forward g g (4+i)
+  forward g g (5+i)
+  forward g g (6+i)
+  use 7
+  ring_nf at *
+  simp [g]
+| Nat.succ (Nat.succ (Nat.succ r1)) => by sorry
+
+
+-- not sure
+theorem n_prime_17 (i r1: ℕ) (l r : List Γ)
+(g :
+nth_cfg i = some ⟨⟨0, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩)
+(hp : ¬ Nat.Prime (r1+1)) :
+∃ j, nth_cfg (i+j) = some ⟨⟨17, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
+match r1 with
+| Nat.zero => by simp_all
+                 forward g g i
+                 forward g g (1+i)
+                 forward g g (2+i)
+                 use 3
+                 rw [← g]
+                 ring_nf
+| Nat.succ Nat.zero => by exfalso
+                          apply hp
+                          decide
+| Nat.succ (Nat.succ Nat.zero) => by exfalso
+                                     apply hp
+                                     decide
+| Nat.succ (Nat.succ (Nat.succ r1)) => by
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  forward g g (3+i)
+  forward g g (4+i)
+  forward g g (5+i)
+  forward g g (6+i)
+  forward g g (7+i)
+  forward g g (8+i)
+  forward g g (9+i)
+  forward g g (10+i)
+  forward g g (11+i)
+  forward g g (12+i)
+  forward g g (13+i)
+  sorry
+
+end Tm27

GoldbachTm/Tm27/Search0.lean

@@ -0,0 +1,117 @@
+-- theorem of recursive states
+-- all these states' usage is to search 0
+import GoldbachTm.Tm27.TuringMachine27
+
+namespace Tm27
+
+-- left
+theorem rec13 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨13, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨13, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one 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 rec17 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨17, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one 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 rec19 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨19, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨19, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one 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 rec21 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one 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 rec24 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨24, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨24, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ r)⟩⟩ := by
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| succ k => rename_i induction_step
+            specialize induction_step (i+1) l (List.cons Γ.one 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]
+
+--right
+theorem rec11 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨11, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨11, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| 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 rec20 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨20, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨20, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| 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 rec23 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨23, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨23, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| 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 rec26 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
+nth_cfg (i + k + 1) = some ⟨⟨26, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+1) Γ.one ++ l), Turing.ListBlank.mk r⟩⟩ := by
+induction k with intros i l r h
+| zero => simp [nth_cfg, h, step, machine, Turing.Tape.write, Turing.Tape.move]
+| 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]
+
+end Tm27

GoldbachTm/Tm27/Transition.lean

@@ -0,0 +1,23 @@
+import GoldbachTm.Tm27.TuringMachine27
+import GoldbachTm.Tm27.Search0
+
+namespace Tm27
+
+theorem lemma_10_to_11 (i : ℕ) (r1: ℕ) (l r : List Γ)
+(h :
+nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.one,
+  Turing.ListBlank.mk l,
+  Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩) :
+
+∃ j, nth_cfg (j + i) = some ⟨⟨11, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩
+:= by
+forward h h i
+cases r1 with
+| zero => use 1
+          simp [h]
+| succ r1 => apply rec11 at h
+             use (r1 + 2)
+             rw [← h]
+             ring_nf
+
+end Tm27

GoldbachTm/Tm27/TuringMachine27.lean

@@ -1,5 +1,6 @@
 -- inspired by https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Computability/TuringMachine.lean
 import Mathlib.Computability.TuringMachine
+import Mathlib.Data.Real.Sqrt
 import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
@@ -91,4 +92,22 @@ def machine : Machine
 | ⟨26, _⟩, Γ.one  => some ⟨⟨26, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
 | ⟨_+27, _⟩, _ => by omega -- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20on.20Fin.20isn't.20exhaustive.20for.20large.20matches/near/428048252
 
+def nth_cfg : (n : Nat) -> Option Cfg
+| 0 => init []
+| Nat.succ n => match (nth_cfg n) with
+                | none => none
+                | some cfg =>  step machine cfg
+
+
+-- g1 = g2
+macro "forward" g1:ident g2:Lean.binderIdent i:term: tactic => `(tactic| (
+have h : nth_cfg ($i + 1) = nth_cfg ($i + 1) := rfl
+nth_rewrite 2 [nth_cfg] at h
+simp [*, step, Option.map, machine, Turing.Tape.write, Turing.Tape.move] at h
+try simp! [*, -nth_cfg] at h
+try ring_nf at h
+clear $g1
+rename_i $g2
+))
+
 end Tm27