sunblaze-ucb/verina huggingface dataset:
-----Description-----  
This task requires writing a Lean 4 method that extracts the last digit of a given non-negative integer. The method should return the last digit, which is obtained by computing the remainder when the number is divided by 10. The result must always be between 0 and 9.

-----Input-----  
The input consists of a single value:  
n: A non-negative integer.

-----Output-----  
The output is an integer:  
Returns the last digit of the input number, ensuring that the digit lies within the range 0 to 9.

-----Note-----  
It is assumed that the input number n is non-negative.
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 lastDigit_precond (n : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def lastDigit (n : Nat) (h_precond : lastDigit_precond (n)) : Nat :=
  -- !benchmark @start code
  n % 10
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def lastDigit_postcond (n : Nat) (result: Nat) (h_precond : lastDigit_precond (n)) :=
  -- !benchmark @start postcond
  (0 ≤ result ∧ result < 10) ∧
  (n % 10 - result = 0 ∧ result - n % 10 = 0)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem lastDigit_spec_satisfied (n: Nat) (h_precond : lastDigit_precond (n)) :
    lastDigit_postcond (n) (lastDigit (n) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold lastDigit lastDigit_postcond
  constructor
  · constructor
    · simp
    · exact Nat.mod_lt n (by decide)
  · simp
  -- !benchmark @end proof


Tests:
input: n: 123
n: 0
n: 987654321
n: 10
n: 999
n: 45
n: 100
n: 5
expected: 3
0
1
0
9
5
0
5
unexpected: 2
1
23
10
5
9
9
0
2
1
10
5
8
99
0
4
0
55
1
10
5
4
0
6

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that returns the smallest natural number missing from a given sorted list of natural numbers. In other words, starting from 0, the method should identify the first natural number that does not appear in the list. The input list is assumed to be sorted in non-decreasing order and contains only natural numbers (including 0).

-----Input-----
The input consists of:
s: A list of natural numbers sorted in non-decreasing order.

-----Output-----
The output is a natural number:
Returns the smallest natural number that does not appear in the input list.

-----Note-----
It is assumed that the input list is sorted and contains only natural numbers.
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 smallestMissingNumber_precond (s : List Nat) : Prop :=
  -- !benchmark @start precond
  List.Pairwise (· ≤ ·) s
  -- !benchmark @end precond

-- !benchmark @start code_aux

-- !benchmark @end code_aux


def smallestMissingNumber (s : List Nat) (h_precond : smallestMissingNumber_precond (s)) : Nat :=
  -- !benchmark @start code
  let rec findMissing (v : Nat) (l : List Nat) : Nat :=
    match l with
    | [] => v
    | x :: xs =>
      if x > v then v
      else if x = v then findMissing (v + 1) xs
      else findMissing v xs
  findMissing 0 s
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def smallestMissingNumber_postcond (s : List Nat) (result: Nat) (h_precond : smallestMissingNumber_precond (s)) :=
  -- !benchmark @start postcond
  ¬ List.elem result s ∧ (∀ k : Nat, k < result → List.elem k s)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem smallestMissingNumber_spec_satisfied (s: List Nat) (h_precond : smallestMissingNumber_precond (s)) :
    smallestMissingNumber_postcond (s) (smallestMissingNumber (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: [0, 1, 2, 6, 9]
s: [4, 5, 10, 11]
s: [0, 1, 2, 3, 4, 5]
s: [0, 2, 3, 4]
expected: 3
0
6
0
1
unexpected: 2
4
5
1
2
5
7
1
2
0
2
3

Inputs rejected by the precondition:
s: [3, 2, 1]
-----Description----- 
This task requires writing a Lean 4 method that given an natural number n, returns the smallest prime factor that is less than 10. If none exist, return 0

-----Input-----
The input consists of one natural number:
n: The main natural number.

-----Output-----
The output is an natural number:
Returns the smallest prime factor that is less than 10 or, if none exist, 0


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 singleDigitPrimeFactor_precond (n : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def singleDigitPrimeFactor (n : Nat) (h_precond : singleDigitPrimeFactor_precond (n)) : Nat :=
  -- !benchmark @start code
  if n == 0 then 0
  else if n % 2 == 0 then 2
  else if n % 3 == 0 then 3
  else if n % 5 == 0 then 5
  else if n % 7 == 0 then 7
  else 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def singleDigitPrimeFactor_postcond (n : Nat) (result: Nat) (h_precond : singleDigitPrimeFactor_precond (n)) : Prop :=
  -- !benchmark @start postcond
  result ∈ [0, 2, 3, 5, 7] ∧
  (result = 0 → (n = 0 ∨ [2, 3, 5, 7].all (n % · ≠ 0))) ∧
  (result ≠ 0 → n ≠ 0 ∧ n % result == 0 ∧ (List.range result).all (fun x => x ∈ [2, 3, 5, 7] → n % x ≠ 0))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem singleDigitPrimeFactor_spec_satisfied (n: Nat) (h_precond : singleDigitPrimeFactor_precond (n)) :
    singleDigitPrimeFactor_postcond (n) (singleDigitPrimeFactor (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: n: 0
n: 98
n: 9
n: 73
n: 529
n: 161
n: 0
expected: 0
2
3
0
0
7
0
unexpected: 1
2
3
7
8
9
4
5
6
1
2
3
7
8
9
0
1
2
1
2
3

Inputs rejected by the precondition:
-----Description-----  
This task requires writing a Lean 4 method that checks whether all characters in an input string are identical. The method should return true if every character in the string is the same, and false if at least one character differs. An empty string or a single-character string is considered to have all characters identical.

-----Input-----  
The input consists of:  
s: A string.

-----Output-----  
The output is a Boolean value:  
Returns true if every character in the string is identical.  
Returns false if there is at least one differing character.

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 allCharactersSame_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def allCharactersSame (s : String) (h_precond : allCharactersSame_precond (s)) : Bool :=
  -- !benchmark @start code
  match s.toList with
  | []      => true
  | c :: cs => cs.all (fun x => x = c)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def allCharactersSame_postcond (s : String) (result: Bool) (h_precond : allCharactersSame_precond (s)) :=
  -- !benchmark @start postcond
  let cs := s.toList
  (result → List.Pairwise (· = ·) cs) ∧
  (¬ result → (cs ≠ [] ∧ cs.any (fun x => x ≠ cs[0]!)))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem allCharactersSame_spec_satisfied (s: String) (h_precond : allCharactersSame_precond (s)) :
    allCharactersSame_postcond (s) (allCharactersSame (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: aaa
s: aba
s: a
s: bbbb
s: bbab
expected: True
False
True
True
True
False
unexpected: False
True
False
False
False
True

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that calculates both the sum and the average of the first n natural numbers. The method should compute the sum of numbers from 0 to n (which equals n * (n + 1) / 2) and then determine the average by dividing this sum by n. The specification assumes that the input n is a positive integer.

-----Input-----
The input consists of:
n: A natural number representing the count of the first natural numbers. The value of n is assumed to be positive.

-----Output-----
The output is a pair consisting of:
- An integer representing the sum of the first n natural numbers.
- A floating-point number representing the average of the first n natural numbers.

-----Note-----
The input n must be a positive integer and should be reasonably bounded (n < 2^53) to ensure floating-point precision in the average calculation.
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 sumAndAverage_precond (n : Nat) : Prop :=
  -- !benchmark @start precond
  n > 0 ∧ n < 9007199254740992  -- n must be positive and bounded for Float precision
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def sumAndAverage (n : Nat) (h_precond : sumAndAverage_precond (n)) : Int × Float :=
  -- !benchmark @start code
  if n ≤ 0 then (0, 0.0)
  else
    let sum := (List.range (n + 1)).sum
    let average : Float := sum.toFloat / (n.toFloat)
    (sum, average)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def sumAndAverage_postcond (n : Nat) (result: Int × Float) (h_precond : sumAndAverage_precond (n)) :=
  -- !benchmark @start postcond
  (n = 0 → result == (0, 0.0)) ∧
  (n > 0 →
    result.1 == n * (n + 1) / 2 ∧
    result.2 == ((n * (n + 1) / 2).toFloat) / (n.toFloat))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem sumAndAverage_spec_satisfied (n: Nat) (h_precond : sumAndAverage_precond (n)) :
    sumAndAverage_postcond (n) (sumAndAverage (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: n: 5
n: 1
n: 10
n: 2
expected: (15, 3.0)
(1, 1.0)
(55, 5.5)
(3, 1.5)
unexpected: (14, 2.8)
(16, 3.2)
(0, 0.0)
(2, 2.0)
(50, 5.0)
(60, 6.0)
(2, 1.0)
(4, 2.0)

Inputs rejected by the precondition:
n: 0
n: 9007199254740992
-----Description----- 
This task requires implementing the insertion sort algorithm to sort a list of integers in ascending order. The function should take a list of integers as input and return a new list containing the same elements sorted in non-decreasing order.

-----Input----- 
The input is:

l: A list of integers to be sorted.

-----Output----- 
The output is:

A list of integers that is sorted in non-decreasing order and is a permutation of the input list.


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 insertionSort_precond (l : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
-- Helper function to insert an integer into a sorted list
def insertElement (x : Int) (l : List Int) : List Int :=
  match l with
  | [] => [x]
  | y :: ys =>
      if x <= y then
        x :: y :: ys
      else
        y :: insertElement x ys

-- Helper function to sort a list using insertion sort
def sortList (l : List Int) : List Int :=
  match l with
  | [] => []
  | x :: xs =>
      insertElement x (sortList xs)
-- !benchmark @end code_aux


def insertionSort (l : List Int) (h_precond : insertionSort_precond (l)) : List Int :=
  -- !benchmark @start code
  let result := sortList l
  result
  -- !benchmark @end code


-- !benchmark @start postcond_aux
-- !benchmark @end postcond_aux


@[reducible]
def insertionSort_postcond (l : List Int) (result: List Int) (h_precond : insertionSort_precond (l)) : Prop :=
  -- !benchmark @start postcond
  List.Pairwise (· ≤ ·) result ∧ List.isPerm l result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem insertionSort_spec_satisfied (l: List Int) (h_precond : insertionSort_precond (l)) :
    insertionSort_postcond (l) (insertionSort (l) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that computes the sum of the fourth power of the first n odd natural numbers. In other words, given a non-negative integer n, the method should calculate the sum: 1⁴ + 3⁴ + 5⁴ + ... for the first n odd numbers.

-----Input-----
The input consists of:
n: A non-negative natural number representing the number of odd natural numbers to consider.

-----Output----- 
The output is a natural number:
Returns the sum of the fourth power of the first n odd natural numbers.

-----Note----- 
The input n is assumed to be a non-negative integer.
The correctness of the result is established by a theorem that relates the computed sum to a specific formula.
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 sumOfFourthPowerOfOddNumbers_precond (n : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def sumOfFourthPowerOfOddNumbers (n : Nat) (h_precond : sumOfFourthPowerOfOddNumbers_precond (n)) : Nat :=
  -- !benchmark @start code
  match n with
  | 0 => 0
  | n + 1 =>
    let prev := sumOfFourthPowerOfOddNumbers n h_precond
    let nextOdd := 2 * n + 1
    prev + nextOdd^4
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def sumOfFourthPowerOfOddNumbers_postcond (n : Nat) (result: Nat) (h_precond : sumOfFourthPowerOfOddNumbers_precond (n)) :=
  -- !benchmark @start postcond
  15 * result = n * (2 * n + 1) * (7 + 24 * n^3 - 12 * n^2 - 14 * n)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem sumOfFourthPowerOfOddNumbers_spec_satisfied (n: Nat) (h_precond : sumOfFourthPowerOfOddNumbers_precond (n)) :
    sumOfFourthPowerOfOddNumbers_postcond (n) (sumOfFourthPowerOfOddNumbers (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: n: 0
n: 1
n: 2
n: 3
n: 4
n: 5
expected: 0
1
82
707
3108
9669
unexpected: 1
10
2
0
5
81
83
80
706
708
700
3107
3109
3000
9668
9670
9000

Inputs rejected by the precondition:
-----Description-----  
This task involves converting a list of integers into an array such that the array contains all the elements of the list in the exact same order. The objective is to ensure that the array has the same number of elements as the list and that each element in the array corresponds exactly to the element at the same position in the list.

-----Input-----  
The input consists of:  
• xs: A list of integer elements.  

-----Output-----  
The output is an array of elements of type integer that:  
• Has a size equal to the length of the input list xs.  
• Contains all the elements from xs in the same order, ensuring that for every valid index i, the array element at i is equal to the list element at i.

-----Note-----  
There are no additional preconditions; the method should work correctly for any list of elements.  
A corresponding specification is provided stating that the array’s size equals the list’s length and that each element is preserved.
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 ToArray_precond (xs : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def ToArray (xs : List Int) (h_precond : ToArray_precond (xs)) : Array Int :=
  -- !benchmark @start code
  xs.toArray
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def ToArray_postcond (xs : List Int) (result: Array Int) (h_precond : ToArray_precond (xs)) :=
  -- !benchmark @start postcond
  result.size = xs.length ∧ ∀ (i : Nat), i < xs.length → result[i]! = xs[i]!
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem ToArray_spec_satisfied (xs: List Int) (h_precond : ToArray_precond (xs)) :
    ToArray_postcond (xs) (ToArray (xs) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: xs: [1, 2, 3]
xs: [0, -1, 5]
xs: [7]
xs: [100, 200, 300, 400]
expected: #[1, 2, 3]
#[]
#[0, -1, 5]
#[7]
#[100, 200, 300, 400]
unexpected: #[1, 2]
#[1, 2, 3, 4]
#[3, 2, 1]
#[0]
#[1]
#[1, 0]
#[-1, 0, 5]
#[0, 5]
#[0, -1, 4]
#[]
#[0, 7]
#[8]
#[100, 200, 300]
#[100, 300, 200, 400]
#[400, 300, 200, 100]

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that determines whether a given string contains all 5 English vowels: a, e, i, o, u.

The check is case-insensitive, meaning that both uppercase and lowercase vowels count.

-----Input-----
The input consists of a string:
s: A string of alphabetic characters (may include uppercase and lowercase)

-----Output-----
The output is true or false:
Returns true if the input string contains all 5 vowels (a, e, i, o, u), false otherwise.


Difficulty: advanced

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def toLower (c : Char) : Char :=
  if 'A' ≤ c && c ≤ 'Z' then
    Char.ofNat (Char.toNat c + 32)
  else
    c

def normalize_str (s : String) : List Char :=
  s.data.map toLower
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def allVowels_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def allVowels (s : String) (h_precond : allVowels_precond (s)) : Bool :=
  -- !benchmark @start code
  let chars := normalize_str s
  let vowelSet := ['a', 'e', 'i', 'o', 'u']
  vowelSet.all (fun v => chars.contains v)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def allVowels_postcond (s : String) (result: Bool) (h_precond : allVowels_precond (s)) : Prop :=
  -- !benchmark @start postcond
  let chars := normalize_str s
  (result ↔ List.all ['a', 'e', 'i', 'o', 'u'] (fun v => chars.contains v))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem allVowels_spec_satisfied (s: String) (h_precond : allVowels_precond (s)) :
    allVowels_postcond (s) (allVowels (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: s: education
s: education123
s: AEIOU
s: hello
s: apple orange union
expected: True
True
True
False
False
True
unexpected: False
False
False
True
True
False

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that returns the majority element from a list of integers.

The majority element is the one that appears more than ⌊n / 2⌋ times in the list, 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 (with at least one majority element).

-----Output-----
Returns the majority element — the value that appears more than ⌊n / 2⌋ times.


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 majorityElement_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  nums.length > 0 ∧ nums.any (fun x => nums.count x > nums.length / 2)  -- majority element must exist
  -- !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
  let rec insert (x : Int) (xs : List Int) : List Int :=
    match xs with
    | [] => [x]
    | h :: t =>
      if x ≤ h then
        x :: h :: t
      else
        h :: insert x t

  let rec insertionSort (xs : List Int) : List Int :=
    match xs with
    | [] => []
    | h :: t =>
      let sortedTail := insertionSort t
      let sorted := insert h sortedTail
      sorted

  let getAt := fun (xs : List Int) (i : Nat) =>
    match xs.drop i with
    | [] => 0
    | h :: _ => h

  let sorted := insertionSort nums

  let len := sorted.length
  let mid := len / 2
  getAt sorted mid
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def majorityElement_postcond (nums : List Int) (result: Int) (h_precond : majorityElement_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let n := nums.length
  (List.count result nums > n / 2) ∧
  nums.all (fun x => x = result ∨ List.count x nums ≤ 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]
nums: [4, 4, 4, 4, 4, 2, 2, 3, 3]
nums: [9, 8, 9, 9, 7, 9, 6, 9, 9]
nums: [0, 0, 0, 0, 1]
nums: [100000, 100000, 100000, 100000, -100000]
nums: [-1, -1, -1, -1, 0, 1, 2]
nums: [5, 5, 5, 5, 5, 5, 5]
nums: [1, 2, 3, 3, 3, 3, 3]
expected: 3
2
1
4
9
0
100000
-1
5
3
unexpected: 2
1
0
2
3
6
7
8
1
-100000
0
1
2
0
1
2

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