Changes
1 changed files (+34/-24)
-
-
@@ -20,6 +20,14 @@ lemma concat_drop (xs ys : List α) (hi : i ≤ xs.length) : (xs ++ ys).drop i =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_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) theorem kadane_correct A : is_max_subarray A.toList (kadane A) := by generalize h : kadane A = x apply Id.of_wp_run_eq h
-
@@ -29,43 +37,45 @@ theorem kadane_correct A : is_max_subarray A.toList (kadane A) := byexact ⇓⟨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 => obtain ⟨h₁, h₂, h₃⟩ := ih expose_names and_intros · grind · by_cases h₄ : cur ≤ b.snd + cur · obtain ⟨i, hi⟩ := h₁ 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 use i rw [concat_drop_sum pref [cur] hi.1, hi.2] grind · use pref.length rw [concat_drop_sum pref [cur] (Nat.le_refl pref.length)] grind · intro i hi 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)] by_cases h₄ : i < pref.length · grind · have : i = pref.length := by grind grind · by_cases h₄ : b.fst ≤ cur_1 · obtain ⟨i, _⟩ := h₁ 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 use i, (by grind), pref.length + 1 constructor · grind · sorry -- obvious · unfold is_max_subarray at h₃ obtain ⟨i, hi, j, hj, _⟩ := h₃.1 · rw [extract_end_drop (pref ++ [cur]) i (pref.length + 1) (by grind)] grind · obtain ⟨i, hi, j, hj, _⟩ := ih.2.2.2.1 use i, (by grind), j, (by grind) sorry rw [extract_in_bounds pref [cur] hi hj] grind · intro i hi j hj by_cases h₄ : i ≤ pref.length · by_cases h₅ : j ≤ pref.length · sorry · sorry · by_cases h₅ : j ≤ pref.length · sorry · have : j - i = 0 := by grind grind 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)] 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 =>
-