better syntax

lengyijun · Nov 9, 2024 · ad1624f · ad1624f
1 parent 3847d75
commit ad1624f
Show file tree

Hide file tree

Showing 10 changed files with 96 additions and 104 deletions.
diff --git 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,16 +64,15 @@ 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
   split at 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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