From 7682d5cde4bf403ec6122b925c4863f2374e6ce5 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Wed, 16 Oct 2024 11:50:06 +0800 Subject: [PATCH] wip --- GoldbachTm.lean | 5 ++ GoldbachTm/Tm27/Content.lean | 16 ++++ GoldbachTm/Tm27/Prime.lean | 118 +++++++++++++++++++++++++++ GoldbachTm/Tm27/Search0.lean | 117 ++++++++++++++++++++++++++ GoldbachTm/Tm27/Transition.lean | 23 ++++++ GoldbachTm/Tm27/TuringMachine27.lean | 19 +++++ 6 files changed, 298 insertions(+) create mode 100644 GoldbachTm/Tm27/Content.lean create mode 100644 GoldbachTm/Tm27/Prime.lean create mode 100644 GoldbachTm/Tm27/Search0.lean create mode 100644 GoldbachTm/Tm27/Transition.lean diff --git a/GoldbachTm.lean b/GoldbachTm.lean index c732ab9..89c6afa 100644 --- a/GoldbachTm.lean +++ b/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 diff --git a/GoldbachTm/Tm27/Content.lean b/GoldbachTm/Tm27/Content.lean new file mode 100644 index 0000000..ec8a6c8 --- /dev/null +++ b/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 diff --git a/GoldbachTm/Tm27/Prime.lean b/GoldbachTm/Tm27/Prime.lean new file mode 100644 index 0000000..7442f0e --- /dev/null +++ b/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 diff --git a/GoldbachTm/Tm27/Search0.lean b/GoldbachTm/Tm27/Search0.lean new file mode 100644 index 0000000..095a05d --- /dev/null +++ b/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 diff --git a/GoldbachTm/Tm27/Transition.lean b/GoldbachTm/Tm27/Transition.lean new file mode 100644 index 0000000..234f8fe --- /dev/null +++ b/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 diff --git a/GoldbachTm/Tm27/TuringMachine27.lean b/GoldbachTm/Tm27/TuringMachine27.lean index f7f8015..5218028 100644 --- a/GoldbachTm/Tm27/TuringMachine27.lean +++ b/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