odd, even

Author: lengyijun

CollatzFunction/NonHalt/Even.lean

@@ -9,7 +9,7 @@ lemma B_even (n: ℕ) (h_even : Even n): ∀ (i: ℕ)(l r: List Γ)(init_cfg: Cf
 nth_cfg init_cfg i =  ⟨B, ⟨one,
   Turing.ListBlank.mk (zero :: l),
   Turing.ListBlank.mk (List.replicate n one ++ zero :: r)⟩⟩ →
-∃ j>i, nth_cfg init_cfg j =  ⟨A, ⟨zero,
+nth_cfg init_cfg (i+ (n^2)/2 + 7 * n/2 + 4) = ⟨A, ⟨zero,
   Turing.ListBlank.mk (List.replicate (1+n/2) one ++ l),
   Turing.ListBlank.mk (List.replicate (1+n/2) one ++ r)⟩⟩
 := by
@@ -21,23 +21,18 @@ cases n with
           forward h
           forward h
           forward h
-          use (4+i)
+          ring_nf at *
           simp [h]
 | succ n => cases n with
   | zero => tauto
   | succ n => ring_nf at h
               apply B_step at h
               specialize IH n (by omega)
               apply IH at h
-              . obtain ⟨j, _, h⟩ := h
-                use j
-                constructor
-                any_goals omega
+              . ring_nf at *
+                have g : 4 + i + (4 + n * 4 + n ^ 2) / 2 + (14 + n * 7) / 2 = (13 + i + n * 2 + n ^ 2 / 2 + n * 7 / 2) := by omega
+                rw [g]
                 simp [h]
-                ring_nf
-                have h : (2+n)/2 = n/2+1 := by omega
-                rw [h]
-                ring_nf
                 rw [List.append_cons]
                 rw [← List.replicate_one]
                 rw [List.replicate_append_replicate]

CollatzFunction/NonHalt/Main.lean

@@ -45,7 +45,6 @@ cases n with
   split_ifs <;> rename_i g
   . rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
     apply B_even at h
-    obtain ⟨j, _, h⟩ := h
     forward h
     rw [add_comm 1 (n/2)] at h
     rw [List.replicate_succ] at h
@@ -55,8 +54,7 @@ cases n with
     forward h
     apply recF at h
     forward h
-    use (5 + j + n / 2 * 2)
-    ring_nf at *
+    use (10 + i + n ^ 2 / 2 + n * 7 / 2 + n / 2 * 2)
     simp [h]
     repeat any_goals apply And.intro
     . omega
@@ -71,6 +69,14 @@ cases n with
       simp
       ring_nf
       tauto
+    . ring_nf
+      apply congr
+      any_goals rfl
+      apply congr
+      any_goals rfl
+      apply congr
+      any_goals rfl
+      omega
     . rw [← Nat.even_iff] at g
       obtain ⟨a, g⟩ := g
       cases a with
@@ -81,7 +87,6 @@ cases n with
     | succ n =>
       rw [← (ListBlank_empty_eq_single_zero (List.replicate (n+1) one))] at h
       apply B_odd at h
-      obtain ⟨j, _, h⟩ := h
       forward h
       have k : (2+n)/2 = n/2 + 1:= by omega
       rw [k] at h
@@ -93,7 +98,7 @@ cases n with
       apply G_to_J at h
       forward h
       forward h
-      use (11 + j + n / 2 * 13 + (n / 2) ^ 2 * 4)
+      use (16 + i + (8 + n * 9 + n ^ 2) / 2 + n / 2 * 13 + (n / 2) ^ 2 * 4)
       simp [h]
       repeat any_goals apply And.intro
       . omega

CollatzFunction/NonHalt/Odd.lean

@@ -44,7 +44,7 @@ lemma B_odd (n: ℕ) (h_odd : Odd n): ∀ (i: ℕ)(l r: List Γ)(init_cfg: Cfg),
 nth_cfg init_cfg i =  ⟨B, ⟨one,
   Turing.ListBlank.mk (zero :: l),
   Turing.ListBlank.mk (List.replicate n one ++ zero :: r)⟩⟩ →
-∃ j>i, nth_cfg init_cfg j =  ⟨C, ⟨zero,
+nth_cfg init_cfg (i + (n^2 + 7 * n)/ 2 + 4) = ⟨C, ⟨zero,
   Turing.ListBlank.mk (List.replicate ((n+1)/2) one ++ l),
   Turing.ListBlank.mk (List.replicate (1+(n+1)/2) one ++ r)⟩⟩
 := by
@@ -62,30 +62,48 @@ cases n with
             forward h
             forward h
             forward h
-            use (8+i)
+            ring_nf at *
             simp [h]
   | succ n => ring_nf at h
               apply B_step at h
               specialize IH n (by omega)
               apply IH at h
-              . obtain ⟨j, _, h⟩ := h
-                use j
-                constructor
-                any_goals omega
+              . ring_nf at *
+                have g : (4 + i + (18 + n * 11 + n ^ 2) / 2) =
+                (13 + i + n * 2 + (n * 7 + n ^ 2) / 2) := by omega
+                rw [g]
                 simp [h]
-                ring_nf
-                have h : (3+n)/2 = (1+n)/2+1 := by omega
-                rw [h]
-                ring_nf
-                rw [List.append_cons]
-                rw [← List.replicate_one]
-                rw [List.replicate_append_replicate]
-                ring_nf
-                rw [List.append_cons]
-                rw [← List.replicate_one]
-                rw [List.replicate_append_replicate]
-                ring_nf
-                tauto
+                constructor
+                . rw [List.append_cons]
+                  rw [← List.replicate_one]
+                  rw [List.replicate_append_replicate]
+                  ring_nf
+                  apply congr
+                  any_goals rfl
+                  apply congr
+                  any_goals rfl
+                  apply congr
+                  any_goals rfl
+                  apply congr
+                  any_goals rfl
+                  apply congr
+                  any_goals rfl
+                  omega
+                . rw [List.append_cons]
+                  rw [← List.replicate_one]
+                  rw [List.replicate_append_replicate]
+                  ring_nf
+                  apply congr
+                  any_goals rfl
+                  apply congr
+                  any_goals rfl
+                  apply congr
+                  any_goals rfl
+                  apply congr
+                  any_goals rfl
+                  apply congr
+                  any_goals rfl
+                  omega
               . obtain ⟨k, h_odd⟩ := h_odd
                 cases k with
                 | zero => omega