Complete proof for segment_length_prop1

Author: shnarazk

LubySequence/Segment.lean

@@ -151,15 +151,22 @@ example : segment_length 0 = 1 := by
 theorem segment_length_prop1 : ∀ n > 0, n = 2 ^ n.size - 2 → 
     segment_length (2 ^ (n + 2).size - 2) = 1 + segment_length n := by
   intro n n_gt_0 n_is_envelope
+  have n_gt_2 : n ≥ 2 := by
+    by_contra n_eq_1
+    simp at n_eq_1
+    have : n = 1 := by exact Nat.eq_of_le_of_lt_succ n_gt_0 n_eq_1
+    simp [this] at n_is_envelope
+  have n2size_ge_3 : (n + 2).size ≥ 3 := by
+    have s1 : (2 + 2).size ≤ (n + 2).size := by
+      have : 2 + 2 ≤ n + 2 := by exact Nat.add_le_add_right n_gt_2 2
+      exact size_le_size this
+    have : (2 + 2).size = 3 := by simp [size, binaryRec]
+    simp [this] at s1
+    exact s1
+  have pow2nsize : 2 ^ n.size - 2 + 2 = 2 ^ n.size := by
+    exact Nat.sub_add_cancel (le_pow (size_pos.mpr n_gt_0))
   have segment_of_n : segment n = 2 ^ (n.size - 1) := by
     rw [segment]
-    have n_gt_2 : n ≥ 2 := by
-      by_contra n_eq_1
-      simp at n_eq_1
-      have : n = 1 := by exact Nat.eq_of_le_of_lt_succ n_gt_0 n_eq_1
-      simp [this] at n_is_envelope
-    have pow2nsize : 2 ^ n.size - 2 + 2 = 2 ^ n.size := by
-      exact Nat.sub_add_cancel (le_pow (size_pos.mpr n_gt_0))
     split
     · expose_names
       rw (occs := .pos [1]) [n_is_envelope]
@@ -181,8 +188,70 @@ theorem segment_length_prop1 : ∀ n > 0, n = 2 ^ n.size - 2 →
   have : trailing_zeros (2 ^ (n.size - 1)) = n.size - 1 := by
     exact trailing_zeros_prop3 (n.size - 1)
   simp [this]
-  --
-  sorry
+  let n' := 2 ^ (n + 2).size - 2
+  have n'_def : n' = value_of% n' := by exact rfl
+  have n'_is_envelope : n' = 2 ^ n'.size - 2 := by
+    simp [n'_def]
+    have : (2 ^ (n + 2).size - 2).size = (n + 2).size := by
+      refine size_sub ?_ ?_ ?_
+      · exact size_pos.mpr (Nat.add_pos_left n_gt_0 2)
+      · exact Nat.zero_lt_two 
+      · refine Nat.le_self_pow ?_ 2
+        · refine Nat.sub_ne_zero_iff_lt.mpr ?_
+          · exact lt_of_add_left_lt n2size_ge_3
+    simp [this]
+  simp [segment_length]
+  have : segment (2 ^ (n + 2).size - 2) = 2 ^ ((n + 2).size - 1) := by
+    rw [segment]
+    simp
+    split
+    · expose_names
+      have : 2 ^ (n + 2).size - 2 + 2 = 2 ^ (n + 2).size := by
+        refine Nat.sub_add_cancel ?_
+        · refine Nat.le_self_pow ?_ 2
+          · exact Nat.ne_zero_of_lt n2size_ge_3
+      simp [this]
+      replace : (2 ^ (n + 2).size).size = (n + 2).size + 1 := by exact size_pow
+      simp [this]
+    · expose_names
+      have : 2 ^ (n + 2).size - 2 + 2 = 2 ^ (n + 2).size := by
+        refine Nat.sub_add_cancel ?_
+        · exact le_pow (zero_lt_of_lt n2size_ge_3)
+      simp only [this] at h
+      replace : (2 ^ (n + 2).size).size - 1 = (n + 2).size := by 
+        have : (2 ^ (n + 2).size).size = (n + 2).size + 1 := by exact size_pow
+        simp [this]
+      simp [this] at h
+    · intro x
+      have c : 2 ^ (n + 2).size - 2 ≥ 6 := by
+        have s1 : 2 ^ (n + 2).size ≥ 2 ^ (2 + 2).size := by
+          refine Luby.pow2_le_pow2 (2 + 2).size (n + 2).size ?_
+          · exact size_le_size (Nat.add_le_add_right n_gt_2 2)
+        have : 2 ^ (2 + 2).size = 8 := by simp [size, binaryRec]
+        simp [this] at s1
+        exact le_sub_of_add_le s1
+      replace c : ¬2 ^ (n + 2).size - 2 = 0 := by exact Nat.ne_zero_of_lt c
+      exact absurd x c
+  simp [this]
+  replace : trailing_zeros (2 ^ ((n + 2).size - 1)) = (n + 2).size - 1 := by
+    exact trailing_zeros_prop3 ((n + 2).size - 1)
+  simp [this]
+  have n_is_envelope' : n + 2 = 2 ^ n.size := by
+    refine Eq.symm (Nat.eq_add_of_sub_eq ?_ (id (Eq.symm n_is_envelope)))
+    · exact tsub_add_cancel_iff_le.mp pow2nsize
+  simp [n_is_envelope']
+  replace : (2 ^ n.size).size = n.size + 1 := by exact size_pow
+  simp [this]
+  replace : n.size - 1 + 1 = n.size := by
+    refine Nat.sub_add_cancel ?_
+    · have : n.size ≥ 2 := by
+        have s1 : n.size ≥ (2 : ℕ).size := by exact size_le_size n_gt_2
+        have s2 : (2 : ℕ).size = 2 := by simp [size, binaryRec]
+        simp [s2] at s1
+        exact s1
+      exact one_le_of_lt this
+  simp [this]
+  exact Nat.add_comm n.size 1
 
 theorem segment_length_prop2 : ∀ n > 0, ¬n = 2 ^ n.size - 2 → 
     segment_length (2 ^ (n + 2).size - 2) = segment_length n := by