Simplify Kadane proof

Changes

1 changed files (+20/-27)

• Sort.lean
  • @@ -14,19 +14,14 @@ def kadane (A : Array ℤ) := Id.run do
    def is_max_subarray (xs : List ℤ) m := (∃ i ≤ xs.length, ∃ j ≤ xs.length, (xs.extract i j).sum = m) ∧ ∀ i ≤ xs.length, ∀ j ≤ xs.length, (xs.extract i j).sum ≤ m - lemma concat_drop (xs ys : List α) (hi : i ≤ xs.length) : (xs ++ ys).drop i = (xs.drop i) ++ ys := by - fun_induction List.drop <;> grind + lemma drop_append_sum [AddMonoid α] (xs ys : List α) (hi : i ≤ xs.length) : (xs ++ ys |>.drop i).sum = (xs.drop i).sum + ys.sum := by + rw [List.drop_append_of_le_length hi, List.sum_append] - lemma concat_drop_sum [AddMonoid α] (xs ys : List α) (hi : i ≤ xs.length) : (xs ++ ys |>.drop i).sum = (xs.drop i).sum + ys.sum := by - rw [concat_drop xs ys hi, List.sum_append] - - lemma extract_end_drop (xs : List α) i j (h : j = xs.length) : xs.extract i j = xs.drop i := by - simp [h] + lemma extract_end_drop (xs : List α) (h : j = xs.length) : xs.extract i j = xs.drop i := by + rw [h, List.extract_eq_drop_take, List.take_eq_self_iff, List.length_drop] lemma extract_in_bounds (xs ys : List α) (hi : i ≤ xs.length) (hj : j ≤ xs.length) : (xs ++ ys).extract i j = xs.extract i j := by - simp - rw [concat_drop xs ys hi] - exact List.take_append_of_le_length (by grind) + rw [List.extract_eq_drop_take, List.drop_append_of_le_length hi, List.take_append_of_le_length (by grind)] theorem kadane_correct A : is_max_subarray A.toList (kadane A) := by generalize h : kadane A = x
  • @@ -40,46 +35,44 @@ theorem kadane_correct A : is_max_subarray A.toList (kadane A) := by
    expose_names have cur_1_exists : ∃ i ≤ (pref ++ [cur]).length, (List.drop i (pref ++ [cur])).sum = cur_1 := by by_cases cur ≤ b.snd + cur - · obtain ⟨i, hi⟩ := ih.2.1 + · obtain ⟨i, hi, hsum⟩ := ih.2.1 use i - rw [concat_drop_sum pref [cur] hi.1, hi.2] + rw [drop_append_sum pref [cur] hi, hsum] grind · use pref.length - rw [concat_drop_sum pref [cur] (Nat.le_refl pref.length)] + rw [drop_append_sum pref [cur] (Nat.le_refl pref.length)] grind have cur_1_max : ∀ i < (pref ++ [cur]).length, (List.drop i (pref ++ [cur])).sum ≤ cur_1 := by - intro i hi - rw [concat_drop_sum pref [cur] (by grind)] + intro i _ + rw [drop_append_sum pref [cur] (by grind)] by_cases i = pref.length <;> grind and_intros · grind · exact cur_1_exists · exact cur_1_max · by_cases b.fst ≤ cur_1 - · obtain ⟨i, hi⟩ := cur_1_exists + · obtain ⟨i, _⟩ := cur_1_exists use i, (by grind), pref.length + 1 constructor · grind - · rw [extract_end_drop (pref ++ [cur]) i (pref.length + 1) (by grind)] + · rw [extract_end_drop (pref ++ [cur]) (by grind)] grind · obtain ⟨i, hi, j, hj, _⟩ := ih.2.2.2.1 use i, (by grind), j, (by grind) rw [extract_in_bounds pref [cur] hi hj] grind - · intro i hi j hj - by_cases hi₂ : i ≤ pref.length - · by_cases hj₂ : j ≤ pref.length - · rw [extract_in_bounds pref [cur] hi₂ hj₂] - grw [ih.2.2.2.2 i hi₂ j hj₂] + · intro i _ j _ + by_cases hi : i ≤ pref.length + · by_cases hj : j ≤ pref.length + · rw [extract_in_bounds pref [cur] hi hj] + grw [ih.2.2.2.2 i hi j hj] exact Int.le_max_left b.fst cur_1 - · rw [extract_end_drop (pref ++ [cur]) i j (by grind)] + · rw [extract_end_drop (pref ++ [cur]) (by grind)] grw [cur_1_max i (by grind)] exact Int.le_max_right b.fst cur_1 · grind - case vc2.a.pre => - simp [is_max_subarray] - case vc3.a.post => - grind + case vc2.a.pre => simp [is_max_subarray] + case vc3.a.post => grind def BubbleSort [LT α] [DecidableLT α] (A : Array α) : Id (Array α) := do