iterate

lengyijun · Nov 10, 2024 · d8171d8 · d8171d8
1 parent 2f8b112
commit d8171d8
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 68 deletions.
diff --git a/GoldbachTm/Tm27/Miscellaneous.lean b/GoldbachTm/Tm27/Miscellaneous.lean
@@ -25,8 +25,7 @@ theorem lemma8 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
 nth_cfg i = some ⟨⟨8, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
 nth_cfg (i + k + 2) = some ⟨⟨9, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
 induction k with (intros i l r h; simp_all)
-| zero => forward h
-          forward h
+| zero => iterate 2 forward h
           rw [← h]
           ring_nf
 | succ k induction_step =>
@@ -42,8 +41,7 @@ theorem lemma5 (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 + 2) = some ⟨⟨4, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
 induction k with (intros i l r h; simp_all)
-| zero => forward h
-          forward h
+| zero => iterate 2 forward h
           rw [← h]
           ring_nf
 | succ k induction_step =>

diff --git a/GoldbachTm/Tm27/PBP.lean b/GoldbachTm/Tm27/PBP.lean
@@ -35,9 +35,7 @@ by_cases hr1 : Nat.Prime (r1+1)
         repeat any_goals apply And.intro
         all_goals rfl
       obtain ⟨m, _, h⟩ := h
-      forward h
-      forward h
-      forward h
+      iterate 3 forward h
       apply rec26 at h
       forward h
       use (5+m+l1)
@@ -264,19 +262,7 @@ induction l1 with
         use 1
         tauto
     obtain ⟨j, _, h⟩ := hp
-    forward h
-    forward h
-    forward h
-    forward h
-    forward h
-    forward h
-    forward h
-    forward h
-    forward h
-    forward h
-    forward h
-    forward h
-    forward h
+    iterate 13 forward h
     use (13+j)
   . apply n_prime_17 at hp
     pick_goal 5
@@ -290,9 +276,7 @@ induction l1 with
         use 1
         tauto
     obtain ⟨j, _, h⟩ := hp
-    forward h
-    forward h
-    forward h
+    iterate 3 forward h
     use (3+j)
 | succ l1 induction_step =>
     intros i r1 h g hpp

diff --git a/GoldbachTm/Tm27/TuringMachine27.lean b/GoldbachTm/Tm27/TuringMachine27.lean
@@ -131,51 +131,7 @@ theorem cfg45 : nth_cfg 45 = some ⟨26,
         { 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
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
-forward h
+iterate 45 forward h
 simp [h]
 constructor
 . tauto