Merge remote-tracking branch 'origin/master' into markus/11

Author: TwoFX

HumanEvalLean/HumanEval139.lean

@@ -1,5 +1,61 @@
-def special_factorial : Unit :=
-  ()
+-- from Mathlib
+def Nat.factorial : Nat → Nat
+  | 0 => 1
+  | .succ n => Nat.succ n * factorial n
+
+notation:10000 n "!" => Nat.factorial n
+
+@[simp] theorem Nat.factorial_zero : 0! = 1 :=
+  rfl
+
+theorem Nat.factorial_succ (n : Nat) : (n + 1)! = (n + 1) * n ! :=
+  rfl
+
+def Nat.brazilianFactorial : Nat → Nat
+  | .zero => 1
+  | .succ n => (Nat.succ n)! * brazilianFactorial n
+
+@[simp] theorem Nat.brazilianFactorial_zero : brazilianFactorial 0 = 1 :=
+  rfl
+
+theorem Nat.brazilianFactorial_succ (n : Nat) : brazilianFactorial (n + 1) = (n + 1)! * (brazilianFactorial n) :=
+  rfl
+
+def special_factorial (n : Nat) : Nat :=
+  special_factorial.go n 1 1 0
+where
+  go (n fact brazilFact curr : Nat) : Nat :=
+    if _h: curr >= n
+    then brazilFact
+    else
+      let fact' := (curr + 1) * fact
+      let brazilFact' := fact' * brazilFact
+      special_factorial.go n fact' brazilFact' (Nat.succ curr)
+  termination_by n - curr
+
+theorem special_factorial_func_correct {n : Nat} :
+    special_factorial n = n.brazilianFactorial := by
+  simp [special_factorial]
+  suffices ∀ (curr fact brazilFact : Nat), fact = curr ! → brazilFact = curr.brazilianFactorial →
+    curr ≤ n → special_factorial.go n fact brazilFact curr = n.brazilianFactorial by
+      apply this
+      · simp [Nat.factorial]
+      · simp [Nat.brazilianFactorial]
+      · simp
+  intro curr fact brazil_fact h₁ h₂ h₃
+  fun_induction special_factorial.go with
+  | case1 fact brazil_fact curr h =>
+    rw [h₂, (show curr = n by omega)]
+  | case2 fact brazilFact curr h fact' brazilFact' ih =>
+    simp only [ge_iff_le, Nat.not_le] at h
+    simp only [h₁, Nat.succ_eq_add_one, Nat.factorial_succ, h₂, Nat.brazilianFactorial_succ,
+      Nat.succ_le_of_lt h, forall_const, fact', brazilFact'] at ih
+    simp only [← ih, fact', h₁, brazilFact', h₂]
+
+theorem test1 : special_factorial 4 = 288 := by native_decide
+theorem test2 : special_factorial 5 = 34560 := by native_decide
+theorem test3 : special_factorial 7 = 125411328000 := by native_decide
+theorem test4 : special_factorial 1 = 1 := by native_decide
 
 /-!
 ## Prompt
@@ -45,4 +101,4 @@ def check(candidate):
     assert candidate(1) == 1, "Test 1"
 
 ```
--/
+-/

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-11
+leanprover/lean4:nightly-2025-06-11