Skip to content

Commit

Permalink
lemma_12
Browse files Browse the repository at this point in the history
  • Loading branch information
@lengyijun
lengyijun committed Oct 12, 2024
1 parent 2d20df7 commit 3e4cee3
Show file tree
Hide file tree
Showing 7 changed files with 434 additions and 1 deletion.
5 changes: 5 additions & 0 deletions GoldbachTm.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,8 @@ import GoldbachTm.Format
import GoldbachTm.ListBlank
import GoldbachTm.Tm27.TuringMachine27
import GoldbachTm.Tm31.TuringMachine31
import GoldbachTm.Tm31.Search0
import GoldbachTm.Tm31.Content
import GoldbachTm.Tm31.Prime
import GoldbachTm.Tm31.PBP
import GoldbachTm.Tm31.Transition
21 changes: 21 additions & 0 deletions GoldbachTm/Tm31/Content.lean
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
import GoldbachTm.Tm31.TuringMachine31
import Mathlib.Data.Nat.Prime.Defs

theorem lemma_25 (k : ℕ): ∀ (i : ℕ),
nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate k Γ.one), Turing.ListBlank.mk []⟩⟩ →
(¬ (∃ x y, x + y = k /\ Nat.Prime x /\ Nat.Prime y)) →
∃ j, nth_cfg (i+j) = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+2) Γ.one), Turing.ListBlank.mk []⟩⟩
:= by
sorry

theorem halt_lemma :
(∃ (k x y: ℕ), k % 2 = 0 /\ k >= 4 /\ x + y = k /\ Nat.Prime x /\ Nat.Prime y) →
∃ i, nth_cfg i = none
:= by
sorry

theorem halt_lemma_rev :
∃ i, nth_cfg i = none →
(∃ (k x y: ℕ), k % 2 = 0 /\ x + y = k /\ Nat.Prime x /\ Nat.Prime y)
:= by
sorry
12 changes: 12 additions & 0 deletions GoldbachTm/Tm31/PBP.lean
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
-- PDP is short for "prime board prime"
import GoldbachTm.Tm31.TuringMachine31
import Mathlib.Data.Nat.Prime.Defs

-- TODO: maybe need double 0
-- l1 : count of 1 on the left
-- r1 : count of 1 on the right
theorem lemma_26 : ∀ (i l1 r1: ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩ →
(¬ Nat.Prime (l1+1)) \/ (¬ Nat.Prime r1) →
∃ j, nth_cfg (i+j) = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate l1 Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
sorry
139 changes: 139 additions & 0 deletions GoldbachTm/Tm31/Prime.lean
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,139 @@
-- theorem of subroutine: judge prime

import GoldbachTm.Tm31.TuringMachine31
import GoldbachTm.Tm31.Transition
import Mathlib.Data.Nat.Prime.Defs
import Mathlib.Data.Nat.ModEq

-- l 0 [la 11] 0 [lb 1] 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
theorem step_12 (i la lb ra rb: ℕ) (l r : List Γ) :
nth_cfg i = some ⟨⟨12, by omega⟩, ⟨Γ.zero,
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 la' lb', nth_cfg (i+j) = some ⟨⟨12, by omega⟩, ⟨Γ.zero,
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_12_to_13 at g
obtain ⟨j, g⟩ := g

forward g g (i+j)

forward g g (i+j+1)
apply rec15 at g

forward g g (i+j+1+1+ra+1)
cases lb with simp_all
| zero => forward g g (i+j+1+1+ra+1+1)
cases la with simp_all
| zero => forward g g (i+j+1+1+ra+1+1+1)
forward g g (i+j+1+1+ra+1+1+1+1)
use! (j+ra+7), 0, 0
simp
constructor
. have h: i+(j+ra+7) = i+ j + 1 + 1 + ra + 1 + 1 + 1 + 1 + 1 := by omega
rw [h, g]
constructor
. apply Nat.modEq_one
| succ la => simp! [*, -nth_cfg] at g
apply rec10 at g
forward g g (i+j+1+1+ra+1+1+1+la+1)
forward g g (i+j+1+1+ra+1+1+1+la+1+1)
rw [List.append_cons, ← List.replicate_succ'] at g
simp! [*, -nth_cfg] at g
apply rec12 at g
use! (j+1+1+ra+1+1+1+la+1+1+1+la+1), 0, (la+1)
simp
constructor
. have h : i + (j + 1 + 1 + ra + 1 + 1 + 1 + la + 1 + 1 + 1 + la + 1) = i + j + 1 + 1 + ra + 1 + 1 + 1 + la + 1 + 1 + 1 + la + 1 := by omega
rw [h, g]
constructor
. apply Nat.ModEq.add_right 1
apply Nat.ModEq.trans hm
rw [Nat.modEq_zero_iff_dvd]
| succ lb => simp! [*, -nth_cfg] at g
apply lemma_8_to_9 at g
obtain ⟨k, g⟩ := g
forward g g (i+j+1+1+ra+1+1+k)
apply lemma_11_to_12 at g
obtain ⟨m, g⟩ := g
use! (j+ra+k+m+5), (la+1), lb
have h : i+(j+ra+k+m+5) = i + j + 1 + 1 + ra + 1 + 1 + k + 1 + m := by omega
rw [h, g]
repeat any_goals constructor
any_goals omega
apply Nat.ModEq.add_right 1 hm

-- l 0 [la 11] 0 [lb 1] 0 [ra 11111111] 0 [rb 1] 0 r
-- c1 ^ c2
--
-- l 0 [la' 1] 0 [lb' 1] 0 [(ra+rb) 111] 0 0 r
-- c1 ^ c2
theorem lemma_12 (rb : ℕ): ∀ (i la lb ra : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨12, by omega⟩, ⟨Γ.zero,
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 Γ.one ++ List.cons Γ.zero r))⟩⟩ →
(ra + 2) ≡ (la + 1) [MOD (la + lb + 1)] →
∃ j la' lb', nth_cfg (i+j) = some ⟨⟨12, by omega⟩, ⟨Γ.zero,
Turing.ListBlank.mk (List.replicate lb' Γ.one ++ List.cons Γ.zero (List.replicate la' Γ.one ++ List.cons Γ.zero l)),
Turing.ListBlank.mk (List.replicate (ra+rb) Γ.one ++ List.cons Γ.zero (List.cons Γ.zero r))⟩⟩
/\ (ra + rb + 2) ≡ (la' + 1) [MOD (la + lb + 1)]
/\ la + lb = la' + lb'
:= by
induction rb with intros i la lb ra l r g hm
| zero => use! 0, la, lb
simp [g, hm]
| succ rb => rename_i induction_step
apply step_12 at g
specialize g hm
obtain ⟨j, la', lb', g, h₁, h₂⟩ := g
apply induction_step at g
rw [← h₂] at g
have h : ra + 1 + 2 = ra + 3 := by omega
rw [h] at g
specialize g h₁
obtain ⟨k, la'', lb'', g, h₃, h₄⟩ := g
use! (j+k), la'', lb''
repeat any_goals constructor
any_goals tauto
. rw [← Nat.add_assoc i, g]
apply congr
any_goals rfl
apply congr
any_goals rfl
apply congr
any_goals rfl
apply congr
any_goals rfl
apply congr
any_goals rfl
apply congr
any_goals rfl
apply congr
any_goals rfl
apply congr
any_goals rfl
omega
. have h : ra + (rb + 1) +2 = ra + 1 + rb + 2:= by omega
rw [h]
assumption

-- r1 : count of 1 on the right
theorem lemma_23 : ∀ (i r1: ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨0, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩ →
Nat.Prime r1 →
∃ j, nth_cfg (i+j) = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩ := by
intros i r1 l r g prime_r1
cases r1 with
| zero => exfalso
apply Nat.not_prime_zero prime_r1
| succ r1 => sorry
176 changes: 176 additions & 0 deletions GoldbachTm/Tm31/Search0.lean
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,176 @@
-- theorem of recursive states
-- all these states' usage is to search 0
import GoldbachTm.Tm31.TuringMachine31


-- left
theorem rec5 (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 + 1) = some ⟨⟨5, 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]
tauto

theorem rec9 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨9, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨9, 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]
tauto

theorem rec10 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨10, 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]
tauto

theorem rec15 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨15, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨15, 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]
tauto

theorem rec16 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨16, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨16, 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]
tauto

theorem rec20 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨20, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨20, 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]
tauto

theorem rec22 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨22, 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]
tauto


-- right
theorem rec12 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨12, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨12, 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]
tauto

theorem rec13 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨13, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨13, 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]
tauto

theorem rec21 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨21, 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]
tauto

theorem rec24 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨24, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨24, 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]
tauto

theorem rec25 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨25, 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]
tauto

theorem rec30 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
nth_cfg i = some ⟨⟨30, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero r) ⟩⟩ →
nth_cfg (i + k + 1) = some ⟨⟨30, 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]
tauto
Loading

0 comments on commit 3e4cee3

Please sign in to comment.