From 77c7568b2be4b50de36726769667282713cd9073 Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Thu, 1 May 2025 08:13:06 +0200 Subject: [PATCH 01/10] Add (partial) solution to HumanEval5 --- HumanEvalLean/HumanEval5.lean | 29 ++++++++++++++++++++++++++--- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean index 7ab1ada..492403c 100644 --- a/HumanEvalLean/HumanEval5.lean +++ b/HumanEvalLean/HumanEval5.lean @@ -1,5 +1,28 @@ -def intersperse : Unit := - () +def intersperse : List Int → Int → List Int + | [], _ => [] + | [i], _ => [i] + | i₁ :: i₂ :: tl, delim => i₁ :: delim :: intersperse (i₂ :: tl) delim + +example : intersperse [] 7 = [] := rfl +example : intersperse [5, 6, 3, 2] 8 = [5, 8, 6, 8, 3, 8, 2] := rfl +example : intersperse [2, 2, 2] 2 = [2, 2, 2, 2, 2] := rfl + +theorem intersperse_length_le : (intersperse nums delim).length ≤ 2 * nums.length - 1 := by + fun_induction intersperse <;> simp only [intersperse, List.length_cons] at * <;> omega + +-- Every element of index `2 * i` is the `i`th element of the input list. +theorem intersperse_get?_num (h : 1 < nums.length) : + (intersperse nums delim)[2 * i]? = nums[i]? := by + fun_induction intersperse generalizing i <;> try contradiction + next tl _ ih => + cases tl <;> cases i + case nil.succ j => + cases j <;> simp +arith [intersperse] + case cons.succ j => + have hj : 2 * (j + 1) = 2 * j + 2 := rfl + rw [intersperse, hj] + simp [ih] + all_goals simp [intersperse] /-! ## Prompt @@ -50,4 +73,4 @@ def check(candidate): assert candidate([5, 6, 3, 2], 8) == [5, 8, 6, 8, 3, 8, 2] assert candidate([2, 2, 2], 2) == [2, 2, 2, 2, 2] ``` --/ \ No newline at end of file +-/ From 38a452823e2689610f6f99a943fb9e72a11f574a Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Mon, 5 May 2025 19:23:15 +0200 Subject: [PATCH 02/10] Use `List.intersperse` --- HumanEvalLean/HumanEval5.lean | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean index 492403c..26f48fc 100644 --- a/HumanEvalLean/HumanEval5.lean +++ b/HumanEvalLean/HumanEval5.lean @@ -1,27 +1,27 @@ -def intersperse : List Int → Int → List Int - | [], _ => [] - | [i], _ => [i] - | i₁ :: i₂ :: tl, delim => i₁ :: delim :: intersperse (i₂ :: tl) delim +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 -example : intersperse [] 7 = [] := rfl -example : intersperse [5, 6, 3, 2] 8 = [5, 8, 6, 8, 3, 8, 2] := rfl -example : intersperse [2, 2, 2] 2 = [2, 2, 2, 2, 2] := rfl +namespace List -theorem intersperse_length_le : (intersperse nums delim).length ≤ 2 * nums.length - 1 := by - fun_induction intersperse <;> simp only [intersperse, List.length_cons] at * <;> omega +theorem intersperse_length_le (l : List α) : (l.intersperse delim).length ≤ 2 * l.length - 1 := by + fun_induction intersperse <;> simp only [intersperse, length_cons] at * <;> try omega + next h _ => + have := length_pos_iff.mpr h + omega -- Every element of index `2 * i` is the `i`th element of the input list. -theorem intersperse_get?_num (h : 1 < nums.length) : - (intersperse nums delim)[2 * i]? = nums[i]? := by +theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) : + (l.intersperse delim)[2 * i]? = l[i]? := by fun_induction intersperse generalizing i <;> try contradiction - next tl _ ih => + next hn ih => + have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn cases tl <;> cases i case nil.succ j => - cases j <;> simp +arith [intersperse] + cases j <;> simp +arith [hn, intersperse] case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl - rw [intersperse, hj] - simp [ih] + rw [intersperse, hj] <;> simp_all all_goals simp [intersperse] /-! From 3ac961c2d3e900ed9876a5d7ed5ee600fb016772 Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Mon, 5 May 2025 19:26:05 +0200 Subject: [PATCH 03/10] Simplify proof --- HumanEvalLean/HumanEval5.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean index 26f48fc..60dceb9 100644 --- a/HumanEvalLean/HumanEval5.lean +++ b/HumanEvalLean/HumanEval5.lean @@ -17,11 +17,8 @@ theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) : next hn ih => have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn cases tl <;> cases i - case nil.succ j => - cases j <;> simp +arith [hn, intersperse] - case cons.succ j => - have hj : 2 * (j + 1) = 2 * j + 2 := rfl - rw [intersperse, hj] <;> simp_all + case nil.succ j => cases j <;> simp_all +arith + case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all all_goals simp [intersperse] /-! From 6a07760da32236f98849e6fb196993d5e1770667 Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Mon, 5 May 2025 19:38:47 +0200 Subject: [PATCH 04/10] Add proof for odd case --- HumanEvalLean/HumanEval5.lean | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean index 60dceb9..3f705a7 100644 --- a/HumanEvalLean/HumanEval5.lean +++ b/HumanEvalLean/HumanEval5.lean @@ -4,7 +4,7 @@ example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2] := rfl namespace List -theorem intersperse_length_le (l : List α) : (l.intersperse delim).length ≤ 2 * l.length - 1 := by +theorem intersperse_length_le (l : List α) : (l.intersperse sep).length ≤ 2 * l.length - 1 := by fun_induction intersperse <;> simp only [intersperse, length_cons] at * <;> try omega next h _ => have := length_pos_iff.mpr h @@ -12,15 +12,25 @@ theorem intersperse_length_le (l : List α) : (l.intersperse delim).length ≤ 2 -- Every element of index `2 * i` is the `i`th element of the input list. theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) : - (l.intersperse delim)[2 * i]? = l[i]? := by + (l.intersperse sep)[2 * i]? = l[i]? := by fun_induction intersperse generalizing i <;> try contradiction - next hn ih => + next hn _ => have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn cases tl <;> cases i case nil.succ j => cases j <;> simp_all +arith case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all all_goals simp [intersperse] +-- Every element of index `2 * i + 1` is the separator element. +theorem intersperse_getElem?_odd {l : List α} (h₁ : 1 < l.length) (h₂ : i < l.length - 1) : + (l.intersperse sep)[2 * i + 1]? = sep := by + fun_induction intersperse generalizing i <;> try contradiction + next hn _ => + have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn + cases tl <;> cases i + case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all + all_goals simp_all + /-! ## Prompt From 52ffa4dd82c3a0ee223306a2df925f4a43482372 Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Mon, 5 May 2025 19:41:11 +0200 Subject: [PATCH 05/10] Gardening --- HumanEvalLean/HumanEval5.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean index 3f705a7..0ca381c 100644 --- a/HumanEvalLean/HumanEval5.lean +++ b/HumanEvalLean/HumanEval5.lean @@ -10,9 +10,10 @@ theorem intersperse_length_le (l : List α) : (l.intersperse sep).length ≤ 2 * have := length_pos_iff.mpr h omega +variable {l : List α} + -- Every element of index `2 * i` is the `i`th element of the input list. -theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) : - (l.intersperse sep)[2 * i]? = l[i]? := by +theorem intersperse_getElem?_even (h : 1 < l.length) : (l.intersperse sep)[2 * i]? = l[i]? := by fun_induction intersperse generalizing i <;> try contradiction next hn _ => have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn @@ -22,7 +23,7 @@ theorem intersperse_getElem?_even {l : List α} (h : 1 < l.length) : all_goals simp [intersperse] -- Every element of index `2 * i + 1` is the separator element. -theorem intersperse_getElem?_odd {l : List α} (h₁ : 1 < l.length) (h₂ : i < l.length - 1) : +theorem intersperse_getElem?_odd (h₁ : 1 < l.length) (h₂ : i < l.length - 1) : (l.intersperse sep)[2 * i + 1]? = sep := by fun_induction intersperse generalizing i <;> try contradiction next hn _ => From c7516756da6dfff0bb7c3e610363042c14845f4b Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Tue, 6 May 2025 13:12:56 +0200 Subject: [PATCH 06/10] Turn < into = --- HumanEvalLean/HumanEval5.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean index 0ca381c..37e6d63 100644 --- a/HumanEvalLean/HumanEval5.lean +++ b/HumanEvalLean/HumanEval5.lean @@ -4,11 +4,9 @@ example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2] := rfl namespace List -theorem intersperse_length_le (l : List α) : (l.intersperse sep).length ≤ 2 * l.length - 1 := by - fun_induction intersperse <;> simp only [intersperse, length_cons] at * <;> try omega - next h _ => - have := length_pos_iff.mpr h - omega +theorem intersperse_length (l : List α) : (l.intersperse sep).length = 2 * l.length - 1 := by + fun_induction intersperse <;> simp only [intersperse, length_cons, length_nil] at * <;> try omega + next h _ => have := length_pos_iff.mpr h; omega variable {l : List α} From ddadf48d2843e8eefb64ffafb931eb89018b945b Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Tue, 6 May 2025 14:06:14 +0200 Subject: [PATCH 07/10] Rename theorem --- HumanEvalLean/HumanEval5.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean index 37e6d63..2e1093d 100644 --- a/HumanEvalLean/HumanEval5.lean +++ b/HumanEvalLean/HumanEval5.lean @@ -4,7 +4,7 @@ example : [2, 2, 2].intersperse 2 = [2, 2, 2, 2, 2] := rfl namespace List -theorem intersperse_length (l : List α) : (l.intersperse sep).length = 2 * l.length - 1 := by +theorem length_intersperse (l : List α) : (l.intersperse sep).length = 2 * l.length - 1 := by fun_induction intersperse <;> simp only [intersperse, length_cons, length_nil] at * <;> try omega next h _ => have := length_pos_iff.mpr h; omega From 08dc3d3331924e391b572f9d1818eaaba3b4497a Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Wed, 14 May 2025 17:38:39 +0200 Subject: [PATCH 08/10] Use Lean's theorems --- HumanEvalLean/HumanEval5.lean | 35 ++++++++--------------------------- 1 file changed, 8 insertions(+), 27 deletions(-) diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean index 2e1093d..605d7ef 100644 --- a/HumanEvalLean/HumanEval5.lean +++ b/HumanEvalLean/HumanEval5.lean @@ -2,33 +2,14 @@ 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 -namespace List - -theorem length_intersperse (l : List α) : (l.intersperse sep).length = 2 * l.length - 1 := by - fun_induction intersperse <;> simp only [intersperse, length_cons, length_nil] at * <;> try omega - next h _ => have := length_pos_iff.mpr h; omega - -variable {l : List α} - --- Every element of index `2 * i` is the `i`th element of the input list. -theorem intersperse_getElem?_even (h : 1 < l.length) : (l.intersperse sep)[2 * i]? = l[i]? := by - fun_induction intersperse generalizing i <;> try contradiction - next hn _ => - have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn - cases tl <;> cases i - case nil.succ j => cases j <;> simp_all +arith - case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all - all_goals simp [intersperse] - --- Every element of index `2 * i + 1` is the separator element. -theorem intersperse_getElem?_odd (h₁ : 1 < l.length) (h₂ : i < l.length - 1) : - (l.intersperse sep)[2 * i + 1]? = sep := by - fun_induction intersperse generalizing i <;> try contradiction - next hn _ => - have ⟨_, tl, hn⟩ := ne_nil_iff_exists_cons.mp hn - cases tl <;> cases i - case cons.succ j => have hj : 2 * (j + 1) = 2 * j + 2 := rfl; simp_all - all_goals simp_all +open List + +#check length_intersperse +#check getElem?_intersperse_two_mul +#check getElem?_intersperse_two_mul_add_one +#check getElem_intersperse_two_mul +#check getElem_intersperse_two_mul_add_one +#check getElem_eq_getElem_intersperse_two_mul /-! ## Prompt From 871954bb026bf7d026a23127ced3dc592e848c2c Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Tue, 3 Jun 2025 20:51:19 +0200 Subject: [PATCH 09/10] Update to Lean v4.21.0-rc2 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index b2153cd..2ed974a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.18.0 +leanprover/lean4:v4.21.0-rc2 From a5eb9f91896038868d583d61f92931adf9f16112 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 1 Jul 2025 08:20:35 +0200 Subject: [PATCH 10/10] Silence output --- HumanEvalLean/HumanEval5.lean | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/HumanEvalLean/HumanEval5.lean b/HumanEvalLean/HumanEval5.lean index 605d7ef..2450881 100644 --- a/HumanEvalLean/HumanEval5.lean +++ b/HumanEvalLean/HumanEval5.lean @@ -4,11 +4,45 @@ 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 /-!