sunblaze-ucb/verina huggingface dataset:
-----Description-----  
This task involves determining the first index in an array where a given condition holds true. The goal is to identify the position of the first element that meets a specified criterion, ensuring that no preceding element does.

-----Input-----  
The input consists of:  
• a: An array of elements (for testing purposes, you can assume it is an array of integers).  
• P: A predicate function on the elements (represented as a string for test cases, e.g., "fun x => x > 5"). It is assumed that at least one element in the array satisfies P.

-----Output-----  
The output is a natural number (Nat) which represents the index of the first element in the array that satisfies the predicate P.  
• The index returned is less than the size of the array.  
• The element at the returned index satisfies P.  
• All elements before the returned index do not satisfy P.

-----Note-----  
It is assumed that the array contains at least one element that satisfies P. In cases where this precondition does not hold, the behavior of the function is not guaranteed by the specification.
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 LinearSearch3_precond (a : Array Int) (P : Int -> Bool) : Prop :=
  -- !benchmark @start precond
  ∃ i, i < a.size ∧ P (a[i]!)
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def LinearSearch3 (a : Array Int) (P : Int -> Bool) (h_precond : LinearSearch3_precond (a) (P)) : Nat :=
  -- !benchmark @start code
  let rec loop (n : Nat) : Nat :=
    if n < a.size then
      if P (a[n]!) then n else loop (n + 1)
    else
      0
  loop 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def LinearSearch3_postcond (a : Array Int) (P : Int -> Bool) (result: Nat) (h_precond : LinearSearch3_precond (a) (P)) :=
  -- !benchmark @start postcond
  result < a.size ∧ P (a[result]!) ∧ (∀ k, k < result → ¬ P (a[k]!))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem LinearSearch3_spec_satisfied (a: Array Int) (P: Int -> Bool) (h_precond : LinearSearch3_precond (a) (P)) :
    LinearSearch3_postcond (a) (P) (LinearSearch3 (a) (P) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[4, 7, 2, 9]
P: fun x => x > 5
a: #[10, 8, 6, 4, 2]
P: fun x => x < 5
a: #[5, 3, 1, 2]
P: fun x => x == 1
a: #[0, 1, 2, 3]
P: fun x => x == 0
a: #[9, 9, 9, 9]
P: fun x => x == 9
expected: 1
3
2
0
0
unexpected: 0
2
3
0
1
4
0
1
3
1
2
3
1
2
3

Inputs rejected by the precondition:
a: #[1, 2, 3, 4, 5]
P: fun x => x > 10
-----Description-----
This task requires writing a Lean 4 function that takes a list of stock prices and returns the maximum profit achievable by buying on one day and selling on a later day.

If no profit is possible, the function should return 0.

-----Input-----
The input consists of:
prices: A list of natural numbers representing stock prices on each day.

-----Output-----
The output is a natural number:
Returns the maximum profit achievable with one transaction (buy once, sell once), or 0 if no profitable transaction is possible.


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


-- !benchmark @start code_aux
def updateMinAndProfit (price : Nat) (minSoFar : Nat) (maxProfit : Nat) : (Nat × Nat) :=
  let newMin := Nat.min minSoFar price
  let profit := if price > minSoFar then price - minSoFar else 0
  let newMaxProfit := Nat.max maxProfit profit
  (newMin, newMaxProfit)

def maxProfitAux (prices : List Nat) (minSoFar : Nat) (maxProfit : Nat) : Nat :=
  match prices with
  | [] => maxProfit
  | p :: ps =>
    let (newMin, newProfit) := updateMinAndProfit p minSoFar maxProfit
    maxProfitAux ps newMin newProfit
-- !benchmark @end code_aux


def maxProfit (prices : List Nat) (h_precond : maxProfit_precond (prices)) : Nat :=
  -- !benchmark @start code
  match prices with
  | [] => 0
  | p :: ps => maxProfitAux ps p 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def maxProfit_postcond (prices : List Nat) (result: Nat) (h_precond : maxProfit_precond (prices)) : Prop :=
  -- !benchmark @start postcond
  -- All valid transactions have profit ≤ result
  List.Pairwise (fun ⟨pi, i⟩ ⟨pj, j⟩ => i < j → pj - pi ≤ result) prices.zipIdx ∧
  -- result = 0 when no profitable transaction exists (empty, single element, or decreasing prices)
  (result = 0 ↔
    (prices.length ≤ 1 ∨
     prices.zipIdx.all (fun ⟨pi, i⟩ =>
       prices.zipIdx.all (fun ⟨pj, j⟩ => i ≥ j ∨ pj ≤ pi)))) ∧
  -- If result > 0, there exists a transaction achieving it
  (result > 0 → prices.zipIdx.any (fun ⟨pi, i⟩ =>
    prices.zipIdx.any (fun ⟨pj, j⟩ => i < j ∧ pj - pi = result)))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem maxProfit_spec_satisfied (prices: List Nat) (h_precond : maxProfit_precond (prices)) :
    maxProfit_postcond (prices) (maxProfit (prices) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
-----Description-----  
This task involves determining the triple of a given integer. The goal is to create a function that, for any integer provided as input, returns a value equal to three times that integer, including handling the case when the input is zero.

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

-----Output-----  
The output is an integer that represents three times the input integer.  
• If x = 0, the output will be 0.  
• Otherwise, the output will be computed as x + 2 * x, which is equivalent to 3 * x.

-----Note-----  
There are no additional preconditions. It is assumed that x is a valid integer.
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 = 0 then 0 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
  split_ifs with h₁
  . rw [h₁]
    simp
  . simp
    rw (occs := [1]) [←Int.one_mul x]
    rw [←Int.add_mul]
    simp +arith
  -- !benchmark @end proof


Tests:
input: x: 0
x: 1
x: -2
x: 10
x: -5
expected: 0
3
-6
30
-15
unexpected: 1
-1
10
2
4
0
-4
-2
6
20
40
0
-10
-5
15

Inputs rejected by the precondition:
-----Description-----
Implement a Lean 4 function that, given a list of integers, removes all duplicates and returns the resulting list in ascending order.

-----Input-----
The input consists of a single list of integers:
arr: A list of integers.

-----Output-----
The output is a list of integers:
Returns a list containing the unique elements of the input, sorted in ascending order. The returned list must not contain any duplicates, and every element in the output must appear in the original 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, simp]
def uniqueSorted_precond (arr : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def uniqueSorted (arr : List Int) (h_precond : uniqueSorted_precond (arr)) : List Int :=
  -- !benchmark @start code
  let rec insert (x : Int) (sorted : List Int) : List Int :=
  match sorted with
  | [] =>
    [x]
  | head :: tail =>
    if x <= head then
      x :: head :: tail
    else
      head :: insert x tail

let rec insertionSort (xs : List Int) : List Int :=
  match xs with
  | [] =>
    []
  | h :: t =>
    let sortedTail := insertionSort t
    insert h sortedTail

let removeDups : List Int → List Int
| xs =>
  let rec aux (remaining : List Int) (seen : List Int) (acc : List Int) : List Int :=
    match remaining with
    | [] =>
      acc.reverse
    | h :: t =>
      if h ∈ seen then
        aux t seen acc
      else
        aux t (h :: seen) (h :: acc)
  aux xs [] []

insertionSort (removeDups arr)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def uniqueSorted_postcond (arr : List Int) (result: List Int) (h_precond : uniqueSorted_precond (arr)) : Prop :=
  -- !benchmark @start postcond
  List.isPerm arr.eraseDups result ∧ List.Pairwise (· ≤ ·) result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem uniqueSorted_spec_satisfied (arr: List Int) (h_precond : uniqueSorted_precond (arr)) :
    uniqueSorted_postcond (arr) (uniqueSorted (arr) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: arr: [1, 1, 2, 3]
arr: [3, 3, 3]
arr: [5, 2, 2, 5]
arr: [1, 2, 3, 4, 5]
expected: [1, 2, 3]
[3]
[2, 5]
[1, 2, 3, 4, 5]
unexpected: [1, 1, 2, 3]
[2, 3, 1]
[1, 3, 2]
[3, 3, 3]
[3, 3]
[3, 3, 3, 3]
[0]
[1]
[999]
[5, 2]
[2, 2, 5]
[2]
[1, 2, 3]
[2, 3, 4, 5]
[5, 4, 3, 2, 1]

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that finds the last occurrence of a specified element in a sorted array of integers. The method should return the index corresponding to the last occurrence of the element if it is present; if the element is absent, it should return -1. Additionally, the array must remain unchanged after the method is executed.

-----Input-----
The input consists of:
arr: A sorted array of integers in non-decreasing order.
elem: An integer whose last occurrence position is to be determined.

-----Output-----
The output is an integer:
Returns the index of the last occurrence of the specified integer in the array if it exists.
Returns -1 if the integer is not found in the array.

-----Note-----
The input array is assumed to be sorted in non-decreasing order and remains unchanged by the method.
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 lastPosition_precond (arr : Array Int) (elem : Int) : Prop :=
  -- !benchmark @start precond
  List.Pairwise (· ≤ ·) arr.toList
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


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

-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def lastPosition_postcond (arr : Array Int) (elem : Int) (result: Int) (h_precond : lastPosition_precond (arr) (elem)) :=
  -- !benchmark @start postcond
  (result ≥ 0 →
    arr[result.toNat]! = elem ∧ (arr.toList.drop (result.toNat + 1)).all (· ≠ elem)) ∧
  (result = -1 → arr.toList.all (· ≠ elem))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem lastPosition_spec_satisfied (arr: Array Int) (elem: Int) (h_precond : lastPosition_precond (arr) (elem)) :
    lastPosition_postcond (arr) (elem) (lastPosition (arr) (elem) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
arr: #[3, 2, 1]
elem: 2
-----Description----- 
This task requires writing a Lean 4 method that determines whether a given string contains the character 'z' or 'Z'. The method should return true if the string includes either the lowercase or uppercase letter 'z', and false otherwise.

-----Input-----
The input consists of:
s: A string.

-----Output-----
The output is a Boolean value:
Returns true if the input string contains the character 'z' or 'Z'.
Returns false if the input string does not contain the character 'z' or 'Z'.

-----Note-----
There are no preconditions; the method will always work as strings and sequences are considered 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 containsZ_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def containsZ (s : String) (h_precond : containsZ_precond (s)) : Bool :=
  -- !benchmark @start code
  s.toList.any fun c => c = 'z' || c = 'Z'
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def containsZ_postcond (s : String) (result: Bool) (h_precond : containsZ_precond (s)) :=
  -- !benchmark @start postcond
  let cs := s.toList
  (∃ x, x ∈ cs ∧ (x = 'z' ∨ x = 'Z')) ↔ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem containsZ_spec_satisfied (s: String) (h_precond : containsZ_precond (s)) :
    containsZ_postcond (s) (containsZ (s) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold containsZ containsZ_postcond
  simp_all
  -- !benchmark @end proof


Tests:
input: s: hello
s: zebra
s: Zebra
s: crazy
s: AZ
s: abc
s: Zz
s: no letter
expected: False
True
True
False
True
True
False
True
False
unexpected: True
False
False
True
False
False
True
False
True

Inputs rejected by the precondition:
-----Description-----  
This task requires writing a Lean 4 method that takes a given string and returns a new string where every occurrence of a space, comma, or dot is replaced with a colon. The transformation must preserve the original string’s length and leave all other characters unmodified.

-----Input-----  
The input consists of:  
s: A string.

-----Output-----  
The output is a string:  
- The returned string must have the same length as the input string.  
- Every space, comma, or dot in the input string is replaced with a colon.  
- All other characters remain unchanged.

-----Note-----  
There are no preconditions; the input string is assumed to be non-null.
Difficulty: basic

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def isSpaceCommaDot (c : Char) : Bool :=
  if c = ' ' then true
  else if c = ',' then true
  else if c = '.' then true
  else false
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

@[reducible, simp]
def replaceWithColon_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def replaceWithColon (s : String) (h_precond : replaceWithColon_precond (s)) : String :=
  -- !benchmark @start code
  let cs := s.toList
  let cs' := cs.map (fun c => if isSpaceCommaDot c then ':' else c)
  String.mk cs'
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def replaceWithColon_postcond (s : String) (result: String) (h_precond : replaceWithColon_precond (s)) :=
  -- !benchmark @start postcond
  let cs := s.toList
  let cs' := result.toList
  result.length = s.length ∧
  (∀ i, i < s.length →
    (isSpaceCommaDot cs[i]! → cs'[i]! = ':') ∧
    (¬isSpaceCommaDot cs[i]! → cs'[i]! = cs[i]!))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem replaceWithColon_spec_satisfied (s: String) (h_precond : replaceWithColon_precond (s)) :
    replaceWithColon_postcond (s) (replaceWithColon (s) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold replaceWithColon replaceWithColon_postcond
  simp
  constructor
  · unfold String.length
    simp
  · intro i hi
    have hi' : i < s.data.length := by
      unfold String.length at hi
      simp at hi
      exact hi
    constructor <;> simp_all
  -- !benchmark @end proof


Tests:
input: s: Hello, world. How are you?
s: No-changes!
s: ,. 
expected: Hello::world::How:are:you?
No-changes!
:::
unexpected: Hello,world,How,are,you?
Hello: world: How: are: you?
No changes!
No–changes!
::
;:;
::: 
 
a

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that removes all occurrences of a given element from a list of natural numbers. The method should return a new list that contains all the elements of the original list except those equal to the target number. The order of the remaining elements must be preserved.

-----Input-----
The input consists of two elements:
lst: A list of natural numbers (List Nat).
target: A natural number to be removed from the list.

-----Output-----
The output is a list of natural numbers:
Returns a new list with all occurrences of the target number removed. The relative order of the remaining elements must be the same as in 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 removeElement_precond (lst : List Nat) (target : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def removeElement (lst : List Nat) (target : Nat) (h_precond : removeElement_precond (lst) (target)) : List Nat :=
  -- !benchmark @start code
  let rec helper (lst : List Nat) (target : Nat) : List Nat :=
    match lst with
    | [] => []
    | x :: xs =>
      let rest := helper xs target
      if x = target then rest else x :: rest
  helper lst target
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def removeElement_postcond (lst : List Nat) (target : Nat) (result: List Nat) (h_precond : removeElement_precond (lst) (target)): Prop :=
  -- !benchmark @start postcond
  -- 1. All elements equal to target are removed from the result.
  -- 2. All other elements are preserved in order.
  -- 3. No new elements are added.

  -- Helper predicate: result contains exactly the elements of lst that are not equal to target, in order
  let lst' := lst.filter (fun x => x ≠ target)
  result.zipIdx.all (fun (x, i) =>
    match lst'[i]? with
    | some y => x = y
    | none => false) ∧ result.length = lst'.length
  -- !benchmark @end postcond


-- !benchmark @start proof_aux
-- !benchmark @end proof_aux


theorem removeElement_spec_satisfied (lst: List Nat) (target: Nat) (h_precond : removeElement_precond (lst) (target)):
    removeElement_postcond (lst) (target) (removeElement (lst) (target) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: lst: [1, 2, 3, 2, 4]
target: 2
lst: [5, 5, 5, 5]
target: 5
lst: [7, 8, 9]
target: 4
target: 3
lst: [0, 1, 0, 2, 0]
target: 0
expected: [1, 3, 4]
[7, 8, 9]
[1, 2]
unexpected: [1, 2, 3, 4]
[1, 2, 3]
[1, 4]
[5]
[0]
[5, 5]
[7, 8]
[8, 9]
[3]
[0]
[1, 2, 3]
[0, 1, 2]
[1]
[1, 0, 2]

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that determines the minimum of two integers. The method should return the smaller of the two numbers. When both numbers are equal, either one may be returned.

-----Input-----
The input consists of two integers:
a: The first integer.
b: The second integer.

-----Output-----
The output is an integer:
Returns the smaller value between the input integers, ensuring that the result is less than or equal to both inputs.
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 myMin_precond (a : Int) (b : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def myMin (a : Int) (b : Int) (h_precond : myMin_precond (a) (b)) : Int :=
  -- !benchmark @start code
  if a <= b then a else b
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def myMin_postcond (a : Int) (b : Int) (result: Int) (h_precond : myMin_precond (a) (b)) :=
  -- !benchmark @start postcond
  (result ≤ a ∧ result ≤ b) ∧
  (result = a ∨ result = b)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem myMin_spec_satisfied (a: Int) (b: Int) (h_precond : myMin_precond (a) (b)) :
    myMin_postcond (a) (b) (myMin (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold myMin myMin_postcond
  constructor
  · split
    case left.isTrue h =>
      simp
      exact h
    case left.isFalse h =>
      simp
      rw [Int.not_le] at h
      exact Int.le_of_lt h
  · split <;> simp
  -- !benchmark @end proof


Tests:
input: a: 3
b: 5
a: 10
b: 7
a: 4
b: 4
a: -3
b: 5
a: 3
b: -5
a: -3
b: -5
a: 0
b: 10
a: 0
b: -10
expected: 3
7
4
-3
-5
-5
0
-10
unexpected: 5
4
8
10
8
9
0
8
2
5
0
-5
3
0
-3
-3
0
-1
10
1
-1
0
-1
-5

Inputs rejected by the precondition: