state-5 recursive

GoldbachTm.lean

@@ -5,3 +5,4 @@ import GoldbachTm.Format
 import GoldbachTm.ListBlank
 import GoldbachTm.Tm27.TuringMachine27
 import GoldbachTm.Tm31.TuringMachine31
+import GoldbachTm.Tm31.Hello

GoldbachTm/Tm31/Hello.lean

@@ -0,0 +1,175 @@
+-- theorem of recursive states
+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

GoldbachTm/Tm31/TuringMachine31.lean

@@ -96,3 +96,9 @@ def machine : Machine
 | ⟨030, _⟩, Γ.zero => some ⟨⟨028, by omega⟩, ⟨Turing.Dir.left, Γ.one⟩⟩
 | ⟨030, _⟩, Γ.one  => some ⟨⟨030, by omega⟩, ⟨Turing.Dir.right, Γ.one⟩⟩
 | ⟨_+31, _⟩, _ => 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