Don't tag Kadane lemmas with @[grind] for perf reasons

Changes

1 changed files (+8/-16)

• Kadane.lean
  • @@ -15,15 +15,12 @@ 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] + simp [List.drop_append_of_le_length hi] - @[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] + simp [h] - @[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)]
  • @@ -41,26 +38,23 @@ 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 - grind + grind [drop_append_sum] · 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 + by_cases i = pref.length <;> grind [is_max_nonempty_suffix] and_intros · exact hcur_1.1 · exact hcur_1.2 - · unfold is_max_subarray at ih - grind + · grind [is_max_subarray] · by_cases b.fst ≤ cur_1 · obtain ⟨i, _⟩ := hcur_1.1 use i, (by grind), pref.length + 1 - grind + grind [extract_end_drop] · obtain ⟨i, hi, j, hj, _⟩ := ih.2.2.1 use i, (by grind), j, (by grind) - grind + grind [extract_in_bounds] · intro i _ j _ by_cases hi : i ≤ pref.length · by_cases hj : j ≤ pref.length
  • @@ -70,8 +64,6 @@ theorem kadane_correct : is_max_subarray A.toList (kadane A) := by
    · rw [extract_end_drop (by grind)] grw [hcur_1.2 i (by grind)] exact le_max_right b.fst cur_1 - · have : j - i = 0 := by grind - rw [List.extract, this, List.take_zero] - grind [is_max_subarray] + · grind [is_max_subarray] case vc2.a.pre => trivial case vc3.a.post => grind