Merge remote-tracking branch 'origin/master' into markus/139-grind

Author: TwoFX

HumanEvalLean/HumanEval11.lean

@@ -1,5 +1,17 @@
-def string_xor : Unit :=
-  ()
+import Std.Data.Iterators
+
+def stringXor (a b : List Bool) : List Bool :=
+  ((a.iter).zip b.iter)
+    |>.map (fun p => Bool.xor p.1 p.2)
+    |>.toList
+
+@[simp, grind]
+theorem length_stringXor {a b : List Bool} : (stringXor a b).length = min a.length b.length := by
+  simp [stringXor]
+
+theorem getElem_stringXor {a b : List Bool} {i : Nat} {hia : i < a.length} {hib : i < b.length} :
+    (stringXor a b)[i]'(by grind) = Bool.xor a[i] b[i] := by
+  simp [stringXor]
 
 /-!
 ## Prompt
@@ -44,4 +56,4 @@ def check(candidate):
     assert candidate('1', '1') == '0'
     assert candidate('0101', '0000') == '0101'
 ```
--/
+-/

HumanEvalLean/HumanEval24.lean

@@ -32,7 +32,7 @@ theorem largestDivisorSpec_go {n i : Nat} (hi : 2 ≤ i)
   fun_induction largestDivisor.go n i
   case case1 i hni =>
     have := @Nat.mul_self_lt_mul_self_iff i
-    grind [LargestDivisorSpec.one]
+    exact LargestDivisorSpec.one (fun j hj hj' => hi' _ hj (Nat.mul_self_lt_mul_self_iff.1 (by grind)))
   case case2 i hni hni' =>
     grind [LargestDivisorSpec.div]
   case case3 i hni hni' ih =>

HumanEvalLean/HumanEval5.lean

@@ -1,5 +1,49 @@
-def intersperse : Unit :=
-  ()
+example : [].intersperse 7 = []                              := rfl
+example : [5, 6, 3, 2].intersperse 8 = [5, 8, 6, 8, 3, 8, 2] := rfl
+example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2]          := rfl
+
+open List
+
+/--
+info: List.length_intersperse.{u_1} {α : Type u_1} {l : List α} {sep : α} : (intersperse sep l).length = 2 * l.length - 1
+-/
+#guard_msgs in
+#check length_intersperse
+
+/--
+info: List.getElem?_intersperse_two_mul.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat} :
+  (intersperse sep l)[2 * i]? = l[i]?
+-/
+#guard_msgs in
+#check getElem?_intersperse_two_mul
+
+/--
+info: List.getElem?_intersperse_two_mul_add_one.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat} (h : i + 1 < l.length) :
+  (intersperse sep l)[2 * i + 1]? = some sep
+-/
+#guard_msgs in
+#check getElem?_intersperse_two_mul_add_one
+
+/--
+info: List.getElem_intersperse_two_mul.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat}
+  (h : 2 * i < (intersperse sep l).length) : (intersperse sep l)[2 * i] = l[i]
+-/
+#guard_msgs in
+#check getElem_intersperse_two_mul
+
+/--
+info: List.getElem_intersperse_two_mul_add_one.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat}
+  (h : 2 * i + 1 < (intersperse sep l).length) : (intersperse sep l)[2 * i + 1] = sep
+-/
+#guard_msgs in
+#check getElem_intersperse_two_mul_add_one
+
+/--
+info: List.getElem_eq_getElem_intersperse_two_mul.{u_1} {α : Type u_1} {l : List α} {sep : α} {i : Nat} (h : i < l.length) :
+  l[i] = (intersperse sep l)[2 * i]
+-/
+#guard_msgs in
+#check getElem_eq_getElem_intersperse_two_mul
 
 /-!
 ## Prompt

HumanEvalLean/HumanEval51.lean

@@ -1,5 +1,48 @@
-def remove_vowels : Unit :=
-  ()
+def IsSubseq (s₁ : String) (s₂ : String) : Prop :=
+  List.Sublist s₁.toList s₂.toList
+
+def vowels : List Char := ['a', 'e', 'i', 'o', 'u', 'A', 'E', 'I', 'O', 'U']
+
+def NoVowels (s : String) : Prop :=
+  List.all s.toList (· ∉ vowels)
+
+def MaximalFor [LE α] (P : ι → Prop) (f : ι → α) (x : ι) : Prop :=
+  -- Same as MaximalFor in Mathlib
+  P x ∧ ∀ y : ι, P y → f x ≤ f y → f y ≤ f x
+
+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))
+
+example : removeVowels "abcdef" = "bcdf" := by native_decide
+example : removeVowels "abcdef\nghijklm" = "bcdf\nghjklm" := by native_decide
+example : removeVowels "aaaaa" = "" := by native_decide
+example : removeVowels "aaBAA" = "B" := by native_decide
+example : removeVowels "zbcd" = "zbcd" := by native_decide
+
+theorem IsSubseq.length_le {s t : String} (hst : IsSubseq s t) :
+    s.length ≤ t.length :=
+  List.Sublist.length_le hst
+
+theorem IsSubseq.removeVowels {s t : String} (hst : IsSubseq s t) :
+    IsSubseq (removeVowels s) (removeVowels t) :=
+  hst.filter _
+
+theorem removeVowels_eq_self {s : String} :
+    removeVowels s = s ↔ NoVowels s := by
+  simp [String.ext_iff, NoVowels, removeVowels]
+
+theorem removeVowels_correct : RemoveVowelsIff removeVowels := by
+  simp [RemoveVowelsIff]
+  intro s
+  constructor
+  · simp [NoVowels, removeVowels, IsSubseq]
+  · simp only [and_imp]
+    intro y hnv hss hle
+    rw [← removeVowels_eq_self.2 hnv]
+    exact IsSubseq.length_le (IsSubseq.removeVowels hss)
 
 /-!
 ## Prompt
@@ -49,4 +92,4 @@ def check(candidate):
     assert candidate('ybcd') == 'ybcd'
 
 ```
--/
+-/

README.md

@@ -10,16 +10,21 @@ platform.
 ## Contributions
 
 Contributions are welcome! You can
-[look at the open issues](https://github.com/TwoFX/human-eval-lean/issues) to see
+[look at the table](https://github.com/users/TwoFX/projects/2/views/1) to see
 which problems do not currently have a solution.
 
 Feel free to add your thoughts about
 a problem to the corresponding issue. A rough estimation of the difficulty is already
 helpful; I will add the corresponding label to the issue.
 
-PRs contributing new solutions to both unsolved and solved problems are welcome,
-as are PRs improving the code of existing solutions. Golfing is welcome as long
-as the resulting code can still be considered idiomatic.
+We accept
+
+- PRs adding complete solutions to unsolved problems,
+- PRs adding additional solutions to problems which are already solved,
+- PRs adding partial solutions (for example just the code and the correctness statement, with the correctness proof sorried, or just developing a bit of related theory), and
+- PRs improving the code of existing solutions.
+
+Golfing is welcome as long as the resulting code can still be considered idiomatic.
 
 We use the [Lean 4 standard library style guide and naming convention](https://github.com/leanprover/lean4/tree/master/doc/std),
 but we won't be very strict about enforcing it.

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-25
+leanprover/lean4:nightly-2025-08-18