Changes
1 changed files (+36/-36)
-
-
@@ -9,21 +9,19 @@ def kadane (A : Array ℤ) := Id.run doans := 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 := def is_max_nonempty_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 0 ≤ 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 drop_append_sum [AddMonoid α] (xs ys : List α) (hi : i ≤ xs.length) : (xs ++ ys |>.drop i).sum = (xs.drop i).sum + ys.sum := by 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 extract_end_drop (xs : List α) (h : j = xs.length) : xs.extract i j = xs.drop i := by 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 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 rw [List.extract_eq_drop_take, List.drop_append_of_le_length hi, List.take_append_of_le_length (by grind)] open Std.Do
-
@@ -32,47 +30,49 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := bygeneralize h : kadane A = x apply Id.of_wp_run_eq h mvcgen invariants · ⇓⟨xs, ans, cur⟩ => ⌜0 ≤ ans ∧ is_max_suffix xs.prefix cur ∧ is_max_subarray xs.prefix ans⌝ · ⇓⟨xs, ans, cur⟩ => ⌜is_max_nonempty_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.1 use i rw [drop_append_sum pref [cur] hi, hsum] grind · use 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 _ rw [drop_append_sum pref [cur] (by grind)] rw [is_max_suffix] at ih by_cases i = pref.length <;> grind have hcur_1 : is_max_nonempty_suffix (pref ++ [cur]) cur_1 := by constructor · by_cases cur ≤ b.snd + cur · obtain ⟨i, hi, hsum⟩ := ih.1.1 use i rw [drop_append_sum hi, hsum] grind · use pref.length rw [drop_append_sum (Nat.le_refl pref.length)] grind · intro i _ rw [drop_append_sum (by grind)] unfold is_max_nonempty_suffix at ih by_cases i = pref.length <;> grind and_intros · grind · exact cur_1_exists · exact cur_1_max · exact hcur_1.1 · exact hcur_1.2 · unfold is_max_subarray at ih grind · by_cases b.fst ≤ cur_1 · obtain ⟨i, _⟩ := cur_1_exists · obtain ⟨i, _⟩ := hcur_1.1 use i, (by grind), pref.length + 1 constructor · grind · rw [extract_end_drop (pref ++ [cur]) (by grind)] grind rw [extract_end_drop (by grind)] grind · obtain ⟨i, hi, j, hj, _⟩ := ih.2.2.1 use i, (by grind), j, (by grind) rw [extract_in_bounds pref [cur] hi hj] rw [extract_in_bounds hi hj] grind · intro i _ j _ by_cases hi : i ≤ pref.length · by_cases hj : j ≤ pref.length · rw [extract_in_bounds pref [cur] hi hj] · rw [extract_in_bounds hi 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)] · rw [extract_end_drop (by grind)] grw [hcur_1.2 i (by grind)] exact le_max_right b.fst cur_1 · grind case vc2.a.pre => simp [is_max_suffix, is_max_subarray] · have : j - i = 0 := by grind rw [List.extract, this, List.take_zero] unfold is_max_subarray at ih grind case vc2.a.pre => simp [is_max_nonempty_suffix, is_max_subarray] case vc3.a.post => grind
-