From 2f8b112f7d567547816a18869ab63b01fbdab7b2 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Sat, 9 Nov 2024 09:11:53 +0800 Subject: [PATCH] better syntax --- GoldbachTm/Basic.lean | 15 +++++---- GoldbachTm/Tm27/Content.lean | 3 +- GoldbachTm/Tm27/Miscellaneous.lean | 14 ++++----- GoldbachTm/Tm27/PBP.lean | 8 ++--- GoldbachTm/Tm27/Prime.lean | 50 +++++++++++++++--------------- GoldbachTm/Tm27/Search0.lean | 20 ++++++------ GoldbachTm/Tm31/Content.lean | 10 +++--- GoldbachTm/Tm31/PBP.lean | 6 ++-- GoldbachTm/Tm31/Prime.lean | 42 ++++++++++++------------- GoldbachTm/Tm31/Search0.lean | 32 +++++++++---------- 10 files changed, 96 insertions(+), 104 deletions(-) diff --git a/GoldbachTm/Basic.lean b/GoldbachTm/Basic.lean index 325ad50..8e069c6 100644 --- a/GoldbachTm/Basic.lean +++ b/GoldbachTm/Basic.lean @@ -40,14 +40,14 @@ induction i with intros k _ _ _ hp2 rw [h] at hp2 apply Nat.Prime.ne_zero at hp2 omega -| succ i => unfold goldbach_search_aux +| succ i induction_step => + unfold goldbach_search_aux simp constructor . omega . split . tauto - . rename_i induction_step _ _ _ _ - apply induction_step (k+1) (by omega) + . apply induction_step (k+1) (by omega) any_goals assumption by_cases x = k . subst x @@ -64,7 +64,7 @@ induction i with intros k _ h unfold goldbach_search_aux at h simp at h omega -| succ i => +| succ i induction_step => unfold goldbach_search_aux at h simp at h obtain ⟨_, h⟩ := h @@ -72,8 +72,7 @@ induction i with intros k _ h . simp at h subst p tauto - . rename_i induction_step _ _ _ - apply induction_step (k+1) (by omega) h + . apply induction_step (k+1) (by omega) h theorem goldbach_def_search (n : ℕ) : Goldbach n ↔ goldbach_search n ≠ none := @@ -116,8 +115,8 @@ induction n with constructor . omega . tauto -| succ n => rename_i h - obtain ⟨m, _, _⟩ := h +| succ n induction_step => + obtain ⟨m, _, _⟩ := induction_step by_cases hm: m = n + 1 . subst m apply hq diff --git a/GoldbachTm/Tm27/Content.lean b/GoldbachTm/Tm27/Content.lean index cad6e0f..cadfa7e 100644 --- a/GoldbachTm/Tm27/Content.lean +++ b/GoldbachTm/Tm27/Content.lean @@ -48,8 +48,7 @@ intros _ use 45 simp [cfg45] tauto -| succ n => -rename_i induction_step +| succ n induction_step => intros h refine (?_ ∘ induction_step) ?_ . intros g diff --git a/GoldbachTm/Tm27/Miscellaneous.lean b/GoldbachTm/Tm27/Miscellaneous.lean index 2abe2ba..c578de9 100644 --- a/GoldbachTm/Tm27/Miscellaneous.lean +++ b/GoldbachTm/Tm27/Miscellaneous.lean @@ -12,8 +12,8 @@ induction k with (intros i l r h; simp_all) | zero => forward h rw [← h] ring_nf -| succ k => forward h - rename_i induction_step +| succ k induction_step => + forward h apply induction_step at h ring_nf at * simp! [h] @@ -29,8 +29,8 @@ induction k with (intros i l r h; simp_all) forward h rw [← h] ring_nf -| succ k => forward h - rename_i induction_step +| succ k induction_step => + forward h apply induction_step at h ring_nf at * simp! [h] @@ -46,8 +46,8 @@ induction k with (intros i l r h; simp_all) forward h rw [← h] ring_nf -| succ k => forward h - rename_i induction_step +| succ k induction_step => + forward h apply induction_step at h ring_nf at * simp! [h] @@ -62,7 +62,7 @@ induction k with (intros i l r h; simp_all) | zero => forward h rw [← h] ring_nf -| succ k => rename_i induction_step +| succ k 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] diff --git a/GoldbachTm/Tm27/PBP.lean b/GoldbachTm/Tm27/PBP.lean index a2e1be3..a9412b4 100644 --- a/GoldbachTm/Tm27/PBP.lean +++ b/GoldbachTm/Tm27/PBP.lean @@ -194,8 +194,7 @@ nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep := by induction l1 with | zero => omega -| succ l1 => - rename_i induction_step +| succ l1 induction_step => intros i r1 h _ g hpp by_cases hp : ¬ Nat.Prime (l1+2) \/ ¬ Nat.Prime (r1+1) . -- induction step @@ -295,11 +294,10 @@ induction l1 with forward h forward h use (3+j) -| succ l1 => +| succ l1 induction_step => intros i r1 h g hpp apply lemma_18 at g - . rename_i induction_step - obtain ⟨j, _, g⟩ := g + . obtain ⟨j, _, g⟩ := g apply induction_step at g any_goals omega apply g diff --git a/GoldbachTm/Tm27/Prime.lean b/GoldbachTm/Tm27/Prime.lean index d3fdc82..ced209a 100644 --- a/GoldbachTm/Tm27/Prime.lean +++ b/GoldbachTm/Tm27/Prime.lean @@ -94,7 +94,7 @@ induction rb with intros i la lb ra l r g hm . omega . use! la, lb simp [g, hm] -| succ rb => rename_i induction_step +| succ rb induction_step => apply step_10_pointer at g specialize g hm obtain ⟨j, _, la', lb', g, h₁, h₂⟩ := g @@ -249,28 +249,28 @@ induction rb with intros i lb l r g p constructor . omega . simp! [g] -| succ rb => apply step_10_n_dvd at g - by_cases h : (lb + 2 ∣ rb + 3) - . have g : (lb + 2 ∣ lb + 2) := Nat.dvd_refl _ - have g := Nat.dvd_add g h - ring_nf at p g - rw [Nat.Prime.dvd_iff_eq] at g - any_goals omega - all_goals assumption - . specialize g h - rename_i induction_step - obtain ⟨j, _, g⟩ := g - apply induction_step at g - ring_nf at g p - specialize g p - obtain ⟨k, _, g⟩ := g - use k - constructor - . omega - . simp! [g] - rw [← List.cons_append] - rw [← List.replicate_succ] - ring_nf +| succ rb induction_step => + apply step_10_n_dvd at g + by_cases h : (lb + 2 ∣ rb + 3) + . have g : (lb + 2 ∣ lb + 2) := Nat.dvd_refl _ + have g := Nat.dvd_add g h + ring_nf at p g + rw [Nat.Prime.dvd_iff_eq] at g + any_goals omega + all_goals assumption + . specialize g h + obtain ⟨j, _, g⟩ := g + apply induction_step at g + ring_nf at g p + specialize g p + obtain ⟨k, _, g⟩ := g + use k + constructor + . omega + . simp! [g] + rw [← List.cons_append] + rw [← List.replicate_succ] + ring_nf theorem prime_21 (i r1: ℕ) (l r : List Γ) (g : @@ -384,12 +384,12 @@ induction rb with intros i lb l r g hd rw [h] at g apply Nat.eq_one_of_dvd_one at g omega -| succ rb => by_cases h : (lb+2) ∣ rb+3 +| succ rb induction_step => + by_cases h : (lb+2) ∣ rb+3 . apply step_10_dvd at g apply g h . apply step_10_n_dvd at g specialize g h - rename_i induction_step obtain ⟨j, _, g⟩ := g apply induction_step at g refine (?_ ∘ g) ?_ diff --git a/GoldbachTm/Tm27/Search0.lean b/GoldbachTm/Tm27/Search0.lean index 4184c80..f6deb3d 100644 --- a/GoldbachTm/Tm27/Search0.lean +++ b/GoldbachTm/Tm27/Search0.lean @@ -10,7 +10,7 @@ nth_cfg i = some ⟨⟨13, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -22,7 +22,7 @@ nth_cfg i = some ⟨⟨14, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep nth_cfg (i + k + 1) = some ⟨⟨14, 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 +| succ k 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] @@ -34,7 +34,7 @@ nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -46,7 +46,7 @@ nth_cfg i = some ⟨⟨19, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -58,7 +58,7 @@ nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -70,7 +70,7 @@ nth_cfg i = some ⟨⟨24, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -83,7 +83,7 @@ nth_cfg i = some ⟨⟨11, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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] @@ -95,7 +95,7 @@ nth_cfg i = some ⟨⟨20, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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] @@ -107,7 +107,7 @@ nth_cfg i = some ⟨⟨23, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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] @@ -119,7 +119,7 @@ nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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] diff --git a/GoldbachTm/Tm31/Content.lean b/GoldbachTm/Tm31/Content.lean index 312961f..2e674ae 100644 --- a/GoldbachTm/Tm31/Content.lean +++ b/GoldbachTm/Tm31/Content.lean @@ -44,8 +44,7 @@ intros _ use 6 simp [cfg6] tauto -| succ n => -rename_i induction_step +| succ n induction_step => intros h refine (?_ ∘ induction_step) ?_ . intros g @@ -96,10 +95,9 @@ apply propagating_induction (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i intro k induction k with | zero => tauto - | succ k => rename_i h₁ - forward h₁ h₁ (j+k) - rw [← h₁] - ring_nf + | succ k h₁ => forward h₁ h₁ (j+k) + rw [← h₁] + ring_nf specialize h₂ (i-j) have h₃ : j + (i-j) = i := by omega rw [h₃] at h₂ diff --git a/GoldbachTm/Tm31/PBP.lean b/GoldbachTm/Tm31/PBP.lean index 9d62b81..c9289b0 100644 --- a/GoldbachTm/Tm31/PBP.lean +++ b/GoldbachTm/Tm31/PBP.lean @@ -167,8 +167,7 @@ nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep := by induction l1 with | zero => omega -| succ l1 => - rename_i induction_step +| succ l1 induction_step => intros i r1 h g hpp by_cases hp : ¬ Nat.Prime (l1+2) \/ ¬ Nat.Prime (r1+1) . -- induction step @@ -266,13 +265,12 @@ induction l1 with forward h h (4+i+j) forward h h (5+i+j) use (6+i+j) -| succ l1 => +| succ l1 induction_step => intros i r1 h g hpp apply lemma_26 at g . obtain ⟨j, g⟩ := g forward g g (i+j) forward g g (1+i+j) - rename_i induction_step repeat rw [← List.replicate_succ] at g apply induction_step at g any_goals omega diff --git a/GoldbachTm/Tm31/Prime.lean b/GoldbachTm/Tm31/Prime.lean index 19b33b2..6bd6fbf 100644 --- a/GoldbachTm/Tm31/Prime.lean +++ b/GoldbachTm/Tm31/Prime.lean @@ -95,7 +95,7 @@ nth_cfg i = some ⟨⟨12, by omega⟩, ⟨Γ.zero, 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 +| succ rb induction_step => apply step_12_pointer at g specialize g hm obtain ⟨j, la', lb', g, h₁, h₂⟩ := g @@ -251,24 +251,24 @@ Nat.Prime (lb+rb+4) → induction rb with intros i lb l r g p | zero => use 0 simp! [g] -| succ rb => apply step_12_n_dvd at g - by_cases h : (lb + 2 ∣ rb + 3) - . have g : (lb + 2 ∣ lb + 2) := Nat.dvd_refl _ - have g := Nat.dvd_add g h - ring_nf at p g - rw [Nat.Prime.dvd_iff_eq] at g - any_goals omega - all_goals assumption - . specialize g h - rename_i induction_step - obtain ⟨j, g⟩ := g - apply induction_step at g - ring_nf at g p - specialize g p - obtain ⟨k, g⟩ := g - use (j+k) - ring_nf at * - rw [g] +| succ rb induction_step => + apply step_12_n_dvd at g + by_cases h : (lb + 2 ∣ rb + 3) + . have g : (lb + 2 ∣ lb + 2) := Nat.dvd_refl _ + have g := Nat.dvd_add g h + ring_nf at p g + rw [Nat.Prime.dvd_iff_eq] at g + any_goals omega + all_goals assumption + . specialize g h + obtain ⟨j, g⟩ := g + apply induction_step at g + ring_nf at g p + specialize g p + obtain ⟨k, g⟩ := g + use (j+k) + ring_nf at * + rw [g] -- r1 : count of 1 on the right theorem lemma_23 (i r1: ℕ) (l r : List Γ) @@ -386,13 +386,13 @@ induction rb with intros i lb l r g hd rw [h] at g apply Nat.eq_one_of_dvd_one at g omega -| succ rb => by_cases h : (lb+2) ∣ rb+3 +| succ rb induction_step => + by_cases h : (lb+2) ∣ rb+3 . apply step_12_dvd at g apply g h . apply step_12_n_dvd at g specialize g h obtain ⟨j, g⟩ := g - rename_i induction_step apply induction_step at g refine (?_ ∘ g) ?_ . intros g diff --git a/GoldbachTm/Tm31/Search0.lean b/GoldbachTm/Tm31/Search0.lean index 7a5dbab..7238e54 100644 --- a/GoldbachTm/Tm31/Search0.lean +++ b/GoldbachTm/Tm31/Search0.lean @@ -10,7 +10,7 @@ nth_cfg i = some ⟨⟨5, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.repl 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 +| succ k 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] @@ -22,7 +22,7 @@ nth_cfg i = some ⟨⟨9, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.repl 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 +| succ k 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] @@ -34,7 +34,7 @@ nth_cfg i = some ⟨⟨10, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -46,7 +46,7 @@ nth_cfg i = some ⟨⟨15, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -58,7 +58,7 @@ nth_cfg i = some ⟨⟨16, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -70,7 +70,7 @@ nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep nth_cfg (i + k + 1) = some ⟨⟨18, 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 +| succ k 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] @@ -82,7 +82,7 @@ nth_cfg i = some ⟨⟨20, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -94,7 +94,7 @@ nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep 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 +| succ k 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] @@ -106,7 +106,7 @@ nth_cfg i = some ⟨⟨27, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.rep nth_cfg (i + k + 1) = some ⟨⟨27, 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 +| succ k 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] @@ -120,7 +120,7 @@ nth_cfg i = some ⟨⟨7, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing. nth_cfg (i + k + 1) = some ⟨⟨7, 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 +| succ k 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] @@ -132,7 +132,7 @@ nth_cfg i = some ⟨⟨12, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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] @@ -144,7 +144,7 @@ nth_cfg i = some ⟨⟨13, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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] @@ -156,7 +156,7 @@ nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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] @@ -168,7 +168,7 @@ nth_cfg i = some ⟨⟨24, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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] @@ -180,7 +180,7 @@ nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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] @@ -192,7 +192,7 @@ nth_cfg i = some ⟨⟨30, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk l, Turing 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 +| succ k 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]