sunblaze-ucb/verina huggingface dataset:
-----Description-----
Given an input string "words_str", this task requires writing a Lean 4 function that reverses the order of its words. A word is defined as a contiguous sequence of non-space characters. The function must remove any extra spaces so that the output string contains words separated by a single space and has no leading or trailing spaces. The characters within each word must stay the same as the original input.

-----Input-----
words_str: A string that may contain leading, trailing, or multiple spaces between words.

-----Output-----
A string with the words from the input reversed, where words are separated by a single space, with no extra spaces at the beginning or end.


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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def reverseWords (words_str : String) (h_precond : reverseWords_precond (words_str)) : String :=
  -- !benchmark @start code
  let rawWords : List String := words_str.splitOn " "
  let rec filterNonEmpty (words : List String) : List String :=
    match words with
    | [] => []
    | h :: t =>
      if h = "" then
        filterNonEmpty t
      else
        h :: filterNonEmpty t
  let filteredWords : List String := filterNonEmpty rawWords
  let revWords : List String := filteredWords.reverse
  let rec joinWithSpace (words : List String) : String :=
    match words with
    | [] => ""
    | [w] => w
    | h :: t =>
      -- Append the current word with a space and continue joining the rest.
      h ++ " " ++ joinWithSpace t
  let result : String := joinWithSpace revWords
  result
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def reverseWords_postcond (words_str : String) (result: String) (h_precond : reverseWords_precond (words_str)) : Prop :=
  -- !benchmark @start postcond
  ∃ words : List String,
    (words = (words_str.splitOn " ").filter (fun w => w ≠ "")) ∧
    result = String.intercalate " " (words.reverse)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem reverseWords_spec_satisfied (words_str: String) (h_precond : reverseWords_precond (words_str)) :
    reverseWords_postcond (words_str) (reverseWords (words_str) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: words_str: the sky is blue
words_str:   hello world  
words_str: a good   example
words_str:   Bob    Loves  Alice   
words_str: this lab is interesting
expected: blue is sky the
world hello
example good a
Alice Loves Bob
interesting is lab this
unexpected: the sky is blue
sky the blue is
hello world
worldhello
a good example
example a good
Bob Loves Alice
Alice Loves Bob 
gnitseretni si bal siht

Inputs rejected by the precondition:
-----Description-----  
This problem involves determining the index of the first occurrence of a specified element within an array of integers. The objective is to identify the correct position where the target element appears for the first time, ensuring that all elements prior to that index are different from the target.

-----Input-----  
The input consists of:  
• a: An array of integers.  
• e: An integer representing the element to search for.

-----Output-----  
The output is a natural number (Nat) representing the index of the first occurrence of e in the array.  
• If the element e exists in the array, the index n will satisfy the conditions specified above.

-----Note-----  
It is assumed that the input satisfies the precondition where at least one index i in a exists such that a[i]! = e.  
The implementation uses a helper function to iterate through the array recursively.
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 LinearSearch_precond (a : Array Int) (e : Int) : Prop :=
  -- !benchmark @start precond
  ∃ i, i < a.size ∧ a[i]! = e
  -- !benchmark @end precond


-- !benchmark @start code_aux
def linearSearchAux (a : Array Int) (e : Int) (n : Nat) : Nat :=
  if n < a.size then
    if a[n]! = e then n else linearSearchAux a e (n + 1)
  else
    0
-- !benchmark @end code_aux


def LinearSearch (a : Array Int) (e : Int) (h_precond : LinearSearch_precond (a) (e)) : Nat :=
  -- !benchmark @start code
  linearSearchAux a e 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def LinearSearch_postcond (a : Array Int) (e : Int) (result: Nat) (h_precond : LinearSearch_precond (a) (e)) :=
  -- !benchmark @start postcond
  (result < a.size) ∧ (a[result]! = e) ∧ (∀ k : Nat, k < result → a[k]! ≠ e)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem LinearSearch_spec_satisfied (a: Array Int) (e: Int) (h_precond : LinearSearch_precond (a) (e)) :
    LinearSearch_postcond (a) (e) (LinearSearch (a) (e) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
a: #[1, 2, 3, 4, 5]
e: 6
-----Description----- 
This task requires writing a Lean 4 method that computes the sum of the squares of the first n odd natural numbers. The result should match the formula: (n * (2 * n - 1) * (2 * n + 1)) / 3.

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

-----Output-----
The output is a natural number:
Returns the sum of the squares of the first n odd natural numbers, as defined by the formula: (n * (2 * n - 1) * (2 * n + 1)) / 3.
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 sumOfSquaresOfFirstNOddNumbers_precond (n : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def sumOfSquaresOfFirstNOddNumbers (n : Nat) (h_precond : sumOfSquaresOfFirstNOddNumbers_precond (n)) : Nat :=
  -- !benchmark @start code
  let rec loop (k : Nat) (sum : Nat) : Nat :=
    if k = 0 then
      sum
    else
      loop (k - 1) (sum + (2 * k - 1) * (2 * k - 1))
  loop n 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def sumOfSquaresOfFirstNOddNumbers_postcond (n : Nat) (result: Nat) (h_precond : sumOfSquaresOfFirstNOddNumbers_precond (n)) :=
  -- !benchmark @start postcond
  result - (n * (2 * n - 1) * (2 * n + 1)) / 3 = 0 ∧
  (n * (2 * n - 1) * (2 * n + 1)) / 3 - result = 0
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem sumOfSquaresOfFirstNOddNumbers_spec_satisfied (n: Nat) (h_precond : sumOfSquaresOfFirstNOddNumbers_precond (n)) :
    sumOfSquaresOfFirstNOddNumbers_postcond (n) (sumOfSquaresOfFirstNOddNumbers (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
n: 10
expected: 0
1
10
35
84
165
1330
unexpected: 1
2
0
2
3
9
11
12
30
34
36
80
85
90
160
166
170
1320
1331
1340

Inputs rejected by the precondition:
-----Description-----  
The task is to compute the element-wise sum of two integer arrays. The result should be a new array where each element is the sum of the corresponding elements from the two input arrays. The problem assumes that both arrays have the same length.

-----Input-----  
The input consists of two parameters:  
• a: An array of integers.  
• b: An array of integers.  
Note: Both arrays must have the same length.

-----Output-----  
The output is an array of integers that:  
• Has the same size as the input arrays.  
• Contains elements where each element at index i is computed as a[i]! + b[i]! from the input arrays.

-----Note-----  
It is assumed that the two input arrays have equal lengths.
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 arraySum_precond (a : Array Int) (b : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size = b.size
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def arraySum (a : Array Int) (b : Array Int) (h_precond : arraySum_precond (a) (b)) : Array Int :=
  -- !benchmark @start code
  if a.size ≠ b.size then
    panic! "Array lengths mismatch"
  else
    let n := a.size;
    let c := Array.mkArray n 0;
    let rec loop (i : Nat) (c : Array Int) : Array Int :=
      if i < n then
        let c' := c.set! i (a[i]! + b[i]!);
        loop (i + 1) c'
      else c;
    loop 0 c
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


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


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem arraySum_spec_satisfied (a: Array Int) (b: Array Int) (h_precond : arraySum_precond (a) (b)) :
    arraySum_postcond (a) (b) (arraySum (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[1, 2, 3]
b: #[4, 5, 6]
a: #[0, 0, 0]
b: #[0, 0, 0]
a: #[-1, 2, 3]
b: #[1, -2, 4]
a: #[10]
b: #[-10]
a: #[100, 200, 300]
b: #[100, 200, 300]
expected: #[5, 7, 9]
#[0, 0, 0]
#[0, 0, 7]
#[0]
#[200, 400, 600]
unexpected: #[5, 6, 9]
#[4, 7, 9]
#[0, 0, 1]
#[1, 0, 0]
#[0, 1, 7]
#[0, 0, 6]
#[1]
#[-1]
#[200, 400, 601]
#[199, 400, 600]
#[200, 399, 600]

Inputs rejected by the precondition:
a: #[1, 2, 3, 4]
b: #[5, 6, 7]
-----Description----- 
This task requires writing a Lean 4 method that determines whether a given integer is a power of two.
An integer n is a power of two if there exists an integer x such that n = 2^x.
The method should return true if n is a power of two, and false otherwise.
Note that negative numbers and zero are not powers of two.

-----Input-----
The input consists of one integer:
n: The integer to be tested.

-----Output-----
The output is a boolean:
Returns true if there exists an integer x such that n = 2^x (with n > 0), otherwise false.


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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isPowerOfTwo (n : Int) (h_precond : isPowerOfTwo_precond (n)) : Bool :=
  -- !benchmark @start code
  if n <= 0 then false
  else
    let rec aux (m : Int) (fuel : Nat) : Bool :=
      if fuel = 0 then false
      else if m = 1 then true
      else if m % 2 ≠ 0 then false
      else aux (m / 2) (fuel - 1)
    aux n n.natAbs
  -- !benchmark @end code


-- !benchmark @start postcond_aux
def pow (base : Int) (exp : Nat) : Int :=
  match exp with
  | 0 => 1
  | n+1 => base * pow base n
-- !benchmark @end postcond_aux


@[reducible]
def isPowerOfTwo_postcond (n : Int) (result: Bool) (h_precond : isPowerOfTwo_precond (n)) : Prop :=
  -- !benchmark @start postcond
  if result then ∃ (x : Nat), (pow 2 x = n) ∧ (n > 0)
  else ¬ (∃ (x : Nat), (pow 2 x = n) ∧ (n > 0))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isPowerOfTwo_spec_satisfied (n: Int) (h_precond : isPowerOfTwo_precond (n)) :
    isPowerOfTwo_postcond (n) (isPowerOfTwo (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: n: 1
n: 16
n: 3
n: 0
n: -2
n: 8
n: 10
expected: True
True
False
False
False
True
False
unexpected: False
False
True
True
True
False
True

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that calculates the difference between the maximum and minimum values in an array of integers. In other words, the method should determine the highest and lowest numbers in the array and return the result of subtracting the minimum from the maximum.

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

-----Output-----
The output is an integer:
Returns the difference between the largest and the smallest values in the input array.

-----Note-----
The input 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 differenceMinMax_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def differenceMinMax (a : Array Int) (h_precond : differenceMinMax_precond (a)) : Int :=
  -- !benchmark @start code
  let rec loop (i : Nat) (minVal maxVal : Int) : Int :=
    if i < a.size then
      let x := a[i]!
      let newMin := if x < minVal then x else minVal
      let newMax := if x > maxVal then x else maxVal
      loop (i + 1) newMin newMax
    else
      maxVal - minVal
  loop 1 (a[0]!) (a[0]!)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def differenceMinMax_postcond (a : Array Int) (result: Int) (h_precond : differenceMinMax_precond (a)) :=
  -- !benchmark @start postcond
  result + (a.foldl (fun acc x => if x < acc then x else acc) (a[0]!)) = (a.foldl (fun acc x => if x > acc then x else acc) (a[0]!))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem differenceMinMax_spec_satisfied (a: Array Int) (h_precond : differenceMinMax_precond (a)) :
    differenceMinMax_postcond (a) (differenceMinMax (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5]
a: #[10, 20, 30, 40, 50]
a: #[-10, -20, -30, -40, -50]
a: #[7]
a: #[5, 5, 5, 5]
a: #[1, -1, 2, -2]
expected: 8
40
40
0
0
4
unexpected: 7
9
10
30
35
45
30
41
20
1
-1
2
1
5
-1
3
0
5

Inputs rejected by the precondition:
a: #[]
-----Description----- 
This task requires writing a Lean 4 method that finds the first missing natural number in an increasingly sorted list. The method should return the smallest natural number that is not in the list, ensuring that all natural numbers that are smaller is inside the list.

-----Input-----
The input consists of a list of natural numbers sorted in increasing order:
l: The sorted list

-----Output-----
The output is a natural number:
Returns the smallest natural number that is not in the list, which means all natural numbers that are smaller than the returned value should be inside 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 smallestMissing_precond (l : List Nat) : Prop :=
  -- !benchmark @start precond
  List.Pairwise (· < ·) l
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def smallestMissing (l : List Nat) (h_precond : smallestMissing_precond (l)) : Nat :=
  -- !benchmark @start code
  let sortedList := l
  let rec search (lst : List Nat) (n : Nat) : Nat :=
    match lst with
    | [] => n
    | x :: xs =>
      let isEqual := x = n
      let isGreater := x > n
      let nextCand := n + 1
      if isEqual then
        search xs nextCand
      else if isGreater then
        n
      else
        search xs n
  let result := search sortedList 0
  result
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def smallestMissing_postcond (l : List Nat) (result: Nat) (h_precond : smallestMissing_precond (l)) : Prop :=
  -- !benchmark @start postcond
  result ∉ l ∧ ∀ candidate : Nat, candidate < result → candidate ∈ l
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem smallestMissing_spec_satisfied (l: List Nat) (h_precond : smallestMissing_precond (l)) :
    smallestMissing_postcond (l) (smallestMissing (l) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
l: [1, 1]
l: [1, 0]
-----Description-----
This task requires writing a Lean 4 function that finds the maximum subarray sum from a given list of integers. 
A subarray is a contiguous sequence of elements within the list. 
The function should return the maximum sum that can be obtained from any subarray.

-----Input-----
The input is a list of integers:
xs: A list of integers (can include negative numbers).

-----Output-----
The output is an integer:
Returns the maximum sum among all contiguous subarrays of xs. 
If the list is empty, the result should be 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 maxSubarraySum_precond (xs : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def maxSubarraySum (xs : List Int) (h_precond : maxSubarraySum_precond (xs)) : Int :=
  -- !benchmark @start code
  let rec helper (lst : List Int) (curMax : Int) (globalMax : Int) : Int :=
    match lst with
    | [] => globalMax
    | x :: rest =>
      let newCurMax := max x (curMax + x)
      let newGlobal := max globalMax newCurMax
      helper rest newCurMax newGlobal
  match xs with
  | [] => 0
  | x :: rest => helper rest x x
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def maxSubarraySum_postcond (xs : List Int) (result: Int) (h_precond : maxSubarraySum_precond (xs)) : Prop :=
  -- !benchmark @start postcond
  -- Find all possible subarrays and their sums
  let subarray_sums := List.range (xs.length + 1) |>.flatMap (fun start =>
    List.range' 1 (xs.length - start) |>.map (fun len =>
      ((xs.drop start).take len).sum
    ))

  -- Check if there exists a subarray with sum equal to result
  let has_result_subarray := subarray_sums.any (fun sum => sum == result)


  -- Check if result is the maximum among all subarray sums
  let is_maximum := subarray_sums.all (· ≤ result)

  match xs with
  | [] => result == 0
  | _ => has_result_subarray ∧ is_maximum
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem maxSubarraySum_spec_satisfied (xs: List Int) (h_precond : maxSubarraySum_precond (xs)) :
    maxSubarraySum_postcond (xs) (maxSubarraySum (xs) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
-----Description-----  
This task involves identifying the maximum value in a non-empty array of integers. The objective is to determine which element in the array is greater than or equal to every other element, ensuring that the selected value is one of the elements in the array.

-----Input-----  
The input consists of:  
• a: An array of integers. It is assumed that the array is non-empty (i.e., its size is at least 1).

-----Output-----  
The output is an integer that represents the maximum element in the array. This value is guaranteed to satisfy the following:  
• It is greater than or equal to every element in the array.  
• It is exactly equal to one of the elements in the array.

-----Note-----  
It is assumed that the provided array is non-empty. In cases where the array is empty, the function's behavior is not defined.
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 maxArray_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux
def maxArray_aux (a : Array Int) (index : Nat) (current : Int) : Int :=
  if index < a.size then
    let new_current := if current > a[index]! then current else a[index]!
    maxArray_aux a (index + 1) new_current
  else
    current
-- !benchmark @end code_aux


def maxArray (a : Array Int) (h_precond : maxArray_precond (a)) : Int :=
  -- !benchmark @start code
  maxArray_aux a 1 a[0]!
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def maxArray_postcond (a : Array Int) (result: Int) (h_precond : maxArray_precond (a)) :=
  -- !benchmark @start postcond
  (∀ (k : Nat), k < a.size → result >= a[k]!) ∧ (∃ (k : Nat), k < a.size ∧ result = a[k]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem maxArray_spec_satisfied (a: Array Int) (h_precond : maxArray_precond (a)) :
    maxArray_postcond (a) (maxArray (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
a: #[]