F_collatz

Author: lengyijun

CollatzFunction/NonHalt/Main.lean

@@ -152,105 +152,20 @@ theorem F_collatz (n: ℕ) (_ : n ≥ 1) (i: ℕ) (init_cfg: Cfg)
   Turing.ListBlank.mk [],
   Turing.ListBlank.mk (List.replicate ((collatz n)-1) one)⟩⟩
 := by
-cases n with
-| zero => omega
-| succ n => forward h
-            cases n with
-            | zero => simp
-                      forward h
-                      unfold collatz
-                      simp
-                      forward h
-                      forward h
-                      use (4+i)
-                      simp [h]
-                      simp! [Turing.ListBlank.mk]
-                      rw [Quotient.eq'']
-                      right
-                      use 1
-                      tauto
-            | succ n =>
-  rw [List.replicate_succ] at h
-  simp at h
-  unfold collatz
-  split_ifs <;> rename_i g
-  . rw [← (ListBlank_empty_eq_single_zero (List.replicate n one))] at h
-    apply B_even at h
-    forward h
-    rw [add_comm 1 (n/2)] at h
-    rw [List.replicate_succ] at h
-    simp at h
-    rw [← (ListBlank_empty_eq_single_zero (List.replicate (n/2) one))] at h
-    apply E_zeroing at h
-    forward h
-    apply recF at h
-    forward h
-    use (10 + i + n ^ 2 / 2 + n * 7 / 2 + n / 2 * 2)
-    simp [h]
-    repeat any_goals apply And.intro
-    . omega
-    . rw [← List.replicate_succ']
-      ring_nf
-      simp! [Turing.ListBlank.mk]
-      rw [Quotient.eq'']
-      right
-      use 3 + n/2
-      rw [← List.replicate_succ]
-      rw [← List.replicate_succ]
-      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
-      | zero => omega
-      | succ a => use a; omega
-  . cases n with
-    | zero => omega
-    | succ n =>
-      rw [← (ListBlank_empty_eq_single_zero (List.replicate (n+1) one))] at h
-      apply B_odd at h
-      forward h
-      have k : (2+n)/2 = n/2 + 1:= by omega
-      rw [k] at h
-      rw [List.replicate_succ] at h
-      simp at h
-      rw [← List.replicate_succ] at h
-      apply copy_half at h
-      rw [← (ListBlank_empty_eq_single_zero (List.replicate _ one))] at h
-      apply G_to_J at h
-      forward h
-      forward h
-      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
-      . simp! [Turing.ListBlank.mk]
-        rw [Quotient.eq'']
-        right
-        use 1
-        tauto
-      . apply congr
-        any_goals rfl
-        rw [← List.replicate_succ']
-        apply congr
-        any_goals rfl
-        apply congr
-        any_goals rfl
-        omega
-      . have g : (n+3) % 2 = 1 := by omega
-        rw [← Nat.odd_iff] at g
-        obtain ⟨a, g⟩ := g
-        cases a with
-        | zero => omega
-        | succ a => use a; omega
+cases (Nat.even_or_odd n) with
+| inl _ =>  apply F_even at h
+            any_goals assumption
+            use (i + (n ^ 2 + 5 * n) / 2 + 3)
+            constructor
+            . omega
+            . simp [h]
+| inr _ =>  apply F_odd at h
+            any_goals assumption
+            use (i + (3 * n ^ 2 + 4 * n + 1) / 2)
+            constructor
+            . cases n with
+              | zero => tauto
+              | succ n => omega
+            . simp [h]
 
 end NonHalt