Refactor Kadane proof

Changes

1 changed files (+11/-6)

• Kadane.lean
  • @@ -9,6 +9,11 @@ def kadane (A : Array ℤ) := Id.run do
    ans := max ans cur return ans + -- cur might be negative which is smaller than [].sum, so we use ∀ i < xs.length instead of ≤ + def is_max_suffix (xs : List ℤ) m := + (∃ i ≤ xs.length, (xs.drop i).sum = m) ∧ ∀ i < xs.length, (xs.drop i).sum ≤ m + + -- ans is always nonnegative 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
  • @@ -27,13 +32,12 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := by
    generalize h : kadane A = x apply Id.of_wp_run_eq h mvcgen invariants - · -- cur might be negative so the loop invariant can only guarantee ∀ i < xs.prefix.length - ⇓⟨xs, ans, cur⟩ => ⌜0 ≤ ans ∧ (∃ i ≤ xs.prefix.length, (xs.prefix.drop i).sum = cur) ∧ (∀ i < xs.prefix.length, (xs.prefix.drop i).sum ≤ cur) ∧ is_max_subarray xs.prefix ans⌝ + · ⇓⟨xs, ans, cur⟩ => ⌜0 ≤ ans ∧ is_max_suffix xs.prefix cur ∧ is_max_subarray xs.prefix ans⌝ case vc1.step ih => 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, hsum⟩ := ih.2.1 + · obtain ⟨i, hi, hsum⟩ := ih.2.1.1 use i rw [drop_append_sum pref [cur] hi, hsum] grind
  • @@ -43,6 +47,7 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := by
    have cur_1_max : ∀ i < (pref ++ [cur]).length, (List.drop i (pref ++ [cur])).sum ≤ cur_1 := by intro i _ rw [drop_append_sum pref [cur] (by grind)] + rw [is_max_suffix] at ih by_cases i = pref.length <;> grind and_intros · grind
  • @@ -55,7 +60,7 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := by
    · grind · rw [extract_end_drop (pref ++ [cur]) (by grind)] grind - · obtain ⟨i, hi, j, hj, _⟩ := ih.2.2.2.1 + · obtain ⟨i, hi, j, hj, _⟩ := ih.2.2.1 use i, (by grind), j, (by grind) rw [extract_in_bounds pref [cur] hi hj] grind
  • @@ -63,11 +68,11 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := by
    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] + grw [ih.2.2.2 i hi j hj] exact le_max_left b.fst cur_1 · rw [extract_end_drop (pref ++ [cur]) (by grind)] grw [cur_1_max i (by grind)] exact le_max_right b.fst cur_1 · grind - case vc2.a.pre => simp [is_max_subarray] + case vc2.a.pre => simp [is_max_suffix, is_max_subarray] case vc3.a.post => grind