MORE GRIND

Changes

1 changed files (+4/-5)

• Kadane.lean
  • @@ -15,12 +15,15 @@ def is_max_nonempty_suffix (xs : List ℤ) m :=
    def is_max_subarray (xs : List ℤ) 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 + @[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] + @[grind] 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] + @[grind] 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)]
  • @@ -38,7 +41,6 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := by
    · 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)]
  • @@ -55,11 +57,9 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := by
    · by_cases b.fst ≤ cur_1 · obtain ⟨i, _⟩ := hcur_1.1 use i, (by grind), pref.length + 1 - 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 hi hj] grind · intro i _ j _ by_cases hi : i ≤ pref.length
  • @@ -72,7 +72,6 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := by
    exact le_max_right b.fst cur_1 · have : j - i = 0 := by grind rw [List.extract, this, List.take_zero] - unfold is_max_subarray at ih - grind + grind [is_max_subarray] case vc2.a.pre => simp [is_max_nonempty_suffix, is_max_subarray] case vc3.a.post => grind