Move Kadane to own file

Changes

2 changed files (+78/-85)

• Kadane.lean (new)
  • @@ -0,0 +1,75 @@
    + import Std.Tactic.Do + import Mathlib + + def kadane (A : Array ℤ) := Id.run do + let mut cur := 0 + let mut ans := 0 + for x in A do + cur := max x (cur + x) + ans := max ans cur + return ans + + 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 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 + 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 + rw [List.extract_eq_drop_take, List.drop_append_of_le_length hi, List.take_append_of_le_length (by grind)] + + open Std.Do + + theorem kadane_correct : is_max_subarray A.toList (kadane A) := by + generalize h : kadane A = x + apply Id.of_wp_run_eq h + mvcgen + case inv1 => + -- cur might be negative so the loop invariant can only guarantee ∀ i < xs.prefix.length + exact ⇓⟨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⌝ + all_goals mleave + 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 + 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)] + 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, _⟩ := cur_1_exists + use i, (by grind), pref.length + 1 + constructor + · 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 _ 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 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 vc3.a.post => grind
• Sort.lean
  • @@ -1,81 +1,7 @@
    import Std.Tactic.Do import Mathlib - open Std.Do - - def kadane (A : Array ℤ) := Id.run do - let mut cur := 0 - let mut ans := 0 - for x in A do - cur := max x (cur + x) - ans := max ans cur - return ans - - 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 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 - 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 - 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 - apply Id.of_wp_run_eq h - mvcgen - case inv1 => - -- cur might be negative so the loop invariant can only guarantee ∀ i < xs.prefix.length - exact ⇓⟨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⌝ - all_goals mleave - 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 - 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)] - 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, _⟩ := cur_1_exists - use i, (by grind), pref.length + 1 - constructor - · 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 _ 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]) (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 - - - def BubbleSort [LT α] [DecidableLT α] (A : Array α) : Id (Array α) := do + def BubbleSort [LT α] [DecidableLT α] (A : Array α) := Id.run do let n := A.size let mut A := A.toVector for i in List.range (n - 1) do
  • @@ -85,7 +11,7 @@ def BubbleSort [LT α] [DecidableLT α] (A : Array α) : Id (Array α) := do
    A := A.swap j (j + 1) return A.toArray - def ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) : Id (Array α) := do + def ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) := Id.run do let N := A.size let mut A := A.toVector for hi : i in [:N] do
  • @@ -94,17 +20,9 @@ def ICan'tBelieveItCanSort [LT α] [DecidableLT α] (A : Array α) : Id (Array
    A := A.swap i j return A.toArray - + open Std.Do theorem SortCorrect [LT α] [DecidableLT α] (A : Array α) : Multiset.ofList A.toList = Multiset.ofList (ICan'tBelieveItCanSort A).toList := by generalize h : ICan'tBelieveItCanSort A = x apply Id.of_wp_run_eq h mvcgen - - - - - theorem SortCorrect [LT α] [DecidableLT α] (A : Array α) : ⦃⌜True⌝⦄ BubbleSort A ⦃⇓ r => ⌜Multiset.ofList r.toList = Multiset.ofList A.toList⌝⦄ := by - -- generalize h : ICan'tBelieveItCanSort A = x - -- apply Id.of_wp_run_eq h - mvcgen