sunblaze-ucb/verina huggingface dataset:
-----Description-----  
This task involves transforming an array of integers by doubling each element.

-----Input-----  
The input consists of:  
• s: An array of integers.

-----Output-----  
The output is an array of integers where for each valid index i, the element at position i is equal to twice the corresponding element in the input array.

-----Note-----  
The implementation makes use of a recursive helper function to update the array in place. It is assumed that the input array is valid and that the doubling operation does not lead to any overflow issues.
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 double_array_elements_precond (s : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def double_array_elements_aux (s_old s : Array Int) (i : Nat) : Array Int :=
  if i < s.size then
    let new_s := s.set! i (2 * (s_old[i]!))
    double_array_elements_aux s_old new_s (i + 1)
  else
    s
-- !benchmark @end code_aux


def double_array_elements (s : Array Int) (h_precond : double_array_elements_precond (s)) : Array Int :=
  -- !benchmark @start code
  double_array_elements_aux s s 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def double_array_elements_postcond (s : Array Int) (result: Array Int) (h_precond : double_array_elements_precond (s)) :=
  -- !benchmark @start postcond
  result.size = s.size ∧ ∀ i, i < s.size → result[i]! = 2 * s[i]!
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem double_array_elements_spec_satisfied (s: Array Int) (h_precond : double_array_elements_precond (s)) :
    double_array_elements_postcond (s) (double_array_elements (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: #[]
s: #[1, 2, 3, 4, 5]
s: #[0, -1, 5]
s: #[100]
s: #[-3, -4]
expected: #[]
#[2, 4, 6, 8, 10]
#[0, -2, 10]
#[200]
#[-6, -8]
unexpected: #[1]
#[0]
#[-1]
#[1, 2, 3, 4, 5]
#[2, 4, 6, 8, 9]
#[0, 4, 6, 8, 10]
#[0, -1, 5]
#[1, -2, 10]
#[0, 0, 10]
#[100]
#[0]
#[201]
#[3, -4]
#[-6, -7]
#[-6, -9]

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that calculates the sum of all the elements in an array of integers. The method should process the entire array and return the total sum of its elements.

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

-----Output-----
The output is an integer:
Returns the sum of all elements in the input array.

-----Note-----
- The input array is assumed not to be null.
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) : Prop :=
  -- !benchmark @start precond
  a.size > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def arraySum (a : Array Int) (h_precond : arraySum_precond (a)) : Int :=
  -- !benchmark @start code
  a.toList.sum
  -- !benchmark @end code


-- !benchmark @start postcond_aux
def sumTo (a : Array Int) (n : Nat) : Int :=
  if n = 0 then 0
  else sumTo a (n - 1) + a[n - 1]!
-- !benchmark @end postcond_aux


@[reducible, simp]
def arraySum_postcond (a : Array Int) (result: Int) (h_precond : arraySum_precond (a)) :=
  -- !benchmark @start postcond
  result - sumTo a a.size = 0 ∧
  result ≥ sumTo a a.size
  -- !benchmark @end postcond


-- !benchmark @start proof_aux
theorem eq_of_sub_zero_and_ge (a b : Int) : a = b → a - b = 0 ∧ a ≥ b := by
  omega
-- !benchmark @end proof_aux


theorem arraySum_spec_satisfied (a: Array Int) (h_precond : arraySum_precond (a)) :
    arraySum_postcond (a) (arraySum (a) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold arraySum arraySum_postcond
  apply eq_of_sub_zero_and_ge a.toList.sum (sumTo a a.size)
  cases a with | mk d =>
    induction d with
    | nil => simp [sumTo]
    | cons x xs ih =>
      simp [ih]

      have h1 : sumTo ⟨x::xs⟩ (xs.length + 1) = sumTo ⟨x::xs⟩ xs.length + (x::xs)[xs.length] := by
        rw [sumTo]
        simp

      rw [h1]

      have h2 : xs = List.nil → (x::xs)[xs.length] = x := by
        intro h_nil
        simp [h_nil]

      have h3 (x' : Int) (xs' : List Int): xs'.length ≠ 0 → sumTo ⟨x'::xs'⟩ xs'.length = x' + sumTo ⟨xs'⟩ (xs'.length - 1) := by
        induction xs'.length with
        | zero => simp
        | succ n ih_len =>
          simp
          cases n with
          | zero => simp [sumTo]
          | succ n' =>
            simp at ih_len
            unfold sumTo
            simp_all
            rw [Int.add_assoc]

      cases xs with
      | nil => simp [h2, sumTo]
      | cons y ys =>
        simp_all
        have h4 : sumTo ⟨x::y::ys⟩ (ys.length + 1) = x + sumTo ⟨y::ys⟩ ys.length := by
          apply h3 x (y::ys)
          simp
        rw [h4, sumTo]
        simp
        rw [Int.add_assoc]
  -- !benchmark @end proof


Tests:
input: a: #[1, 2, 3, 4, 5]
a: #[13, 14, 15, 16, 17]
a: #[-1, -2, -3]
a: #[10, -10]
expected: 15
75
-6
0
unexpected: 14
10
16
74
76
70
-5
-7
0
5
-5
10

Inputs rejected by the precondition:
a: #[]
-----Description-----  
This task involves finding the minimum element in a non-empty array of integers. The goal is to identify and return the smallest number present in the array.

-----Input-----  
The input consists of:  
• a: An array of integers (the array is assumed to be non-empty).

-----Output-----  
The output is an integer that:  
• Is the smallest element from the input array.  
• Satisfies the property that it is less than or equal to every element in the array and is exactly equal to at least one element of the array.

-----Note-----  
It is assumed that the input array contains at least one element. The implementation uses a helper function (loop) to recursively compare elements and determine the minimum value.
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 minArray_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux
def loop (a : Array Int) (i : Nat) (currentMin : Int) : Int :=
  if i < a.size then
    let newMin := if currentMin > a[i]! then a[i]! else currentMin
    loop a (i + 1) newMin
  else
    currentMin
-- !benchmark @end code_aux


def minArray (a : Array Int) (h_precond : minArray_precond (a)) : Int :=
  -- !benchmark @start code
  loop a 1 (a[0]!)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


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


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem minArray_spec_satisfied (a: Array Int) (h_precond : minArray_precond (a)) :
    minArray_postcond (a) (minArray (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[5, 3, 8, 2, 7]
a: #[10, 10, 10]
a: #[-1, -5, 3, 0]
a: #[42]
a: #[3, -2, 0, -2, 5]
expected: 2
10
-5
42
-2
unexpected: 3
5
7
0
5
11
-1
0
3
0
-42
100
0
3
5

Inputs rejected by the precondition:
a: #[]
-----Description-----  
This task requires writing a Lean 4 method that locates the first occurrence of a specified integer within a sorted array of integers. The method returns the index corresponding to the first time the target value appears in the array; if the target is absent, it returns -1. It is also essential that the original array remains unchanged.

-----Input-----  
The input consists of:  
• arr: An array of integers sorted in non-decreasing order.  
• target: An integer representing the value to search for.

-----Output-----  
The output is an integer:  
• If the target is found, the method returns the index of its first occurrence.  
• If the target is not found, the method returns -1.

-----Note-----  
• The input array must be sorted in non-decreasing order.  
• The array is guaranteed to remain unmodified after the method executes.
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 findFirstOccurrence_precond (arr : Array Int) (target : Int) : Prop :=
  -- !benchmark @start precond
  List.Pairwise (· ≤ ·) arr.toList
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def findFirstOccurrence (arr : Array Int) (target : Int) (h_precond : findFirstOccurrence_precond (arr) (target)) : Int :=
  -- !benchmark @start code
  let rec loop (i : Nat) : Int :=
    if i < arr.size then
      let a := arr[i]!
      if a = target then i
      else if a > target then -1
      else loop (i + 1)
    else -1
  loop 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def findFirstOccurrence_postcond (arr : Array Int) (target : Int) (result: Int) (h_precond : findFirstOccurrence_precond (arr) (target)) :=
  -- !benchmark @start postcond
  (result ≥ 0 →
    arr[result.toNat]! = target ∧
    (∀ i : Nat, i < result.toNat → arr[i]! ≠ target)) ∧
  (result = -1 →
    (∀ i : Nat, i < arr.size → arr[i]! ≠ target))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem findFirstOccurrence_spec_satisfied (arr: Array Int) (target: Int) (h_precond : findFirstOccurrence_precond (arr) (target)) :
    findFirstOccurrence_postcond (arr) (target) (findFirstOccurrence (arr) (target) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: arr: #[1, 2, 2, 3, 4, 5]
target: 2
arr: #[1, 2, 2, 3, 4, 5]
target: 6
arr: #[1, 2, 3, 4, 5]
target: 1
arr: #[1, 2, 3, 4, 5]
target: 5
arr: #[1, 2, 3, 4, 5]
target: 0
expected: 1
-1
0
4
-1
unexpected: 0
2
-1
0
1
2
1
-1
2
3
5
0
0
1
2

Inputs rejected by the precondition:
arr: #[3, 2, 1]
target: 2
-----Description-----
This task involves computing three times a given integer. Given an integer, the goal is to produce a value that is exactly three times its value.

-----Input-----
The input consists of a single integer:
x: An integer.

-----Output-----
The output is an integer:
Returns the product of the input integer and 3.

-----Note-----
There are no additional preconditions.
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 Triple_precond (x : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def Triple (x : Int) (h_precond : Triple_precond (x)) : Int :=
  -- !benchmark @start code
  x * 3
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def Triple_postcond (x : Int) (result: Int) (h_precond : Triple_precond (x)) :=
  -- !benchmark @start postcond
  result / 3 = x ∧ result / 3 * 3 = result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem Triple_spec_satisfied (x: Int) (h_precond : Triple_precond (x)) :
    Triple_postcond (x) (Triple (x) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold Triple_postcond Triple
  simp +arith
  -- !benchmark @end proof


Tests:
input: x: 0
x: 2
x: -4
x: 10
x: -1
expected: 0
6
-12
30
-3
unexpected: -1
1
2
4
5
7
-8
-10
-16
20
25
35
-2
-4
0

Inputs rejected by the precondition:
-----Description----- 
This test implements a function in Lean 4 that finds the maximum sum of any contiguous subarray within a list of integers. A subarray is a continuous section of the original array. If all integers in the list are negative, the function should return 0 (representing the empty subarray).

-----Input-----
numbers: A list of integers that may contain positive, negative, or zero values.

-----Output-----
An integer representing the maximum sum of any contiguous subarray. If the list is empty or contains only negative numbers, the function returns 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 (numbers : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def maxSubarraySum (numbers : List Int) (h_precond : maxSubarraySum_precond (numbers)) : Int :=
  -- !benchmark @start code
  let rec isAllNegative : List Int → Bool
    | [] => true
    | x :: xs => if x >= 0 then false else isAllNegative xs

  let rec findMaxProduct : List Int → Int → Int → Int
    | [], currMax, _ => currMax
    | [x], currMax, _ => max currMax x
    | x :: y :: rest, currMax, currSum =>
        let newSum := max y (currSum + y)
        let newMax := max currMax newSum
        findMaxProduct (y :: rest) newMax newSum

  let handleList : List Int → Nat
    | [] => 0
    | xs =>
        if isAllNegative xs then
          0
        else
          match xs with
          | [] => 0
          | x :: rest =>
              let initialMax := max 0 x
              let startSum := max 0 x
              let result := findMaxProduct (x :: rest) initialMax startSum
              result.toNat

  handleList numbers
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def maxSubarraySum_postcond (numbers : List Int) (result: Int) (h_precond : maxSubarraySum_precond (numbers)) : Prop :=
  -- !benchmark @start postcond
  let subArraySums :=
    List.range (numbers.length + 1) |>.flatMap (fun start =>
      List.range (numbers.length - start + 1) |>.map (fun len =>
        numbers.drop start |>.take len |>.sum))
  subArraySums.contains result ∧ subArraySums.all (· ≤ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


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




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

Inputs rejected by the precondition:
-----Description-----
This task involves determining how many numbers within an array are less than a specified threshold. The problem is focused on identifying and counting such numbers based purely on their value in relation to the threshold.

-----Input-----
The input consists of:
• numbers: An array of integers (which may be empty or non-empty).
• threshold: An integer that serves as the comparison threshold.

-----Output-----
The output is a natural number (Nat) representing the count of elements in the array that are less than the given threshold.

-----Note-----
There are no additional preconditions; the function should work correctly for any array of integers and any integer threshold.
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 CountLessThan_precond (numbers : Array Int) (threshold : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def countLessThan (numbers : Array Int) (threshold : Int) : Nat :=
  let rec count (i : Nat) (acc : Nat) : Nat :=
    if i < numbers.size then
      let new_acc := if numbers[i]! < threshold then acc + 1 else acc
      count (i + 1) new_acc
    else
      acc
  count 0 0
-- !benchmark @end code_aux


def CountLessThan (numbers : Array Int) (threshold : Int) (h_precond : CountLessThan_precond (numbers) (threshold)) : Nat :=
  -- !benchmark @start code
  countLessThan numbers threshold
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def CountLessThan_postcond (numbers : Array Int) (threshold : Int) (result: Nat) (h_precond : CountLessThan_precond (numbers) (threshold)) :=
  -- !benchmark @start postcond
  result - numbers.foldl (fun count n => if n < threshold then count + 1 else count) 0 = 0 ∧
  numbers.foldl (fun count n => if n < threshold then count + 1 else count) 0 - result = 0
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem CountLessThan_spec_satisfied (numbers: Array Int) (threshold: Int) (h_precond : CountLessThan_precond (numbers) (threshold)) :
    CountLessThan_postcond (numbers) (threshold) (CountLessThan (numbers) (threshold) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: numbers: #[1, 2, 3, 4, 5]
threshold: 3
numbers: #[]
threshold: 10
numbers: #[-1, 0, 1]
threshold: 0
numbers: #[5, 6, 7, 2, 1]
threshold: 5
numbers: #[3, 3, 3, 3]
threshold: 3
expected: 2
0
1
2
0
unexpected: 3
1
0
1
2
3
0
2
3
3
4
1
1
2
3

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that returns true if the input n is divisible by 8 or has 8 as one of it's digits.

-----Input-----
The input consists of one integer:
n: The main integer.

-----Output-----
The output is an boolean:
Returns true if the input is divisible by 8 or has 8 as one of it's digits.


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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isItEight (n : Int) (h_precond : isItEight_precond (n)) : Bool :=
  -- !benchmark @start code
  let rec hasDigitEight (m : Nat) : Bool :=
    if m <= 0 then false
    else if m % 10 == 8 then true
    else hasDigitEight (m / 10)
    termination_by m

  let absN := Int.natAbs n
  n % 8 == 0 || hasDigitEight absN
  -- !benchmark @end code

-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def isItEight_postcond (n : Int) (result: Bool) (h_precond : isItEight_precond (n)) : Prop :=
  -- !benchmark @start postcond
  let absN := Int.natAbs n;
  (n % 8 == 0 ∨ ∃ i, absN / (10^i) % 10 == 8) ↔ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isItEight_spec_satisfied (n: Int) (h_precond : isItEight_precond (n)) :
    isItEight_postcond (n) (isItEight (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: n: 8
n: 98
n: 1224
n: 73
n: 208
n: 0
n: -123456780
n: 1
n: -9999
n: -123453
expected: True
True
True
False
True
True
True
False
False
False
unexpected: False
False
False
True
False
False
False
True
True
True

Inputs rejected by the precondition:
-----Description-----
Implement a Lean 4 function that merges two ascendingly sorted lists of integers into one single sorted list (ascending). The resulting list must contain all elements from both input lists, preserving their ascending order.

-----Input-----
The input consists of two lists of integers:
arr1: A sorted list of integers (ascending)
arr2: Another sorted list of integers (ascending)

-----Output-----
The output is a list of integers:
Returns a new list containing all elements from arr1 and arr2, sorted in ascending 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]
def mergeSortedLists_precond (arr1 : List Int) (arr2 : List Int) : Prop :=
  -- !benchmark @start precond
  List.Pairwise (· ≤ ·) arr1 ∧ List.Pairwise (· ≤ ·) arr2
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def mergeSortedLists (arr1 : List Int) (arr2 : List Int) (h_precond : mergeSortedLists_precond (arr1) (arr2)) : List Int :=
  -- !benchmark @start code
  let rec merge (xs : List Int) (ys : List Int) : List Int :=
    match xs, ys with
    | [], _ => ys
    | _, [] => xs
    | x :: xt, y :: yt =>
      if x <= y then
        x :: merge xt (y :: yt)
      else
        y :: merge (x :: xt) yt

  merge arr1 arr2
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def mergeSortedLists_postcond (arr1 : List Int) (arr2 : List Int) (result: List Int) (h_precond : mergeSortedLists_precond (arr1) (arr2)) : Prop :=
  -- !benchmark @start postcond
  List.Pairwise (· ≤ ·) result ∧ List.isPerm (arr1 ++ arr2) result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem mergeSortedLists_spec_satisfied (arr1: List Int) (arr2: List Int) (h_precond : mergeSortedLists_precond (arr1) (arr2)) :
    mergeSortedLists_postcond (arr1) (arr2) (mergeSortedLists (arr1) (arr2) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: arr1: [1, 3, 5]
arr2: [2, 4, 6]
arr1: [-2, 0, 1]
arr2: [-3, -1]
arr1: [10, 20, 30]
arr2: [5, 25, 35]
arr1: [1, 2, 2]
arr2: [2, 3, 3]
expected: [1, 2, 3, 4, 5, 6]
[-3, -2, -1, 0, 1]
[5, 10, 20, 25, 30, 35]
[1, 2, 2, 2, 3, 3]
unexpected: [1, 3, 5]
[2, 4, 6]
[1, 3, 2, 4, 5, 6]
[0]
[999]
[-3, -1]
[0, 1]
[-2, 0, 1]
[10, 20, 30]
[5, 25, 35]
[10, 20, 25, 30, 35]
[1, 2, 3]
[2, 2, 2, 3, 3]

Inputs rejected by the precondition:
arr1: [3, 2, 1]
arr2: [6, 5, 4]