sunblaze-ucb/verina huggingface dataset:
-----Description-----  
This task is about processing an array of integers by producing a new array that excludes the first element. The objective is to define a clear behavior: if the array contains at least one element, return a modified array starting from the second element.

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

-----Output-----  
The output is an array of integers that:  
• Has a length equal to the original array's length minus one.  
• Contains the same elements as the input array except for the first element.  
• Satisfies the condition that for every index i in the output array, the element at position i is equal to the element at position i+1 in the input array.

-----Note-----  
It is assumed that the input array is non-empty.
Difficulty: basic

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

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible, simp]
def remove_front_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  a.size > 0
  -- !benchmark @end precond


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


def remove_front (a : Array Int) (h_precond : remove_front_precond (a)) : Array Int :=
  -- !benchmark @start code
  if a.size > 0 then
    let c := copyFrom a 1 (Array.mkEmpty (a.size - 1))
    c
  else
    panic "Precondition violation: array is empty"
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def remove_front_postcond (a : Array Int) (result: Array Int) (h_precond : remove_front_precond (a)) :=
  -- !benchmark @start postcond
  a.size > 0 ∧ result.size = a.size - 1 ∧ (∀ i : Nat, i < result.size → result[i]! = a[i + 1]!)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem remove_front_spec_satisfied (a: Array Int) (h_precond : remove_front_precond (a)) :
    remove_front_postcond (a) (remove_front (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: a: #[1, 2, 3, 4, 5]
a: #[10, 20, 30]
a: #[0, -1, -2, -3]
a: #[7]
a: #[100, 0, 50]
expected: #[2, 3, 4, 5]
#[20, 30]
#[-1, -2, -3]
#[]
#[0, 50]
unexpected: #[1, 2, 3, 4, 5]
#[3, 4, 5]
#[2, 3, 4]
#[10, 20, 30]
#[10, 30]
#[10, 20]
#[0, -1, -2, -3]
#[-1, -3]
#[-2, -3]
#[7]
#[0]
#[7, 7]
#[100, 0, 50]
#[50]
#[0]

Inputs rejected by the precondition:
a: #[]
-----Description----- 
This task requires writing a Lean 4 method that determines whether two given integers have opposite signs. In other words, the method should return true if one integer is positive and the other is negative. Note that zero is considered neither positive nor negative; therefore, if either integer is zero, the method should return false.

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

-----Output-----
The output is a Boolean value:
Returns true if one of the integers is positive and the other is negative (i.e., they have opposite signs).
Returns false if both integers are either non-negative or non-positive, or if one (or both) is zero.
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 hasOppositeSign_precond (a : Int) (b : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def hasOppositeSign (a : Int) (b : Int) (h_precond : hasOppositeSign_precond (a) (b)) : Bool :=
  -- !benchmark @start code
  a * b < 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def hasOppositeSign_postcond (a : Int) (b : Int) (result: Bool) (h_precond : hasOppositeSign_precond (a) (b)) :=
  -- !benchmark @start postcond
  (((a < 0 ∧ b > 0) ∨ (a > 0 ∧ b < 0)) → result) ∧
  (¬((a < 0 ∧ b > 0) ∨ (a > 0 ∧ b < 0)) → ¬result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem hasOppositeSign_spec_satisfied (a: Int) (b: Int) (h_precond : hasOppositeSign_precond (a) (b)) :
    hasOppositeSign_postcond (a) (b) (hasOppositeSign (a) (b) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold hasOppositeSign hasOppositeSign_postcond
  constructor

  · intro h
    cases h with
    | inl h1 =>
      simp
      have ⟨ha, hb⟩ := h1
      exact Int.mul_neg_of_neg_of_pos ha hb
    | inr h2 =>
      simp
      have ⟨ha, hb⟩ := h2
      rw [Int.mul_comm]
      exact Int.mul_neg_of_neg_of_pos hb ha

  · rw [Bool.decide_iff, mul_neg_iff]
    simp_all
  -- !benchmark @end proof


Tests:
input: a: -5
b: 10
a: 5
b: -10
a: 5
b: 10
a: -5
b: -10
a: 0
b: 10
a: 10
b: 0
a: 0
b: -10
a: -10
b: 0
a: 0
b: 0
a: -1
b: 1
a: 1
b: -1
expected: True
True
False
False
False
False
False
False
False
True
True
unexpected: False
False
True
True
True
True
True
True
True
False
False

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that determines whether a natural number is a power of four. The method should return a boolean value that indicates whether the given natural number is a power of four. An integer n is a power of four, if there exists an natural number x such that n = 4^x. 

-----Input-----
The input consists of one natural number:
n: A natural number.

-----Output-----
The output is a boolean value:
Return a boolean value that indicates whether the given natural number is a power of four. Return "true" if it is a power of four. Otherwise, return "false". 


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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def ifPowerOfFour (n : Nat) (h_precond : ifPowerOfFour_precond (n)) : Bool :=
  -- !benchmark @start code
  let rec helper (n : Nat) : Bool :=
    match n with
    | 0 =>
      false
    | Nat.succ m =>
      match m with
      | 0 =>
        true
      | Nat.succ l =>
        if (l+2)%4=0 then
          helper ((l+2)/4)
        else
          false
  helper n
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def ifPowerOfFour_postcond (n : Nat) (result: Bool) (h_precond : ifPowerOfFour_precond (n)) : Prop :=
  -- !benchmark @start postcond
  result ↔ (∃ m:Nat, n=4^m)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem ifPowerOfFour_spec_satisfied (n: Nat) (h_precond : ifPowerOfFour_precond (n)) :
    ifPowerOfFour_postcond (n) (ifPowerOfFour (n) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: n: 0
n: 1
n: 2
n: 3
n: 4
n: 8
n: 16
n: 64
n: 95
n: 100
n: 256
n: 520
n: 1024
expected: False
True
False
False
True
False
True
True
False
False
True
False
True
unexpected: True
False
True
True
False
True
False
False
True
True
False
True
False

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that finds the length of the longest increasing sequence in a given array. The method should return the length of the longest increasing subsequence, in which every element is strictly less than the latter element.

-----Input-----
The input consists of an arrat:
a: The input array.

-----Output-----
The output is an integer:
Returns the length of the longest increasing subsequence, assuring that it is a subsequence of the input sequence and that every element in it is strictly less than the latter one.


Difficulty: advanced

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


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


def LongestIncreasingSubsequence (a : Array Int) (h_precond : LongestIncreasingSubsequence_precond (a)) : Int :=
  -- !benchmark @start code
  let n := a.size
  let dp := Id.run do
    let mut dp := Array.mkArray n 1
    for i in [1:n] do
      for j in [0:i] do
        if a[j]! < a[i]! then
          let newVal := intMax (dp[i]!) (dp[j]! + 1)
          dp := dp.set! i newVal
    return dp
  match dp with
  | #[] => 0
  | _   => dp.foldl intMax 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def LongestIncreasingSubsequence_postcond (a : Array Int) (result: Int) (h_precond : LongestIncreasingSubsequence_precond (a)) : Prop :=
  -- !benchmark @start postcond
  let allSubseq := (a.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 LongestIncreasingSubsequence_spec_satisfied (a: Array Int) (h_precond : LongestIncreasingSubsequence_precond (a)) :
    LongestIncreasingSubsequence_postcond (a) (LongestIncreasingSubsequence (a) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: a: #[5, 2, 8, 6, 3, 6, 9, 7]
a: #[3, 1, 2, 1, 0]
a: #[2, 3, -2, -1, 7, 19, 3, 6, -4, 6, -7, 0, 9, 12, 10]
a: #[5, -5, -3, 2, 4, 1, 0, -1, 3, 2, 0]
a: #[1, 7, 23, 14, -4, 21, 8, 2, -1, 9, 12, 2]
a: #[]
expected: 4
2
6
4
5
0
unexpected: 2
3
1
3
5
3
10
2
5
2
4
1
2

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that determines whether a list of integers follows a peak-valley pattern.

A list follows this pattern if:
A. It strictly increases at first,
B. Then strictly decreases,
C. Both parts are non-empty.

Examples:
- [1, 3, 5, 4, 2] -> true
- [1, 2, 3] -> false
- [5, 4, 3] -> false
- [1, 2, 2, 1] -> false

-----Input-----
The input consists of a list of integers:

-----Output-----
The output is an integer:
Returns true if the list has a peak-valley structure, false otherwise.


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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isPeakValley (lst : List Int) (h_precond : isPeakValley_precond (lst)) : Bool :=
  -- !benchmark @start code
  let rec aux (l : List Int) (increasing : Bool) (startedDecreasing : Bool) : Bool :=
    match l with
    | x :: y :: rest =>
      if x < y then
        if startedDecreasing then false
        else aux (y :: rest) true startedDecreasing
      else if x > y then
        if increasing then aux (y :: rest) increasing true
        else false
      else false
    | _ => increasing && startedDecreasing
  aux lst false false
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def isPeakValley_postcond (lst : List Int) (result: Bool) (h_precond : isPeakValley_precond (lst)) : Prop :=
  -- !benchmark @start postcond
  let len := lst.length
  let validPeaks :=
    List.range len |>.filter (fun p =>
      1 ≤ p ∧ p < len - 1 ∧

      -- check strictly increasing before peak
      (List.range p).all (fun i =>
        lst[i]! < lst[i + 1]!
      ) ∧

      -- check strictly decreasing after peak
      (List.range (len - 1 - p)).all (fun i =>
        lst[p + i]! > lst[p + i + 1]!
      )
    )
  (validPeaks != [] → result) ∧
  (validPeaks.length = 0 → ¬ result)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isPeakValley_spec_satisfied (lst: List Int) (h_precond : isPeakValley_precond (lst)) :
    isPeakValley_postcond (lst) (isPeakValley (lst) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: lst: [1, 3, 5, 2, 1]
lst: [1, 2, 3, 4, 5]
lst: [1]
lst: [1, 1, 1, 1, 1]
lst: [1, 10, 100, 1]
expected: True
False
False
False
False
True
unexpected: False
True
True
True
True
False

Inputs rejected by the precondition:
-----Description----- 
This task requires writing a Lean 4 method that checks whether an array of integers is sorted in non-decreasing order. The method should return true if every element is less than or equal to the element that follows it, and false otherwise.

-----Input-----
The input consists of:
a: An array of integers. The array can be empty or have any length.

-----Output-----
The output is a Boolean value:
Returns true if the array is sorted in non-decreasing order.
Returns false if the array is not sorted in non-decreasing order.

-----Note-----
A true result guarantees that for every valid pair of indices i and j (with i < j), the element at position i is less than or equal to the element at position j. A false result indicates that there exists at least one adjacent pair of elements where the first element is greater than the second.
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 isSorted_precond (a : Array Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def isSorted (a : Array Int) (h_precond : isSorted_precond (a)) : Bool :=
  -- !benchmark @start code
  if a.size ≤ 1 then
    true
  else
    a.mapIdx (fun i x =>
      if h : i + 1 < a.size then
        decide (x ≤ a[i + 1])
      else
        true) |>.all id
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def isSorted_postcond (a : Array Int) (result: Bool) (h_precond : isSorted_precond (a)) :=
  -- !benchmark @start postcond
  (∀ i, (hi : i < a.size - 1) → a[i] ≤ a[i + 1]) ↔ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isSorted_spec_satisfied (a: Array Int) (h_precond : isSorted_precond (a)) :
    isSorted_postcond (a) (isSorted (a) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold isSorted isSorted_postcond
  simp_all
  cases a with | mk a =>
    simp
    cases a with
    | nil => simp
    | cons x xs =>
      simp
      cases xs with
      | nil => simp
      | cons x' xs =>
        simp
        constructor <;> simp_all

  -- !benchmark @end proof


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

Inputs rejected by the precondition:
-----Description-----  
This task requires determining the smaller of two integers. Given two input numbers, the goal is to compare them and return the one that is less than or equal to the other.

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

-----Output-----  
The output is an integer representing the minimum of the two input integers:  
• Returns x if x is less than or equal to y.  
• Returns y if x is greater than y.
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 (x : Int) (y : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


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


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def myMin_postcond (x : Int) (y : Int) (result: Int) (h_precond : myMin_precond (x) (y)) :=
  -- !benchmark @start postcond
  (x ≤ y → result = x) ∧ (x > y → result = y)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem myMin_spec_satisfied (x: Int) (y: Int) (h_precond : myMin_precond (x) (y)) :
    myMin_postcond (x) (y) (myMin (x) (y) h_precond) h_precond := by
  -- !benchmark @start proof
  unfold myMin_postcond myMin
  simp
  have h_left : (x ≤ y → y ≤ x → y = x) := by
    intro h₁ h₂
    exact Int.le_antisymm h₂ h₁
  have h_right : (y < x → x < y → x = y) := by
    intro h₁ h₂
    have h_contr : False := Int.lt_irrefl x (Int.lt_trans h₂ h₁)
    contradiction
  exact ⟨h_left, h_right⟩
  -- !benchmark @end proof


Tests:
input: x: 3
y: 5
x: 10
y: 7
x: 4
y: 4
x: -5
y: 0
x: 0
y: -10
expected: 3
7
4
-5
-10
unexpected: 5
8
10
17
0
8
0
-4
0
-8

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 function that returns the maximum element from a non-empty list of natural numbers.

-----Input-----
The input consists of:
lst: a non-empty list of natural numbers.

-----Output-----
The output is:
A natural number representing the largest element in the 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 maxOfList_precond (lst : List Nat) : Prop :=
  -- !benchmark @start precond
  lst.length > 0
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def maxOfList (lst : List Nat) (h_precond : maxOfList_precond (lst)) : Nat :=
  -- !benchmark @start code
  let rec helper (lst : List Nat) : Nat :=
    match lst with
    | [] => 0  -- technically shouldn't happen if input is always non-empty
    | [x] => x
    | x :: xs =>
      let maxTail := helper xs
      if x > maxTail then x else maxTail

  helper lst
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def maxOfList_postcond (lst : List Nat) (result: Nat) (h_precond : maxOfList_precond (lst)) : Prop :=
  -- !benchmark @start postcond
  result ∈ lst ∧ ∀ x ∈ lst, x ≤ result
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem maxOfList_spec_satisfied (lst: List Nat) (h_precond : maxOfList_precond (lst)) :
    maxOfList_postcond (lst) (maxOfList (lst) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




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

Inputs rejected by the precondition:
-----Description-----
This task requires writing a Lean 4 method that checks whether a given string is a palindrome. A palindrome is a string that reads the same forwards and backwards. The function should ignore whitespace, punctuation, and capitalization when checking for palindromes.

-----Input-----
The input consists of:
s: A string to be checked.

-----Output-----
The output is a boolean:
Returns true if the input string is a palindrome when non-alphabetic characters are removed and letters are treated case-insensitively, and false otherwise.


Difficulty: advanced

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

-- !benchmark @end import

-- !benchmark @start solution_aux
-- Check if a character is an uppercase alphabet letter
def isUpperAlpha (c : Char) : Bool :=
  'A' ≤ c ∧ c ≤ 'Z'

-- Check if a character is a lowercase alphabet letter
def isLowerAlpha (c : Char) : Bool :=
  'a' ≤ c ∧ c ≤ 'z'

-- Determine if a character is alphabetic
def isAlpha (c : Char) : Bool :=
  isUpperAlpha c ∨ isLowerAlpha c

-- Convert a single character to lowercase
def toLower (c : Char) : Char :=
  if isUpperAlpha c then Char.ofNat (c.toNat + 32) else c

-- Normalize a character: keep only lowercase letters
def normalizeChar (c : Char) : Option Char :=
  if isAlpha c then some (toLower c) else none

-- Normalize a string into a list of lowercase alphabetic characters
def normalizeString (s : String) : List Char :=
  s.toList.foldr (fun c acc =>
    match normalizeChar c with
    | some c' => c' :: acc
    | none    => acc
  ) []
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def isCleanPalindrome_precond (s : String) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux
-- Reverse the list
def reverseList (xs : List Char) : List Char :=
  xs.reverse
-- !benchmark @end code_aux


def isCleanPalindrome (s : String) (h_precond : isCleanPalindrome_precond (s)) : Bool :=
  -- !benchmark @start code
  let norm := normalizeString s
  norm = reverseList norm
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def isCleanPalindrome_postcond (s : String) (result: Bool) (h_precond : isCleanPalindrome_precond (s)) : Prop :=
  -- !benchmark @start postcond
  let norm := normalizeString s
  (result = true → norm = norm.reverse) ∧
  (result = false → norm ≠ norm.reverse)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem isCleanPalindrome_spec_satisfied (s: String) (h_precond : isCleanPalindrome_precond (s)) :
    isCleanPalindrome_postcond (s) (isCleanPalindrome (s) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: s: A man, a plan, a canal, Panama
s: No lemon, no melon
s: OpenAI
s: Was it a car or a cat I saw?
s: Hello, World!
expected: True
True
False
True
False
unexpected: False
False
True
False
True

Inputs rejected by the precondition: