sunblaze-ucb/verina huggingface dataset:
-----Description-----
This task requires writing a Lean 4 method that takes two sorted (non-decreasing) integer lists and merges them into a single sorted list. The output must preserve order and include all elements from both input lists.

-----Input-----
The input consists of:
a: A list of integers sorted in non-decreasing order.
b: Another list of integers sorted in non-decreasing order.

-----Output-----
The output is a list of integers:
Returns a merged list that contains all elements from both input lists, sorted in non-decreasing order.


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 mergeSorted_precond (a : List Int) (b : List Int) : Prop :=
  -- !benchmark @start precond
  List.Pairwise (· ≤ ·) a ∧ List.Pairwise (· ≤ ·) b
  -- !benchmark @end precond


-- !benchmark @start code_aux
def mergeSortedAux : List Int → List Int → List Int
| [], ys => ys
| xs, [] => xs
| x :: xs', y :: ys' =>
  if x ≤ y then
    let merged := mergeSortedAux xs' (y :: ys')
    x :: merged
  else
    let merged := mergeSortedAux (x :: xs') ys'
    y :: merged

-- !benchmark @end code_aux


def mergeSorted (a : List Int) (b : List Int) (h_precond : mergeSorted_precond (a) (b)) : List Int :=
  -- !benchmark @start code
  let merged := mergeSortedAux a b
  merged
  -- !benchmark @end code


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


@[reducible, simp]
def mergeSorted_postcond (a : List Int) (b : List Int) (result: List Int) (h_precond : mergeSorted_precond (a) (b)) : Prop :=
  -- !benchmark @start postcond
  List.Pairwise (· ≤ ·) result ∧
  List.isPerm result (a ++ b)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem mergeSorted_spec_satisfied (a: List Int) (b: List Int) (h_precond : mergeSorted_precond (a) (b)) :
    mergeSorted_postcond (a) (b) (mergeSorted (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: a: [1, 3, 5]
b: [2, 4, 6]
a: [1, 2]
b: [1, 2, 3]
b: [4, 5]
a: [0, 3, 4]
a: [1, 4, 6]
b: [2, 3, 5]
expected: [1, 2, 3, 4, 5, 6]
[1, 1, 2, 2, 3]
[4, 5]
[0, 3, 4]
[1, 2, 3, 4, 5, 6]
unexpected: [1, 3, 5]
[2, 4, 6]
[6, 5, 4]
[1, 2, 3]
[4, 3, 0]
[1, 4, 6, 2, 3, 5]

Inputs rejected by the precondition:
a: [1, 2, 3]
b: [6, 5, 4]
a: [3, 2, 1]
b: [6, 5, 4]
-----Description-----
This task requires writing a Lean 4 function that returns the maximum element from a non-empty list of natural numbers.

-----Input-----
The input consists of:
lst: a non-empty list of natural numbers.

-----Output-----
The output is:
A natural number representing the largest element in the 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 maxOfList_precond (lst : List Nat) : Prop :=
  -- !benchmark @start precond
  lst ≠ []  -- Ensure the list is non-empty
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def maxOfList (lst : List Nat) (h_precond : maxOfList_precond (lst)) : Nat :=
  -- !benchmark @start code
  let rec helper (lst : List Nat) : Nat :=
    match lst with
    | [] => 0  -- technically shouldn't happen if input is always non-empty
    | [x] => x
    | x :: xs =>
      let maxTail := helper xs
      if x > maxTail then x else maxTail
  helper lst
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def maxOfList_postcond (lst : List Nat) (result: Nat) (h_precond : maxOfList_precond (lst)) : Prop :=
  -- !benchmark @start postcond
  result ∈ lst ∧ ∀ x ∈ lst, x ≤ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem maxOfList_spec_satisfied (lst: List Nat) (h_precond : maxOfList_precond (lst)) :
    maxOfList_postcond (lst) (maxOfList (lst) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that multiplies two integers. The method should return the product of the two input numbers.

-----Input-----
The input consists of:
a: The first integer.
b: The second integer.

-----Output-----
The output is an integer:
Returns the product of the two input integers (a * b).
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 multiply_precond (a : Int) (b : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def multiply (a : Int) (b : Int) (h_precond : multiply_precond (a) (b)) : Int :=
  -- !benchmark @start code
  a * b
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def multiply_postcond (a : Int) (b : Int) (result: Int) (h_precond : multiply_precond (a) (b)) :=
  -- !benchmark @start postcond
  result - a * b = 0 ∧ a * b - result = 0
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem multiply_spec_satisfied (a: Int) (b: Int) (h_precond : multiply_precond (a) (b)) :
    multiply_postcond (a) (b) (multiply (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold multiply multiply_postcond
  simp
  -- !benchmark @end proof


Tests:
input: a: 3
b: 4
a: 3
b: -4
a: -3
b: 4
a: -3
b: -4
a: 0
b: 5
a: 5
b: 0
a: 0
b: 0
expected: 12
-12
-12
12
0
0
0
unexpected: 0
11
15
0
-11
12
0
-11
12
0
11
-12
1
-1
5
1
-1
5
1
-1
5

Inputs rejected by the precondition:
-----Description-----  
This problem focuses on reversing an array of integers. The goal is to take an input array and produce a new array with the elements arranged in the reverse order.  

-----Input-----  
The input consists of:  
• a: An array of integers, which may be empty, contain one element, or many elements.

-----Output-----  
The output is an array of integers that:  
• Has the same length as the input array.  
• Contains the same elements as the input array, but in reverse order.  
• For every valid index i in the input array, the output at index i is equal to the element at index (a.size - 1 - i) from the input array.

-----Note-----  
There are no specific preconditions; the method should correctly handle any array of integers.
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 reverse_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def reverse_core (arr : Array Int) (i : Nat) : Array Int :=
  if i < arr.size / 2 then
    let j := arr.size - 1 - i
    let temp := arr[i]!
    let arr' := arr.set! i (arr[j]!)
    let arr'' := arr'.set! j temp
    reverse_core arr'' (i + 1)
  else
    arr
-- !benchmark @end code_aux


def reverse (a : Array Int) (h_precond : reverse_precond (a)) : Array Int :=
  -- !benchmark @start code
  reverse_core a 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def reverse_postcond (a : Array Int) (result: Array Int) (h_precond : reverse_precond (a)) :=
  -- !benchmark @start postcond
  (result.size = a.size) ∧ (∀ i : Nat, i < a.size → result[i]! = a[a.size - 1 - i]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem reverse_spec_satisfied (a: Array Int) (h_precond : reverse_precond (a)) :
    reverse_postcond (a) (reverse (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[1, 2, 3, 4, 5]
a: #[10, 20, 30, 40]
a: #[]
a: #[7]
a: #[-1, 0, 1]
expected: #[5, 4, 3, 2, 1]
#[40, 30, 20, 10]
#[]
#[7]
#[1, 0, -1]
unexpected: #[1, 2, 3, 4, 5]
#[5, 3, 4, 2, 1]
#[2, 3, 4, 5, 6]
#[10, 20, 30, 40]
#[40, 20, 30, 10]
#[30, 20, 10, 40]
#[0]
#[-1]
#[1]
#[0]
#[7, 7]
#[1]
#[-1, 0, 1]
#[0, 1, -1]
#[1, -1, 0]

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that converts all uppercase characters in a given string to their lowercase equivalents while keeping the other characters unchanged. The output string must have the same length as the input string.

-----Input-----
The input consists of:
s: A string that may contain both uppercase and lowercase characters.

-----Output-----
The output is a string:
Returns a new string where every uppercase letter has been converted to lowercase, and every non-uppercase character remains exactly as in the input.

-----Note-----
There are no preconditions; the method is expected to work for any non-null string.
Difficulty: basic

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def isUpperCase (c : Char) : Bool :=
  'A' ≤ c ∧ c ≤ 'Z'

def shift32 (c : Char) : Char :=
  Char.ofNat (c.toNat + 32)
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

@[reducible, simp]
def toLowercase_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def toLowercase (s : String) (h_precond : toLowercase_precond (s)) : String :=
  -- !benchmark @start code
  let cs := s.toList
  let cs' := cs.map (fun c => if isUpperCase c then shift32 c else c)
  String.mk cs'
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def toLowercase_postcond (s : String) (result: String) (h_precond : toLowercase_precond (s)) :=
  -- !benchmark @start postcond
  let cs := s.toList
  let cs' := result.toList
  (result.length = s.length) ∧
  (∀ i : Nat, i < s.length →
    (isUpperCase cs[i]! → cs'[i]! = shift32 cs[i]!) ∧
    (¬isUpperCase cs[i]! → cs'[i]! = cs[i]!))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem toLowercase_spec_satisfied (s: String) (h_precond : toLowercase_precond (s)) :
    toLowercase_postcond (s) (toLowercase (s) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold toLowercase toLowercase_postcond
  simp_all
  constructor
  · unfold String.length
    simp
  · intro i hi
    have hi' : i < s.data.length := by
      unfold String.length at hi
      simp at hi
      exact hi
    constructor <;> simp_all
  -- !benchmark @end proof


Tests:
input: s: Hello, World!
s: ABC
s: abc
s: 1234!@
s: MixedCASE123
expected: hello, world!
abc
abc
1234!@
mixedcase123
unexpected: Hello, world!
HELLO, WORLD!
hello, World!
ABC
Abc
aBC
ABC
aBc
abC
 
empty
null
1234!#
12345!@
Mixedcase123
mixedCASE123
MIXEDCASE123

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that finds the majority element in a list of natural numbers. The majority element is defined as the element that appears more than ⌊n / 2⌋ times in the list, where n is the total number of elements.

You may assume that the input list always contains a majority element.

-----Input-----
The input consists of one list:
xs: A list of natural numbers (List Nat), where a majority element is guaranteed to exist.

-----Output-----
The output is a natural number:
Returns the element that appears more than half the time in 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 majorityElement_precond (xs : List Nat) : Prop :=
  -- !benchmark @start precond
  xs.length > 0 ∧ xs.any (fun x => xs.count x > xs.length / 2)
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def majorityElement (xs : List Nat) (h_precond : majorityElement_precond (xs)) : Nat :=
  -- !benchmark @start code
  let rec countOccurrences (target : Nat) (lst : List Nat) : Nat :=
    match lst with
    | [] => 0
    | y :: ys =>
      if y = target then 1 + countOccurrences target ys
      else countOccurrences target ys

  let rec findCandidate (lst : List Nat) (candidate : Option Nat) (count : Nat) : Nat :=
    match lst with
    | [] =>
      match candidate with
      | some c => c
      | none => 0 -- unreachable since we assume majority element exists
    | x :: xs =>
      match candidate with
      | some c =>
        if x = c then
          findCandidate xs (some c) (count + 1)
        else if count = 0 then
          findCandidate xs (some x) 1
        else
          findCandidate xs (some c) (count - 1)
      | none =>
        findCandidate xs (some x) 1

  let cand := findCandidate xs none 0
  cand
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def majorityElement_postcond (xs : List Nat) (result: Nat) (h_precond : majorityElement_precond (xs)) : Prop :=
  -- !benchmark @start postcond
  let count := xs.count result
  count > xs.length / 2
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


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




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

Inputs rejected by the precondition:
xs: [1, 2, 3]
-----Description-----  
Determine whether two strings match based on a specific pattern: for each position in the strings, either the characters are the same, or the character in p is a wildcard represented by a question mark '?' that may match any character.

-----Input-----  
The input consists of:  
• s: A string that is to be matched.  
• p: A pattern string of equal length, where each character is either a specific character or the wildcard '?'.

-----Output-----  
The output is a Boolean value:  
• Returns true if the length of s is equal to the length of p and each corresponding character in s and p are either identical or the character in p is a '?'.  
• Returns false if any character in s does not match the corresponding character in p and the character in p is not a '?'.

-----Note-----  
It is assumed that both strings provided have the same length.
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 Match_precond (s : String) (p : String) : Prop :=
  -- !benchmark @start precond
  s.toList.length = p.toList.length
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def Match (s : String) (p : String) (h_precond : Match_precond (s) (p)) : Bool :=
  -- !benchmark @start code
  let sList := s.toList
  let pList := p.toList
  let rec loop (i : Nat) : Bool :=
    if i < sList.length then
      if (sList[i]! ≠ pList[i]!) ∧ (pList[i]! ≠ '?') then false
      else loop (i + 1)
    else true
  loop 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def Match_postcond (s : String) (p : String) (result: Bool) (h_precond : Match_precond (s) (p)) :=
  -- !benchmark @start postcond
  (result = true ↔ ∀ n : Nat, n < s.toList.length → ((s.toList[n]! = p.toList[n]!) ∨ (p.toList[n]! = '?')))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem Match_spec_satisfied (s: String) (p: String) (h_precond : Match_precond (s) (p)) :
    Match_postcond (s) (p) (Match (s) (p) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: abc
p: a?c
s: hello
p: he?lo
s: world
p: w?rld
s: test
p: te?t
s: abc
p: abd
expected: True
True
True
True
False
unexpected: False
False
False
False
True

Inputs rejected by the precondition:
s: abc
p: ac
-----Description-----  
This task involves determining whether every character in a provided string is a digit. The objective is to check if all characters fall within the standard digit range, returning true if they do and false otherwise.

-----Input-----  
The input consists of:  
• s: A string whose characters will be analyzed to determine if they are all digits.

-----Output-----  
The output is a boolean value:  
• true if every character in the string is a digit;  
• false if at least one character is not a digit (note that the empty string returns true).

-----Note-----  
It is assumed that the input is a well-formed string. The function uses an iterator to examine every character.
Difficulty: basic

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def isDigit (c : Char) : Bool :=
  (c ≥ '0') && (c ≤ '9')
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def allDigits (s : String) (h_precond : allDigits_precond (s)) : Bool :=
  -- !benchmark @start code
  let rec loop (it : String.Iterator) : Bool :=
    if it.atEnd then
      true
    else
      if !isDigit it.curr then
        false
      else
        loop it.next
  loop s.iter
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def allDigits_postcond (s : String) (result: Bool) (h_precond : allDigits_precond (s)) :=
  -- !benchmark @start postcond
  (result = true ↔ ∀ c ∈ s.toList, isDigit c)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem allDigits_spec_satisfied (s: String) (h_precond : allDigits_precond (s)) :
    allDigits_postcond (s) (allDigits (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: 123456
s: 123a56
s: 007
s: 98 76
expected: True
False
True
True
False
unexpected: False
True
False
False
True

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that calculates the product of all distinct integers in an array. The method should consider each unique integer only once when computing the product and return the resulting value. If the array is empty, the method should return 1.

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

-----Output-----
The output is an integer:
Returns the product of all unique integers from the input array.

-----Note-----
The order in which the unique integers are multiplied does not affect the final product.
Difficulty: basic

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

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def uniqueProduct (arr : Array Int) (h_precond : uniqueProduct_precond (arr)) : Int :=
  -- !benchmark @start code
  let rec loop (i : Nat) (seen : Std.HashSet Int) (product : Int) : Int :=
    if i < arr.size then
      let x := arr[i]!
      if seen.contains x then
        loop (i + 1) seen product
      else
        loop (i + 1) (seen.insert x) (product * x)
    else
      product
  loop 0 Std.HashSet.empty 1
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def uniqueProduct_postcond (arr : Array Int) (result: Int) (h_precond : uniqueProduct_precond (arr)) :=
  -- !benchmark @start postcond
  result - (arr.toList.eraseDups.foldl (· * ·) 1) = 0 ∧
  (arr.toList.eraseDups.foldl (· * ·) 1) - result = 0
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem uniqueProduct_spec_satisfied (arr: Array Int) (h_precond : uniqueProduct_precond (arr)) :
    uniqueProduct_postcond (arr) (uniqueProduct (arr) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: arr: #[2, 3, 2, 4]
arr: #[5, 5, 5, 5]
arr: #[]
arr: #[1, 2, 3]
arr: #[0, 2, 3]
arr: #[-1, -2, -1, -3]
arr: #[10, 10, 20, 20, 30]
expected: 24
5
1
6
0
-6
6000
unexpected: 12
30
0
25
0
10
0
-1
2
5
7
2
1
-1
10
-1
6
-3
600
0
5000

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that finds the kth element in a given array using 1-based indexing. The method should return the element at the specified position, where the first element is at position 1.

-----Input-----
The input consists of:
arr: An array of integers.
k: An integer representing the position (1-based index) of the element to find.

-----Output-----
The output is an integer:
Returns the element at the kth position in the array.

-----Note-----
The input k is assumed to be valid (between 1 and array length inclusive).
The array is assumed to be non-empty.
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 kthElement_precond (arr : Array Int) (k : Nat) : Prop :=
  -- !benchmark @start precond
  k ≥ 1 ∧ k ≤ arr.size
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def kthElement (arr : Array Int) (k : Nat) (h_precond : kthElement_precond (arr) (k)) : Int :=
  -- !benchmark @start code
  arr[k - 1]!
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def kthElement_postcond (arr : Array Int) (k : Nat) (result: Int) (h_precond : kthElement_precond (arr) (k)) :=
  -- !benchmark @start postcond
  arr.any (fun x => x = result ∧ x = arr[k - 1]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem kthElement_spec_satisfied (arr: Array Int) (k: Nat) (h_precond : kthElement_precond (arr) (k)) :
    kthElement_postcond (arr) (k) (kthElement (arr) (k) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold kthElement kthElement_postcond
  unfold kthElement_precond at h_precond
  have ⟨hp1, hp2⟩ := h_precond
  simp_all
  have h': k - 1 < arr.size := by
    exact Nat.sub_one_lt_of_le hp1 hp2
  exists k - 1
  exists h'
  exact Eq.symm (getElem!_pos arr (k - 1) ((Iff.of_eq (Eq.refl (k - 1 < arr.size))).mpr h'))
  -- !benchmark @end proof


Tests:
input: arr: #[10, 20, 30, 40, 50]
k: 1
arr: #[10, 20, 30, 40, 50]
k: 3
arr: #[10, 20, 30, 40, 50]
k: 5
arr: #[5]
k: 1
arr: #[1, 2, 3]
k: 3
arr: #[1, 2, 3]
k: 2
arr: #[9, 9, 9]
k: 2
arr: #[0, -1, -2]
k: 1
arr: #[0, -1, -2]
k: 2
arr: #[0, -1, -2]
k: 3
expected: 10
30
50
5
3
2
9
0
-1
-2
unexpected: 20
30
10
40
50
10
40
0
1
1
2
1
3
0
0
7
1
-1
2
0
-2
0
-1

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