sunblaze-ucb/verina huggingface dataset:
-----Description-----  
This task is about determining the minimum absolute difference between any pair of integers, where one integer is taken from the first sorted array and the other integer is taken from the second sorted array. The focus is on accurately finding the smallest absolute difference between any two elements from the arrays, independent of the specific techniques or programming language used.

-----Input-----  
The input consists of:  
• a: An array of integers, sorted in non-decreasing order and guaranteed to be non-empty.  
• b: An array of integers, also sorted in non-decreasing order and non-empty.

-----Output-----  
The output is a natural number (Nat) representing the minimum absolute difference between any element a[i] from the first array and b[j] from the second array.

-----Note-----  
• It is assumed that both arrays are non-empty.  
• The arrays are assumed to be sorted in non-decreasing order.
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 CanyonSearch_precond (a : Array Int) (b : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size > 0 ∧ b.size > 0 ∧ List.Pairwise (· ≤ ·) a.toList ∧ List.Pairwise (· ≤ ·) b.toList
  -- !benchmark @end precond


-- !benchmark @start code_aux
def canyonSearchAux (a : Array Int) (b : Array Int) (m n d : Nat) : Nat :=
  if m < a.size ∧ n < b.size then
    let diff : Nat := ((a[m]! - b[n]!).natAbs)
    let new_d := if diff < d then diff else d
    if a[m]! <= b[n]! then
      canyonSearchAux a b (m + 1) n new_d
    else
      canyonSearchAux a b m (n + 1) new_d
  else
    d
termination_by a.size + b.size - m - n
-- !benchmark @end code_aux


def CanyonSearch (a : Array Int) (b : Array Int) (h_precond : CanyonSearch_precond (a) (b)) : Nat :=
  -- !benchmark @start code
  let init : Nat :=
    if a[0]! < b[0]! then (b[0]! - a[0]!).natAbs
    else (a[0]! - b[0]!).natAbs
  canyonSearchAux a b 0 0 init
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def CanyonSearch_postcond (a : Array Int) (b : Array Int) (result: Nat) (h_precond : CanyonSearch_precond (a) (b)) :=
  -- !benchmark @start postcond
  (a.any (fun ai => b.any (fun bi => result = (ai - bi).natAbs))) ∧
  (a.all (fun ai => b.all (fun bi => result ≤ (ai - bi).natAbs)))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem CanyonSearch_spec_satisfied (a: Array Int) (b: Array Int) (h_precond : CanyonSearch_precond (a) (b)) :
    CanyonSearch_postcond (a) (b) (CanyonSearch (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: #[-5, -2, 0]
b: #[1, 3]
a: #[10, 20, 30]
b: #[5, 15, 25]
a: #[1, 2, 3, 4, 5]
b: #[3]
a: #[-10, -5, 0, 5, 10]
b: #[-3, 2, 8]
expected: 1
1
5
0
2
unexpected: 0
2
3
0
2
5
3
7
10
1
2
3
1
3
4

Inputs rejected by the precondition:
a: #[]
b: #[]
-----Description----- 
This task requires writing a Lean 4 method that calculates the surface area of a cube based on the length of one of its edges. The method should compute the surface area using the standard formula for a cube.

-----Input-----
The input consists of:
size: An natural number representing the length of an edge of the cube.

-----Output-----
The output is an natural number:
Returns the surface area of the cube.

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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def cubeSurfaceArea (size : Nat) (h_precond : cubeSurfaceArea_precond (size)) : Nat :=
  -- !benchmark @start code
  6 * size * size
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def cubeSurfaceArea_postcond (size : Nat) (result: Nat) (h_precond : cubeSurfaceArea_precond (size)) :=
  -- !benchmark @start postcond
  result - 6 * size * size = 0 ∧ 6 * size * size - result = 0
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem cubeSurfaceArea_spec_satisfied (size: Nat) (h_precond : cubeSurfaceArea_precond (size)) :
    cubeSurfaceArea_postcond (size) (cubeSurfaceArea (size) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold cubeSurfaceArea cubeSurfaceArea_postcond
  simp
  -- !benchmark @end proof


Tests:
input: size: 3
size: 1
size: 10
size: 5
size: 2
expected: 54
6
600
150
24
unexpected: 27
48
60
1
2
3
100
500
610
25
100
125
8
16
20

Inputs rejected by the precondition:
-----Description-----  
The problem involves finding the first occurrence of a specified key in an array of integers. Your task is to identify the index at which the key appears for the first time in the array and return that index. If the key is not found, return -1.

-----Input-----  
The input consists of:  
• a: An array of integers.  
• key: An integer representing the value to search for in the array.

-----Output-----  
The output is an integer which represents:  
• The index in the array where the key is found, provided that the index is in the range [0, a.size).  
• -1 if the key is not present in the array.  
In addition, if the output is not -1, then a[(Int.toNat result)]! equals key and every element in the array prior to this index is not equal to key.

-----Note-----  
The function performs a linear search beginning at index 0 and returns the first occurrence of the key. There are no additional preconditions on the input array; it can be empty or 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 Find_precond (a : Array Int) (key : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def Find (a : Array Int) (key : Int) (h_precond : Find_precond (a) (key)) : Int :=
  -- !benchmark @start code
  let rec search (index : Nat) : Int :=
    if index < a.size then
      if a[index]! = key then Int.ofNat index
      else search (index + 1)
    else -1
  search 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def Find_postcond (a : Array Int) (key : Int) (result: Int) (h_precond : Find_precond (a) (key)) :=
  -- !benchmark @start postcond
  (result = -1 ∨ (result ≥ 0 ∧ result < Int.ofNat a.size))
  ∧ ((result ≠ -1) → (a[(Int.toNat result)]! = key ∧ ∀ (i : Nat), i < Int.toNat result → a[i]! ≠ key))
  ∧ ((result = -1) → ∀ (i : Nat), i < a.size → a[i]! ≠ key)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem Find_spec_satisfied (a: Array Int) (key: Int) (h_precond : Find_precond (a) (key)) :
    Find_postcond (a) (key) (Find (a) (key) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
-----Description-----
This task involves determining whether two integer values are equal. The goal is simply to compare the two provided numbers and indicate with a Boolean result whether they are the same.

-----Input-----
The input consists of two elements:
• a: An element of type Int.
• b: An element of type Int.

-----Output-----
The output is a Boolean:
• Returns true if a equals b.
• Returns false if a does not equal 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 Compare_precond (a : Int) (b : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def Compare (a : Int) (b : Int) (h_precond : Compare_precond (a) (b)) : Bool :=
  -- !benchmark @start code
  if a = b then true else false
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def Compare_postcond (a : Int) (b : Int) (result: Bool) (h_precond : Compare_precond (a) (b)) :=
  -- !benchmark @start postcond
  (a = b → result = true) ∧ (a ≠ b → result = false)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem Compare_spec_satisfied (a: Int) (b: Int) (h_precond : Compare_precond (a) (b)) :
    Compare_postcond (a) (b) (Compare (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold Compare_postcond Compare
  simp
  -- !benchmark @end proof


Tests:
input: a: 1
b: 1
a: 1
b: 2
expected: True
False
unexpected: False
True

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that finds the difference between the first even number and the first odd number in an array of integers. The method should process the array sequentially until it identifies the first even number and the first odd number, and then return the difference calculated as (first even number) minus (first odd number).

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

-----Output-----
The output is an integer:
Returns the difference computed as the first even number minus the first odd number found in the array.

-----Note-----
The input array is assumed to be non-empty and to contain at least one even number and one odd number.
Difficulty: basic

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

-- !benchmark @end import

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

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

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

@[reducible, simp]
def firstEvenOddDifference_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size > 1 ∧
  (∃ x ∈ a, isEven x) ∧
  (∃ x ∈ a, isOdd x)
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def firstEvenOddDifference (a : Array Int) (h_precond : firstEvenOddDifference_precond (a)) : Int :=
  -- !benchmark @start code
  let rec findFirstEvenOdd (i : Nat) (firstEven firstOdd : Option Nat) : Int :=
    if i < a.size then
      let x := a[i]!
      let firstEven := if firstEven.isNone && isEven x then some i else firstEven
      let firstOdd := if firstOdd.isNone && isOdd x then some i else firstOdd
      match firstEven, firstOdd with
      | some e, some o => a[e]! - a[o]!
      | _, _ => findFirstEvenOdd (i + 1) firstEven firstOdd
    else
      -- This case is impossible due to h2, but we need a value
      0
  findFirstEvenOdd 0 none none
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def firstEvenOddDifference_postcond (a : Array Int) (result: Int) (h_precond : firstEvenOddDifference_precond (a)) :=
  -- !benchmark @start postcond
  ∃ i j, i < a.size ∧ j < a.size ∧ isEven (a[i]!) ∧ isOdd (a[j]!) ∧
    result = a[i]! - a[j]! ∧
    (∀ k, k < i → isOdd (a[k]!)) ∧ (∀ k, k < j → isEven (a[k]!))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem firstEvenOddDifference_spec_satisfied (a: Array Int) (h_precond : firstEvenOddDifference_precond (a)) :
    firstEvenOddDifference_postcond (a) (firstEvenOddDifference (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
a: #[2]
-----Description-----  
This task involves determining whether a specified key appears exactly once in an array. The goal is to verify the uniqueness of the key's occurrence without prescribing any specific approach or implementation method.

-----Input-----  
The input consists of:  
• a: An array of integers.  
• key: An integer representing the element whose occurrence is to be checked.

-----Output-----  
The output is a Boolean value that:  
• Is true if the key appears exactly once in the array.  
• Is false otherwise.

-----Note-----  
The function should correctly handle arrays with no occurrences of the key, multiple occurrences, and exactly one occurrence.
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 only_once_precond (a : Array Int) (key : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def only_once_loop {T : Type} [DecidableEq T] (a : Array T) (key : T) (i keyCount : Nat) : Bool :=
  if i < a.size then
    match a[i]? with
    | some val =>
        let newCount := if val = key then keyCount + 1 else keyCount
        only_once_loop a key (i + 1) newCount
    | none => keyCount == 1
  else
    keyCount == 1
-- !benchmark @end code_aux


def only_once (a : Array Int) (key : Int) (h_precond : only_once_precond (a) (key)) : Bool :=
  -- !benchmark @start code
  only_once_loop a key 0 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux
def count_occurrences {T : Type} [DecidableEq T] (a : Array T) (key : T) : Nat :=
  a.foldl (fun cnt x => if x = key then cnt + 1 else cnt) 0
-- !benchmark @end postcond_aux


@[reducible, simp]
def only_once_postcond (a : Array Int) (key : Int) (result: Bool) (h_precond : only_once_precond (a) (key)) :=
  -- !benchmark @start postcond
  ((count_occurrences a key = 1) → result) ∧
  ((count_occurrences a key ≠ 1) → ¬ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem only_once_spec_satisfied (a: Array Int) (key: Int) (h_precond : only_once_precond (a) (key)) :
    only_once_postcond (a) (key) (only_once (a) (key) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[1, 2, 3, 4]
key: 2
a: #[1, 2, 2, 3, 4]
key: 2
a: #[1, 1, 1, 1]
key: 1
a: #[10]
key: 10
a: #[]
key: 5
expected: true
false
false
true
false
unexpected: False
True
True
False
True

Inputs rejected by the precondition: