1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30

import Std.Tactic.Do
import Mathlib.Analysis.Normed.Ring.Lemmas

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_nonempty_suffix (xs : List ℤ) m :=
  (∃ i ≤ xs.length, (xs.drop i).sum = m) ∧ ∀ i < xs.length, (xs.drop i).sum ≤ 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

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 invariants
  · ⇓⟨xs, ans, cur⟩ => ⌜is_max_nonempty_suffix xs.prefix cur ∧ is_max_subarray xs.prefix ans⌝
  case vc1.step ih =>
    sorry
  case vc2.a.pre =>
    sorry
  case vc3.a.post =>
    sorry