Bug fix of specs/implementations in benchmark

src/lean4/human_eval/problem_1.lean

@@ -26,6 +26,7 @@ def problem_spec
 -- spec
 let paren_string_filtered := (paren_string.toList.filter (fun c => c == '(' ∨  c == ')')).asString;
 let spec (result_list: List String) :=
+balanced_paren_non_computable paren_string_filtered '(' ')' →
 -- concat of result is input_filtered
 (result_list.foldl (· ++ ·) "" = paren_string_filtered) ∧
 -- each item in result is balanced and has only one group

src/lean4/human_eval/problem_101.lean

@@ -23,9 +23,10 @@ def problem_spec
 -- spec
 let spec (result: List String) :=
   let chars := s.toList;
-  let first := s.takeWhile (fun c => c ≠ ',' ∧ c ≠ ' ');
+  let trimmed := String.mk (chars.dropWhile (fun c => c = ' ' ∨ c = ','));
+  let first := trimmed.takeWhile (fun c => c ≠ ',' ∧ c ≠ ' ');
   (result = [] ↔ (∀ x ∈ chars, x = ' ' ∨ x = ',') ∨ s = "") ∧
-  (result ≠ [] ↔ result = [first] ++ (implementation (s.drop (first.length + 1))))
+  (result ≠ [] ↔ result = [first] ++ (implementation (trimmed.drop (first.length + 1))))
 
 -- program termination
 ∃ result, implementation s = result ∧
@@ -57,7 +58,8 @@ sorry
 def implementation (s: String) : List String :=
 -- end_def implementation_signature
 -- start_def implementation
-  List.map (fun s => (s.toList.filter (fun c => c != ',')).asString) ((s.splitOn).filter (fun s => s != "" ∧ s != ","))
+  let normalized := String.mk (s.toList.map (fun c => if c = ',' then ' ' else c))
+  normalized.split (· == ' ') |>.filter (fun w => w ≠ "")
 -- end_def implementation
 
 -- Uncomment the following test cases after implementing the function

src/lean4/human_eval/problem_108.lean

@@ -28,7 +28,7 @@ def problem_spec
 -- spec
 let spec (result: Int) :=
   let dig_sum (x: Int): Int :=
-    let digs := x.natAbs.digits 10;
+    let digs := Nat.digits 10 x.natAbs;
     if x >= 0 then
       (List.map (fun t => (t: Int)) digs).sum
     else

src/lean4/human_eval/problem_13.lean

@@ -27,9 +27,10 @@ def problem_spec
 let spec (result: Int) :=
 (result ∣ a) ∧
 (result ∣ b) ∧
+(result ≥ 0) ∧
 (∀ (d': Int),
-(d' > 0) → (d' ∣ a) → (d' ∣ b) →
-d' ≤ result);
+(d' ∣ a) → (d' ∣ b) →
+d' ∣ result);
 -- program termination
 ∃ result, implementation a b = result ∧
 spec result

src/lean4/human_eval/problem_18.lean

@@ -29,16 +29,19 @@ def problem_spec
 (string substring: String) :=
 -- spec
 let spec (result: Nat) :=
+(substring.length = 0 → result = string.length)
+∧
+(substring.length ≠ 0 →
 (string.length < substring.length → result = 0)
 ∧
 (string.length = substring.length →
 ((string = substring ↔ result = 1) ∧
 (substring ≠ string ↔ result = 0)))
 ∧
 (substring.length < string.length  →
-let subtring_start_idx := {i: Nat | i ≤ string.length - substring.length};
-let substring_occurrences := {i ∈ subtring_start_idx | (string.take (i + substring.length)).drop i = substring };
-result = substring_occurrences.toFinset.card);
+let substring_start_idx := {i: Nat | i < string.length - substring.length + 1};
+let substring_occurrences := {i ∈ substring_start_idx | (string.drop i).take substring.length = substring };
+result = substring_occurrences.toFinset.card));
 -- program termination
 ∃ result, implementation string substring = result ∧
 spec result

src/lean4/human_eval/problem_19.lean

@@ -39,7 +39,7 @@ let rec is_sorted_asc_helper : List Int → Bool → Bool := fun numbers is_sort
   | [] => is_sorted
   | [x] => is_sorted
   | x::y::rest => if x <= y then is_sorted_asc_helper (y::rest) true else false;
-is_sorted_asc_helper numbers false;
+is_sorted_asc_helper numbers true;
 let spec (result: String) :=
 let result_split := result.splitOn " ";
 let numbers_split := numbers.splitOn " ";
@@ -114,7 +114,7 @@ let numbers_mapped_to_numbers := numbers_split.map word_to_number_map;
 let sorted_numbers := numbers_mapped_to_numbers.mergeSort;
 let sorted_numbers_mapped_to_words := sorted_numbers.map number_to_word_map;
 let join: List String → String := fun words =>
-  let head := words.get! 0;
+  let head := words.head!;
   let tail := words.drop 1;
   tail.foldl (fun acc word => acc ++ " " ++ word) head;
 join sorted_numbers_mapped_to_words

src/lean4/human_eval/problem_20.lean

@@ -28,8 +28,8 @@ let abs_diff := |larger - smaller|;
 smaller ≤ larger ∧
 smaller ∈ numbers ∧
 larger ∈ numbers ∧
-(∀ x y, x ∈ numbers → y ∈ numbers →  abs_diff ≤ |x - y|) ∧
-(smaller = larger → 1 ≤ (numbers.filter (fun z => z = smaller)).length));
+(∀ x y, x ∈ numbers → y ∈ numbers → x ≠ y → abs_diff ≤ |x - y|) ∧
+(smaller = larger → 2 ≤ (numbers.filter (fun z => z = smaller)).length));
 -- program termination
 ∃ result, implementation numbers = result ∧
 spec result
@@ -62,13 +62,13 @@ def implementation (numbers: List Rat): (Rat × Rat) :=
 -- start_def implementation
 let n := numbers.length;
 let sorted_numbers := numbers.mergeSort;
-let min_diff := sorted_numbers.get! 1 - sorted_numbers.get! 0;
-let min_pair := (sorted_numbers.get! 0, sorted_numbers.get! 1);
+let min_diff := sorted_numbers[1]! - sorted_numbers[0]!;
+let min_pair := (sorted_numbers[0]!, sorted_numbers[1]!);
 let rec loop (i: Nat) (min_diff: Rat) (min_pair: (Rat × Rat)): (Rat × Rat) :=
   if i < n - 1 then
-    let diff := sorted_numbers.get! (i + 1) - sorted_numbers.get! i;
+    let diff := sorted_numbers[i + 1]! - sorted_numbers[i]!;
     if diff < min_diff then
-      loop (i + 1) diff (sorted_numbers.get! i, sorted_numbers.get! (i + 1))
+      loop (i + 1) diff (sorted_numbers[i]!, sorted_numbers[i + 1]!)
     else
       loop (i + 1) min_diff min_pair
   else

src/lean4/human_eval/problem_25.lean

@@ -61,12 +61,14 @@ def implementation (n: Nat) : List Nat :=
 -- end_def implementation_signature
 -- start_def implementation
 Id.run do
-let mut result := []
-for num in List.range' 2 n.sqrt do
-  let mut n' := n
+let mut result : List Nat := []
+let mut n' := n
+for num in List.range' 2 (n.sqrt + 1) do
   while n' % num = 0 do
     n' := n' / num
     result := result ++ [num]
+if n' > 1 then
+  result := result ++ [n']
 result
 -- end_def implementation
 

src/lean4/human_eval/problem_31.lean

@@ -31,7 +31,7 @@ def problem_spec
 (n: Nat) :=
 -- spec
 let spec (result: Bool) :=
-  result ↔ ¬ (∃ k, 2 ≤ k ∧ k < n ∧ n % k = 0);
+  result ↔ (2 ≤ n ∧ ¬ (∃ k, 2 ≤ k ∧ k < n ∧ n % k = 0));
 -- program termination
 ∃ result,
   implementation n = result ∧

src/lean4/human_eval/problem_32.lean

@@ -14,7 +14,7 @@ test_cases:
   - input: [1, 2]
     output: -0.5
   - input: [-6, 11, -6, 1]
-    output: 1.0
+    output: 3.0
 -/
 -- end_def problem_details
 
@@ -30,7 +30,7 @@ let spec (result: Rat) :=
   xs.length ≥ 1 → xs.length % 2 = 0 →
   ∀ poly : Polynomial Rat,
     poly.degree = some (xs.length - 1) →
-    (∀ i, i ≤ xs.length - 1 → poly.coeff i = xs.get! i) →
+    (∀ i, i ≤ xs.length - 1 → poly.coeff i = xs[i]!) →
     |poly.eval result| ≤ eps;
 -- program termination
 ∃ result,
@@ -64,26 +64,34 @@ def implementation (xs: List Rat) : Rat :=
 -- end_def implementation_signature
 -- start_def implementation
 let rec poly (xs: List Rat) (x: Rat) := xs.reverse.foldl (λ acc a => acc * x + a) 0;
-let rec poly' (xs: List Rat) (x: Rat) := (xs.drop 1).reverse.foldl (λ acc a => acc * x + a) 0;
 let rec eps := (1: Rat) / 1000000;
-let rec find_zero (xs: List Rat) (guess: Rat) (fuel: Nat) :=
-let eval := poly xs guess;
-let eval' := poly' xs guess;
-if eval ≤ eps ∨ fuel = 0 then (guess, fuel)
-else
-let guess' := (eval' * guess - eval) / eval';
-find_zero xs guess' (fuel - 1);
-(find_zero xs 1.0 1000000).1
--- Note: The above implementation can fail to converge in some cases. For example,
--- on the test case [-6, 11, -6, 1] as the derivative of the polynomial
--- can be zero at if the guess is 0. In such cases, the implementation will not
--- converge. The implementation can be improved by using a better guess.
+let lc := |xs.getLast!|;
+let initBound : Rat := if lc = 0 then 1
+  else 1 + xs.dropLast.foldl (fun acc a => acc + |a|) 0 / lc;
+let rec findBound (xs: List Rat) (b: Rat) (fuel: Nat) : Rat :=
+  match fuel with
+  | 0 => b
+  | fuel' + 1 =>
+    if poly xs b * poly xs (-b) ≤ 0 then b
+    else findBound xs (b * 2) fuel';
+let rec bisect (xs: List Rat) (lo hi: Rat) (fuel: Nat) : Rat :=
+  match fuel with
+  | 0 => (lo + hi) / 2
+  | fuel' + 1 =>
+    let mid := (lo + hi) / 2;
+    if |poly xs mid| ≤ eps then mid
+    else if poly xs lo * poly xs mid ≤ 0 then bisect xs lo mid fuel'
+    else bisect xs mid hi fuel';
+let bound := findBound xs initBound 100;
+let coeffBits := xs.foldl (fun acc a => acc + a.num.natAbs.size + a.den.size) 0;
+let fuel := 1000000 + coeffBits * (xs.length + 1) * 40;
+bisect xs (-bound) bound fuel
 -- end_def implementation
 
 -- Uncomment the following test cases after implementing the function
 -- start_def test_cases
-#test implementation [1, 2] = -0.5
-#test implementation [-6, 11, -6, 1] = 1.0
+#test |implementation [1, 2] - (-1/2)| ≤ 1/1000000
+#test |implementation [-6, 11, -6, 1] - 1| ≤ 1/1000000 ∨ |implementation [-6, 11, -6, 1] - 2| ≤ 1/1000000 ∨ |implementation [-6, 11, -6, 1] - 3| ≤ 1/1000000
 -- end_def test_cases
 
 -- start_def correctness_definition

src/lean4/human_eval/problem_36.lean

@@ -25,10 +25,10 @@ def problem_spec
 let spec (result: Nat) :=
   (n = 0 → result = 0) ∧
   (0 < n → result = implementation (n - 1) →
-    (n % 11 ≠  0 ∧  n % 13 ≠  0) ∨ n.repr.count '7' = 0) ∧
+    ((n - 1) % 11 ≠  0 ∧  (n - 1) % 13 ≠  0) ∨ (n - 1).repr.count '7' = 0) ∧
   (0 < n → result ≠ implementation (n - 1) →
-    (n % 11 = 0 ∨  n % 13 = 0) ∧
-    result - implementation (n - 1) = n.repr.count '7')
+    ((n - 1) % 11 = 0 ∨  (n - 1) % 13 = 0) ∧
+    result - implementation (n - 1) = (n - 1).repr.count '7')
 -- program termination
 ∃ result, implementation n = result ∧
 spec result

src/lean4/human_eval/problem_6.lean

@@ -16,18 +16,18 @@ test_cases:
 -- start_def problem_spec
 def problem_spec
 -- function signature
-(implementation: String → List Int)
+(implementation: String → List Nat)
 -- inputs
 (paren_string: String)
 :=
 -- spec
-let spec (result: List Int) :=
+let spec (result: List Nat) :=
 let paren_space_split := paren_string.split (fun x => x = ' ');
 result.length = paren_space_split.length ∧
 ∀ i, i < result.length →
 let group := paren_space_split[i]!;
 balanced_paren_non_computable group '(' ')' →
-0 < result[i]! ∧ count_max_paren_depth group = result[i]!.toNat;
+count_max_paren_depth group = result[i]!;
 -- program termination
 ∃ result, implementation paren_string = result ∧
 spec result
@@ -36,7 +36,7 @@ spec result
 -- start_def generated_spec
 def generated_spec
 -- function signature
-(implementation: String → List Int)
+(implementation: String → List Nat)
 -- inputs
 (paren_string: String) : Prop :=
 --end_def generated_spec
@@ -55,7 +55,7 @@ sorry
 -- end_def spec_isomorphism_proof
 
 -- start_def implementation_signature
-def implementation (paren_string: String) : List Int :=
+def implementation (paren_string: String) : List Nat :=
 -- end_def implementation_signature
 -- start_def implementation
 (paren_string.split (fun x => x = ' ')).map (fun x => count_max_paren_depth x)

src/lean4/human_eval/problem_73.lean

@@ -25,10 +25,16 @@ def problem_spec
 (arr: List Int) :=
 -- spec
 let spec (result : Int) :=
-  let swaps_done (arr1: List Int) (arr2: List Int) :=
-    ((List.finRange (arr1.length)).filter (fun idx => arr1[idx]? ≠ arr2[idx]?)).length/2
-  ∀ palin_perm, (List.Perm arr palin_perm) ∧ (List.Palindrome palin_perm) →
-    result ≤ (swaps_done arr palin_perm)
+  let changes_needed (arr1: List Int) (arr2: List Int) :=
+    ((List.finRange (arr1.length)).filter (fun idx => arr1[idx]? ≠ arr2[idx]?)).length
+  (∃ palin : List Int,
+    palin.length = arr.length ∧
+    List.Palindrome palin ∧
+    result = changes_needed arr palin) ∧
+  (∀ palin : List Int,
+    palin.length = arr.length →
+    List.Palindrome palin →
+    result ≤ changes_needed arr palin)
 -- program termination
 ∃ result, implementation arr = result ∧
 spec result

src/lean4/human_eval/problem_78.lean

@@ -45,10 +45,11 @@ let spec (result: Int) :=
   0 < num.length →
   (
     let char_val := num_val num.toList[0]!;
-    (Nat.Prime char_val →
-      (1 < num.length → result = char_val + implementation (num.drop 1)) ∧
-      (1 = num.length → result = char_val)) ∧
-    (¬Nat.Prime char_val →
+    let is_prime_hex := Nat.Prime char_val ∧ char_val ≤ 15;
+    (is_prime_hex →
+      (1 < num.length → result = 1 + implementation (num.drop 1)) ∧
+      (1 = num.length → result = 1)) ∧
+    (¬is_prime_hex →
       (1 < num.length → result = implementation (num.drop 1)) ∧
       (1 = num.length → result = 0))
   )

src/lean4/human_eval/problem_82.lean

@@ -27,7 +27,7 @@ def problem_spec
 -- spec
 let spec (result : Bool) :=
 let is_prime (n: Nat) : Prop :=
-  ¬ (∃ k, 2 ≤ k ∧ k < n ∧ n % k = 0);
+  2 ≤ n ∧ ¬ (∃ k, 2 ≤ k ∧ k < n ∧ n % k = 0);
   result ↔ is_prime s.length
 -- program termination
 ∃ result,
@@ -86,6 +86,7 @@ simp [implementation]
 apply Iff.intro
 intro h_is_prime
 simp [Nat.prime_def] at h_is_prime
+refine ⟨h_is_prime.1, ?_⟩
 intro x h_2_le_x h_x_lt_s_len
 have h_p' := h_is_prime.2 x
 by_contra h_s_len_mod_x

src/lean4/human_eval/problem_9.lean

@@ -54,14 +54,17 @@ sorry
 def implementation (numbers: List Int) : List Int :=
 -- end_def implementation_signature
 -- start_def implementation
-let rec rolling_max (numbers: List Int) (results: List Int) (acc: Int) : List Int :=
-  match numbers with
-  | [] => results
-  | n :: ns =>
-    let new_acc := max acc n
-    let new_results := results ++ [new_acc]
-    rolling_max ns new_results new_acc
-rolling_max numbers [] 0
+match numbers with
+| [] => []
+| x :: xs =>
+  let rec rolling_max (nums: List Int) (results: List Int) (acc: Int) : List Int :=
+    match nums with
+    | [] => results
+    | n :: ns =>
+      let new_acc := max acc n
+      let new_results := results ++ [new_acc]
+      rolling_max ns new_results new_acc
+  rolling_max xs [x] x
 -- end_def implementation
 
 -- Uncomment the following test cases after implementing the function

src/lean4/sample_examples/problem_0.lean

@@ -61,17 +61,16 @@ sorry
 def implementation (paren_string: String) : Bool :=
 -- end_def implementation_signature
 -- start_def implementation
-let rec loop (s_chars: List Char) (num_open: Int): Int :=
+let rec loop (s_chars: List Char) (num_open: Nat): Option Nat :=
   match s_chars with
-  | [] => num_open
+  | [] => some num_open
   | '(' :: tail => loop tail (num_open + 1)
   | ')' :: tail =>
-    if num_open > 0 then
-      loop tail (num_open - 1)
-    else
-      loop tail num_open
+    match num_open with
+    | 0 => none  -- More ')' than '(' encountered
+    | n + 1 => loop tail n
   | _ :: tail => loop tail num_open
-(loop paren_string.toList 0) = 0
+(loop paren_string.toList 0) = some 0
 -- end_def implementation
 
 -- Uncomment the following test cases after implementing the function