sunblaze-ucb/verina huggingface dataset:
-----Description-----  
This task requires writing a Lean 4 method that rotates a list of integers to the right by a specified number of positions. The method should produce a new list where each element is shifted to the right while preserving the original list's length.

-----Input-----  
The input consists of:  
• l: A list of integers.  
• n: A non-negative natural number that indicates the number of positions by which to rotate the list.

-----Output-----  
The output is a list of integers:  
• Returns a list with the same length as the input list, where the elements have been rotated to the right by n positions.

-----Note-----  
• The precondition requires that n is non-negative.  
• If the input list is empty, it should be returned unchanged.
Difficulty: basic

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, simp]
def rotateRight_precond (l : List Int) (n : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def rotateRight (l : List Int) (n : Nat) (h_precond : rotateRight_precond (l) (n)) : List Int :=
  -- !benchmark @start code
  let len := l.length
  if len = 0 then l
  else
    (List.range len).map (fun i : Nat =>
      let idx_int : Int := ((Int.ofNat i - Int.ofNat n + Int.ofNat len) % Int.ofNat len)
      let idx_nat : Nat := Int.toNat idx_int
      l.getD idx_nat (l.headD 0)
    )
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def rotateRight_postcond (l : List Int) (n : Nat) (result: List Int) (h_precond : rotateRight_precond (l) (n)) :=
  -- !benchmark @start postcond
  result.length = l.length ∧
  (∀ i : Nat, i < l.length →
    let len := l.length
    let rotated_index := Int.toNat ((Int.ofNat i - Int.ofNat n + Int.ofNat len) % Int.ofNat len)
    result[i]? = l[rotated_index]?)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem rotateRight_spec_satisfied (l: List Int) (n: Nat) (h_precond : rotateRight_precond (l) (n)) :
    rotateRight_postcond (l) (n) (rotateRight (l) (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: l: [1, 2, 3, 4, 5]
n: 2
l: [1, 2, 3, 4, 5]
n: 7
l: [1, 2, 3, 4, 5]
n: 0
n: 2
expected: 4
5
1
2
3
4
5
1
2
3
1
2
3
4
5
unexpected: [5, 1, 2, 3, 4]
[3, 4, 5, 1, 2]
[5, 1, 2, 3, 4]
[3, 4, 5, 1, 2]
[5, 1, 2, 3, 4]
[4, 5, 1, 2, 3]
[0]
[42]

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 function that calculates how much water can be trapped between elevations after it rains. The input is a list of non-negative integers representing an elevation map. Each index traps water depending on the min of max heights to its left and right.

-----Input-----
- height: A list of natural numbers representing elevations.

-----Output-----
- A natural number: total units of water that can be trapped.


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, simp]
def trapRainWater_precond (height : List Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def trapRainWater (height : List Nat) (h_precond : trapRainWater_precond (height)) : Nat :=
  -- !benchmark @start code
  Id.run do
    let mut left := 0
    let mut right := height.length - 1
    let mut leftMax := 0
    let mut rightMax := 0
    let mut water := 0

    while left < right do
      let hLeft := height[left]!
      let hRight := height[right]!

      if hLeft < hRight then
        if hLeft >= leftMax then
          leftMax := hLeft
        else
          water := water + (leftMax - hLeft)
        left := left + 1
      else
        if hRight >= rightMax then
          rightMax := hRight
        else
          water := water + (rightMax - hRight)
        right := right - 1

    return water
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def trapRainWater_postcond (height : List Nat) (result: Nat) (h_precond : trapRainWater_precond (height)) : Prop :=
  -- !benchmark @start postcond
  let waterAt := List.range height.length |>.map (fun i =>
    let lmax := List.take (i+1) height |>.foldl Nat.max 0
    let rmax := List.drop i height |>.foldl Nat.max 0
    Nat.min lmax rmax - height[i]!)

  result - (waterAt.foldl (· + ·) 0) = 0 ∧ (waterAt.foldl (· + ·) 0) ≤ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem trapRainWater_spec_satisfied (height: List Nat) (h_precond : trapRainWater_precond (height)) :
    trapRainWater_postcond (height) (trapRainWater (height) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that determines whether a given number `n` is an Armstrong number (also known as a Narcissistic number). An Armstrong number is a number that is equal to the sum of its own digits raised to the power of the number of digits.

-----Input-----
The input consists of one natural number:
- `n: Nat`: The number to check if it satisfies the Armstrong property.

-----Output-----
The output is a boolean value:
- `Bool`: Return `true` if `n` is an Armstrong number, otherwise return `false`.


Difficulty: advanced

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def countDigits (n : Nat) : Nat :=
  let rec go (n acc : Nat) : Nat :=
    if n = 0 then acc
    else go (n / 10) (acc + 1)
  go n (if n = 0 then 1 else 0)
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def isArmstrong_precond (n : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def sumPowers (n : Nat) (k : Nat) : Nat :=
  let rec go (n acc : Nat) : Nat :=
    if n = 0 then acc
    else
      let digit := n % 10
      go (n / 10) (acc + digit ^ k)
  go n 0
-- !benchmark @end code_aux


def isArmstrong (n : Nat) (h_precond : isArmstrong_precond (n)) : Bool :=
  -- !benchmark @start code
  let k := countDigits n
  sumPowers n k = n
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def isArmstrong_postcond (n : Nat) (result: Bool) (h_precond : isArmstrong_precond (n)) : Prop :=
  -- !benchmark @start postcond
  let n' := List.foldl (fun acc d => acc + d ^ countDigits n) 0 (List.map (fun c => c.toNat - '0'.toNat) (toString n).toList)
  (result → (n = n')) ∧
  (¬ result → (n ≠ n'))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isArmstrong_spec_satisfied (n: Nat) (h_precond : isArmstrong_precond (n)) :
    isArmstrong_postcond (n) (isArmstrong (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: n: 0
n: 1
n: 10
n: 153
n: 9474
n: 9475
expected: True
True
False
True
True
False
unexpected: False
False
True
False
False
True

Inputs rejected by the precondition:
-----Description-----
Implement a Lean 4 function that checks if a given string is a palindrome. A string is considered a palindrome
if it reads the same forward and backward.

-----Input-----
The input consists of a single string:
s: A string

-----Output-----
The output is a boolean:
Returns true if s is a palindrome, false otherwise.


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, simp]
def isPalindrome_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isPalindrome (s : String) (h_precond : isPalindrome_precond (s)) : Bool :=
  -- !benchmark @start code
  let length := s.length

if length <= 1 then
  true
else
  let arr := s.toList

  let rec checkIndices (left : Nat) (right : Nat) (chars : List Char) : Bool :=
    if left >= right then
      true
    else
      match chars[left]?, chars[right]? with
      | some cLeft, some cRight =>
        if cLeft == cRight then
          checkIndices (left + 1) (right - 1) chars
        else
          false
      | _, _ => false
  let approach1 := checkIndices 0 (length - 1) arr

  let rec reverseList (acc : List Char) (xs : List Char) : List Char :=
    match xs with
    | []      => acc
    | h :: t  => reverseList (h :: acc) t
  let reversed := reverseList [] arr
  let approach2 := (arr == reversed)

  approach1 && approach2
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def isPalindrome_postcond (s : String) (result: Bool) (h_precond : isPalindrome_precond (s)) : Prop :=
  -- !benchmark @start postcond
  (result → (s.toList == s.toList.reverse)) ∧
  (¬ result → (s.toList ≠ [] ∧ s.toList != s.toList.reverse))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isPalindrome_spec_satisfied (s: String) (h_precond : isPalindrome_precond (s)) :
    isPalindrome_postcond (s) (isPalindrome (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: racecar
s: abba
s: abc
s: a
expected: True
True
False
True
True
unexpected: False
False
True
False
False

Inputs rejected by the precondition:
-----Description-----  
This task requires developing a solution that sorts an array of integers in non-decreasing order. The solution must return an array that is a rearrangement of the input, containing exactly the same elements but ordered from smallest to largest.

-----Input-----  
The input consists of:  
• a: An array of integers. This array can be empty or non-empty.

-----Output-----  
The output is an array of integers that:  
• Is sorted in non-decreasing order (i.e., for any indices i and j with i < j, a[i]! ≤ a[j]!).  
• Has the same size as the input array.  
• Contains exactly the same elements as the input array, ensuring that the multiset of elements is preserved.

-----Note-----  
The implementation uses helper functions for swapping elements and performing inner and outer loops of the bubble sort algorithm. No additional preconditions are required as the function should correctly handle empty and non-empty arrays.
Difficulty: basic

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, simp]
def BubbleSort_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def swap (a : Array Int) (i j : Nat) : Array Int :=
  let temp := a[i]!
  let a₁ := a.set! i (a[j]!)
  a₁.set! j temp

def bubbleInner (j i : Nat) (a : Array Int) : Array Int :=
  if j < i then
    let a' := if a[j]! > a[j+1]! then swap a j (j+1) else a
    bubbleInner (j+1) i a'
  else
    a

def bubbleOuter (i : Nat) (a : Array Int) : Array Int :=
  if i > 0 then
    let a' := bubbleInner 0 i a
    bubbleOuter (i - 1) a'
  else
    a
-- !benchmark @end code_aux


def BubbleSort (a : Array Int) (h_precond : BubbleSort_precond (a)) : Array Int :=
  -- !benchmark @start code
  if a.size = 0 then a else bubbleOuter (a.size - 1) a
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def BubbleSort_postcond (a : Array Int) (result: Array Int) (h_precond : BubbleSort_precond (a)) :=
  -- !benchmark @start postcond
  List.Pairwise (· ≤ ·) result.toList ∧ List.isPerm result.toList a.toList
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem BubbleSort_spec_satisfied (a: Array Int) (h_precond : BubbleSort_precond (a)) :
    BubbleSort_postcond (a) (BubbleSort (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[5, 4, 3, 2, 1]
a: #[1, 2, 3, 4, 5]
a: #[3, 1, 2, 1, 5]
a: #[10]
a: #[4, 4, 4, 2, 2, 8]
expected: #[1, 2, 3, 4, 5]
#[1, 2, 3, 4, 5]
#[1, 1, 2, 3, 5]
#[10]
#[2, 2, 4, 4, 4, 8]
unexpected: #[5, 4, 3, 2, 1]
#[2, 3, 1, 4, 5]
#[5, 4, 3, 2, 1]
#[1, 3, 2, 4, 5]
#[1, 2, 3, 1, 5]
#[3, 1, 2, 5, 1]
#[0]
#[10, 10]
#[2, 4, 4, 2, 4, 8]
#[4, 2, 4, 2, 4, 8]
#[2, 4, 2, 4, 4, 8]

Inputs rejected by the precondition:
-----Description-----  
This problem involves determining the longest common prefix shared by two lists of characters. Given two sequences, the goal is to identify and return the maximal contiguous sequence of characters from the beginning of both lists that are identical. 

-----Input-----  
The input consists of:  
• str1: A list of characters.  
• str2: A list of characters.

-----Output-----  
The output is a list of characters representing the longest common prefix of the two input lists. The output list satisfies the following conditions:  
• Its length is less than or equal to the length of each input list.  
• It is exactly the prefix of both str1 and str2.  
• It is empty if the first characters of the inputs differ or if one of the lists is empty.

-----Note-----  
It is assumed that both inputs are provided as valid lists of characters. The function always returns the correct longest common prefix based on the inputs.
Difficulty: basic

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, simp]
def LongestCommonPrefix_precond (str1 : List Char) (str2 : List Char) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def LongestCommonPrefix (str1 : List Char) (str2 : List Char) (h_precond : LongestCommonPrefix_precond (str1) (str2)) : List Char :=
  -- !benchmark @start code
  let minLength := Nat.min str1.length str2.length
  let rec aux (idx : Nat) (acc : List Char) : List Char :=
    if idx < minLength then
      match str1[idx]?, str2[idx]? with
      | some c1, some c2 =>
          if c1 ≠ c2 then acc
          else aux (idx + 1) (acc ++ [c1])
      | _, _ => acc
    else acc
  aux 0 []
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def LongestCommonPrefix_postcond (str1 : List Char) (str2 : List Char) (result: List Char) (h_precond : LongestCommonPrefix_precond (str1) (str2)) :=
  -- !benchmark @start postcond
  (result.length ≤ str1.length) ∧ (result = str1.take result.length) ∧
  (result.length ≤ str2.length) ∧ (result = str2.take result.length) ∧
  (result.length = str1.length ∨ result.length = str2.length ∨
    (str1[result.length]? ≠ str2[result.length]?))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem LongestCommonPrefix_spec_satisfied (str1: List Char) (str2: List Char) (h_precond : LongestCommonPrefix_precond (str1) (str2)) :
    LongestCommonPrefix_postcond (str1) (str2) (LongestCommonPrefix (str1) (str2) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: str1: a, b, c
str2: a, b, d
str1: x, y, z
str2: x, y, z
str1: w, o
str2: w, o, w
str1: a, x
str2: b, y
str2: h, e, l, l, o
expected: a, b
x, y, z
w, o
unexpected: a
a, b, c
x, y
x, z
w
o
w, o, w
a
b
h
e

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that extracts even numbers from an array of integers. The method should return a new array containing only the even numbers found in the input array, while preserving the order in which they appear.

-----Input-----
The input consists of:
arr: An array of integers.

-----Output-----
The output is an array of integers:
Returns an array containing all the even numbers from the input array. Specifically:
- Every element in the output array is an even integer.
- All even integers present in the input array are included in the output array.
- The relative order of the even integers is preserved as in the input array.

-----Note-----
There are no preconditions for this task; the method will work with any array, including empty arrays (which are not null).
Difficulty: basic

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def isEven (n : Int) : Bool :=
  n % 2 = 0
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

@[reducible, simp]
def findEvenNumbers_precond (arr : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def findEvenNumbers (arr : Array Int) (h_precond : findEvenNumbers_precond (arr)) : Array Int :=
  -- !benchmark @start code
  arr.foldl (fun acc x => if isEven x then acc.push x else acc) #[]
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def findEvenNumbers_postcond (arr : Array Int) (result: Array Int) (h_precond : findEvenNumbers_precond (arr)) :=
  -- !benchmark @start postcond
  (∀ x, x ∈ result → isEven x ∧ x ∈ arr.toList) ∧
  (∀ x, x ∈ arr.toList → isEven x → x ∈ result) ∧
  (∀ x y, x ∈ arr.toList → y ∈ arr.toList →
    isEven x → isEven y →
    arr.toList.idxOf x ≤ arr.toList.idxOf y →
    result.toList.idxOf x ≤ result.toList.idxOf y)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem findEvenNumbers_spec_satisfied (arr: Array Int) (h_precond : findEvenNumbers_precond (arr)) :
    findEvenNumbers_postcond (arr) (findEvenNumbers (arr) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: arr: #[1, 2, 3, 4, 5, 6]
arr: #[7, 8, 10, 13, 14]
arr: #[1, 3, 5, 7]
arr: #[]
arr: #[0, -2, -3, -4, 5]
expected: #[2, 4, 6]
#[8, 10, 14]
#[]
#[]
#[0, -2, -4]
unexpected: #[1, 2, 3]
#[2, 3, 4, 6]
#[7, 8, 10]
#[8, 14]
#[1]
#[1, 3]
#[0]
#[1]
#[0, -3, -4]
#[-2, -4]

Inputs rejected by the precondition:
-----Description-----  
This task involves computing the integer square root of a given natural number. The goal is to determine the largest natural number r that satisfies r * r ≤ N and N < (r + 1) * (r + 1).

-----Input-----  
The input consists of:  
• N: A natural number.

-----Output-----  
The output is a natural number r that meets the following conditions:  
• r * r ≤ N  
• N < (r + 1) * (r + 1)

-----Note-----  
The implementation relies on a recursive strategy to iteratively increment r until (r + 1)*(r + 1) exceeds N. Edge cases, such as N = 0, should be handled correctly.
Difficulty: basic

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, simp]
def SquareRoot_precond (N : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def SquareRoot (N : Nat) (h_precond : SquareRoot_precond (N)) : Nat :=
  -- !benchmark @start code
  let rec boundedLoop : Nat → Nat → Nat
    | 0, r => r
    | bound+1, r =>
        if (r + 1) * (r + 1) ≤ N then
          boundedLoop bound (r + 1)
        else
          r
  boundedLoop (N+1) 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def SquareRoot_postcond (N : Nat) (result: Nat) (h_precond : SquareRoot_precond (N)) :=
  -- !benchmark @start postcond
  result * result ≤ N ∧ N < (result + 1) * (result + 1)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem SquareRoot_spec_satisfied (N: Nat) (h_precond : SquareRoot_precond (N)) :
    SquareRoot_postcond (N) (SquareRoot (N) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: N: 0
N: 1
N: 15
N: 16
N: 26
expected: 0
1
3
4
5
unexpected: 1
2
0
2
2
4
5
3
5
6
4
6
7

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 function that finds the majority element in a list of integers. The majority element is the element that appears more than ⌊n/2⌋ times, where n is the list’s length. You may assume that a majority element always exists in the input.

-----Input-----
- nums: A list of integers of length ≥ 1, containing a majority element.

-----Output-----
- An integer: the element that appears more than ⌊n/2⌋ times.


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 majorityElement_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  nums.length > 0 ∧ nums.any (fun x => nums.count x > nums.length / 2)
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def majorityElement (nums : List Int) (h_precond : majorityElement_precond (nums)) : Int :=
  -- !benchmark @start code
  Id.run do
    let mut counts : HashMap Int Nat := {}
    let n := nums.length
    for x in nums do
      let count := counts.getD x 0
      counts := counts.insert x (count + 1)
    match counts.toList.find? (fun (_, c) => c > n / 2) with
    | some (k, _) => k
    | none      => 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def majorityElement_postcond (nums : List Int) (result: Int) (h_precond : majorityElement_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let n := nums.length
  (nums.count result) > n / 2
  ∧ ∀ x ∈ nums, x ≠ result → nums.count x ≤ n / 2
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem majorityElement_spec_satisfied (nums: List Int) (h_precond : majorityElement_precond (nums)) :
    majorityElement_postcond (nums) (majorityElement (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: [3, 2, 3]
nums: [2, 2, 1, 1, 1, 2, 2]
nums: [1, 1, 1, 2, 3, 1]
nums: [0, 0, 0, 0]
nums: [7]
expected: 3
2
1
0
7
unexpected: 2
1
2
3
1

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