101

HumanEvalLean/HumanEval101.lean

@@ -1,5 +1,108 @@
-def words_string : Unit :=
-  ()
+module
+
+import Std
+open Std Std.Do
+
+set_option mvcgen.warning false
+
+def delimiters : TreeSet Char := .ofList [' ', ',', '\t', '\n', '\r']
+
+def wordsString (str : String) : Array String :=
+  str.split (· ∈ delimiters)
+    |>.filter (! ·.isEmpty)
+    |>.map String.Slice.toString
+    |>.toArray
+
+def wordsString₂ (str : String) : Array String := Id.run do
+  let mut words : Array String := #[]
+  let mut currentWord : String := ""
+  for c in str.chars do
+    if c ∈ delimiters then
+      if ! currentWord.isEmpty then
+        words := words.push currentWord
+        currentWord := ""
+    else
+      currentWord := currentWord.push c
+  if ! currentWord.isEmpty then
+    words := words.push currentWord
+  return words
+
+/-!
+## Tests
+-/
+
+example : wordsString "Hi, my name is John" = #["Hi", "my", "name", "is", "John"] := by
+  native_decide
+
+example : wordsString "One, two, three, four, five, six" =
+      #["One", "two", "three", "four", "five", "six"] := by
+  native_decide
+
+example : wordsString "Hi, my name" = #["Hi", "my", "name"] := by
+  native_decide
+
+example : wordsString "One,, two, three, four, five, six," =
+      #["One", "two", "three", "four", "five", "six"] := by
+  native_decide
+
+example : wordsString "ahmed     , gamal" = #["ahmed", "gamal"] := by
+  native_decide
+
+example : wordsString "" = #[] := by
+  native_decide
+
+/-!
+# Verification
+-/
+
+@[grind =]
+theorem not_contains_empty {c : Char} :
+    "".contains c = false := by
+  sorry
+
+@[grind =]
+theorem contains_push {s : String} {c d : Char} :
+    (s.push c).contains d = (s.contains d || c = d) := by
+  sorry
+
+theorem not_contains_of_mem_delimiters {s : String} {c : Char} (h : c ∈ delimiters) :
+    (wordsString₂ s).all (! ·.contains c) := by
+  generalize hret : wordsString₂ s = ret
+  apply Id.of_wp_run_eq hret
+  mvcgen
+  case inv1 => exact ⇓⟨_, currentWord, words⟩ => ⌜¬ currentWord.contains c ∧ words.all (! ·.contains c)⌝
+  all_goals grind
+
+@[simp, grind =]
+theorem toList_chars_empty : "".chars.toList = [] := by
+  sorry
+
+@[simp, grind =]
+theorem isEmpty_empty : "".isEmpty := by
+  sorry
+
+@[simp, grind =]
+theorem wordsString₂_empty :
+    wordsString₂ "" = #[] := by
+  simp [wordsString₂, ← Iter.forIn_toList]
+
+theorem wordsString₂_push_of_mem {s : String} {c : Char} (h : c ∈ delimiters) :
+    wordsString₂ (str.push c) = wordsString₂ str := by
+  sorry
+
+theorem wordsString₂_push {s : String} {c : Char} :
+    wordsString₂ (str.push c) =
+      if c ∈ delimiters then
+        wordsString₂ str
+      else if str.startPos.get?.all (· ∈ delimiters) then
+        (wordsString₂ str).push (Char.toString c)
+      else
+        (wordsString₂ str).modify ((wordsString₂ str).size - 1) (·.push c) := by
+  sorry
+
+theorem wordsString_eq_append {s t : String} {c : Char} (h : c ∈ delimiters) :
+    wordsString₂ (s ++ Char.toString c ++ t) = wordsString₂ s ++ wordsString₂ t := by
+  sorry
 
 /-!
 ## Prompt
@@ -10,7 +113,7 @@ def words_string(s):
     """
     You will be given a string of words separated by commas or spaces. Your task is
     to split the string into words and return an array of the words.
-    
+
     For example:
     words_string("Hi, my name is John") == ["Hi", "my", "name", "is", "John"]
     words_string("One, two, three, four, five, six") == ["One", "two", "three", "four", "five", "six"]
@@ -53,4 +156,4 @@ def check(candidate):
     assert candidate("ahmed     , gamal") == ["ahmed", "gamal"]
 
 ```
--/
+-/

HumanEvalLean/HumanEval109.lean

@@ -63,7 +63,7 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i
         rw [List.sum_eq_zero]
         intro x hx
         specialize h (x+1)
-        simp only [Nat.add_lt_add_iff_right, Nat.right_eq_add, Nat.add_eq_zero, Nat.succ_ne_self,
+        simp only [Nat.add_lt_add_iff_right, Nat.right_eq_add, Nat.add_eq_zero_iff, Nat.succ_ne_self,
           and_false, not_false_eq_true, getElem_cons_succ, forall_const] at h
         apply h
         exact hx
@@ -72,7 +72,7 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i
         left
         constructor
         · specialize h 0
-          simp only [Nat.zero_lt_succ, Nat.add_eq_zero, Nat.succ_ne_self, and_false,
+          simp only [Nat.zero_lt_succ, Nat.add_eq_zero_iff, Nat.succ_ne_self, and_false,
             not_false_eq_true, getElem_cons_zero, forall_const] at h
           assumption
         · rw [ih]
@@ -158,7 +158,7 @@ theorem List.two_le_sum_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length
             rw [List.sum_eq_one_iff] at htl
             rcases htl with ⟨i, hi,hi', _⟩
             exists (i+1)
-            simp only [Nat.right_eq_add, Nat.add_eq_zero, Nat.succ_ne_self, and_false,
+            simp only [Nat.right_eq_add, Nat.add_eq_zero_iff, Nat.succ_ne_self, and_false,
               not_false_eq_true, getElem_cons_succ, Nat.add_lt_add_iff_right, true_and]
             exists hi
         · intro h₁

HumanEvalLean/HumanEval150.lean

@@ -2,7 +2,9 @@ import Std.Data.Iterators
 import Init.Notation
 import Std.Tactic.Do
 
-open Std.Iterators
+open Std
+
+set_option mvcgen.warning false
 
 /-!
 ## Implementation
@@ -49,6 +51,10 @@ theorem isPrime_eq_true_iff {n : Nat} :
         (List.filter (· ∣ n) (List.takeWhile (fun i => i * i ≤ n) (2...n).toList)).length = 0 := by
   simp [isPrime, ← Iter.foldl_toList]
 
+example {n d : Nat} (h : n / d * d = n) (h' : n * n < n / d * d * (n / d * d)) : False := by
+  rw [h] at h' -- Why do we need this?
+  grind
+
 theorem isPrime_iff_mul_self {n : Nat} :
     IsPrime n ↔ (2 ≤ n ∧ ∀ (a : Nat), 2 ≤ a ∧ a < n → a ∣ n → n < a * a) := by
   rw [IsPrime]
@@ -57,29 +63,25 @@ theorem isPrime_iff_mul_self {n : Nat} :
   · grind
   · rintro ⟨hn, h⟩
     refine ⟨hn, fun d hd => ?_⟩
-    · have : 0 < d := Nat.pos_of_dvd_of_pos hd (by grind)
-      have : d ≤ n := Nat.le_of_dvd (by grind) hd
-      false_or_by_contra
-      by_cases hsq : d * d ≤ n
-      · specialize h d
-        grind
-      · replace h := h (n / d) ?_ ?_; rotate_left
-        · have : d ≥ 2 := by grind
-          refine ⟨?_, Nat.div_lt_self (n := n) (k := d) (by grind) (by grind)⟩
-          false_or_by_contra; rename_i hc
-          have : n / d * d ≤ 1 * d := Nat.mul_le_mul_right d (Nat.le_of_lt_succ (Nat.lt_of_not_ge hc))
-          grind [Nat.dvd_iff_div_mul_eq]
-        · exact Nat.div_dvd_of_dvd hd
-        simp only [Nat.not_le] at hsq
-        have := Nat.mul_lt_mul_of_lt_of_lt h hsq
-        replace : n * n < ((n / d) * d) * ((n / d) * d) := by grind
-        rw [Nat.dvd_iff_div_mul_eq] at hd
-        grind
-
-theorem ClosedOpen.toList_eq_nil_of_le {m n : Nat} (h : n ≤ m) :
-    (m...n).toList = [] := by
-  simp [Std.PRange.toList_eq_nil_iff, Std.PRange.BoundedUpwardEnumerable.init?,
-    Std.PRange.SupportsUpperBound.IsSatisfied, show n ≤ m by grind]
+    have : 0 < d := Nat.pos_of_dvd_of_pos hd (by grind)
+    have : d ≤ n := Nat.le_of_dvd (by grind) hd
+    false_or_by_contra
+    by_cases hsq : d * d ≤ n
+    · specialize h d
+      grind
+    · replace h := h (n / d) ?_ ?_; rotate_left
+      · have : d ≥ 2 := by grind
+        refine ⟨?_, Nat.div_lt_self (n := n) (k := d) (by grind) (by grind)⟩
+        false_or_by_contra; rename_i hc
+        have : n / d * d ≤ 1 * d := Nat.mul_le_mul_right d (Nat.le_of_lt_succ (Nat.lt_of_not_ge hc))
+        grind [Nat.dvd_iff_div_mul_eq]
+      · exact Nat.div_dvd_of_dvd hd
+      simp only [Nat.not_le] at hsq
+      have := Nat.mul_lt_mul_of_lt_of_lt h hsq
+      replace : n * n < ((n / d) * d) * ((n / d) * d) := by grind
+      rw [Nat.dvd_iff_div_mul_eq] at hd
+      rw [hd] at this
+      grind
 
 theorem List.takeWhile_eq_filter {P : α → Bool} {xs : List α}
     (h : xs.Pairwise (fun x y => P y → P x)) :
@@ -97,16 +99,14 @@ theorem isPrime_eq_true_iff_isPrime {n : Nat} :
     isPrime n ↔ IsPrime n := by
   simp only [isPrime_eq_true_iff]
   by_cases hn : 2 ≤ n; rotate_left
-  · rw [ClosedOpen.toList_eq_nil_of_le (by grind)]
-    grind [IsPrime]
+  · grind [IsPrime]
   rw [List.takeWhile_eq_filter]; rotate_left
-  · apply Std.PRange.pairwise_toList_le.imp
+  · apply Std.Rco.pairwise_toList_le.imp
     intro a b hab hb
     have := Nat.mul_self_le_mul_self hab
     grind
-  simp [Std.PRange.mem_toList_iff_mem, Std.PRange.mem_iff_isSatisfied,
-    Std.PRange.SupportsLowerBound.IsSatisfied, Std.PRange.SupportsUpperBound.IsSatisfied,
-    isPrime_iff_mul_self]
+  -- `mem_toList_iff_mem` and `mem_iff` should be simp lemmas
+  simp [hn, isPrime_iff_mul_self, Std.Rco.mem_toList_iff_mem, Std.Rco.mem_iff]
 
 open Classical in
 theorem x_or_y_of_isPrime {n : Int} {x y : α} :

HumanEvalLean/HumanEval43.lean

@@ -138,17 +138,6 @@ def check(candidate):
 theorem List.exists_append (l : List α) (n : Nat) (h : n ≤ l.length) : ∃ xs ys, ys.length = n ∧ l = xs ++ ys :=
   ⟨l.take (l.length - n), l.drop (l.length - n), by grind, by simp⟩
 
-@[simp]
-theorem Std.HashSet.toList_emptyWithCapacity {α : Type u} [BEq α] [Hashable α]
-    [EquivBEq α] [LawfulHashable α] {n : Nat} :
-    (HashSet.emptyWithCapacity n : HashSet α).toList = [] := by
-  simp [← List.isEmpty_iff]
-
-@[simp]
-theorem Std.HashSet.toList_empty {α : Type u} [BEq α] [Hashable α]
-    [EquivBEq α] [LawfulHashable α] : (∅ : HashSet α).toList = [] := by
-  simp [← List.isEmpty_iff]
-
 theorem List.Any₂.append_left {P : α → α → Prop} (xs : List α) {ys : List α} (h : ys.Any₂ P) : (xs ++ ys).Any₂ P :=
   List.any₂_append.2 (by simp [h])
 

HumanEvalLean/HumanEval51.lean

@@ -14,7 +14,7 @@ def RemoveVowelsIff (solution : String → String) : Prop :=
     (s x : String) → (solution s = x) → MaximalFor (fun i => NoVowels i ∧ IsSubseq i s) (String.length) x
 
 def removeVowels (s : String) : String :=
-    String.mk (s.toList.filter (· ∉ vowels))
+    String.ofList (s.toList.filter (· ∉ vowels))
 
 example : removeVowels "abcdef" = "bcdf" := by native_decide
 example : removeVowels "abcdef\nghijklm" = "bcdf\nghjklm" := by native_decide
@@ -27,8 +27,8 @@ theorem IsSubseq.length_le {s t : String} (hst : IsSubseq s t) :
   List.Sublist.length_le hst
 
 theorem IsSubseq.removeVowels {s t : String} (hst : IsSubseq s t) :
-    IsSubseq (removeVowels s) (removeVowels t) :=
-  hst.filter _
+    IsSubseq (removeVowels s) (removeVowels t) := by
+  simpa [IsSubseq, _root_.removeVowels] using hst.filter _
 
 theorem removeVowels_eq_self {s : String} :
     removeVowels s = s ↔ NoVowels s := by

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-09-18
+leanprover/lean4-pr-releases:pr-release-11716