sunblaze-ucb/verina huggingface dataset:
-----Description----- 
This task requires writing a Lean 4 method that finds the length of the logest common subsequence of two input arrays.

-----Input-----
The input consists of two arrays:
a: The first array.
b: The second array.


-----Output-----
The output is an integer:
Returns the length of array a and b's longest common subsequence.


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 LongestCommonSubsequence_precond (a : Array Int) (b : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def intMax (x y : Int) : Int :=
  if x < y then y else x
-- !benchmark @end code_aux


def LongestCommonSubsequence (a : Array Int) (b : Array Int) (h_precond : LongestCommonSubsequence_precond (a) (b)) : Int :=
  -- !benchmark @start code
  let m := a.size
  let n := b.size

  let dp := Id.run do
    let mut dp := Array.mkArray (m + 1) (Array.mkArray (n + 1) 0)
    for i in List.range (m + 1) do
      for j in List.range (n + 1) do
        if i = 0 ∨ j = 0 then
          ()
        else if a[i - 1]! = b[j - 1]! then
          let newVal := ((dp[i - 1]!)[j - 1]!) + 1
          dp := dp.set! i (dp[i]!.set! j newVal)
        else
          let newVal := intMax ((dp[i - 1]!)[j]!) ((dp[i]!)[j - 1]!)
          dp := dp.set! i (dp[i]!.set! j newVal)
    return dp
  (dp[m]!)[n]!
  -- !benchmark @end code


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


@[reducible]
def LongestCommonSubsequence_postcond (a : Array Int) (b : Array Int) (result: Int) (h_precond : LongestCommonSubsequence_precond (a) (b)) : Prop :=
  -- !benchmark @start postcond
  let allSubseq (arr : Array Int) := (arr.foldl fun acc x => acc ++ acc.map (fun sub => x :: sub)) [[]] |>.map List.reverse
  let subseqA := allSubseq a
  let subseqB := allSubseq b
  let commonSubseqLens := subseqA.filter (fun l => subseqB.contains l) |>.map (·.length)
  commonSubseqLens.contains result ∧ commonSubseqLens.all (· ≤ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem LongestCommonSubsequence_spec_satisfied (a: Array Int) (b: Array Int) (h_precond : LongestCommonSubsequence_precond (a) (b)) :
    LongestCommonSubsequence_postcond (a) (b) (LongestCommonSubsequence (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that finds the smallest number in an array of integers.

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

-----Output-----
The output is an option integer:
Returns the smallest number found in the input array or none if the array is 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 findSmallest_precond (s : Array Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def findSmallest (s : Array Nat) (h_precond : findSmallest_precond (s)) : Option Nat :=
  -- !benchmark @start code
  s.toList.min?
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def findSmallest_postcond (s : Array Nat) (result: Option Nat) (h_precond : findSmallest_precond (s)) :=
  -- !benchmark @start postcond
  let xs := s.toList
  match result with
  | none => xs = []
  | some r => r ∈ xs ∧ (∀ x, x ∈ xs → r ≤ x)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem findSmallest_spec_satisfied (s: Array Nat) (h_precond : findSmallest_precond (s)) :
    findSmallest_postcond (s) (findSmallest (s) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold findSmallest_postcond findSmallest
  cases res : s.toList.min? with
  | none =>
    simp only [res]
    rw [List.min?_eq_none_iff] at res
    exact res
  | some r =>
    simp only [res]
    rw [List.min?_eq_some_iff'] at res
    exact res
  -- !benchmark @end proof


Tests:
input: s: #[3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5]
s: #[0, 1, 2, 3, 4, 5]
s: #[1]
s: #[10, 10, 10]
s: #[3, 2, 2, 2, 2, 2, 2, 1]
s: #[0]
s: #[100, 99, 98]
s: #[]
expected: some (1)
some (0)
some (1)
some (10)
some (1)
some (0)
some (98)
none
unexpected: some (2)
some (0)
none
some (1)
none
some (0)
some (2)
none
some (9)
some (0)
none
some (2)
some (0)
none
some (1)
none
some (99)
some (97)
none
some (0)

Inputs rejected by the precondition:
-----Description-----  
This problem involves updating an array of integers by modifying two specific positions. Specifically, the element at index 4 should be increased by 3, and the element at index 7 should be changed to 516. The goal is to correctly update these positions while leaving the rest of the array unchanged. The description assumes that the array contains at least 8 elements.

-----Input-----  
The input consists of:  
• a: An array of integers. The array must contain at least 8 elements.

-----Output-----  
The output is an array of integers that meets the following criteria:  
• The element at index 4 is updated to its original value plus 3.  
• The element at index 7 is set to 516.  
• All other elements in the array remain the same as in the input array.

-----Note-----  
It is assumed that the input array has a size of at least 8 elements. Indices are 0-indexed.
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 UpdateElements_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size ≥ 8
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def UpdateElements (a : Array Int) (h_precond : UpdateElements_precond (a)) : Array Int :=
  -- !benchmark @start code
  let a1 := a.set! 4 ((a[4]!) + 3)
  let a2 := a1.set! 7 516
  a2
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def UpdateElements_postcond (a : Array Int) (result: Array Int) (h_precond : UpdateElements_precond (a)) :=
  -- !benchmark @start postcond
  result[4]! = (a[4]!) + 3 ∧
  result[7]! = 516 ∧
  (∀ i, i < a.size → i ≠ 4 → i ≠ 7 → result[i]! = a[i]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem UpdateElements_spec_satisfied (a: Array Int) (h_precond : UpdateElements_precond (a)) :
    UpdateElements_postcond (a) (UpdateElements (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[0, 1, 2, 3, 4, 5, 6, 7, 8]
a: #[10, 20, 30, 40, 50, 60, 70, 80]
a: #[-1, -2, -3, -4, -5, -6, -7, -8, -9, -10]
a: #[0, 0, 0, 0, 0, 0, 0, 0]
a: #[5, 5, 5, 5, 5, 5, 5, 5]
expected: #[0, 1, 2, 3, 7, 5, 6, 516, 8]
#[10, 20, 30, 40, 53, 60, 70, 516]
#[-1, -2, -3, -4, -2, -6, -7, 516, -9, -10]
#[0, 0, 0, 0, 3, 0, 0, 516]
#[5, 5, 5, 5, 8, 5, 5, 516]
unexpected: #[0, 1, 2, 3, 4, 5, 6, 516, 8]
#[0, 1, 2, 3, 7, 5, 6, 7, 8]
#[10, 20, 30, 40, 50, 60, 70, 80]
#[10, 20, 30, 40, 53, 60, 70, 80]
#[-1, -2, -3, -4, -5, -6, -7, 516, -9, -10]
#[-1, -2, -3, -4, -2, -6, -7, -8, -9, -10]
#[0, 0, 0, 0, 0, 0, 0, 516]
#[0, 0, 0, 0, 3, 0, 0, 0]
#[5, 5, 5, 5, 5, 5, 5, 5]
#[5, 5, 5, 5, 8, 5, 5, 5]

Inputs rejected by the precondition:
a: #[1, 2, 3, 4, 5, 6]
-----Description-----  
This task requires determining whether a given list of characters is a palindrome; that is, whether the sequence reads the same forward and backward.

-----Input-----  
The input consists of:  
• x: A list of characters (List Char). The list can be empty or non-empty.

-----Output-----  
The output is a Boolean value (Bool):  
• Returns true if the input list is a palindrome.  
• Returns false otherwise.

-----Note-----  
An empty list is considered a palindrome. The function does not impose any 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 IsPalindrome_precond (x : List Char) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def isPalindromeHelper (x : List Char) (i j : Nat) : Bool :=
  if i < j then
    match x[i]?, x[j]? with
    | some ci, some cj =>
      if ci ≠ cj then false else isPalindromeHelper x (i + 1) (j - 1)
    | _, _ => false  -- This case should not occur due to valid indices
  else true
-- !benchmark @end code_aux


def IsPalindrome (x : List Char) (h_precond : IsPalindrome_precond (x)) : Bool :=
  -- !benchmark @start code
  if x.length = 0 then true else isPalindromeHelper x 0 (x.length - 1)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def IsPalindrome_postcond (x : List Char) (result: Bool) (h_precond : IsPalindrome_precond (x)) :=
  -- !benchmark @start postcond
  result ↔ ∀ i : Nat, i < x.length → (x[i]! = x[x.length - i - 1]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem IsPalindrome_spec_satisfied (x: List Char) (h_precond : IsPalindrome_precond (x)) :
    IsPalindrome_postcond (x) (IsPalindrome (x) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: x: a
x: a, b, a
x: a, b, c
x: r, a, c, e, c, a, r
expected: true
true
true
false
true
unexpected: false
false
false
true
false

Inputs rejected by the precondition:
-----Description-----  
This task requires swapping two integer values. Given two integers as input, the objective is to produce an output where their order is reversed: the first element of the output corresponds to the second input and the second element corresponds to the first input.

-----Input-----  
The input consists of two integers:  
• X: An integer value.  
• Y: Another integer value.

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

-----Note-----  
There are no additional preconditions for this task. The function simply returns a swapped tuple of its two input 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 SwapSimultaneous_precond (X : Int) (Y : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def SwapSimultaneous (X : Int) (Y : Int) (h_precond : SwapSimultaneous_precond (X) (Y)) : Int × Int :=
  -- !benchmark @start code
  (Y, X)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def SwapSimultaneous_postcond (X : Int) (Y : Int) (result: Int × Int) (h_precond : SwapSimultaneous_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 SwapSimultaneous_spec_satisfied (X: Int) (Y: Int) (h_precond : SwapSimultaneous_precond (X) (Y)) :
    SwapSimultaneous_postcond (X) (Y) (SwapSimultaneous (X) (Y) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold SwapSimultaneous_postcond SwapSimultaneous
  simp_all
  exact fun a a_1 => a (id (Eq.symm a_1))
  -- !benchmark @end proof


Tests:
input: X: 3
Y: 4
X: -10
Y: 20
X: 0
Y: 0
X: 123
Y: -456
X: -1
Y: -2
expected: (4, 3)
(20, -10)
(0, 0)
(-456, 123)
(-2, -1)
unexpected: (3, 4)
(3, 3)
(20, -20)
(-10, 20)
(0, 1)
(1, 0)
(123, -456)
(-123, 456)
(-1, -2)
(-2, 2)

Inputs rejected by the precondition:
-----Description-----  
This task involves creating a function that swaps two integer values. Given two integers, the function should return a pair where the first element is the second input value and the second element is the first input value.

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

-----Output-----  
The output is a pair (Int × Int) that:  
• Contains the original Y as the first element.  
• Contains the original X as the second element.

-----Note-----  
There are no additional preconditions. The function simply swaps the two input values.
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 Swap_precond (X : Int) (Y : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def Swap (X : Int) (Y : Int) (h_precond : Swap_precond (X) (Y)) : Int × Int :=
  -- !benchmark @start code
  let x := X
  let y := Y
  let tmp := x
  let x := y
  let y := tmp
  (x, y)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


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


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem Swap_spec_satisfied (X: Int) (Y: Int) (h_precond : Swap_precond (X) (Y)) :
    Swap_postcond (X) (Y) (Swap (X) (Y) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold Swap_postcond Swap
  simp_all
  exact fun a a_1 => a (id (Eq.symm a_1))
  -- !benchmark @end proof


Tests:
input: X: 1
Y: 2
X: 0
Y: 0
X: -1
Y: 5
X: 100
Y: -100
X: 42
Y: 42
expected: (2, 1)
(0, 0)
(5, -1)
(-100, 100)
(42, 42)
unexpected: (1, 2)
(2, 2)
(0, 1)
(1, 0)
(-1, 5)
(5, 5)
(100, -100)
(-100, -100)
(41, 42)
(42, 41)

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that determines whether a given integer is divisible by 11. The method should return true if the number is divisible by 11 and false otherwise.

-----Input-----
The input consists of:
n: An integer to check for divisibility by 11.

-----Output-----
The output is a Boolean value:
Returns true if the input number is divisible by 11.
Returns false if the input number is not divisible by 11.
Difficulty: basic

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

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isDivisibleBy11 (n : Int) (h_precond : isDivisibleBy11_precond (n)) : Bool :=
  -- !benchmark @start code
  n % 11 == 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def isDivisibleBy11_postcond (n : Int) (result: Bool) (h_precond : isDivisibleBy11_precond (n)) :=
  -- !benchmark @start postcond
  (result → (∃ k : Int, n = 11 * k)) ∧ (¬ result → (∀ k : Int, ¬ n = 11 * k))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isDivisibleBy11_spec_satisfied (n: Int) (h_precond : isDivisibleBy11_precond (n)) :
    isDivisibleBy11_postcond (n) (isDivisibleBy11 (n) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold isDivisibleBy11 isDivisibleBy11_postcond
  constructor
  · simp_all
    exact fun a => a
  · apply Not.imp_symm
    rw [not_forall_not]
    intro h
    rw [beq_iff_eq]
    exact Int.emod_eq_zero_of_dvd h
  -- !benchmark @end proof


Tests:
input: n: 0
n: 11
n: 22
n: 23
n: 33
n: 44
n: -11
n: -22
n: 1
n: -1
n: 121
n: 123
expected: True
True
True
False
True
True
True
True
False
False
True
False
unexpected: False
False
False
True
False
False
False
False
True
True
False
True

Inputs rejected by the precondition:
-----Description-----  
This task requires writing a Lean 4 method that rotates an array of integers to the left by a specified offset.

-----Input-----  
The input consists of:  
• a: An array of integers (which may be empty or non-empty).  
• offset: An integer representing the number of positions to rotate the array. The offset is assumed to be non-negative.

-----Output-----  
The output is an array of integers that:  
• Has the same length as the input array.  
• For every valid index i, the output element at index i is equal to the input element at index ((i + offset) mod n), where n is the array size.

-----Note-----  
If the array is empty, the method should return an empty 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 rotate_precond (a : Array Int) (offset : Int) : Prop :=
  -- !benchmark @start precond
  offset ≥ 0
  -- !benchmark @end precond


-- !benchmark @start code_aux
def rotateAux (a : Array Int) (offset : Int) (i : Nat) (len : Nat) (b : Array Int) : Array Int :=
  if i < len then
    let idx_int : Int := (Int.ofNat i + offset) % (Int.ofNat len)
    let idx_int_adjusted := if idx_int < 0 then idx_int + Int.ofNat len else idx_int
    let idx_nat : Nat := Int.toNat idx_int_adjusted
    let new_b := b.set! i (a[idx_nat]!)
    rotateAux a offset (i + 1) len new_b
  else b
-- !benchmark @end code_aux


def rotate (a : Array Int) (offset : Int) (h_precond : rotate_precond (a) (offset)) : Array Int :=
  -- !benchmark @start code
  let len := a.size
  let default_val : Int := if len > 0 then a[0]! else 0
  let b0 := Array.mkArray len default_val
  rotateAux a offset 0 len b0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def rotate_postcond (a : Array Int) (offset : Int) (result: Array Int) (h_precond : rotate_precond (a) (offset)) :=
  -- !benchmark @start postcond
  result.size = a.size ∧
  (∀ i : Nat, i < a.size →
    result[i]! = a[Int.toNat ((Int.ofNat i + offset) % (Int.ofNat a.size))]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem rotate_spec_satisfied (a: Array Int) (offset: Int) (h_precond : rotate_precond (a) (offset)) :
    rotate_postcond (a) (offset) (rotate (a) (offset) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
a: #[1, 2, 3, 4, 5]
offset: -1
-----Description-----  
This task requires computing three times the given integer. The goal is to determine the product of the input integer and 3.

-----Input-----  
The input consists of:  
• x: An integer.

-----Output-----  
The output is an integer that represents three times the input value.

-----Note-----  
The implementation uses two different branches based on the value of x (i.e., x < 18 or x ≥ 18), but both branches guarantee that the result equals 3*x.
Difficulty: basic

Lean 4 solution:
-- !benchmark @start import type=solution
import Mathlib
-- !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
  if x < 18 then
    let a := 2 * x
    let b := 4 * x
    (a + b) / 2
  else
    let y := 2 * x
    x + y
  -- !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
  split_ifs with h₁
  . rw [←Int.add_mul]
    simp
    have h : (6: ℤ) = 3 * 2 := by simp
    rw [h, Int.mul_comm, Int.mul_ediv_assoc, Int.mul_ediv_assoc]
    simp
    rw [Int.mul_comm]
    rfl
    simp
  . rw (occs := [1]) [←Int.one_mul x]
    rw [←Int.add_mul]
    simp +arith
  -- !benchmark @end proof


Tests:
input: x: 10
x: 18
x: 0
x: -5
x: 25
expected: 30
54
0
-15
75
unexpected: 20
25
35
50
56
60
1
-1
5
-10
-20
0
70
80
65

Inputs rejected by the precondition:
-----Description-----  
This task involves computing the average of two integers. The objective is to determine a value that closely approximates the true arithmetic mean when using integer division, ensuring that the result reflects the necessary rounding behavior.

-----Input-----  
The input consists of:  
• a: An integer.  
• b: An integer.

-----Output-----  
The output is an integer representing the computed average of a and b using integer division.

-----Note-----  
The specification requires that the computed average satisfies the condition that 2 * avg is between (a + b - 1) and (a + b + 1), ensuring that the result meets the expected rounding boundaries.
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 ComputeAvg_precond (a : Int) (b : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def ComputeAvg (a : Int) (b : Int) (h_precond : ComputeAvg_precond (a) (b)) : Int :=
  -- !benchmark @start code
  (a + b) / 2
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def ComputeAvg_postcond (a : Int) (b : Int) (result: Int) (h_precond : ComputeAvg_precond (a) (b)) :=
  -- !benchmark @start postcond
  2 * result = a + b - ((a + b) % 2)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem ComputeAvg_spec_satisfied (a: Int) (b: Int) (h_precond : ComputeAvg_precond (a) (b)) :
    ComputeAvg_postcond (a) (b) (ComputeAvg (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: 4
b: 6
a: 3
b: 5
a: 3
b: 4
a: -3
b: 7
a: -5
b: 5
expected: 5
4
3
2
0
unexpected: 4
6
7
3
5
6
2
4
5
1
3
0
1
-1
2

Inputs rejected by the precondition: