sunblaze-ucb/verina huggingface dataset:
-----Description----- 
This task requires writing a Lean 4 method that adds two non-empty linked lists representing non-negative integers.
The digits are stored in reverse order (i.e., the first element is the least significant digit).
Each node (list element) holds a single digit (ranging from 0 to 9). The function should add the two numbers and return the sum 
as a linked list, also in reverse order.

-----Input-----
The input consists of:
- l1: A list of natural numbers representing the digits of the first number in reverse order.
- l2: A list of natural numbers representing the digits of the second number in reverse order.

-----Output-----
The output is a list of natural numbers:
Returns a list of digits (in reverse order) representing the sum of the two input numbers.


Difficulty: advanced

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def listToNat : List Nat → Nat
| []       => 0
| d :: ds  => d + 10 * listToNat ds
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def addTwoNumbers_precond (l1 : List Nat) (l2 : List Nat) : Prop :=
  -- !benchmark @start precond
  l1.length > 0 ∧ l2.length > 0 ∧
  (∀ d ∈ l1, d < 10) ∧ (∀ d ∈ l2, d < 10) ∧
  (l1.getLast! ≠ 0 ∨ l1 = [0]) ∧
  (l2.getLast! ≠ 0 ∨ l2 = [0])
  -- !benchmark @end precond


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


def addTwoNumbers (l1 : List Nat) (l2 : List Nat) (h_precond : addTwoNumbers_precond (l1) (l2)) : List Nat :=
  -- !benchmark @start code
  let rec addAux (l1 l2 : List Nat) (carry : Nat) : List Nat :=
    match l1, l2 with
    | [], [] =>
      if carry = 0 then [] else [carry]
    | h1::t1, [] =>
      let sum := h1 + carry
      (sum % 10) :: addAux t1 [] (sum / 10)
    | [], h2::t2 =>
      let sum := h2 + carry
      (sum % 10) :: addAux [] t2 (sum / 10)
    | h1::t1, h2::t2 =>
      let sum := h1 + h2 + carry
      (sum % 10) :: addAux t1 t2 (sum / 10)
  addAux l1 l2 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def addTwoNumbers_postcond (l1 : List Nat) (l2 : List Nat) (result: List Nat) (h_precond : addTwoNumbers_precond (l1) (l2)) : Prop :=
  -- !benchmark @start postcond
  listToNat result = listToNat l1 + listToNat l2 ∧
  (∀ d ∈ result, d < 10) ∧
  -- No leading zeros unless the result is zero
  (result.getLast! ≠ 0 ∨ (l1 = [0] ∧ l2 = [0] ∧ result = [0]))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem addTwoNumbers_spec_satisfied (l1: List Nat) (l2: List Nat) (h_precond : addTwoNumbers_precond (l1) (l2)) :
    addTwoNumbers_postcond (l1) (l2) (addTwoNumbers (l1) (l2) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: l1: [2,4,3]
l2: [5,6,4]
l1: [0]
l2: [0]
l1: [9,9,9,9,9,9,9]
l2: [9,9,9,9]
l1: [1,2,3]
l2: [4,5]
expected: [7,0,8]
[0]
[8,9,9,9,0,0,0,1]
[5,7,3]
unexpected: [2,4,3]
[0]
[0,0]
[9,9,9,9,9,9,9,9]
[5,7]
[5,7,4]

Inputs rejected by the precondition:
l1: [0, 0]
l2: [0, 0]
-----Description-----  
This problem involves computing the triple of a given integer. The goal is to produce an output that is exactly three times the input value.

-----Input-----  
The input consists of:  
• x: An integer representing the value to be tripled.

-----Output-----  
The output is an integer that is three times the input value (i.e., 3 * x).

-----Note-----  
The implementation uses a local variable to first compute double the input and then adds the original input to get the final result. The accompanying theorem asserts that the function satisfies the specification of computing 3 * x.
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 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
  let y := x * 2
  y + x
  -- !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
  rw (occs := [2]) [←Int.mul_one x]
  rw [←Int.mul_add]
  simp +arith
  -- !benchmark @end proof


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

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that finds the maximum among three given integers. The method should return the largest value, ensuring that the result is greater than or equal to each of the input numbers and that it is one of the provided integers.

-----Input-----
The input consists of three integers:
a: The first integer.
b: The second integer.
c: The third integer.

-----Output-----
The output is an integer:
Returns the maximum of the three input numbers, assuring that the returned value is greater than or equal to a, b, and c, and that it matches one of these values.


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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def maxOfThree (a : Int) (b : Int) (c : Int) (h_precond : maxOfThree_precond (a) (b) (c)) : Int :=
  -- !benchmark @start code
  if a >= b && a >= c then a
  else if b >= a && b >= c then b
  else c
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def maxOfThree_postcond (a : Int) (b : Int) (c : Int) (result: Int) (h_precond : maxOfThree_precond (a) (b) (c)) : Prop :=
  -- !benchmark @start postcond
  (result >= a ∧ result >= b ∧ result >= c) ∧ (result = a ∨ result = b ∨ result = c)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem maxOfThree_spec_satisfied (a: Int) (b: Int) (c: Int) (h_precond : maxOfThree_precond (a) (b) (c)) :
    maxOfThree_postcond (a) (b) (c) (maxOfThree (a) (b) (c) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: a: 3
b: 2
c: 1
a: 5
b: 5
c: 5
a: 10
b: 20
c: 15
a: -1
b: -2
c: -3
a: 0
b: -10
c: -5
expected: 3
5
20
-1
0
unexpected: 2
1
-1
6
4
10
15
-2
-3
-5
-10

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that identifies the first repeated character in a given string. The method should return a tuple containing a Boolean value and a character. The Boolean value indicates whether any character in the string is repeated. If it is true, the accompanying character is the first character that appears more than once. If it is false, it indicates that there are no repeated characters in the string.

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

-----Output-----
The output is a tuple (Bool × Char):
- Returns true and the first repeated character in the string if any repeated character is found.
- Returns false and an arbitrary character if no repeated characters are present.

-----Note-----
There are no preconditions; the method is expected to work for any non-null string.
Difficulty: basic

Lean 4 solution:
-- !benchmark @start import type=solution
import Std.Data.HashSet
-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def findFirstRepeatedChar (s : String) (h_precond : findFirstRepeatedChar_precond (s)) : Option Char :=
  -- !benchmark @start code
  let cs := s.toList
  let rec loop (i : Nat) (seen : Std.HashSet Char) : Option Char :=
    if i < cs.length then
      let c := cs[i]!
      if seen.contains c then
        some c
      else
        loop (i + 1) (seen.insert c)
    else
      -- When no repeated char is found, return (false, arbitrary char)
      none
  loop 0 Std.HashSet.empty
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def findFirstRepeatedChar_postcond (s : String) (result: Option Char) (h_precond : findFirstRepeatedChar_precond (s)) :=
  -- !benchmark @start postcond
  let cs := s.toList
  match result with
  | some c =>
    let secondIdx := cs.zipIdx.findIdx (fun (x, i) => x = c && i ≠ cs.idxOf c)
    -- Exists repeated char
    cs.count c ≥ 2 ∧
    -- There is no other repeated char before the found one
    List.Pairwise (· ≠ ·) (cs.take secondIdx)
  | none =>
    -- There is no repeated char
    List.Pairwise (· ≠ ·) cs
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem findFirstRepeatedChar_spec_satisfied (s: String) (h_precond : findFirstRepeatedChar_precond (s)) :
    findFirstRepeatedChar_postcond (s) (findFirstRepeatedChar (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: s: abca
s: abcdef
s: aabbcc
s: abbc
s: Aa
expected: some ('a')
none
some ('a')
none
some ('b')
none
unexpected: some ('b')
some ('c')
none
some ('a')
some ('z')
some ('b')
some ('c')
none
some ('x')
some ('y')
some ('a')
some ('c')
none
some ('A')
some ('a')

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that determines whether a given natural number is prime. A number (with n ≥ 2) is considered prime if it is divisible only by 1 and itself. The method should return true when the input number is prime and false otherwise.

-----Input-----
The input consists of:
n: A natural number (Nat) such that n ≥ 2.

-----Output-----
The output is a Boolean value:
Returns true if the input number is prime (i.e., there is no integer k with 1 < k < n that divides n).
Returns false if the input number is not prime (i.e., there exists an integer k with 1 < k < n that divides n).

-----Note-----
The input is expected to satisfy the condition n ≥ 2.
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 isPrime_precond (n : Nat) : Prop :=
  -- !benchmark @start precond
  n ≥ 2
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isPrime (n : Nat) (h_precond : isPrime_precond (n)) : Bool :=
  -- !benchmark @start code
  let bound := n
  let rec check (i : Nat) (fuel : Nat) : Bool :=
    if fuel = 0 then true
    else if i * i > n then true
    else if n % i = 0 then false
    else check (i + 1) (fuel - 1)
  check 2 bound
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def isPrime_postcond (n : Nat) (result: Bool) (h_precond : isPrime_precond (n)) :=
  -- !benchmark @start postcond
  (result → (List.range' 2 (n - 2)).all (fun k => n % k ≠ 0)) ∧
  (¬ result → (List.range' 2 (n - 2)).any (fun k => n % k = 0))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isPrime_spec_satisfied (n: Nat) (h_precond : isPrime_precond (n)) :
    isPrime_postcond (n) (isPrime (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: n: 2
n: 3
n: 4
n: 5
n: 9
n: 11
n: 12
n: 13
expected: True
True
False
True
False
True
False
True
unexpected: False
False
True
False
True
False
True
False

Inputs rejected by the precondition:
n: 0
-----Description----- 
This task requires writing a Lean 4 method that solves the Two Sum problem. Given a list of integers and a target integer, the method must return a pair of indices such that the sum of the numbers at those indices equals the target. You may assume that each input has exactly one solution and that you may not use the same element twice. The answer should be returned with first index is smaller than the second.

-----Input-----
The input consists of:
- nums: A list of integers.
- target: An integer representing the target sum.

-----Output-----
The output is a pair (tuple) of integers representing the indices of the two numbers in the input list that add up to the target.


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 twoSum_precond (nums : List Int) (target : Int) : Prop :=
  -- !benchmark @start precond
  let pairwiseSum := List.range nums.length |>.flatMap (fun i =>
    nums.drop (i + 1) |>.map (fun y => nums[i]! + y))
  nums.length > 1 ∧ pairwiseSum.count target = 1
  -- !benchmark @end precond


-- !benchmark @start code_aux
def findComplement (nums : List Int) (target : Int) (i : Nat) (x : Int) : Option Nat :=
  let rec aux (nums : List Int) (j : Nat) : Option Nat :=
    match nums with
    | []      => none
    | y :: ys => if x + y = target then some (i + j + 1) else aux ys (j + 1)
  aux nums 0

def twoSumAux (nums : List Int) (target : Int) (i : Nat) : Prod Nat Nat :=
  match nums with
  | []      => panic! "No solution exists"
  | x :: xs =>
    match findComplement xs target i x with
    | some j => (i, j)
    | none   => twoSumAux xs target (i + 1)
-- !benchmark @end code_aux


def twoSum (nums : List Int) (target : Int) (h_precond : twoSum_precond (nums) (target)) : Prod Nat Nat :=
  -- !benchmark @start code
  twoSumAux nums target 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def twoSum_postcond (nums : List Int) (target : Int) (result: Prod Nat Nat) (h_precond : twoSum_precond (nums) (target)) : Prop :=
  -- !benchmark @start postcond
  let i := result.fst;
  let j := result.snd;
  (i < j) ∧
  (i < nums.length) ∧ (j < nums.length) ∧
  (nums[i]!) + (nums[j]!) = target
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem twoSum_spec_satisfied (nums: List Int) (target: Int) (h_precond : twoSum_precond (nums) (target)) :
    twoSum_postcond (nums) (target) (twoSum (nums) (target) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: [2, 7, 11, 15]
target: 9
nums: [3, 2, 4]
target: 6
nums: [3, 3]
target: 6
nums: [1, 2, 3, 4]
target: 7
nums: [0, 4, 3, 0]
target: 0
expected: (0, 1)
(1, 2)
(0, 1)
(2, 3)
(0, 3)
unexpected: (2, 3)
(0, 2)
(1, 0)
(0, 1)
(1, 2)

Inputs rejected by the precondition:
nums: [1, 2]
target: 0
-----Description-----
This task requires writing a Lean 4 method that counts the unique elements from a sorted array.

-----Input-----
The input is a single list of integers:
nums: An array of integers sorted in non-decreasing order.

-----Output-----
The output is a single integer:
Returns the number of unique elements (k).
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 removeDuplicates_precond (nums : List Int) : Prop :=
  -- !benchmark @start precond
  -- nums are sorted in non-decreasing order
  List.Pairwise (· ≤ ·) nums
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def removeDuplicates (nums : List Int) (h_precond : removeDuplicates_precond (nums)) : Nat :=
  -- !benchmark @start code
  match nums with
  | [] =>
    0
  | h :: t =>
    let init := h
    let initCount := 1
    let rec countUniques (prev : Int) (xs : List Int) (k : Nat) : Nat :=
      match xs with
      | [] =>
        k
      | head :: tail =>
        let isDuplicate := head = prev
        if isDuplicate then
          countUniques prev tail k
        else
          let newK := k + 1
          countUniques head tail newK
    countUniques init t initCount
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def removeDuplicates_postcond (nums : List Int) (result: Nat) (h_precond : removeDuplicates_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  result - nums.eraseDups.length = 0 ∧
  nums.eraseDups.length ≤ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem removeDuplicates_spec_satisfied (nums: List Int) (h_precond : removeDuplicates_precond (nums)) :
    removeDuplicates_postcond (nums) (removeDuplicates (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: nums: [1, 1, 2]
nums: [0, 0, 1, 1, 1, 2, 2, 3, 3, 4]
nums: [-1, -1, 0, 1, 2, 2, 3]
nums: [1, 2, 3, 4, 5]
nums: [1, 1, 1, 1]
nums: [1]
nums: [-100, -100, -100]
nums: [-100, -99, -99, -50, 0, 0, 100, 100]
nums: [-1, 0, 0, 0, 1, 2, 2, 3, 4, 4, 5]
nums: [100, 100, 100, 101, 102, 102, 103, 104, 105, 105]
expected: 2
5
5
5
1
0
1
1
5
7
6
unexpected: 1
3
4
10
3
4
2
4
1
0
2
2
3
6
7
6
10
5
7

Inputs rejected by the precondition:
nums: [3, 2, 1]
-----Description-----  
This task requires writing a Lean 4 method that determines whether one list is a sublist of another. In other words, the method should check if the first list appears as a contiguous sequence within the second list and return true if it does, and false otherwise.

-----Input-----  
The input consists of two lists of integers:  
sub: A list of integers representing the potential sublist.  
main: A list of integers in which to search for the sublist.

-----Output-----  
The output is a Boolean value:  
Returns true if the first list appears as a contiguous sequence within the second list.  
Returns false if the first list does not appear as a contiguous sequence in the second list.

-----Note-----  
There are no preconditions for this method; the sequences are always 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 isSublist_precond (sub : List Int) (main : List Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isSublist (sub : List Int) (main : List Int) (h_precond : isSublist_precond (sub) (main)) : Bool :=
  -- !benchmark @start code
  let subLen := sub.length
  let mainLen := main.length
  if subLen > mainLen then
    false
  else
    let rec check (i : Nat) : Bool :=
      if i + subLen > mainLen then
        false
      else if sub = (main.drop i).take subLen then
        true
      else if i + 1 ≤ mainLen then
        check (i + 1)
      else
        false
    termination_by mainLen - i
    check 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def isSublist_postcond (sub : List Int) (main : List Int) (result: Bool) (h_precond : isSublist_precond (sub) (main)) :=
  -- !benchmark @start postcond
  (∃ i, i + sub.length ≤ main.length ∧ sub = (main.drop i).take sub.length) ↔ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isSublist_spec_satisfied (sub: List Int) (main: List Int) (h_precond : isSublist_precond (sub) (main)) :
    isSublist_postcond (sub) (main) (isSublist (sub) (main) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: sub: [1, 2]
main: [3, 1, 2, 4]
sub: [2, 3]
main: [3, 1, 2, 4]
sub: [3, 1]
main: [3, 1, 2, 4]
sub: [4]
main: [3, 1, 2, 4]
sub: [5]
main: [3, 1, 2, 4]
main: [3, 1, 2, 4]
sub: [1, 2]
expected: True
False
True
True
False
True
False
True
unexpected: False
True
False
False
True
False
True
False

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that converts a given string to uppercase. The method should replace every lowercase letter in the input string with its corresponding uppercase character while leaving all other characters unchanged. The output string must have the same length as the input string.

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

-----Output-----
The output is a string:
Returns a new string in which every lowercase letter from the input string is converted to uppercase, and all other characters are exactly the same as in the input string, ensuring the output string has the same length as the input.

-----Note-----
There are no preconditions since the method assumes that the input string is always valid (i.e., non-null).
Difficulty: basic

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def isLowerCase (c : Char) : Bool :=
  'a' ≤ c ∧ c ≤ 'z'

def shiftMinus32 (c : Char) : Char :=
  Char.ofNat ((c.toNat - 32) % 128)
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


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


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


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


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem toUppercase_spec_satisfied (s: String) (h_precond : toUppercase_precond (s)) :
    toUppercase_postcond (s) (toUppercase (s) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold toUppercase toUppercase_postcond
  simp_all
  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!
s: abc
s: ABC
s: 123!?@
expected: HELLO, WORLD!
ABC
ABC
123!?@
unexpected: hello, world!
HeLLo, WORld!
AbC
abc
abc
aBC
Abc
123!@?
321!?@
 
a

Inputs rejected by the precondition: