Chore/bump to v4 24 0

pyproject.toml

@@ -18,7 +18,7 @@ packages = ["src/clever_bench"]
 
 [project]
 name = "clever-bench"
-version = "1.2.0"
+version = "1.3.0"
 authors = [
   { name="Amitayush Thakur", email="[email protected]" },
 ]

src/lean4/Imports/AllImports.lean

@@ -123,7 +123,7 @@ decreasing_by
     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] 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
@@ -203,7 +203,7 @@ decreasing_by
     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] 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
@@ -260,7 +260,7 @@ decreasing_by
     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] 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

src/lean4/human_eval/problem_105.lean

@@ -29,7 +29,7 @@ let spec (result: List String) :=
   (forall s: String, (s ∈ result → s ∈ digits)) ∧
   (arr.length ≥ result.length) ∧
   (forall x: Nat, ((x: Int) ∈ arr ∧ 1 ≤ x ∧ x ≤ 9) → (digits[x-1]! ∈ result)) ∧
-  (List.Sorted Int.le (List.map (fun (s: String) => (List.indexOf s digits) + 1) result).reverse)
+  (List.Sorted Int.le (List.map (fun (s: String) => (List.idxOf s digits) + 1) result).reverse)
 -- program termination
 ∃ result, implementation arr = result ∧
 spec result

src/lean4/human_eval/problem_117.lean

@@ -43,7 +43,7 @@ let spec (result : List String) :=
     let first_word := result[0]!
     first_word ∈ words ∧
     (first_word.data.filter (fun c => is_consonant c)).length = n ∧
-    let first_word_idx := words.indexOf first_word
+    let first_word_idx := words.idxOf first_word
     (∀ i, i < first_word_idx →
       (words[i]!.data.filter (fun c => is_consonant c)).length ≠ n) ∧
     result.tail! =

src/lean4/human_eval/problem_145.lean

@@ -32,7 +32,7 @@ match result with
   (∀ num ∈ nums,
     let sum := digit_sum num;
     sum > head_sum ∨
-   (sum = head_sum ∧ nums.indexOf num ≥ nums.indexOf head))
+   (sum = head_sum ∧ nums.idxOf num ≥ nums.idxOf head))
   ∧ impl (nums.erase head) = tail
 -- program termination
 ∃ result, impl nums = result ∧

src/lean4/human_eval/problem_148.lean

@@ -36,15 +36,15 @@ let planets := ["Mercury", "Venus", "Earth", "Mars", "Jupiter", "Saturn", "Uranu
 if planet1 ∉ planets ∨ planet2 ∉ planets then
   result = []
 else
-  let index1 := planets.indexOf planet1;
-  let index2 := planets.indexOf planet2;
+  let index1 := planets.idxOf planet1;
+  let index2 := planets.idxOf planet2;
   let minIdx := if index1 < index2 then index1 else index2;
   let maxIdx := if index1 < index2 then index2 else index1;
   (∀ str ∈ result, str ∈ planets) ∧
   (∀ planet ∈ planets, planet ∈ result ↔
-    planets.indexOf planet < maxIdx ∧
-    minIdx < planets.indexOf planet) ∧
-  result.Sorted (fun a b => planets.indexOf a < planets.indexOf b)
+    planets.idxOf planet < maxIdx ∧
+    minIdx < planets.idxOf planet) ∧
+  result.Sorted (fun a b => planets.idxOf a < planets.idxOf b)
 -- program termination
 ∃ result, impl planet1 planet2 = result ∧
 -- return value satisfies spec

src/lean4/human_eval/problem_16.lean

@@ -87,8 +87,6 @@ have h1: "".toLower = "" := by
   unfold String.map
   unfold String.mapAux
   simp
-  intros
-  contradiction
 simp [h1]
 rename_i head tail ih
 unfold String.toLower

src/lean4/human_eval/problem_25.lean

@@ -90,7 +90,5 @@ let result := implementation n
 use result
 simp [result]
 simp [implementation, Id.run]
-unfold List.foldl
-intro h_2_lt_n
 sorry
 -- end_def correctness_proof

src/lean4/lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
+   "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.24.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,61 +35,61 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "rev": "d768126816be17600904726ca7976b185786e6b9",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.74",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
+   "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "clever",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake"}

src/lean4/lakefile.lean

@@ -6,7 +6,7 @@ package «clever» where
   leanOptions := #[
     ⟨`autoImplicit, false⟩
   ]
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.15.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.24.0"
 
 @[default_target]
 lean_lib «clever» where

src/lean4/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.24.0