sunblaze-ucb/verina huggingface dataset:
-----Description-----  
This problem asks you to design a solution that transforms a list with possible duplicate entries into a new list where each element appears only once, maintaining the order of its first occurrence.

-----Input-----  
The input consists of:  
• s: A list of integers (or any type supporting decidable equality) that may contain duplicate elements.

-----Output-----  
The output is a list of integers (or the original type) in which every duplicate element is removed. The order of elements is preserved based on their first appearance in the input list, ensuring that the set of elements in the output is identical to the set in the input.

-----Note-----  
No additional preconditions are required. The method should correctly handle any list, including an empty list.
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 SetToSeq_precond (s : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def SetToSeq (s : List Int) (h_precond : SetToSeq_precond (s)) : List Int :=
  -- !benchmark @start code
  s.foldl (fun acc x => if acc.contains x then acc else acc ++ [x]) []
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def SetToSeq_postcond (s : List Int) (result: List Int) (h_precond : SetToSeq_precond (s)) :=
  -- !benchmark @start postcond
  -- Contains exactly the elements of the set
  result.all (fun a => a ∈ s) ∧ s.all (fun a => a ∈ result) ∧
  -- All elements are unique in the result
  result.all (fun a => result.count a = 1) ∧
  -- The order of elements in the result is preserved
  List.Pairwise (fun a b => (result.idxOf a < result.idxOf b) → (s.idxOf a < s.idxOf b)) result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem SetToSeq_spec_satisfied (s: List Int) (h_precond : SetToSeq_precond (s)) :
    SetToSeq_postcond (s) (SetToSeq (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: [1, 2, 2, 3, 1]
s: [5, 5, 5, 5]
s: [11, 22, 33]
s: [3, 1, 4, 1, 5, 9, 2, 6, 5]
expected: [1, 2, 3]
[5]
[11, 22, 33]
[3, 1, 4, 5, 9, 2, 6]
unexpected: [1, 3, 2]
[1, 2, 2, 3]
[2, 1, 3]
[5, 5]
[6]
[1]
[2]
[0]
[33, 22, 11]
[11, 11, 22, 33]
[11, 33]
[3, 1, 4, 1, 5, 9, 2, 6, 5]
[1, 3, 4, 5, 9, 2, 6]
[3, 1, 4, 5, 9, 6]

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that finds the second-smallest number in an array of integers. The method should determine and return the number that is larger than the smallest element in the array. It is crucial that the input array remains unchanged after the computation.

-----Input-----
The input consists of:
s: An array of integers containing at least two elements.

-----Output-----
The output is an integer:
Returns the second-smallest number in the input array.

-----Note-----
- The input array must contain at least two elements.
- The array must contain at least two distinct values (enforced by precondition).
- The original array remains unmodified.
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 secondSmallest_precond (s : Array Int) : Prop :=
  -- !benchmark @start precond
  s.size > 1 ∧ ∃ i j, i < s.size ∧ j < s.size ∧ s[i]! ≠ s[j]!  -- at least two distinct values
  -- !benchmark @end precond


-- !benchmark @start code_aux
def minListHelper : List Int → Int
| [] => panic! "minListHelper: empty list"
| [_] => panic! "minListHelper: singleton list"
| a :: b :: [] => if a ≤ b then a else b
| a :: b :: c :: xs =>
    let m := minListHelper (b :: c :: xs)
    if a ≤ m then a else m

def minList (l : List Int) : Int :=
  minListHelper l

def secondSmallestAux (s : Array Int) (i minIdx secondIdx : Nat) : Int :=
  if i ≥ s.size then
    s[secondIdx]!
  else
    let x    := s[i]!
    let m    := s[minIdx]!
    let smin := s[secondIdx]!
    if x < m then
      secondSmallestAux s (i + 1) i minIdx
    else if x < smin then
      secondSmallestAux s (i + 1) minIdx i
    else
      secondSmallestAux s (i + 1) minIdx secondIdx
termination_by s.size - i
-- !benchmark @end code_aux


def secondSmallest (s : Array Int) (h_precond : secondSmallest_precond (s)) : Int :=
  -- !benchmark @start code
  let (minIdx, secondIdx) :=
    if s[1]! < s[0]! then (1, 0) else (0, 1)
  secondSmallestAux s 2 minIdx secondIdx
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def secondSmallest_postcond (s : Array Int) (result: Int) (h_precond : secondSmallest_precond (s)) :=
  -- !benchmark @start postcond
  (∃ i, i < s.size ∧ s[i]! = result) ∧
  (∃ j, j < s.size ∧ s[j]! < result ∧
    ∀ k, k < s.size → s[k]! ≠ s[j]! → s[k]! ≥ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem secondSmallest_spec_satisfied (s: Array Int) (h_precond : secondSmallest_precond (s)) :
    secondSmallest_postcond (s) (secondSmallest (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: #[5, 3, 1, 4, 2]
s: #[7, 2, 5, 3]
s: #[10, 20]
s: #[20, 10]
s: #[3, 1, 2]
expected: 2
3
20
20
2
unexpected: 1
3
4
2
5
7
10
30
25
10
30
15
1
3
4

Inputs rejected by the precondition:
s: #[1]
s: #[5, 5]
s: #[3, 3, 3]
s: #[-1, -1, -1, -1]
-----Description-----  
This task involves updating an array of integers such that the element at a specified index is set to 60 while all other elements remain unchanged.

-----Input-----  
The input consists of:  
• a: An array of integers.  
• j: A natural number representing the index (0-indexed) to update. It is assumed that j is a valid index (j < a.size).

-----Output-----  
The output is an array of integers where:  
• The element at index j is set to 60.  
• All other elements remain the same as in the input array.

-----Note-----  
It is assumed that j is a valid index (0 ≤ j < a.size).
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 TestArrayElements_precond (a : Array Int) (j : Nat) : Prop :=
  -- !benchmark @start precond
  j < a.size
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def TestArrayElements (a : Array Int) (j : Nat) (h_precond : TestArrayElements_precond (a) (j)) : Array Int :=
  -- !benchmark @start code
  a.set! j 60
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def TestArrayElements_postcond (a : Array Int) (j : Nat) (result: Array Int) (h_precond : TestArrayElements_precond (a) (j)) :=
  -- !benchmark @start postcond
  (result[j]! = 60) ∧ (∀ k, k < a.size → k ≠ j → result[k]! = a[k]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem TestArrayElements_spec_satisfied (a: Array Int) (j: Nat) (h_precond : TestArrayElements_precond (a) (j)) :
    TestArrayElements_postcond (a) (j) (TestArrayElements (a) (j) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold TestArrayElements_postcond TestArrayElements
  unfold TestArrayElements_precond at h_precond
  apply And.intro
  . rw [Array.getElem!_eq_getD, Array.getD]
    simp
    exact h_precond
  . intro k
    intro hk hxk
    simp [Array.getElem!_eq_getD, Array.getD]
    split
    . rw [Array.getElem_setIfInBounds]
      split
      . rename_i h h₁
        rw [eq_comm] at h₁
        contradiction
      . rfl
    . rw [Array.getElem_setIfInBounds]
      split
      . rename_i h h₁
        rw [eq_comm] at h₁
        contradiction
      . rfl
  -- !benchmark @end proof


Tests:
input: a: #[1, 2, 3, 4, 5]
j: 2
a: #[60, 30, 20]
j: 1
a: #[10, 20, 30]
j: 0
a: #[5, 10, 15]
j: 2
a: #[0]
j: 0
expected: #[1, 2, 60, 4, 5]
#[60, 60, 20]
#[60, 20, 30]
#[5, 10, 60]
#[60]
unexpected: #[1, 2, 3, 4, 5]
#[1, 60, 3, 4, 5]
#[60, 30, 20]
#[60, 30, 60]
#[10, 20, 30]
#[10, 60, 30]
#[5, 10, 15]
#[5, 60, 15]
#[0]
#[70]

Inputs rejected by the precondition:
a: #[1, 2, 3, 4]
j: 5
-----Description-----  
Given two integers, the task is to compute two output values: one being the sum of the integers and the other being their difference.

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

-----Output-----  
The output is a tuple of two integers:  
• The first element is x + y.  
• The second element is x - y.

-----Note-----  
It is assumed that x and y are valid integers. There are no additional constraints on the 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 MultipleReturns_precond (x : Int) (y : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def MultipleReturns (x : Int) (y : Int) (h_precond : MultipleReturns_precond (x) (y)) : (Int × Int) :=
  -- !benchmark @start code
  let more := x + y
  let less := x - y
  (more, less)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def MultipleReturns_postcond (x : Int) (y : Int) (result: (Int × Int)) (h_precond : MultipleReturns_precond (x) (y)) :=
  -- !benchmark @start postcond
  result.1 = x + y ∧ result.2 + y = x
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem MultipleReturns_spec_satisfied (x: Int) (y: Int) (h_precond : MultipleReturns_precond (x) (y)) :
    MultipleReturns_postcond (x) (y) (MultipleReturns (x) (y) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold MultipleReturns_postcond MultipleReturns
  simp
  -- !benchmark @end proof


Tests:
input: x: 3
y: 2
x: -2
y: 3
x: 0
y: 0
x: 10
y: 5
x: -5
y: -10
expected: (5, 1)
(1, -5)
(0, 0)
(15, 5)
(-15, 5)
unexpected: (6, 2)
(5, 2)
(4, 1)
(-1, 5)
(2, -3)
(1, 5)
(1, 0)
(0, 1)
(-1, 0)
(14, 5)
(15, 6)
(10, 5)
(-15, -5)
(-5, 15)
(-10, 0)

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that reverses a given string. The method should return a new string which consists of the characters of the input string in reverse order.

-----Input-----
The input consists of:
s: A string (which may be empty).

-----Output-----
The output is a string:
Returns a string where the characters are in reverse order from the original input.


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 reverseString_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def reverseString (s : String) (h_precond : reverseString_precond (s)) : String :=
  -- !benchmark @start code
  let rec reverseAux (chars : List Char) (acc : List Char) : List Char :=
    match chars with
    | [] => acc
    | h::t => reverseAux t (h::acc)
  String.mk (reverseAux (s.toList) [])
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def reverseString_postcond (s : String) (result: String) (h_precond : reverseString_precond (s)) : Prop :=
  -- !benchmark @start postcond
  result.length = s.length ∧ result.toList = s.toList.reverse
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem reverseString_spec_satisfied (s: String) (h_precond : reverseString_precond (s)) :
    reverseString_postcond (s) (reverseString (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: s: hello
s: a
s: racecar
s: Lean
expected: olleh
a
racecar
naeL
unexpected: hello
helo
hell
aa
 
a
rceacar
raeccar
Lean
aenL

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that performs run-length encoding on a given string. The method should scan the string from left to right and group consecutive identical characters into pairs. Each pair consists of the character itself and the number of times it appears consecutively. For example, "aaabbc" becomes [(’a’, 3), (’b’, 2), (’c’, 1)].

The resulting encoded list must satisfy the following properties:
1. No pair has a zero or negative run-length.
2. Consecutive pairs in the encoding list must not have the same character.
3. Decoding the output should return the original string.

-----Input-----
The input is a single string, `s`.

-----Output-----
The output is a list of pairs `(Char, Nat)`, which represents the run-length-encoded form of the input string.


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 runLengthEncode_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def runLengthEncode (s : String) (h_precond : runLengthEncode_precond (s)) : List (Char × Nat) :=
  -- !benchmark @start code
  let chars := s.data

  let rec encodeAux (acc : List (Char × Nat)) (rest : List Char) : List (Char × Nat) :=
    match rest with
    | [] => acc.reverse
    | h :: t =>
      match acc with
      | (ch, count) :: accTail =>
        if ch = h then
          encodeAux ((ch, count + 1) :: accTail) t
        else
          encodeAux ((h, 1) :: (ch, count) :: accTail) t
      | [] =>
        encodeAux ([(h, 1)]) t

  let encoded := encodeAux [] chars
  encoded
  -- !benchmark @end code


-- !benchmark @start postcond_aux
def decodeRLE (lst : List (Char × Nat)) : String :=
  match lst with
  | [] => ""
  | (ch, cnt) :: tail =>
    let repeated := String.mk (List.replicate cnt ch)
    repeated ++ decodeRLE tail
-- !benchmark @end postcond_aux


@[reducible, simp]
def runLengthEncode_postcond (s : String) (result: List (Char × Nat)) (h_precond : runLengthEncode_precond (s)) : Prop :=
  -- !benchmark @start postcond
  (∀ pair ∈ result, pair.snd > 0) ∧
  (∀ i : Nat, i < result.length - 1 → (result[i]!).fst ≠ (result[i+1]!).fst) ∧
  decodeRLE result = s
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem runLengthEncode_spec_satisfied (s: String) (h_precond : runLengthEncode_precond (s)) :
    runLengthEncode_postcond (s) (runLengthEncode (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: s: aaa
s: abbbcccaa
s: xyz
s: aabbaa
expected: [('a', 3)]
[('a', 1), ('b', 3), ('c', 3), ('a', 2)]
[('x', 1), ('y', 1), ('z', 1)]
[('a', 2), ('b', 2), ('a', 2)]
unexpected: [('x', 1)]
[('a', 2), ('b', 3)]
[('a', 2), ('b', 3), ('c', 3), ('a', 2)]
[('x', 3)]
[('z', 1)]
[('a', 2), ('b', 2), ('a', 3)]

Inputs rejected by the precondition:
-----Description-----

This task requires writing a Lean 4 method that takes a list of natural numbers and partitions it into two separate lists: one containing all the even numbers and the other containing all the odd numbers. The order of elements in each sublist should match their appearance in the original list. Assume there are no duplicates in the input.

-----Input-----

The input consists of a single list with no duplicate natural numbers:
- nums: A list of natural numbers (Nat)

-----Output-----

The output is a tuple of two lists:
- The first list contains all even numbers from the input list, in order.
- The second list contains all odd numbers from the input list, in order.


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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def partitionEvensOdds (nums : List Nat) (h_precond : partitionEvensOdds_precond (nums)) : (List Nat × List Nat) :=
  -- !benchmark @start code
  let rec helper (nums : List Nat) : (List Nat × List Nat) :=
    match nums with
    | [] => ([], [])
    | x :: xs =>
      let (evens, odds) := helper xs
      if x % 2 == 0 then (x :: evens, odds)
      else (evens, x :: odds)
  helper nums
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def partitionEvensOdds_postcond (nums : List Nat) (result: (List Nat × List Nat)) (h_precond : partitionEvensOdds_precond (nums)): Prop :=
  -- !benchmark @start postcond
  let evens := result.fst
  let odds := result.snd
  -- All elements from nums are in evens ++ odds, no extras
  evens ++ odds = nums.filter (fun n => n % 2 == 0) ++ nums.filter (fun n => n % 2 == 1) ∧
  evens.all (fun n => n % 2 == 0) ∧
  odds.all (fun n => n % 2 == 1)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem partitionEvensOdds_spec_satisfied (nums: List Nat) (h_precond : partitionEvensOdds_precond (nums)) :
    partitionEvensOdds_postcond (nums) (partitionEvensOdds (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: [1, 2, 3, 4, 5, 6]
nums: [0, 7, 8, 9, 10]
nums: [2, 4, 6, 8]
nums: [1, 3, 5, 7]
expected: ([2, 4, 6], [1, 3, 5])
([0, 8, 10], [7, 9])
([], [])
([2, 4, 6, 8], [])
([], [1, 3, 5, 7])
unexpected: ([1, 3, 5], [2, 4, 6])
([8, 0, 10], [9, 7])
([0], [1])
([], [2, 4, 6, 8])
([1, 3, 5, 7], [])

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 function that finds the length of the longest strictly increasing subsequence in a list of integers. A subsequence is any sequence that can be derived from the list by deleting zero or more elements without changing the order of the remaining elements. The function must return the length of the longest possible such sequence.

-----Input-----
The input consists of a single value:
xs: A list of integers of type `List Int`.

-----Output-----
The output is a natural number:
Returns the length of the longest strictly increasing subsequence found in the 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 longestIncreasingSubseqLength_precond (xs : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
-- Generate all subsequences
def subsequences {α : Type} : List α → List (List α)
  | [] => [[]]
  | x :: xs =>
    let subs := subsequences xs
    subs ++ subs.map (fun s => x :: s)

-- Check if a list is strictly increasing
def isStrictlyIncreasing : List Int → Bool
  | [] => true
  | [_] => true
  | x :: y :: rest => if x < y then isStrictlyIncreasing (y :: rest) else false
-- !benchmark @end code_aux


def longestIncreasingSubseqLength (xs : List Int) (h_precond : longestIncreasingSubseqLength_precond (xs)) : Nat :=
  -- !benchmark @start code
  let subs := subsequences xs
  let increasing := subs.filter isStrictlyIncreasing
  increasing.foldl (fun acc s => max acc s.length) 0
  -- !benchmark @end code


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


@[reducible]
def longestIncreasingSubseqLength_postcond (xs : List Int) (result: Nat) (h_precond : longestIncreasingSubseqLength_precond (xs)) : Prop :=
  -- !benchmark @start postcond
  let allSubseq := (xs.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 longestIncreasingSubseqLength_spec_satisfied (xs: List Int) (h_precond : longestIncreasingSubseqLength_precond (xs)) :
    longestIncreasingSubseqLength_postcond (xs) (longestIncreasingSubseqLength (xs) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
-----Description-----  
This task is about calculating the absolute value of an integer. The goal is to determine the non-negative value of a given integer: if the integer is non-negative, it remains unchanged; if it is negative, its positive counterpart is returned.

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

-----Output-----  
The output is an integer that represents the absolute value of the input. Specifically:  
• If x is non-negative, the output is x.  
• If x is negative, the output is the negation of x (that is, a value y such that x + y = 0).

-----Note-----  
This function should correctly handle zero, positive, and negative integers.
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 Abs_precond (x : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def Abs (x : Int) (h_precond : Abs_precond (x)) : Int :=
  -- !benchmark @start code
  if x < 0 then -x else x
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def Abs_postcond (x : Int) (result: Int) (h_precond : Abs_precond (x)) :=
  -- !benchmark @start postcond
  (x ≥ 0 → x = result) ∧ (x < 0 → x + result = 0)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem Abs_spec_satisfied (x: Int) (h_precond : Abs_precond (x)) :
    Abs_postcond (x) (Abs (x) h_precond) h_precond := by
  -- !benchmark @start proof
    simp [Abs_postcond, Abs]
    apply And.intro
    . intro h
      split
      case isTrue ht =>
        have h': ¬0 ≤ x := not_le.mpr ht
        contradiction
      case isFalse =>
        rfl
    . intro h
      split
      case isTrue =>
        simp
      case isFalse =>
        contradiction
  -- !benchmark @end proof


Tests:
input: x: 5
x: 0
x: -5
x: 10
x: -10
expected: 5
0
5
10
10
unexpected: -5
0
10
-1
1
-5
-5
-10
0
-10
0
5
-10
-1
0

Inputs rejected by the precondition: