-----Description----- 
You are given a natural number array nums and a natural number k.
The frequency of an element x is the number of times it occurs in an array.
An array is called good if the frequency of each element in this array is less than or equal to k.
Return the length of the longest good subarray of nums.
A subarray is a contiguous non-empty sequence of elements within an array.

-----Input-----
The input consists of an array of natural numbers nums and a positive natural number k:
nums: an array of natural numbers.
k: a positive natural number (k > 0)

-----Output-----
The output is a natural number:
Return the length of the longest good subarray of nums.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution
import Std.Data.HashMap
open Std
-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def longestGoodSubarray_precond (nums : List Nat) (k : Nat) : Prop :=
  -- !benchmark @start precond
  k > 0  -- k must be positive for non-trivial subarrays
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def longestGoodSubarray (nums : List Nat) (k : Nat) (h_precond : longestGoodSubarray_precond (nums) (k)) : Nat :=
  -- !benchmark @start code
  Id.run do
    let arr := nums.toArray
    let mut left := 0
    let mut maxLen := 0
    let mut freq : HashMap Nat Nat := {}

    for right in [0:arr.size] do
      let num := arr[right]!
      let count := freq.getD num 0
      freq := freq.insert num (count + 1)

      -- If any frequency > k, shrink the window from the left
      while freq.toList.any (fun (_, v) => v > k) do
        let lnum := arr[left]!
        let lcount := freq.getD lnum 0
        if lcount = 1 then
          freq := freq.erase lnum
        else
          freq := freq.insert lnum (lcount - 1)
        left := left + 1

      maxLen := max maxLen (right - left + 1)

    return maxLen
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def longestGoodSubarray_postcond (nums : List Nat) (k : Nat) (result: Nat) (h_precond : longestGoodSubarray_precond (nums) (k)) : Prop :=
  -- !benchmark @start postcond
  let subArrays :=
    List.range (nums.length + 1) |>.flatMap (fun start =>
      List.range (nums.length - start + 1) |>.map (fun len =>
        nums.drop start |>.take len))
  let subArrayFreqs := subArrays.map (fun arr => arr.map (fun x => arr.count x))
  let validSubArrays := subArrayFreqs.filter (fun arr => arr.all (fun x => x ≤ k))

  (nums = [] ∧ result = 0) ∨
  (nums ≠ [] ∧
    validSubArrays.any (fun arr => arr.length = result) ∧
    validSubArrays.all (fun arr => arr.length ≤ result))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem longestGoodSubarray_spec_satisfied (nums: List Nat) (k: Nat) (h_precond : longestGoodSubarray_precond (nums) (k)) :
    longestGoodSubarray_postcond (nums) (k) (longestGoodSubarray (nums) (k) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: [1, 2, 3, 1, 2, 3, 1, 2]
k: 2
nums: [1, 2, 1, 2, 1, 2, 1, 2]
k: 1
nums: [5, 5, 5, 5, 5, 5, 5]
k: 4
nums: [1]
k: 1
nums: [2, 2, 1, 1, 3]
k: 2
expected: 6
2
4
1
5
unexpected: 5
7
8
1
3
4
3
5
7
0
2
2
3
4
6

Inputs rejected by the precondition:
nums: [1, 2, 3]
k: 0
k: 0