-----Description----- 
Given an integer array arr and a positive integer k, this task requires writing a Lean 4 method that finds the
maximum sum of a subarray of arr, such that the length of the subarray is divisible by k.
If the array is empty, or generally if there exists no subarray with length divisible by k, 
the default return value should be 0.

-----Input-----
The input consists of:
arr: The array of integers.
k: An integer larger than 1.

-----Output-----
The output is an integer:
Returns the maximum positive integer x such that there exists a subarray where the sum equals x, and the length
of the subarray is divisible by k.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def maxSubarraySumDivisibleByK_precond (arr : Array Int) (k : Int) : Prop :=
  -- !benchmark @start precond
  k > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def maxSubarraySumDivisibleByK (arr : Array Int) (k : Int) : Int :=
  -- !benchmark @start code
  let n := arr.size
  if n = 0 || k = 0 then 0
  else
    --compute prefix sums for efficient subarray sum calculation
    let prefixSums := Id.run do
      let mut prefixSums := Array.mkArray (n + 1) 0
      for i in [0:n] do
        prefixSums := prefixSums.set! (i+1) (prefixSums[i]! + arr[i]!)
      prefixSums

    let minElem := Id.run do -- find minimum element
      let mut minElem := arr[0]!
      for elem in arr do
        minElem := min minElem elem
      minElem
    let maxSum := Id.run do
      let mut maxSum := minElem - 1
      --check all subarrays with length divisible by k
      for len in List.range (n+1) do
        if len % k = 0 && len > 0 then
          for start in [0:(n - len + 1)] do
            let endIdx := start + len
            let subarraySum := prefixSums[endIdx]! - prefixSums[start]!
            maxSum := max maxSum subarraySum
      maxSum

    let default : Int := minElem - 1
    if maxSum = default then 0 else maxSum
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def maxSubarraySumDivisibleByK_postcond (arr : Array Int) (k : Int) (result: Int) : Prop :=
  -- !benchmark @start postcond
  let subarrays := List.range (arr.size) |>.flatMap (fun start =>
    List.range (arr.size - start + 1) |>.map (fun len => arr.extract start (start + len)))
  let divisibleSubarrays := subarrays.filter (fun subarray => subarray.size % k.toNat = 0 && subarray.size > 0)
  let subarraySums := divisibleSubarrays.map (fun subarray => subarray.toList.sum)
  -- No valid subarrays -> result is 0
  (subarraySums.length = 0 → result = 0) ∧
  -- Valid subarrays exist -> result is the maximum sum
  (subarraySums.length > 0 → result ∈ subarraySums ∧ subarraySums.all (fun sum => sum ≤ result))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem maxSubarraySumDivisibleByK_spec_satisfied (arr: Array Int) (k: Int) :
    maxSubarraySumDivisibleByK_postcond (arr) (k) (maxSubarraySumDivisibleByK (arr) (k)) := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: arr: #[1, 2, 3, 4, 5]
k: 2
arr: #[1, -2, 3, -4, 5]
k: 3
arr: #[]
k: 5
arr: #[1, 2, 3, 4]
k: 1
arr: #[-2, 7, 1, 3]
k: 2
arr: #[-100, 0, 1]
k: 5
arr: #[1999, 1, -1023, 12351, -9999]
k: 2
expected: 14
4
0
10
9
0
13328
unexpected: 9
5
15
10
2
5
3
-1
3
4
7
9
8
11
7
1
-99
1999
12351
3329
2352

Inputs rejected by the precondition: