Bump Lean and mathlib versions to v4.27.0

pyproject.toml

@@ -18,7 +18,7 @@ packages = ["src/clever_bench"]
 
 [project]
 name = "clever-bench"
-version = "1.6.0"
+version = "1.7.0"
 authors = [
   { name="Amitayush Thakur", email="amitayush@utexas.edu" },
 ]

src/lean4/Imports/AllImports.lean

@@ -72,15 +72,11 @@ sample_problems:
 def string_eq_iff_data_eq (s1: String) (s2: String)
 : s1.data = s2.data ↔ s1 = s2 :=
 by
-  apply Iff.intro
-  intro h
-  cases s1
-  cases s2
-  simp at h
-  simp [h]
-  intro h
-  apply String.data_eq_of_eq
-  exact h
+  constructor
+  · intro h
+    exact String.ext h
+  · intro h
+    exact congrArg String.data h
 -- end_def helper_definitions
 
 -- start_def helper_definitions
@@ -104,29 +100,22 @@ if paren_string.isEmpty then
 else
   let c := paren_string.get! 0
   if c == '(' then
-    string_is_paren_balanced_helper (paren_string.drop 1) (num_open + 1)
+    string_is_paren_balanced_helper (String.ofList (paren_string.toList.drop 1)) (num_open + 1)
   else if c == ')' then
-    string_is_paren_balanced_helper (paren_string.drop 1) (num_open - 1)
+    string_is_paren_balanced_helper (String.ofList (paren_string.toList.drop 1)) (num_open - 1)
   else
-    string_is_paren_balanced_helper (paren_string.drop 1) num_open
+    string_is_paren_balanced_helper (String.ofList (paren_string.toList.drop 1)) num_open
 termination_by paren_string.length
 decreasing_by
   all_goals
   {
-    rename_i h_non_empty_string
-    rw [String.drop_eq, String.length]
-    simp
+    simp only [String.length_ofList, List.length_drop]
+    have h_non_empty_string : ¬ paren_string.isEmpty = true := by assumption
     rw [String.isEmpty_iff] at h_non_empty_string
-    by_cases h_paren_nil : paren_string.length ≤ 0
-    rw [Nat.le_zero_eq] at h_paren_nil
-    rw [←string_eq_iff_data_eq] at h_non_empty_string
-    have h_temp : "".data = [] := by simp
-    rw [h_temp] at h_non_empty_string
-    rw [String.length] at h_paren_nil
-    rw [List.length_eq_zero_iff] at h_paren_nil
-    contradiction
-    have h_temp : paren_string.length > 0 := by linarith
-    assumption
+    have hne : paren_string.toList ≠ [] := by simpa using h_non_empty_string
+    have hpos : 0 < paren_string.toList.length := List.length_pos_of_ne_nil hne
+    have hlen : paren_string.length = paren_string.toList.length := by simp
+    omega
   }
 -- end_def helper_definitions
 
@@ -182,31 +171,24 @@ if paren_string.isEmpty then
 else
   let c := paren_string.get! 0
   if c == '(' then
-    count_paren_groups_helper (paren_string.drop 1) (num_open + 1) num_groups
+    count_paren_groups_helper (String.ofList (paren_string.toList.drop 1)) (num_open + 1) num_groups
   else if c == ')' then
     let new_num_groups :=
     if num_open == 1 then num_groups + 1 else num_groups
-    count_paren_groups_helper (paren_string.drop 1) (num_open - 1) new_num_groups
+    count_paren_groups_helper (String.ofList (paren_string.toList.drop 1)) (num_open - 1) new_num_groups
   else
-    count_paren_groups_helper (paren_string.drop 1) num_open num_groups
+    count_paren_groups_helper (String.ofList (paren_string.toList.drop 1)) num_open num_groups
 termination_by paren_string.length
 decreasing_by
   all_goals
   {
-    rename_i h_non_empty_string
-    rw [String.drop_eq, String.length]
-    simp
+    simp only [String.length_ofList, List.length_drop]
+    have h_non_empty_string : ¬ paren_string.isEmpty = true := by assumption
     rw [String.isEmpty_iff] at h_non_empty_string
-    by_cases h_paren_nil : paren_string.length ≤ 0
-    rw [Nat.le_zero_eq] at h_paren_nil
-    rw [←string_eq_iff_data_eq] at h_non_empty_string
-    have h_temp : "".data = [] := by simp
-    rw [h_temp] at h_non_empty_string
-    rw [String.length] at h_paren_nil
-    rw [List.length_eq_zero_iff] at h_paren_nil
-    contradiction
-    have h_temp : paren_string.length > 0 := by linarith
-    assumption
+    have hne : paren_string.toList ≠ [] := by simpa using h_non_empty_string
+    have hpos : 0 < paren_string.toList.length := List.length_pos_of_ne_nil hne
+    have hlen : paren_string.length = paren_string.toList.length := by simp
+    omega
   }
 -- end_def helper_definitions
 
@@ -241,29 +223,22 @@ else
   let c := paren_string.get! 0
   if c == '(' then
     let new_num_open := num_open + 1
-    count_max_paren_depth_helper (paren_string.drop 1) (new_num_open) (max_depth.max new_num_open.toNat)
+    count_max_paren_depth_helper (String.ofList (paren_string.toList.drop 1)) (new_num_open) (max_depth.max new_num_open.toNat)
   else if c == ')' then
-    count_max_paren_depth_helper (paren_string.drop 1) (num_open - 1) max_depth
+    count_max_paren_depth_helper (String.ofList (paren_string.toList.drop 1)) (num_open - 1) max_depth
   else
-    count_max_paren_depth_helper (paren_string.drop 1) num_open max_depth
+    count_max_paren_depth_helper (String.ofList (paren_string.toList.drop 1)) num_open max_depth
 termination_by paren_string.length
 decreasing_by
   all_goals
   {
-    rename_i h_non_empty_string
-    rw [String.drop_eq, String.length]
-    simp
+    simp only [String.length_ofList, List.length_drop]
+    have h_non_empty_string : ¬ paren_string.isEmpty = true := by assumption
     rw [String.isEmpty_iff] at h_non_empty_string
-    by_cases h_paren_nil : paren_string.length ≤ 0
-    rw [Nat.le_zero_eq] at h_paren_nil
-    rw [←string_eq_iff_data_eq] at h_non_empty_string
-    have h_temp : "".data = [] := by simp
-    rw [h_temp] at h_non_empty_string
-    rw [String.length] at h_paren_nil
-    rw [List.length_eq_zero_iff] at h_paren_nil
-    contradiction
-    have h_temp : paren_string.length > 0 := by linarith
-    assumption
+    have hne : paren_string.toList ≠ [] := by simpa using h_non_empty_string
+    have hpos : 0 < paren_string.toList.length := List.length_pos_of_ne_nil hne
+    have hlen : paren_string.length = paren_string.toList.length := by simp
+    omega
   }
 -- end_def helper_definitions
 

src/lean4/human_eval/problem_0.lean

@@ -22,7 +22,7 @@ def problem_spec
 -- spec
 let numbers_within_threshold :=
 (∃ i j, i < numbers.length ∧ j < numbers.length ∧
-i ≠ j ∧ |numbers.get! i - numbers.get! j| < threshold);
+i ≠ j ∧ |numbers[i]! - numbers[j]!| < threshold);
 let spec (res: Bool) :=
 numbers.length > 1 →
 if res then numbers_within_threshold else ¬numbers_within_threshold;
@@ -273,14 +273,12 @@ by_cases h_1_lt_tail : 1 < tail.length
 simp [h_1_lt_tail] at ih
 obtain ⟨ i, h_i_lt_tail_len, h_i_in_threshold ⟩ := ih
 use i + 1
-have h_i_lt_tail_len' : i + 1 < tail.length + 1 := by linarith
-simp [h_i_lt_tail_len']
+refine ⟨by omega, ?_⟩
 obtain ⟨ j, h_j_lt_tail_len, h_i_neq_j, h_j_in_threshold ⟩ := h_i_in_threshold
-use j + 1
-simp [h_j_lt_tail_len]
-simp [h_i_neq_j]
-simp [h_i_lt_tail_len, h_j_lt_tail_len] at h_j_in_threshold
-assumption
+refine ⟨j + 1, by omega, ?_, ?_⟩
+· simp [h_i_neq_j]
+· simp [h_i_lt_tail_len, h_j_lt_tail_len] at h_j_in_threshold ⊢
+  exact h_j_in_threshold
 use 0
 simp
 use 1
@@ -292,7 +290,7 @@ simp [h_tail_empty] at h_tail_has_close_elements
 simp at h_1_lt_tail
 have h_0_lt_tail_len : tail.length = 1 := by linarith
 have h_tail_singleton: ∃ x, tail = [x] := by
-  rw [List.length_eq_one] at h_0_lt_tail_len
+  rw [List.length_eq_one_iff] at h_0_lt_tail_len
   assumption
 obtain ⟨ x, h_tail_singleton ⟩ := h_tail_singleton
 simp [h_0_lt_tail_len]

src/lean4/human_eval/problem_101.lean

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

src/lean4/human_eval/problem_103.lean

@@ -36,7 +36,7 @@ let spec (result: Option String) :=
     let xs := List.Ico n (m+1);
     let avg := xs.sum / xs.length;
     (val.take 2 = "0b") ∧
-    (Nat.ofDigits 2 ((val.drop 2).toList.map (fun c => c.toNat - '0'.toNat)).reverse = avg)))
+    (Nat.ofDigits 2 ((val.drop 2).toString.toList.map (fun c => c.toNat - '0'.toNat)).reverse = avg)))
 -- program termination
 ∃ result, implementation n m = result ∧
 spec result

src/lean4/human_eval/problem_11.lean

@@ -28,9 +28,8 @@ let spec (result: String) :=
   result.length = a.length ∧
   result.all (fun c => c = '0' ∨ c = '1') ∧
   (∀ i, i < a.length →
-  let i_pos := String.Pos.mk i;
-  (a.get i_pos = b.get i_pos → result.get i_pos = '0') ∧
-  (a.get i_pos ≠ b.get i_pos → result.get i_pos = '1'));
+  (a.data[i]! = b.data[i]! → result.data[i]! = '0') ∧
+  (a.data[i]! ≠ b.data[i]! → result.data[i]! = '1'));
 -- program termination
 ∃ result, implementation a b = result ∧
 spec result

src/lean4/human_eval/problem_110.lean

@@ -37,11 +37,11 @@ let spec (result : String) :=
     lst1_idxs.Nodup ∧
     lst2_idxs.Nodup ∧
     ∀ i, i < lst1.length →
-      (i ∉ lst1_idxs → Even (lst1.get! i)) ∧
+      (i ∉ lst1_idxs → Even (lst1[i]!)) ∧
       (i ∈ lst1_idxs →
         -- find the (a, b) in exchange where a = i
         let i_idx := (lst1_idxs.indexesOf i).head!
-        Even (lst2.get! (lst2_idxs.get! i_idx)))
+        Even (lst2[lst2_idxs[i_idx]!]!))
   (bool_result → result = "YES") ∧
   (result = "NO" → ¬ bool_result) ∧
   (result ≠ "YES" ∧ result ≠ "NO" → False)

src/lean4/human_eval/problem_112.lean

@@ -35,7 +35,7 @@ let spec (result : String × Bool) :=
     result_str =
     (implementation
       (String.join ((s.data.filter (fun x => x ≠ c.data.head!)).map (fun c => String.mk [c])))
-      (c.drop 1)).fst)
+      (c.drop 1).toString).fst)
 
 -- program termination
 ∃ result,

src/lean4/human_eval/problem_116.lean

@@ -26,8 +26,8 @@ let spec (result : List Nat) :=
   ∀ x : Nat, lst.count x = result.count x ∧
   result.length = lst.length ∧
   (∀ i j : Nat, i < j → j < result.length →
-    Nat.digits 2 (result.get! i) < Nat.digits 2 (result.get! j) ∨
-    (Nat.digits 2 (result.get! i) = Nat.digits 2 (result.get! j) ∧ result.get! i < result.get! j))
+    Nat.digits 2 (result[i]!) < Nat.digits 2 (result[j]!) ∨
+    (Nat.digits 2 (result[i]!) = Nat.digits 2 (result[j]!) ∧ result[i]! < result[j]!))
 -- program termination
 ∃ result,
   implementation lst = result ∧

src/lean4/human_eval/problem_125.lean

@@ -41,24 +41,24 @@ def problem_spec
 -- spec
 let lexographically_less (a b: List Nat) : Prop :=
   a.length = b.length ∧ a.length = k ∧
-  (∃ i, i < k ∧ a.get! i < b.get! i ∧
-  (∀ j, j < i → a.get! j = b.get! j));
+  (∃ i, i < k ∧ a[i]! < b[i]! ∧
+  (∀ j, j < i → a[j]! = b[j]!));
 let rec is_valid_path (k': Nat) (path: List Nat) (grid: List (List Nat)) : Prop :=
   let n := grid.length;
   path.length = k' →
   (∃ i j,
-    (i < n ∧ j < n ∧ path.get! 0 = (grid.get! i).get! j) ∧
+    (i < n ∧ j < n ∧ path[0]! = (grid[i]!)[j]!) ∧
     (1 < path.length →
       ( ∃ i' j', i' < n ∧ j' < n ∧
-        (path.get! 1 = (grid.get! i').get! j') ∧
+        (path[1]! = (grid[i']!)[j']!) ∧
         ((abs ((i: Int) - (i': Int)) = 1 ∧ j = j') ∨
          (abs ((j: Int) - (j': Int)) = 1 ∧ i = i'))) ∧
       (is_valid_path (k' - 1) (path.drop 1) grid))
   );
 let spec (result: List Nat) :=
   let n := grid.length;
-  (∀ i, i < n → (grid.get! i).length = n) →
-  (∀ i j, i < n → j < n ↔ ((grid.get! i).get! j) ∈ [1, n^2]) →
+  (∀ i, i < n → (grid[i]!).length = n) →
+  (∀ i j, i < n → j < n ↔ ((grid[i]!)[j]!) ∈ [1, n^2]) →
   is_valid_path k result grid ∧ (∀ path, is_valid_path k path grid → lexographically_less result path);
 -- program terminates
 ∃ result, impl grid k = result ∧

src/lean4/human_eval/problem_129.lean

@@ -34,11 +34,11 @@ let spec (result: Option (List String) × Option Nat) :=
     (words = none ↔ ∀ ch, ch ∈ text.toList →  (ch = ',' ∨ ch = ' ')) ∧
     (∀ num, ord = some num → (text.get! 0).toNat = num) ∧
     (∀ lst, words = some lst → ∀ i, i < lst.length →
-      let str := lst.get! i;
+      let str := lst[i]!;
       text.containsSubstr str) ∧
     (∀ lst, words = some lst →
-      let first := text.takeWhile (fun c => c ≠ ',' ∧ c ≠ ' ');
-      let nextImpl := impl (text.drop (first.length + 1));
+      let first := (text.takeWhile (fun c => c ≠ ',' ∧ c ≠ ' ')).toString;
+      let nextImpl := impl ((text.drop (first.length + 1)).toString);
       let nextWords := nextImpl.fst;
       (∃ nextLst, nextWords = some nextLst ∧
         lst = [first] ++ nextLst))

src/lean4/human_eval/problem_140.lean

@@ -36,8 +36,8 @@ let spec (result: String) :=
     ∨
     (∃ pref s : String, text = pref ++ s ∧ pref ≠ "" ∧ (∀ ch, ch ∈ pref.toList → ch = ' ')
       ∧ let k := pref.length;
-        (k ≤ 2 → result = (String.replicate k '_') ++ (impl (text.drop k)))
-      ∧ (2 < k → result = "-" ++ (impl (text.drop k)))) )
+        (k ≤ 2 → result = (String.replicate k '_') ++ (impl (text.drop k).toString))
+      ∧ (2 < k → result = "-" ++ (impl (text.drop k).toString))) )
   )
 -- program termination
 ∃ result, impl text = result ∧

src/lean4/human_eval/problem_153.lean

@@ -40,8 +40,8 @@ let last_pos := result.revPosOf '.';
 0 < extensions.length ∧ extensions.all (fun x => 0 < x.length) ∧ 0 < class_name.length →
 0 < result.length ∧
 last_pos.isSome ∧
-let class_name' := result.take (last_pos.get!).byteIdx;
-let extension_name := result.drop ((last_pos.get!).byteIdx + 1);
+let class_name' := (result.take (last_pos.get!).byteIdx).toString;
+let extension_name := (result.drop ((last_pos.get!).byteIdx + 1)).toString;
 class_name' = class_name ∧
 extension_name ∈ extensions ∧
 let strength_of_extensions := extensions.map (fun ext => strength ext);

src/lean4/human_eval/problem_154.lean

@@ -33,7 +33,7 @@ let spec (result: Bool) :=
 (0 < b.length →
 result ↔ ((b.length ≤ a.length) ∧
   (∃ i : Nat, i < b.length ∧
-  let b_rotation := b.drop i ++ b.take i;
+  let b_rotation := (b.drop i).toString ++ (b.take i).toString;
   a.containsSubstr b_rotation)));
 -- program terminates
 ∃ result, impl a b = result ∧

src/lean4/human_eval/problem_158.lean

@@ -26,7 +26,7 @@ def problem_spec
 (words: List String) :=
 let unique_chars (string: String) :=
   let string_idx := {i: Nat | i < string.length}.toFinset;
-  let characters := string_idx.image (fun i => string.toList.get! i);
+  let characters := string_idx.image (fun i => string.toList[i]!);
   characters.card;
 -- spec
 let spec (result: String) :=

src/lean4/human_eval/problem_16.lean

@@ -22,7 +22,7 @@ def problem_spec
 -- spec
 let spec (result: Nat) :=
 let string_idx := {i: Nat | i < string.length}.toFinset
-let characters := string_idx.image (fun i => string.toList.get! i)
+let characters := string_idx.image (fun i => string.toList[i]!)
 let lowercase_characters := characters.image (fun c => c.toLower)
 result = lowercase_characters.card;
 -- program termination
@@ -80,17 +80,12 @@ simp [result]
 simp [implementation]
 rcases string with ⟨data⟩
 induction data
-simp
+try simp
 have h1: "".toLower = "" := by
   unfold String.toLower
   unfold Char.toLower
   unfold String.map
   unfold String.mapAux
   simp
-simp [h1]
-rename_i head tail ih
-unfold String.toLower
-rw [String.map_eq]
-simp
 sorry
 -- end_def correctness_proof

src/lean4/human_eval/problem_17.lean

@@ -33,7 +33,7 @@ let not_map := fun
 let spec (result: List Nat) :=
 let space_split := string.splitOn " ";
 space_split.length = result.length ∧
-∀ i < result.length, not_map (space_split.get! i) = result.get! i;
+∀ i < result.length, not_map (space_split[i]!) = result[i]!;
 -- program termination
 ∃ result, implementation string = result ∧
 spec result

src/lean4/human_eval/problem_23.lean

@@ -23,7 +23,7 @@ def problem_spec
 let spec (result: Nat) :=
 -- every character in the string is counted once
 result = 0 ↔ string.isEmpty ∧
-(0 < result → result - 1 = implementation (string.drop 1))
+(0 < result → result - 1 = implementation (string.drop 1).toString)
 -- program termination
 ∃ result, implementation string = result ∧
 spec result