sunblaze-ucb/verina huggingface dataset:
-----Description---
This task requires writing a Lean 4 method that's goal is to determine the minimum number of adjacent swaps needed to make the array semi-ordered. You may repeatedly swap 2 adjacent elements in the array. A permutation is called semi-ordered if the first number equals 1 and the last number equals n.

-----Input-----

The input consists of:
- nums: A permutation of [1, 2, ..., n] where n is the length of the list (all distinct integers in range [1, n]).

----Output-----

The output is an integer representing the minimum number of adjacent swaps needed.


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 semiOrderedPermutation_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  let n := nums.length
  n > 0 ∧
  -- Must be a permutation of [1..n]: all distinct, all in range
  List.Nodup nums ∧
  nums.all (fun x => 1 ≤ x ∧ x ≤ Int.ofNat n)
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def semiOrderedPermutation (nums : List Int) (h_precond : semiOrderedPermutation_precond (nums)) : Int :=
  -- !benchmark @start code
  let lengthList := nums.length
  let numOne : Int := 1
  let largestNum : Int := Int.ofNat lengthList

  let firstIndex := nums.idxOf numOne
  let lastIndex := nums.idxOf largestNum

  let startPosition := 0
  let endPosition := lengthList - 1

  let shouldMoveOne := firstIndex != startPosition
  let shouldMoveLast := lastIndex != endPosition

  let distanceOne := if shouldMoveOne then firstIndex else 0
  let distanceLast := if shouldMoveLast then endPosition - lastIndex else 0

  let totalMoves := distanceOne + distanceLast
  let needAdjustment := firstIndex > lastIndex
  let adjustedMoves := if needAdjustment then totalMoves - 1 else totalMoves

  adjustedMoves
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def semiOrderedPermutation_postcond (nums : List Int) (result: Int) (h_precond : semiOrderedPermutation_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let n := nums.length
  let pos1 := nums.idxOf 1
  let posn := nums.idxOf (Int.ofNat n)
  if pos1 > posn then
    pos1 + n = result + 2 + posn
  else
    pos1 + n = result + 1 + posn
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem semiOrderedPermutation_spec_satisfied (nums: List Int) (h_precond : semiOrderedPermutation_precond (nums)) :
    semiOrderedPermutation_postcond (nums) (semiOrderedPermutation (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
{'nums': []}
{'nums': [2, 3, 4]}
{'nums': [1, 1, 2]}
{'nums': [0, 1, 2]}
-----Description----- 
This task requires writing a Lean 4 method that computes the sum of the digits of a non-negative integer. The method should process each digit of the input number and return the total sum. The output is guaranteed to be a non-negative natural number.

-----Input-----
The input consists of:
n: A non-negative integer.

-----Output-----
The output is a natural number:
Returns the sum of the digits of the input integer.

-----Note-----
The input is assumed to be a valid non-negative integer.
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 sumOfDigits_precond (n : Nat) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def sumOfDigits (n : Nat) (h_precond : sumOfDigits_precond (n)) : Nat :=
  -- !benchmark @start code
  let rec loop (n : Nat) (acc : Nat) : Nat :=
    if n = 0 then acc
    else loop (n / 10) (acc + n % 10)
  loop n 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def sumOfDigits_postcond (n : Nat) (result: Nat) (h_precond : sumOfDigits_precond (n)) :=
  -- !benchmark @start postcond
  result - List.sum (List.map (fun c => Char.toNat c - Char.toNat '0') (String.toList (Nat.repr n))) = 0 ∧
  List.sum (List.map (fun c => Char.toNat c - Char.toNat '0') (String.toList (Nat.repr n))) - result = 0
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem sumOfDigits_spec_satisfied (n: Nat) (h_precond : sumOfDigits_precond (n)) :
    sumOfDigits_postcond (n) (sumOfDigits (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: n: 12345
n: 0
n: 987654321
n: 11111
n: 1001
n: 9999
expected: 15
0
45
5
2
36
unexpected: 12
16
14
1
10
5
44
46
50
6
4
7
1
3
11
35
37
34

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that determines if a given integer is strictly greater than every element in a provided array. The method should return true only if the integer is larger than each element in the array; otherwise, it should return false.

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

-----Output-----
The output is a Boolean value:
Returns true if the integer is greater than all elements in the array.
Returns false if there is at least one element in the array that is greater than or equal to the integer.

-----Note-----
The array is 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 isGreater_precond (n : Int) (a : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isGreater (n : Int) (a : Array Int) (h_precond : isGreater_precond (n) (a)) : Bool :=
  -- !benchmark @start code
  a.all fun x => n > x
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def isGreater_postcond (n : Int) (a : Array Int) (result: Bool) (h_precond : isGreater_precond (n) (a)) :=
  -- !benchmark @start postcond
  (∀ i, (hi : i < a.size) → n > a[i]) ↔ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isGreater_spec_satisfied (n: Int) (a: Array Int) (h_precond : isGreater_precond (n) (a)) :
    isGreater_postcond (n) (a) (isGreater (n) (a) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold isGreater isGreater_postcond
  simp [Array.all_eq]
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
n: 0
a: #[]
-----Description-----
Implement the insertion sort algorithm in Lean 4. The function takes a single list of integers
as input and returns a new list that contains the same integers in ascending order.

Implementation must follow a standard insertion sort approach, placing each element into its correct position.
The resulting list must be sorted in ascending order.
The returned list must be a permutation of the input list (i.e., contain exactly the same elements).

-----Input-----
A single list of integers, denoted as xs.

-----Output-----
A list of integers, sorted in ascending order.

Example:
Input:  [3, 1, 4, 2]
Output: [1, 2, 3, 4]


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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def insertionSort (xs : List Int) (h_precond : insertionSort_precond (xs)) : List Int :=
  -- !benchmark @start code
    let rec insert (x : Int) (ys : List Int) : List Int :=
      match ys with
      | []      => [x]
      | y :: ys' =>
        if x <= y then
          x :: y :: ys'
        else
          y :: insert x ys'

    let rec sort (arr : List Int) : List Int :=
      match arr with
      | []      => []
      | x :: xs => insert x (sort xs)

    sort xs
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def insertionSort_postcond (xs : List Int) (result: List Int) (h_precond : insertionSort_precond (xs)) : Prop :=
  -- !benchmark @start postcond
  List.Pairwise (· ≤ ·) result ∧ List.isPerm xs result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem insertionSort_spec_satisfied (xs: List Int) (h_precond : insertionSort_precond (xs)) :
    insertionSort_postcond (xs) (insertionSort (xs) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: xs: [42]
xs: [3, 1, 4, 2]
xs: [5, -1, 0, 10, -1]
xs: [2, 2, 2, 2, 2]
expected: [42]
[1, 2, 3, 4]
[-1, -1, 0, 5, 10]
[2, 2, 2, 2, 2]
unexpected: [0]
[1, 2, 3]
[24]
[42, 42]
[1, 3, 2, 4]
[4, 3, 2, 1]
[-1, -1, 0, 10, 5]
[10, 5, 0, -1, -1]
[2, 2, 2, 2]

Inputs rejected by the precondition:
-----Description-----  
The problem asks you to construct a new list by adding an extra number to the end of an existing list of numbers. The focus is on understanding what the final list should look like when a given number is included as the last element.

-----Input-----  
The input consists of:  
• a: An array of integers.  
• b: An integer to be appended to the array.

-----Output-----  
The output is an array of integers which represents the original array with the element b added at the end. That is, the output array’s list representation equals a.toList concatenated with [b].

-----Note-----  
There are no special preconditions; the method is expected to work correctly for any array of integers and any integer 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 append_precond (a : Array Int) (b : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
def copy (a : Array Int) (i : Nat) (acc : Array Int) : Array Int :=
  if i < a.size then
    copy a (i + 1) (acc.push (a[i]!))
  else
    acc
-- !benchmark @end code_aux


def append (a : Array Int) (b : Int) (h_precond : append_precond (a) (b)) : Array Int :=
  -- !benchmark @start code
  let c_initial := copy a 0 (Array.empty)
  let c_full := c_initial.push b
  c_full
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def append_postcond (a : Array Int) (b : Int) (result: Array Int) (h_precond : append_precond (a) (b)) :=
  -- !benchmark @start postcond
  (List.range' 0 a.size |>.all (fun i => result[i]! = a[i]!)) ∧
  result[a.size]! = b ∧
  result.size = a.size + 1
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem append_spec_satisfied (a: Array Int) (b: Int) (h_precond : append_precond (a) (b)) :
    append_postcond (a) (b) (append (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that determines whether a given integer is even. In other words, the method should return true if the number is even and false if the number is odd.

-----Input-----
The input consists of:
n: An integer.

-----Output-----
The output is a Boolean value:
Returns true if the input number is even.
Returns false if the input number is odd.

-----Note-----
There are no preconditions; the method will always work for any integer input.
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 isEven_precond (n : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isEven (n : Int) (h_precond : isEven_precond (n)) : Bool :=
  -- !benchmark @start code
  n % 2 == 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def isEven_postcond (n : Int) (result: Bool) (h_precond : isEven_precond (n)) :=
  -- !benchmark @start postcond
  (result → n % 2 = 0) ∧ (¬ result → n % 2 ≠ 0)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isEven_spec_satisfied (n: Int) (h_precond : isEven_precond (n)) :
    isEven_postcond (n) (isEven (n) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold isEven isEven_postcond
  simp
  -- !benchmark @end proof


Tests:
input: n: 4
n: 7
n: 0
n: -2
n: -3
expected: True
False
True
True
False
unexpected: False
True
False
False
True

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 function that finds the single number in a non-empty list of integers, where every element appears exactly twice except for one element that appears only once. The function 
should return the integer that appears only once.

-----Input-----
The input is a non-empty list of integers:
- nums: A list in which each integer appears exactly twice except for one element that appears only once.

-----Output-----
The output is a single integer:
Returns the unique integer that appears exactly once in the list.


Difficulty: advanced

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def filterlist (x : Int) (nums : List Int) : List Int :=
  let rec aux (lst : List Int) : List Int :=
    match lst with
    | []      => []
    | y :: ys => if y = x then y :: aux ys else aux ys
  aux nums
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def FindSingleNumber_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  let numsCount := nums.map (fun x => nums.count x)
  numsCount.all (fun count => count = 1 ∨ count = 2) ∧ numsCount.count 1 = 1
  -- !benchmark @end precond


-- !benchmark @start code_aux
-- !benchmark @end code_aux


def FindSingleNumber (nums : List Int) (h_precond : FindSingleNumber_precond (nums)) : Int :=
  -- !benchmark @start code
  let rec findUnique (remaining : List Int) : Int :=
    match remaining with
    | [] =>
      0
    | x :: xs =>
      let filtered : List Int :=
        filterlist x nums
      let count : Nat :=
        filtered.length
      if count = 1 then
        x
      else
        findUnique xs
  findUnique nums
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def FindSingleNumber_postcond (nums : List Int) (result: Int) (h_precond : FindSingleNumber_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  (nums.length > 0)
  ∧
  ((filterlist result nums).length = 1)
  ∧
  (∀ (x : Int),
    x ∈ nums →
    (x = result) ∨ ((filterlist x nums).length = 2))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem FindSingleNumber_spec_satisfied (nums: List Int) (h_precond : FindSingleNumber_precond (nums)) :
    FindSingleNumber_postcond (nums) (FindSingleNumber (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: [2, 2, 3]
nums: [1, 2, 2]
nums: [3, 3, 4, 4, 1]
nums: [0, 1, 3, 1, 3, 88, 88, 100, 100]
nums: [-1, -1, 7, 9, 7]
expected: 3
1
1
0
9
unexpected: 2
1
4
2
-1
3
4
1
2
100
-1
7
10

Inputs rejected by the precondition:
nums: [2, 2]
nums: [2, 2, 3, 3]
-----Description-----  
This task requires writing a Lean 4 method that determines whether an array of integers contains only one distinct element. The method should return true if the array is empty or if every element in the array is the same, and false if there are at least two different elements.

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

-----Output-----  
The output is a Boolean value:  
Returns true if the array is empty or if all elements in the array are identical.  
Returns false if the array contains at least two distinct elements.

-----Note-----  
The input array is 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 hasOnlyOneDistinctElement_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def hasOnlyOneDistinctElement (a : Array Int) (h_precond : hasOnlyOneDistinctElement_precond (a)) : Bool :=
  -- !benchmark @start code
  if a.size = 0 then
    true
  else
    let firstElement := a[0]!
    let rec loop (i : Nat) : Bool :=
      if h : i < a.size then
        if a[i]! = firstElement then loop (i + 1) else false
      else
        true
    loop 1
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def hasOnlyOneDistinctElement_postcond (a : Array Int) (result: Bool) (h_precond : hasOnlyOneDistinctElement_precond (a)) :=
  -- !benchmark @start postcond
  let l := a.toList
  (result → List.Pairwise (· = ·) l) ∧
  (¬ result → (l.any (fun x => x ≠ l[0]!)))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem hasOnlyOneDistinctElement_spec_satisfied (a: Array Int) (h_precond : hasOnlyOneDistinctElement_precond (a)) :
    hasOnlyOneDistinctElement_postcond (a) (hasOnlyOneDistinctElement (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
a: #[]
-----Description-----
This task requires writing a Lean 4 function that returns the nth "ugly number". Ugly numbers are positive integers whose only prime factors are 2, 3, or 5.

The function should generate ugly numbers in ascending order and return the nth one. The first ugly number is 1.

-----Input-----
The input is a natural number:

n: The index (1-based) of the ugly number to return.

-----Output-----
The output is a natural number:
The nth smallest ugly number.


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 nthUglyNumber_precond (n : Nat) : Prop :=
  -- !benchmark @start precond
  n > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux
def nextUgly (seq : List Nat) (c2 c3 c5 : Nat) : (Nat × Nat × Nat × Nat) :=
  let i2 := seq[c2]! * 2
  let i3 := seq[c3]! * 3
  let i5 := seq[c5]! * 5
  let next := min i2 (min i3 i5)
  let c2' := if next = i2 then c2 + 1 else c2
  let c3' := if next = i3 then c3 + 1 else c3
  let c5' := if next = i5 then c5 + 1 else c5
  (next, c2', c3', c5')

-- !benchmark @end code_aux


def nthUglyNumber (n : Nat) (h_precond : nthUglyNumber_precond (n)) : Nat :=
  -- !benchmark @start code
  let rec loop (i : Nat) (seq : List Nat) (c2 c3 c5 : Nat) : List Nat :=
    match i with
    | 0 => seq
    | Nat.succ i' =>
      let (next, c2', c3', c5') := nextUgly seq c2 c3 c5
      loop i' (seq ++ [next]) c2' c3' c5'
  (loop (n - 1) [1] 0 0 0)[(n - 1)]!
  -- !benchmark @end code


-- !benchmark @start postcond_aux
def divideOut : Nat → Nat → Nat
  | n, p =>
    if h : p > 1 ∧ n > 0 ∧ n % p = 0 then
      have : n / p < n := by
        apply Nat.div_lt_self
        · exact h.2.1  -- n > 0
        · exact Nat.lt_of_succ_le (Nat.succ_le_of_lt h.1)  -- 1 < p, so 2 ≤ p
      divideOut (n / p) p
    else n
termination_by n p => n

def isUgly (x : Nat) : Bool :=
  if x = 0 then
    false
  else
    let n1 := divideOut x 2
    let n2 := divideOut n1 3
    let n3 := divideOut n2 5
    n3 = 1
-- !benchmark @end postcond_aux


@[reducible, simp]
def nthUglyNumber_postcond (n : Nat) (result: Nat) (h_precond : nthUglyNumber_precond (n)) : Prop :=
  -- !benchmark @start postcond
  isUgly result = true ∧
  ((List.range (result)).filter (fun i => isUgly i)).length = n - 1
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem nthUglyNumber_spec_satisfied (n: Nat) (h_precond : nthUglyNumber_precond (n)) :
    nthUglyNumber_postcond (n) (nthUglyNumber (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: n: 1
n: 10
n: 15
n: 5
n: 7
expected: 1
12
24
5
8
unexpected: 0
2
13
10
15
20
25
6
7
9
10

Inputs rejected by the precondition: