-----Description-----
This task requires writing a Lean 4 method that returns the integer that appears most frequently in the input list. If multiple integers have the same maximum frequency, return the one that appears first in the original list. You should implement a frequency counter using a fold over the list, extract the maximum frequency, and return the first element in the list that matches it.

-----Input-----
The input consists of:
xs: A list of integers (possibly with duplicates). The list is guaranteed to be non-empty.

-----Output-----
The output is an integer:
Returns the number that appears the most frequently in the list. If there is a tie, the element that occurs first in the original list should be returned.


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 mostFrequent_precond (xs : List Int) : Prop :=
  -- !benchmark @start precond
  xs ≠ []
  -- !benchmark @end precond


-- !benchmark @start code_aux
-- Build a frequency map from the list
def countMap (xs : List Int) : HashMap Int Nat :=
  let step := fun m x =>
    let current := m.getD x 0
    m.insert x (current + 1)
  let init := (HashMap.empty : HashMap Int Nat)
  xs.foldl step init

-- Compute the maximum frequency in the map
def getMaxFrequency (m : HashMap Int Nat) : Nat :=
  let step := fun acc (_k, v) =>
    if v > acc then v else acc
  let init := 0
  m.toList.foldl step init

-- Extract all keys whose frequency == maxFreq
def getCandidates (m : HashMap Int Nat) (maxFreq : Nat) : List Int :=
  let isTarget := fun (_k, v) => v = maxFreq
  let extract := fun (k, _) => k
  m.toList.filter isTarget |>.map extract

-- Return the first candidate element from original list
def getFirstWithFreq (xs : List Int) (candidates : List Int) : Int :=
  match xs.find? (fun x => candidates.contains x) with
  | some x => x
  | none => 0
-- !benchmark @end code_aux


def mostFrequent (xs : List Int) (h_precond : mostFrequent_precond (xs)) : Int :=
  -- !benchmark @start code
  let freqMap := countMap xs
  let maxF := getMaxFrequency freqMap
  let candidates := getCandidates freqMap maxF
  getFirstWithFreq xs candidates
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def mostFrequent_postcond (xs : List Int) (result: Int) (h_precond : mostFrequent_precond (xs)) : Prop :=
  -- !benchmark @start postcond
  let count := fun x => xs.countP (fun y => y = x)
  result ∈ xs ∧
  xs.all (fun x => count x ≤ count result) ∧
  ((xs.filter (fun x => count x = count result)).head? = some result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem mostFrequent_spec_satisfied (xs: List Int) (h_precond : mostFrequent_precond (xs)) :
    mostFrequent_postcond (xs) (mostFrequent (xs) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: xs: [1, 2, 2, 3]
xs: [4, 4, 5, 5, 4]
xs: [9]
xs: [1, 2, 3, 1, 2, 3, 2]
xs: [7, 7, 8, 8, 9, 9, 7]
expected: 2
4
9
2
7
unexpected: 1
3
5
0
1
3
8
9

Inputs rejected by the precondition: