sunblaze-ucb/verina huggingface dataset:
-----Description-----
This task involves taking an array as input and producing a new array that has the same size and identical elements in the same order as the input.

-----Input-----
The input consists of:
• s: An array of elements (for testing purposes, assume an array of integers, i.e., Array Int).

-----Output-----
The output is an array of the same type as the input:
• The output array has the same size as the input array.
• Each element in the output array is identical to the corresponding element in the input array.

-----Note-----
There are no special preconditions for the input array (it can be empty or non-empty); the function simply performs a straightforward copy operation on the array.
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 iter_copy_precond (s : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def iter_copy (s : Array Int) (h_precond : iter_copy_precond (s)) : Array Int :=
  -- !benchmark @start code
  let rec loop (i : Nat) (acc : Array Int) : Array Int :=
    if i < s.size then
      match s[i]? with
      | some val => loop (i + 1) (acc.push val)
      | none => acc  -- This case shouldn't happen when i < s.size
    else
      acc
  loop 0 Array.empty
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


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


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem iter_copy_spec_satisfied (s: Array Int) (h_precond : iter_copy_precond (s)) :
    iter_copy_postcond (s) (iter_copy (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: #[1, 2, 3]
s: #[10, 20, 30, 40]
s: #[]
s: #[-1, -2, -3]
s: #[5, 5, 5, 5]
expected: #[1, 2, 3]
#[10, 20, 30, 40]
#[]
#[-1, -2, -3]
#[5, 5, 5, 5]
unexpected: #[1, 3, 2]
#[1, 2]
#[10, 20, 30]
#[10, 20, 40, 30]
#[0]
#[1]
#[-1, -3, -2]
#[-1, -2]
#[5, 5, 5]
#[5, 5, 5, 0]
#[0, 5, 5, 5]

Inputs rejected by the precondition:
-----Description-----
This task involves merging two sorted arrays of natural numbers (it is ill defined if inputs aren't sorted.)
-----Input-----
The input consists of two arrays:
a1: A sorted array of natural numbers
a2: A sorted array of natural numbers
-----Output-----
The output is an array:
Returns a new array with all elements from both input arrays (included once and only once)
The resulting array is sorted itself


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 mergeSorted_precond (a1 : Array Nat) (a2 : Array Nat) : Prop :=
  -- !benchmark @start precond
  List.Pairwise (· ≤ ·) a1.toList ∧ List.Pairwise (· ≤ ·) a2.toList
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def mergeSorted (a1 : Array Nat) (a2 : Array Nat) (h_precond : mergeSorted_precond (a1) (a2)) : Array Nat :=
  -- !benchmark @start code
  Id.run <| do
    let mut i := 0
    let mut j := 0
    let mut result := #[]
    while i < a1.size ∧ j < a2.size do
      if a1[i]! ≤ a2[j]! then
        result := result.push a1[i]!
        i := i + 1
      else
        result := result.push a2[j]!
        j := j + 1
    while i < a1.size do
      result := result.push a1[i]!
      i := i + 1
    while j < a2.size do
      result := result.push a2[j]!
      j := j + 1
    return result
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def mergeSorted_postcond (a1 : Array Nat) (a2 : Array Nat) (result: Array Nat) (h_precond : mergeSorted_precond (a1) (a2)) : Prop :=
  -- !benchmark @start postcond
  List.Pairwise (· ≤ ·) result.toList ∧
  result.toList.isPerm (a1.toList ++ a2.toList)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem mergeSorted_spec_satisfied (a1: Array Nat) (a2: Array Nat) (h_precond : mergeSorted_precond (a1) (a2)) :
    mergeSorted_postcond (a1) (a2) (mergeSorted (a1) (a2) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: a1: #[1, 3, 5]
a2: #[2, 4, 6]
a1: #[]
a2: #[1, 2, 3]
a1: #[1, 2, 3]
a2: #[]
a1: #[]
a2: #[]
a1: #[1, 1, 2]
a2: #[1, 2, 2]
a1: #[10, 20, 30]
a2: #[5, 15, 25]
a1: #[1, 3, 5, 7, 9]
a2: #[2, 4, 6, 8, 10]
a1: #[5, 5, 5]
a2: #[5, 5, 5]
expected: #[1, 2, 3, 4, 5, 6]
#[1, 2, 3]
#[1, 2, 3]
#[]
#[1, 1, 1, 2, 2, 2]
#[5, 10, 15, 20, 25, 30]
#[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
#[5, 5, 5, 5, 5, 5]
unexpected: #[1, 3, 5, 2, 4, 6]
#[2, 1, 3, 4, 5, 6]
#[]
#[3, 2, 1]
#[]
#[3, 2, 1]
#[1]
#[1, 1, 2, 1, 2, 2]
#[1, 2]
#[10, 20, 30, 5, 15, 25]
#[1, 3, 5, 7, 9, 2, 4, 6, 8, 10]
#[5, 5, 5]

Inputs rejected by the precondition:
a1: #[3, 2, 1]
a2: #[6, 5, 4]
-----Description----- 
This task requires implementing a Lean 4 method that finds the length of the longest strictly increasing subsequence in an array of integers. A subsequence is a sequence that can be derived from an array by deleting some or no elements without changing the order of the remaining elements.

-----Input-----
The input consists of one parameter:
nums: A list of integers representing the input array.

-----Output-----
The output is an integer:
Returns the length of the longest strictly increasing subsequence in the input array. 


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution
import Mathlib.Data.List.Basic
-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def lengthOfLIS_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def maxInArray (arr : Array Nat) : Nat :=
  arr.foldl (fun a b => if a ≥ b then a else b) 0
-- !benchmark @end code_aux


def lengthOfLIS (nums : List Int) (h_precond : lengthOfLIS_precond (nums)) : Nat :=
  -- !benchmark @start code
  if nums.isEmpty then 0
  else
    let n := nums.length
    Id.run do
      let mut dp : Array Nat := Array.mkArray n 1

      for i in [1:n] do
        for j in [0:i] do
          if nums[j]! < nums[i]! && dp[j]! + 1 > dp[i]! then
            dp := dp.set! i (dp[j]! + 1)

      maxInArray dp
  -- !benchmark @end code


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


@[reducible]
def lengthOfLIS_postcond (nums : List Int) (result: Nat) (h_precond : lengthOfLIS_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let allSubseq := (nums.foldl fun acc x => acc ++ acc.map (fun sub => x :: sub)) [[]] |>.map List.reverse
  let increasingSubseqLens := allSubseq.filter (fun l => List.Pairwise (· < ·) l) |>.map (·.length)
  increasingSubseqLens.contains result ∧ increasingSubseqLens.all (· ≤ result)
  -- !benchmark @end postcond

-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem lengthOfLIS_spec_satisfied (nums: List Int) (h_precond : lengthOfLIS_precond (nums)) :
    lengthOfLIS_postcond (nums) (lengthOfLIS (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: [10, 9, 2, 5, 3, 7, 101, 18]
nums: [0, 1, 0, 3, 2, 3]
nums: [7, 7, 7, 7, 7, 7, 7]
nums: [4, 10, 4, 3, 8, 9]
nums: [1, 3, 6, 7, 9, 4, 10, 5, 6]
nums: [10, 22, 9, 33, 21, 50, 41, 60, 80]
nums: [0, 8, 4, 12, 2, 10, 6, 14, 1, 9, 5, 13, 3, 11, 7, 15]
nums: [-2, -1]
expected: 4
4
1
0
3
6
6
6
2
unexpected: 3
5
8
3
5
0
7
1
2
4
6
5
7
9
5
7
9
5
7
16
1
0

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that checks whether two arrays of integers have any elements in common. In other words, the method should return true if there is at least one element that appears in both arrays, and false if no such element exists.

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

-----Output-----
The output is a Boolean value:
Returns true if there is at least one common element between the two arrays.
Returns false if there are no common elements shared by the arrays.

-----Note-----
Both arrays are assumed to be non-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 hasCommonElement_precond (a : Array Int) (b : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size > 0 ∧ b.size > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def hasCommonElement (a : Array Int) (b : Array Int) (h_precond : hasCommonElement_precond (a) (b)) : Bool :=
  -- !benchmark @start code
  a.any fun x => b.any fun y => x = y
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def hasCommonElement_postcond (a : Array Int) (b : Array Int) (result: Bool) (h_precond : hasCommonElement_precond (a) (b)) :=
  -- !benchmark @start postcond
  (∃ i j, i < a.size ∧ j < b.size ∧ a[i]! = b[j]!) ↔ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem hasCommonElement_spec_satisfied (a: Array Int) (b: Array Int) (h_precond : hasCommonElement_precond (a) (b)) :
    hasCommonElement_postcond (a) (b) (hasCommonElement (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold hasCommonElement hasCommonElement_postcond
  constructor
  · intro h
    rcases h with ⟨i, j, hi, hj, heq⟩
    simp [Array.any_eq]
    exists i
    exists hi
    exists j
    exists hj
    have heqa : a[i]! = a[i] := by
      exact getElem!_pos a i hi
    have heqb : b[j]! = b[j] := by
      exact getElem!_pos b j hj
    rw [heqa, heqb] at heq
    exact heq
  · intro h
    simp [Array.any_eq] at h
    rcases h with ⟨i, hi, j, hj, heq⟩
    exists i
    exists j
    simp [hi, hj]
    have heqa : a[i]! = a[i] := by
      exact getElem!_pos a i hi
    have heqb : b[j]! = b[j] := by
      exact getElem!_pos b j hj
    rw [heqa, heqb]
    exact heq
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
a: #[]
b: #[]
-----Description-----
This problem asks for a method to determine the sum of the first N natural numbers. The task focuses on computing the total when given an input N, ensuring that the value is 0 when N is 0 and correctly calculated for positive values of N.

-----Input-----
The input consists of:
• N: A natural number (Nat) representing the count of the first natural numbers to sum.

-----Output-----
The output is a natural number (Nat), which is the sum of the first N natural numbers computed as: N * (N + 1) / 2.

-----Note-----
The computation leverages a recursive implementation. There are no additional preconditions beyond providing a valid natural number.
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 CalSum_precond (N : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def CalSum (N : Nat) (h_precond : CalSum_precond (N)) : Nat :=
  -- !benchmark @start code
  let rec loop (n : Nat) : Nat :=
    if n = 0 then 0
    else n + loop (n - 1)
  loop N
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def CalSum_postcond (N : Nat) (result: Nat) (h_precond : CalSum_precond (N)) :=
  -- !benchmark @start postcond
  2 * result = N * (N + 1)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem CalSum_spec_satisfied (N: Nat) (h_precond : CalSum_precond (N)) :
    CalSum_postcond (N) (CalSum (N) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold CalSum_postcond CalSum
  induction N with
  | zero =>
    unfold CalSum.loop
    simp
  | succ n ih =>
    unfold CalSum_precond at ih
    simp at ih
    unfold CalSum.loop
    simp
    rw [Nat.mul_add]
    rw [ih]
    rw [← Nat.add_mul]
    rw [Nat.add_comm, Nat.mul_comm]
  -- !benchmark @end proof


Tests:
input: N: 0
N: 1
N: 5
N: 10
N: 20
expected: 0
1
15
55
210
unexpected: 1
2
3
0
2
3
10
16
20
54
56
50
200
220
205

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method of which given a number n and divisor d, it counts all the number that is smaller than
n whose sum of digits is divisible by d. 
-----Input-----
The input consists of three Nat:
n: Nat
d:Nat where d > 0

-----Output-----
The output is an Natural number:
Ensure this match the count that satisfy the property.


Difficulty: advanced

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def sumOfDigits (x : Nat) : Nat :=
  let rec go (n acc : Nat) : Nat :=
    if n = 0 then acc
    else go (n / 10) (acc + (n % 10))
  go x 0
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def countSumDivisibleBy_precond (n : Nat) (d : Nat) : Prop :=
  -- !benchmark @start precond
  d > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux
def isSumDivisibleBy (x : Nat) (d:Nat) : Bool :=
  (sumOfDigits x) % d = 0
-- !benchmark @end code_aux


def countSumDivisibleBy (n : Nat) (d : Nat) (h_precond : countSumDivisibleBy_precond (n) (d)) : Nat :=
  -- !benchmark @start code
  let rec go (i acc : Nat) : Nat :=
    match i with
    | 0 => acc
    | i'+1 =>
      let acc' := if isSumDivisibleBy i' d then acc + 1 else acc
      go i' acc'
  go n 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def countSumDivisibleBy_postcond (n : Nat) (d : Nat) (result: Nat) (h_precond : countSumDivisibleBy_precond (n) (d)) : Prop :=
  -- !benchmark @start postcond
  (List.length (List.filter (fun x => x < n ∧ (sumOfDigits x) % d = 0) (List.range n))) - result = 0 ∧
  result ≤ (List.length (List.filter (fun x => x < n ∧ (sumOfDigits x) % d = 0) (List.range n)))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem countSumDivisibleBy_spec_satisfied (n: Nat) (d: Nat) (h_precond : countSumDivisibleBy_precond (n) (d)) :
    countSumDivisibleBy_postcond (n) (d) (countSumDivisibleBy (n) (d) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: n: 0
d: 2
n: 1
d: 2
n: 10
d: 3
n: 12
d: 2
n: 20
d: 5
expected: 0
1
4
6
4
unexpected: 1
0
3
5
3
5
0
10

Inputs rejected by the precondition:
n: 1
d: 0
-----Description----- 
This task requires writing a Lean 4 method that finds the length of the longest strictly increasing subsequence from a given list of integers. 

-----Input-----
The input consists of a list of integers called nums

-----Output-----
The output is an integer:
Returns a number representing the length of the longest strictly increasing subsequence found in the input list.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution
import Mathlib.Data.List.Basic
-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def longestIncreasingSubsequence_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def longestIncreasingSubsequence (nums : List Int) (h_precond : longestIncreasingSubsequence_precond (nums)) : Int :=
  -- !benchmark @start code
  Id.run do
    if nums.isEmpty then return 0
    let mut sub : Array Int := Array.empty
    sub := sub.push nums.head!
    for num in nums.tail do
      if num > sub[sub.size - 1]! then
        sub := sub.push num
      else
       -- << binary search >>
        let mut left : Nat := 0
        let mut right : Nat := sub.size - 1
        while left < right do
          let mid := (left + right) / 2
          if sub[mid]! == num then
            right := mid
          else if sub[mid]! < num then
            left := mid + 1
          else
            right := mid
        sub := sub.set! left num
    return Int.ofNat sub.size
  -- !benchmark @end code


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


@[reducible]
def longestIncreasingSubsequence_postcond (nums : List Int) (result: Int) (h_precond : longestIncreasingSubsequence_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let allSubseq := (nums.foldl fun acc x => acc ++ acc.map (fun sub => x :: sub)) [[]] |>.map List.reverse
  let increasingSubseqLens := allSubseq.filter (fun l => List.Pairwise (· < ·) l) |>.map (·.length)
  increasingSubseqLens.contains result ∧ increasingSubseqLens.all (· ≤ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem longestIncreasingSubsequence_spec_satisfied (nums: List Int) (h_precond : longestIncreasingSubsequence_precond (nums)) :
    longestIncreasingSubsequence_postcond (nums) (longestIncreasingSubsequence (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: [10, 9, 2, 5, 3, 7, 101, 18]
nums: [0, 1, 0, 3, 2, 3]
nums: [7, 7, 7, 7, 7, 7, 7]
nums: [1, 3, 2, 4]
nums: [10]
expected: 4
4
1
3
1
unexpected: 3
100
3
100
7
7
2
4
0

Inputs rejected by the precondition:
-----Description-----  
This problem involves swapping the values of two integers. Given two integers as inputs, the objective is to return the two numbers in reversed order.

-----Input-----  
The input consists of two integers:  
• X: The first integer.  
• Y: The second integer.

-----Output-----  
The output is a tuple of two integers (Int × Int) where:  
• The first element is equal to Y.  
• The second element is equal to X.

-----Note-----  
There are no restrictions on the input values. The function must correctly swap the inputs regardless of whether they are positive, negative, or zero.
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 SwapArithmetic_precond (X : Int) (Y : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def SwapArithmetic (X : Int) (Y : Int) (h_precond : SwapArithmetic_precond (X) (Y)) : (Int × Int) :=
  -- !benchmark @start code
  let x1 := X
  let y1 := Y
  let x2 := y1 - x1
  let y2 := y1 - x2
  let x3 := y2 + x2
  (x3, y2)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def SwapArithmetic_postcond (X : Int) (Y : Int) (result: (Int × Int)) (h_precond : SwapArithmetic_precond (X) (Y)) :=
  -- !benchmark @start postcond
  result.1 = Y ∧ result.2 = X ∧
  (X ≠ Y → result.fst ≠ X ∧ result.snd ≠ Y)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem SwapArithmetic_spec_satisfied (X: Int) (Y: Int) (h_precond : SwapArithmetic_precond (X) (Y)) :
    SwapArithmetic_postcond (X) (Y) (SwapArithmetic (X) (Y) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold SwapArithmetic_postcond SwapArithmetic
  simp
  rw [Int.sub_sub_self]
  simp_all
  exact fun a a_1 => a (id (Eq.symm a_1))
  -- !benchmark @end proof


Tests:
input: X: 3
Y: 4
X: -1
Y: 10
X: 0
Y: 0
X: 100
Y: 50
X: -5
Y: -10
expected: (4, 3)
(10, -1)
(0, 0)
(50, 100)
(-10, -5)
unexpected: (3, 4)
(3, 3)
(4, 4)
(-1, 10)
(10, 1)
(-10, -1)
(0, 1)
(1, 0)
(-1, 0)
(100, 50)
(50, 50)
(100, 100)
(-5, -10)
(-10, -10)
(-5, -5)

Inputs rejected by the precondition:
-----Description-----  
This task requires writing a Lean 4 method that computes the product of the first even and the first odd number encountered in a list of integers. The method should search the list for the earliest even number and the earliest odd number, then return the product of these two numbers.

-----Input-----  
The input consists of:  
lst: A list of integers.

-----Output-----  
The output is an integer:  
Returns the product resulting from multiplying the first even number and the first odd number found in the list.

-----Note-----  
The input list is assumed 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

def firstEvenOddIndices (lst : List Int) : Option (Nat × Nat) :=
  let evenIndex := lst.findIdx? isEven
  let oddIndex := lst.findIdx? isOdd
  match evenIndex, oddIndex with
  | some ei, some oi => some (ei, oi)
  | _, _ => none
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

@[reducible, simp]
def findProduct_precond (lst : List Int) : Prop :=
  -- !benchmark @start precond
  lst.length > 1 ∧
  (∃ x ∈ lst, isEven x) ∧
  (∃ x ∈ lst, isOdd x)
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def findProduct (lst : List Int) (h_precond : findProduct_precond (lst)) : Int :=
  -- !benchmark @start code
  match firstEvenOddIndices lst with
  | some (ei, oi) => lst[ei]! * lst[oi]!
  | none => 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def findProduct_postcond (lst : List Int) (result: Int) (h_precond : findProduct_precond (lst)) :=
  -- !benchmark @start postcond
  match firstEvenOddIndices lst with
  | some (ei, oi) => result = lst[ei]! * lst[oi]!
  | none => True
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem findProduct_spec_satisfied (lst: List Int) (h_precond : findProduct_precond (lst)) :
    findProduct_postcond (lst) (findProduct (lst) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold findProduct findProduct_postcond
  split
  case h_1 _ ei oi _ =>
    split
    case h_1 _ ei' oi' heq =>
      have : ei = ei' ∧ oi = oi' := by
        rw [Option.some_inj] at heq
        cases heq with
        | refl => exact ⟨rfl, rfl⟩
      simp [this]
    case h_2 _ heq => contradiction
  case h_2 => simp
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
lst: [2]