From 4dee5cf3e9ec4949ec48507e0dd2859dbdb08b3b Mon Sep 17 00:00:00 2001 From: jt0202 Date: Mon, 5 May 2025 22:12:32 +0200 Subject: [PATCH 01/14] Left shift theory --- HumanEvalLean/HumanEval109.lean | 155 ++++++++++++++++++++++++++++++-- 1 file changed, 146 insertions(+), 9 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 902b37e..dbc4ec0 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -1,5 +1,142 @@ -def move_one_ball : Unit := - () +variable {α : Type _} + +def leftShift (l : List α) (n : Nat) : List α := + match n with + | .zero => l + | .succ m => + match l with + | .nil => [] + | .cons hd tl => leftShift (tl ++ [hd]) m + +@[simp] +theorem leftShift_zero {l : List α} : + leftShift l 0 = l := rfl + +@[simp] +theorem leftShift_nil {n : Nat} : + leftShift ([] : List α) n = [] := by + cases n <;> simp [leftShift] + +@[simp] +theorem leftShift_cons_one {hd : α} {tl : List α} : + leftShift (hd::tl) 1 = tl ++ [hd] := rfl + +theorem leftShift_of_le_length {l : List α} {n : Nat} (h : n ≤ l.length) : + leftShift l n = l.drop n ++ l.take n := by + induction n generalizing l with + | zero => simp + | succ m ih => + have : m ≤ l.length := by + apply Nat.le_of_succ_le h + cases l with + | nil => simp + | cons hd tl => + simp [leftShift] + rw [ih] + · simp only [List.length_cons, Nat.add_le_add_iff_right] at h + simp [List.drop_append_of_le_length h, List.take_append_of_le_length h] + · simpa + +theorem leftShift_add_one {l : List α} {n1 : Nat} : + leftShift l (n1 + 1) = leftShift (leftShift l n1) 1 := by + induction n1 generalizing l with + | zero => simp + | succ m ih => + cases l with + | nil => simp + | cons hd tl => + conv => + lhs + unfold leftShift -- prevent multiple unfolding + simp + rw [ih] + have : leftShift (hd :: tl) (m + 1) = leftShift (tl ++ [hd]) m := by + conv => + lhs + simp [leftShift] + rw [this] + +theorem leftShift_add {l : List α} {n1 n2 : Nat} : + leftShift l (n1 + n2) = leftShift (leftShift l n1) n2 := by + induction n2 with + | zero => simp + | succ m ih => + simp [← Nat.add_assoc, leftShift_add_one, ih] + +theorem leftShift_mul_length_eq_self {l : List α} {k : Nat}: + leftShift l (k * l.length) = l := by + induction k with + | zero => simp + | succ m ih => + simp only [Nat.add_mul, Nat.one_mul, leftShift_add, ih] + rw [leftShift_of_le_length (by omega)] + simp + +@[simp] +theorem isEmpty_leftShift_eq_isEmpty (l : List α) (n : Nat) : + (leftShift l n).isEmpty = l.isEmpty := by + induction n generalizing l with + | zero => simp [leftShift] + | succ m ih => + cases l with + | nil => simp [leftShift] + | cons hd tl => + simp [leftShift, ih] + +theorem Nat.exists_eq_mul_mod (n m : Nat) : + ∃ k, n = k * m + n % m := by + exists (n - n % m)/m + sorry + -- currently only in nightly + --rw [← Nat.div_eq_sub_mod_div] + + +theorem leftShift_eq_leftShift_mod_length (l : List α) (n : Nat) : + leftShift l n = leftShift l (n % l.length) := by + have := Nat.exists_eq_mul_mod n l.length + rcases this with ⟨k, hk⟩ + conv => + lhs + rw [hk, leftShift_add, leftShift_mul_length_eq_self] + +def isleftShiftOf (l l' : List α) : Prop := ∃ (n : Nat), l' = leftShift l n + +theorem isleftShiftOf_iff_exists (l l' : List α) : + isleftShiftOf l l' ↔ ∃ (u v : List α), l = u ++ v ∧ l' = v ++ u := by + simp [isleftShiftOf] + by_cases hl : l = [] + · simp [hl] + constructor + · intro h + exists [] + exists [] + · intro h + rcases h with ⟨u,v, huv, h⟩ + simp [h, huv] + · constructor + · intro h' + rcases h' with ⟨n , h⟩ + rw [leftShift_eq_leftShift_mod_length] at h + rw [leftShift_of_le_length] at h + · exists (l.take (n % l.length)) + exists (l.drop (n % l.length)) + refine And.intro ?_ h + exact Eq.symm (List.take_append_drop (n % l.length) l) + · apply Nat.le_of_lt + apply Nat.mod_lt + exact List.length_pos_iff.mpr hl + · intro h' + rcases h' with ⟨u, v, h, h'⟩ + exists u.length + simp [h, h', leftShift_of_le_length] + + +def move_one_ball (l : List Int) : Bool := + sorry + +theorem move_one_ball_correct_iff (l : List Int) : + move_one_ball l = true ↔ ∃ (l' : List Int), isleftShiftOf l l' ∧ List.Pairwise (fun (a b : Int) => a ≤ b) l' := by + sorry /-! ## Prompt @@ -9,13 +146,13 @@ def move_one_ball : Unit := def move_one_ball(arr): """We have an array 'arr' of N integers arr[1], arr[2], ..., arr[N].The numbers in the array will be randomly ordered. Your task is to determine if - it is possible to get an array sorted in non-decreasing order by performing + it is possible to get an array sorted in non-decreasing order by performing the following operation on the given array: You are allowed to perform right shift operation any number of times. - + One right shift operation means shifting all elements of the array by one position in the right direction. The last element of the array will be moved to - the starting position in the array i.e. 0th index. + the starting position in the array i.e. 0th index. If it is possible to obtain the sorted array by performing the above operation then return True else return False. @@ -24,14 +161,14 @@ def move_one_ball(arr): Note: The given list is guaranteed to have unique elements. For Example: - + move_one_ball([3, 4, 5, 1, 2])==>True Explanation: By performin 2 right shift operations, non-decreasing order can be achieved for the given array. move_one_ball([3, 5, 4, 1, 2])==>False Explanation:It is not possible to get non-decreasing order for the given array by performing any number of right shift operations. - + """ ``` @@ -42,7 +179,7 @@ def move_one_ball(arr): return True sorted_array=sorted(arr) my_arr=[] - + min_value=min(arr) min_index=arr.index(min_value) my_arr=arr[min_index:]+arr[0:min_index] @@ -65,4 +202,4 @@ def check(candidate): assert candidate([3, 5, 4, 1, 2])==False, "This prints if this assert fails 2 (also good for debugging!)" assert candidate([])==True ``` --/ \ No newline at end of file +-/ From 4b3989705c6e6326d4e4fecbec3c649e13ead3aa Mon Sep 17 00:00:00 2001 From: jt0202 Date: Tue, 6 May 2025 20:42:40 +0200 Subject: [PATCH 02/14] Algorithm --- HumanEvalLean/HumanEval109.lean | 188 ++++++++++++++++++++++++++++++-- lean-toolchain | 2 +- 2 files changed, 181 insertions(+), 9 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index dbc4ec0..0297cd1 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -31,7 +31,7 @@ theorem leftShift_of_le_length {l : List α} {n : Nat} (h : n ≤ l.length) : cases l with | nil => simp | cons hd tl => - simp [leftShift] + simp only [leftShift, List.drop_succ_cons, List.take_succ_cons] rw [ih] · simp only [List.length_cons, Nat.add_le_add_iff_right] at h simp [List.drop_append_of_le_length h, List.take_append_of_le_length h] @@ -86,10 +86,8 @@ theorem isEmpty_leftShift_eq_isEmpty (l : List α) (n : Nat) : theorem Nat.exists_eq_mul_mod (n m : Nat) : ∃ k, n = k * m + n % m := by exists (n - n % m)/m - sorry - -- currently only in nightly - --rw [← Nat.div_eq_sub_mod_div] - + rw [← Nat.div_eq_sub_mod_div] + rw [div_add_mod'] theorem leftShift_eq_leftShift_mod_length (l : List α) (n : Nat) : leftShift l n = leftShift l (n % l.length) := by @@ -130,13 +128,187 @@ theorem isleftShiftOf_iff_exists (l l' : List α) : exists u.length simp [h, h', leftShift_of_le_length] +def countBreakPointsAndGetEnd (l : List Int) (hl : l ≠ []) : Nat × Int := + go l 0 hl where + go (l : List Int) (curr : Nat) (hl : l ≠ []) : Nat × Int := + match l with + | .nil => by simp at hl + | .cons hd tl => + match tl with + | .nil => (curr, hd) + | .cons hd' tl' => + if hd < hd' + then go (hd' :: tl') curr (by simp) + else go (hd' :: tl') (curr + 1) (by simp) + +theorem countBreakPointsAndGetEndGoIncreasing (l : List Int) (curr : Nat) (hl : l ≠ []) : + (countBreakPointsAndGetEnd.go l curr hl).fst ≥ curr := by + induction l generalizing curr with + | nil => simp at hl + | cons hd tl ih => + cases tl with + | nil => simp [countBreakPointsAndGetEnd.go] + | cons hd' tl' => + simp only [countBreakPointsAndGetEnd.go, ge_iff_le] + split + · apply ih + · specialize ih (curr + 1) (by simp) + apply Nat.le_trans ?_ ih + simp + +theorem countBreakPointsAndGetEnd_fst_eq_zero_iff_sorted (l : List Int) (hl : l ≠ []) : + (countBreakPointsAndGetEnd l hl).fst = 0 ↔ List.Pairwise (fun (a b : Int) => a < b) l := by + simp [countBreakPointsAndGetEnd] + induction l with + | nil => simp at hl + | cons hd tl ih => + cases tl with + | nil => simp [countBreakPointsAndGetEnd.go] + | cons hd' tl' => + simp only [countBreakPointsAndGetEnd.go, Nat.zero_add, List.pairwise_cons, List.mem_cons, + forall_eq_or_imp] + simp only [ne_eq, reduceCtorEq, not_false_eq_true, List.pairwise_cons] at ih + split + · rename_i hhd + rw [ih True.intro] + simp only [hhd, true_and, iff_and_self, and_imp] + intro h₁ _ x hx + apply Int.lt_trans hhd (h₁ x hx) + · rename_i hhd + simp only [hhd, false_and, iff_false] + intro h + have := countBreakPointsAndGetEndGoIncreasing (hd' :: tl') 1 (by simp) + simp [h] at this + +def countGlobalBreakPoints (l : List Int) : Nat := + if h : l.length < 2 + then 0 + else + have : l ≠ [] := by + rw [List.ne_nil_iff_length_pos] + simp at h + exact Nat.zero_lt_of_lt h + let (count, listEnd) := countBreakPointsAndGetEnd l this + let start := l.head this + + if start < listEnd + then count + 1 + else count + +theorem countBreakPointsAndGetEnd_fst_eq_zero_of_countGlobalBreakPoints + {l : List Int} (hl : l ≠ []) (h : countGlobalBreakPoints l = 0) : + (countBreakPointsAndGetEnd l hl).fst = 0 := by + cases l with + | nil => simp at hl + | cons hd tl => + cases tl with + | nil => rfl + | cons hd' tl' => + simp [countGlobalBreakPoints] at h + specialize h True.intro + split at h + · simp at h + · exact h + +theorem countGlobalBreakPoints_of_countBreakPointsAndGetEnd {l : List Int} {hl : l ≠ []} {n : Nat} + (h : (countBreakPointsAndGetEnd l hl).fst = n) : + countGlobalBreakPoints l = n ∨ countGlobalBreakPoints l = n + 1 := by + cases l with + | nil => simp at hl + | cons hd tl => + cases tl with + | nil => + simp [countBreakPointsAndGetEnd, countBreakPointsAndGetEnd.go] at h + simpa [countGlobalBreakPoints] + | cons hd' tl' => + simp [countGlobalBreakPoints, h] + split + · rename_i htl + false_or_by_contra + revert htl + simp + · split <;> simp + +theorem countGlobalBreakPoints_leftShift_eq (l : List Int) (hl : l ≠ []) (n : Nat) : + countGlobalBreakPoints (leftShift l n) = countGlobalBreakPoints l := by + induction n generalizing l with + | zero => simp + | succ m ih => + simp [leftShift] + cases l with + | nil => simp + | cons hd tl => + simp + rw [ih _ (by simp)] + sorry def move_one_ball (l : List Int) : Bool := - sorry + countGlobalBreakPoints l ≤ 1 theorem move_one_ball_correct_iff (l : List Int) : - move_one_ball l = true ↔ ∃ (l' : List Int), isleftShiftOf l l' ∧ List.Pairwise (fun (a b : Int) => a ≤ b) l' := by - sorry + move_one_ball l = true ↔ + ∃ (l' : List Int), isleftShiftOf l l' ∧ List.Pairwise (fun (a b : Int) => a < b) l' := by + simp [move_one_ball, Nat.le_succ_iff] + by_cases hl: l.length < 2 + · simp [countGlobalBreakPoints, hl] + exists l + simp [isleftShiftOf] + constructor + · exists 0 + · cases l with + | nil => simp + | cons hd tl => + cases tl with + | nil => simp + | cons hd' tl' => + simp at hl + omega + · have hl' : l ≠ [] := by + apply List.ne_nil_of_length_pos + simp at hl + exact Nat.zero_lt_of_lt hl + constructor + · intro h + cases h with + | inl h => + exists l + simp [isleftShiftOf] + have := countBreakPointsAndGetEnd_fst_eq_zero_of_countGlobalBreakPoints hl' h + rw [countBreakPointsAndGetEnd_fst_eq_zero_iff_sorted] at this + refine And.intro ?_ this + exists 0 + | inr h => + simp [countGlobalBreakPoints, hl] at h + split at h + · simp at h + exists l + rw [countBreakPointsAndGetEnd_fst_eq_zero_iff_sorted] at h + refine And.intro ?_ h + simp [isleftShiftOf] + exists 0 + · sorry + · false_or_by_contra + rename_i h h' + simp at h' + rcases h with ⟨l', hshift, hsort⟩ + simp [isleftShiftOf] at hshift + rcases hshift with ⟨n, hshift⟩ + have leftShift_ne_nil : leftShift l n ≠ [] := by + rw [ne_eq, ← List.isEmpty_iff] + simpa + rw [hshift, ← countBreakPointsAndGetEnd_fst_eq_zero_iff_sorted _ leftShift_ne_nil] at hsort + simp [← countGlobalBreakPoints_leftShift_eq l hl' n] at h' + have := countGlobalBreakPoints_of_countBreakPointsAndGetEnd hsort + simp at this + cases this with + | inl this => simp [this] at h' + | inr this => simp [this] at h' + +theorem testCase1 : move_one_ball [3,4,5,1,2] = True := by native_decide +theorem testCase2 : move_one_ball [3,5,10,1,2] = True := by native_decide +theorem testCase3 : move_one_ball [4,3,1,2] = False := by native_decide +theorem testCase4 : move_one_ball [3,5,4,1,2] = False := by native_decide +theorem testCase5 : move_one_ball [] = True := by native_decide /-! ## Prompt diff --git a/lean-toolchain b/lean-toolchain index 7aca1d8..6625aac 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.19.0 +leanprover/lean4:v4.20.0-rc4 From fe8aa770319ff7ce0cf276e4b25c61ec00b21fa2 Mon Sep 17 00:00:00 2001 From: jt0202 Date: Wed, 7 May 2025 22:06:35 +0200 Subject: [PATCH 03/14] Next try --- HumanEvalLean/HumanEval109.lean | 445 ++++++++++++-------------------- 1 file changed, 158 insertions(+), 287 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 0297cd1..ef733f9 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -1,308 +1,153 @@ variable {α : Type _} -def leftShift (l : List α) (n : Nat) : List α := - match n with - | .zero => l - | .succ m => - match l with - | .nil => [] - | .cons hd tl => leftShift (tl ++ [hd]) m +section helper -@[simp] -theorem leftShift_zero {l : List α} : - leftShift l 0 = l := rfl - -@[simp] -theorem leftShift_nil {n : Nat} : - leftShift ([] : List α) n = [] := by - cases n <;> simp [leftShift] - -@[simp] -theorem leftShift_cons_one {hd : α} {tl : List α} : - leftShift (hd::tl) 1 = tl ++ [hd] := rfl - -theorem leftShift_of_le_length {l : List α} {n : Nat} (h : n ≤ l.length) : - leftShift l n = l.drop n ++ l.take n := by - induction n generalizing l with - | zero => simp - | succ m ih => - have : m ≤ l.length := by - apply Nat.le_of_succ_le h - cases l with - | nil => simp - | cons hd tl => - simp only [leftShift, List.drop_succ_cons, List.take_succ_cons] - rw [ih] - · simp only [List.length_cons, Nat.add_le_add_iff_right] at h - simp [List.drop_append_of_le_length h, List.take_append_of_le_length h] - · simpa - -theorem leftShift_add_one {l : List α} {n1 : Nat} : - leftShift l (n1 + 1) = leftShift (leftShift l n1) 1 := by - induction n1 generalizing l with - | zero => simp - | succ m ih => - cases l with - | nil => simp - | cons hd tl => - conv => - lhs - unfold leftShift -- prevent multiple unfolding - simp - rw [ih] - have : leftShift (hd :: tl) (m + 1) = leftShift (tl ++ [hd]) m := by - conv => - lhs - simp [leftShift] - rw [this] - -theorem leftShift_add {l : List α} {n1 n2 : Nat} : - leftShift l (n1 + n2) = leftShift (leftShift l n1) n2 := by - induction n2 with +theorem Nat.lt_two_iff {n : Nat} : n < 2 ↔ n = 0 ∨ n = 1 := by + cases n with | zero => simp - | succ m ih => - simp [← Nat.add_assoc, leftShift_add_one, ih] + | succ m => + cases m with + | zero => simp + | succ o => simp -theorem leftShift_mul_length_eq_self {l : List α} {k : Nat}: - leftShift l (k * l.length) = l := by - induction k with - | zero => simp - | succ m ih => - simp only [Nat.add_mul, Nat.one_mul, leftShift_add, ih] - rw [leftShift_of_le_length (by omega)] +theorem List.sum_eq_zero {l : List Nat} : l.sum = 0 ↔ ∀ x ∈ l, x = 0 := by + induction l with + | nil => simp + | cons hd tl ih => simp + intro _ + exact ih -@[simp] -theorem isEmpty_leftShift_eq_isEmpty (l : List α) (n : Nat) : - (leftShift l n).isEmpty = l.isEmpty := by - induction n generalizing l with - | zero => simp [leftShift] - | succ m ih => - cases l with - | nil => simp [leftShift] - | cons hd tl => - simp [leftShift, ih] - -theorem Nat.exists_eq_mul_mod (n m : Nat) : - ∃ k, n = k * m + n % m := by - exists (n - n % m)/m - rw [← Nat.div_eq_sub_mod_div] - rw [div_add_mod'] - -theorem leftShift_eq_leftShift_mod_length (l : List α) (n : Nat) : - leftShift l n = leftShift l (n % l.length) := by - have := Nat.exists_eq_mul_mod n l.length - rcases this with ⟨k, hk⟩ - conv => - lhs - rw [hk, leftShift_add, leftShift_mul_length_eq_self] - -def isleftShiftOf (l l' : List α) : Prop := ∃ (n : Nat), l' = leftShift l n - -theorem isleftShiftOf_iff_exists (l l' : List α) : - isleftShiftOf l l' ↔ ∃ (u v : List α), l = u ++ v ∧ l' = v ++ u := by - simp [isleftShiftOf] - by_cases hl : l = [] - · simp [hl] +theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i < l.length), + l[i] = 1 ∧ ∀ (j : Nat) (hj : j < l.length), i ≠ j → l[j] = 0 := by + induction l with + | nil => simp + | cons hd tl ih => + simp [Nat.add_eq_one_iff] constructor · intro h - exists [] - exists [] - · intro h - rcases h with ⟨u,v, huv, h⟩ - simp [h, huv] - · constructor - · intro h' - rcases h' with ⟨n , h⟩ - rw [leftShift_eq_leftShift_mod_length] at h - rw [leftShift_of_le_length] at h - · exists (l.take (n % l.length)) - exists (l.drop (n % l.length)) - refine And.intro ?_ h - exact Eq.symm (List.take_append_drop (n % l.length) l) - · apply Nat.le_of_lt - apply Nat.mod_lt - exact List.length_pos_iff.mpr hl - · intro h' - rcases h' with ⟨u, v, h, h'⟩ - exists u.length - simp [h, h', leftShift_of_le_length] - -def countBreakPointsAndGetEnd (l : List Int) (hl : l ≠ []) : Nat × Int := - go l 0 hl where - go (l : List Int) (curr : Nat) (hl : l ≠ []) : Nat × Int := - match l with - | .nil => by simp at hl - | .cons hd tl => - match tl with - | .nil => (curr, hd) - | .cons hd' tl' => - if hd < hd' - then go (hd' :: tl') curr (by simp) - else go (hd' :: tl') (curr + 1) (by simp) - -theorem countBreakPointsAndGetEndGoIncreasing (l : List Int) (curr : Nat) (hl : l ≠ []) : - (countBreakPointsAndGetEnd.go l curr hl).fst ≥ curr := by - induction l generalizing curr with - | nil => simp at hl - | cons hd tl ih => - cases tl with - | nil => simp [countBreakPointsAndGetEnd.go] - | cons hd' tl' => - simp only [countBreakPointsAndGetEnd.go, ge_iff_le] - split - · apply ih - · specialize ih (curr + 1) (by simp) - apply Nat.le_trans ?_ ih + cases h with + | inl h => + rcases h with ⟨hl, hr⟩ + rw [ih] at hr + rcases hr with ⟨i, hi, h⟩ + exists (i + 1) simp - -theorem countBreakPointsAndGetEnd_fst_eq_zero_iff_sorted (l : List Int) (hl : l ≠ []) : - (countBreakPointsAndGetEnd l hl).fst = 0 ↔ List.Pairwise (fun (a b : Int) => a < b) l := by - simp [countBreakPointsAndGetEnd] + constructor + · exists hi + simp [h] + · intro j hj hij + cases j with + | zero => simp[hl] + | succ k => + simp + apply (And.right h) + simp at hij + assumption + | inr h => + exists 0 + simp [h] + rw [sum_eq_zero] at h + intro j hj hij + cases j with + | zero => simp at hij + | succ k => + simp + rcases h with ⟨_, h⟩ + apply h + simp + · intro h + rcases h with ⟨i, hi, h⟩ + cases i with + | zero => + right + simp at hi + simp [hi] + rw [List.sum_eq_zero] + intro x hx + rw [List.mem_iff_getElem] at hx + rcases hx with ⟨k, hk, tlk⟩ + specialize h (k + 1) + simp at h + rw [← tlk] + apply h hk + | succ k => + simp at hi + left + constructor + · specialize h 0 + simp at h + assumption + · rw [ih] + exists k + rcases hi with ⟨hk, tlk⟩ + exists hk + simp [tlk] + intro j hj hkj + specialize h (j + 1) + simp at h + apply h hj hkj + +theorem List.Pairwise_lt_of_forall_neighbor (l : List Int) + (h : ∀ (i : Nat) (hi : i + 1 < l.length), l[i] < l[i+1]) : + List.Pairwise (fun (a b : Int) => a < b) l := by induction l with - | nil => simp at hl + | nil => simp | cons hd tl ih => - cases tl with - | nil => simp [countBreakPointsAndGetEnd.go] - | cons hd' tl' => - simp only [countBreakPointsAndGetEnd.go, Nat.zero_add, List.pairwise_cons, List.mem_cons, - forall_eq_or_imp] - simp only [ne_eq, reduceCtorEq, not_false_eq_true, List.pairwise_cons] at ih - split - · rename_i hhd - rw [ih True.intro] - simp only [hhd, true_and, iff_and_self, and_imp] - intro h₁ _ x hx - apply Int.lt_trans hhd (h₁ x hx) - · rename_i hhd - simp only [hhd, false_and, iff_false] - intro h - have := countBreakPointsAndGetEndGoIncreasing (hd' :: tl') 1 (by simp) - simp [h] at this - -def countGlobalBreakPoints (l : List Int) : Nat := - if h : l.length < 2 - then 0 + simp + + + +end helper + + +def rightShift (l : List α) (n : Nat) := + l.drop (l.length - n) ++ l.take (l.length - n) + +theorem rightShiftExample : rightShift [3,4,5,1,2] 2 = [1,2,3,4,5] := by native_decide + +@[simp] +theorem rightShift_zero {l : List α} : rightShift l 0 = l := by + simp [rightShift] + +def isBreakPoint (l : List Int) (pos : Nat) (h : pos < l.length) := + if h:pos + 1 < l.length + then + if l[pos] < l[pos + 1] + then 0 + else 1 else - have : l ≠ [] := by - rw [List.ne_nil_iff_length_pos] - simp at h - exact Nat.zero_lt_of_lt h - let (count, listEnd) := countBreakPointsAndGetEnd l this - let start := l.head this - - if start < listEnd - then count + 1 - else count - -theorem countBreakPointsAndGetEnd_fst_eq_zero_of_countGlobalBreakPoints - {l : List Int} (hl : l ≠ []) (h : countGlobalBreakPoints l = 0) : - (countBreakPointsAndGetEnd l hl).fst = 0 := by - cases l with - | nil => simp at hl - | cons hd tl => - cases tl with - | nil => rfl - | cons hd' tl' => - simp [countGlobalBreakPoints] at h - specialize h True.intro - split at h - · simp at h - · exact h - -theorem countGlobalBreakPoints_of_countBreakPointsAndGetEnd {l : List Int} {hl : l ≠ []} {n : Nat} - (h : (countBreakPointsAndGetEnd l hl).fst = n) : - countGlobalBreakPoints l = n ∨ countGlobalBreakPoints l = n + 1 := by - cases l with - | nil => simp at hl - | cons hd tl => - cases tl with - | nil => - simp [countBreakPointsAndGetEnd, countBreakPointsAndGetEnd.go] at h - simpa [countGlobalBreakPoints] - | cons hd' tl' => - simp [countGlobalBreakPoints, h] - split - · rename_i htl - false_or_by_contra - revert htl - simp - · split <;> simp + if l[pos] > l[0] + then 1 + else 0 -theorem countGlobalBreakPoints_leftShift_eq (l : List Int) (hl : l ≠ []) (n : Nat) : - countGlobalBreakPoints (leftShift l n) = countGlobalBreakPoints l := by - induction n generalizing l with - | zero => simp - | succ m ih => - simp [leftShift] +def countBreakPoints (l : List Int) : Nat := + if l.length < 2 + then 0 + else + ((List.range l.length).attach.map (fun ⟨x,h⟩ => + isBreakPoint l x (by simp at h; assumption))).sum + +theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ l.length < 2 := by + simp [countBreakPoints, List.sum_eq_zero] + constructor + · intro h + false_or_by_contra + rename_i hl + simp at hl + specialize h hl cases l with - | nil => simp + | nil => simp at hl | cons hd tl => - simp - rw [ih _ (by simp)] - sorry + cases tl with + | nil => simp at hl + | cons hd' tl' => + sorry + · omega + def move_one_ball (l : List Int) : Bool := - countGlobalBreakPoints l ≤ 1 - -theorem move_one_ball_correct_iff (l : List Int) : - move_one_ball l = true ↔ - ∃ (l' : List Int), isleftShiftOf l l' ∧ List.Pairwise (fun (a b : Int) => a < b) l' := by - simp [move_one_ball, Nat.le_succ_iff] - by_cases hl: l.length < 2 - · simp [countGlobalBreakPoints, hl] - exists l - simp [isleftShiftOf] - constructor - · exists 0 - · cases l with - | nil => simp - | cons hd tl => - cases tl with - | nil => simp - | cons hd' tl' => - simp at hl - omega - · have hl' : l ≠ [] := by - apply List.ne_nil_of_length_pos - simp at hl - exact Nat.zero_lt_of_lt hl - constructor - · intro h - cases h with - | inl h => - exists l - simp [isleftShiftOf] - have := countBreakPointsAndGetEnd_fst_eq_zero_of_countGlobalBreakPoints hl' h - rw [countBreakPointsAndGetEnd_fst_eq_zero_iff_sorted] at this - refine And.intro ?_ this - exists 0 - | inr h => - simp [countGlobalBreakPoints, hl] at h - split at h - · simp at h - exists l - rw [countBreakPointsAndGetEnd_fst_eq_zero_iff_sorted] at h - refine And.intro ?_ h - simp [isleftShiftOf] - exists 0 - · sorry - · false_or_by_contra - rename_i h h' - simp at h' - rcases h with ⟨l', hshift, hsort⟩ - simp [isleftShiftOf] at hshift - rcases hshift with ⟨n, hshift⟩ - have leftShift_ne_nil : leftShift l n ≠ [] := by - rw [ne_eq, ← List.isEmpty_iff] - simpa - rw [hshift, ← countBreakPointsAndGetEnd_fst_eq_zero_iff_sorted _ leftShift_ne_nil] at hsort - simp [← countGlobalBreakPoints_leftShift_eq l hl' n] at h' - have := countGlobalBreakPoints_of_countBreakPointsAndGetEnd hsort - simp at this - cases this with - | inl this => simp [this] at h' - | inr this => simp [this] at h' + countBreakPoints l < 2 theorem testCase1 : move_one_ball [3,4,5,1,2] = True := by native_decide theorem testCase2 : move_one_ball [3,5,10,1,2] = True := by native_decide @@ -310,6 +155,32 @@ theorem testCase3 : move_one_ball [4,3,1,2] = False := by native_decide theorem testCase4 : move_one_ball [3,5,4,1,2] = False := by native_decide theorem testCase5 : move_one_ball [] = True := by native_decide +theorem move_one_ball_correct {l : List Int} : + move_one_ball l = true ↔ ∃ (n : Nat), List.Pairwise (fun (a b : Int) => a < b) (rightShift l n) := by + by_cases hl : l.length < 2 + · simp [move_one_ball, hl, countBreakPoints] + exists 0 + cases l with + | nil => simp + | cons hd tl => + cases tl with + | nil => simp + | cons hd' tl' => + simp at hl + omega + · simp [move_one_ball] + constructor + · intro h + rw [Nat.lt_two_iff] at h + cases h with + | inl h => + sorry + | inr h => + simp [countBreakPoints, hl, List.sum_eq_one_iff] at h + rcases h with ⟨i, hi1, hi2⟩ + exists i + sorry + · /-! ## Prompt From 1106cf3369fa55da365bed94ffa019ba52033695 Mon Sep 17 00:00:00 2001 From: jt0202 Date: Wed, 7 May 2025 22:31:25 +0200 Subject: [PATCH 04/14] Further --- HumanEvalLean/HumanEval109.lean | 56 +++++++++++++++++++++++++++++++-- 1 file changed, 53 insertions(+), 3 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index ef733f9..4ac7335 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -95,8 +95,51 @@ theorem List.Pairwise_lt_of_forall_neighbor (l : List Int) | nil => simp | cons hd tl ih => simp - - + have : ∀ (i j : Nat) (h : i + j < tl.length), j ≠ 0 → tl[i] < tl[i + j] := by + intro i j hij + induction j with + | zero => simp + | succ k ih => + cases k with + | zero => + simp + specialize h (i+1) + simp at h + apply h + simpa + | succ l => + simp + apply Int.lt_trans + · apply ih + · omega + · simp + · specialize h ((i + (l + 1)) + 1) + simp at h + apply h + omega + constructor + · intro a ha + rw [mem_iff_getElem] at ha + rcases ha with ⟨i, hi, tli⟩ + cases i with + | zero => + rw [← tli] + apply h + simpa + | succ j => + rw [← tli] + specialize this 0 (j + 1) + simp [hi] at this + apply Int.lt_trans + · specialize h 0 + simp at h + apply h + · apply this trivial + · apply ih + intro i hi + specialize h (i+1) + apply h + simpa end helper @@ -110,6 +153,10 @@ theorem rightShiftExample : rightShift [3,4,5,1,2] 2 = [1,2,3,4,5] := by native_ theorem rightShift_zero {l : List α} : rightShift l 0 = l := by simp [rightShift] +theorem length_rightShift {l : List α} {n : Nat} : + (rightShift l n).length = l.length := by + simp [rightShift] + def isBreakPoint (l : List Int) (pos : Nat) (h : pos < l.length) := if h:pos + 1 < l.length then @@ -179,8 +226,11 @@ theorem move_one_ball_correct {l : List Int} : simp [countBreakPoints, hl, List.sum_eq_one_iff] at h rcases h with ⟨i, hi1, hi2⟩ exists i + apply List.Pairwise_lt_of_forall_neighbor + intro j hj + simp [rightShift] sorry - · + · sorry /-! ## Prompt From f8e1502d60c4c5b9bb69a5c6f38ce5546ef34752 Mon Sep 17 00:00:00 2001 From: jt0202 Date: Tue, 13 May 2025 20:53:31 +0200 Subject: [PATCH 05/14] Progress on 0 and 1 cases --- HumanEvalLean/HumanEval109.lean | 222 ++++++++++++++++++++++---------- 1 file changed, 152 insertions(+), 70 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 4ac7335..31c0b23 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -10,13 +10,24 @@ theorem Nat.lt_two_iff {n : Nat} : n < 2 ↔ n = 0 ∨ n = 1 := by | zero => simp | succ o => simp -theorem List.sum_eq_zero {l : List Nat} : l.sum = 0 ↔ ∀ x ∈ l, x = 0 := by +theorem List.sum_eq_zero {l : List Nat} : l.sum = 0 ↔ + ∀ (i : Nat) (hi : i < l.length), l[i]'hi = 0 := by induction l with | nil => simp | cons hd tl ih => - simp - intro _ - exact ih + simp [ih] + constructor + · intro h i hi + cases i with + | zero => simp [h] + | succ m => + simp + apply And.right h + · intro h + constructor + · apply h 0 (by simp) + · intro i hi + apply h (i + 1) (by omega) theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i < l.length), l[i] = 1 ∧ ∀ (j : Nat) (hj : j < l.length), i ≠ j → l[j] = 0 := by @@ -88,59 +99,6 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i simp at h apply h hj hkj -theorem List.Pairwise_lt_of_forall_neighbor (l : List Int) - (h : ∀ (i : Nat) (hi : i + 1 < l.length), l[i] < l[i+1]) : - List.Pairwise (fun (a b : Int) => a < b) l := by - induction l with - | nil => simp - | cons hd tl ih => - simp - have : ∀ (i j : Nat) (h : i + j < tl.length), j ≠ 0 → tl[i] < tl[i + j] := by - intro i j hij - induction j with - | zero => simp - | succ k ih => - cases k with - | zero => - simp - specialize h (i+1) - simp at h - apply h - simpa - | succ l => - simp - apply Int.lt_trans - · apply ih - · omega - · simp - · specialize h ((i + (l + 1)) + 1) - simp at h - apply h - omega - constructor - · intro a ha - rw [mem_iff_getElem] at ha - rcases ha with ⟨i, hi, tli⟩ - cases i with - | zero => - rw [← tli] - apply h - simpa - | succ j => - rw [← tli] - specialize this 0 (j + 1) - simp [hi] at this - apply Int.lt_trans - · specialize h 0 - simp at h - apply h - · apply this trivial - · apply ih - intro i hi - specialize h (i+1) - apply h - simpa - end helper @@ -153,10 +111,46 @@ theorem rightShiftExample : rightShift [3,4,5,1,2] 2 = [1,2,3,4,5] := by native_ theorem rightShift_zero {l : List α} : rightShift l 0 = l := by simp [rightShift] +@[simp] theorem length_rightShift {l : List α} {n : Nat} : (rightShift l n).length = l.length := by simp [rightShift] +def leftShift (l : List α) (n : Nat) := + l.drop n ++ l.take n + +theorem leftShiftExample1 : leftShift [3,4,5,1,2] 2 = [5,1,2,3,4] := by native_decide + +theorem leftShiftExample2 : leftShift [3,4,5,1,2] 3 = [1,2,3,4,5] := by native_decide + +-- from mathlib +@[simp] theorem List.take_eq_self_iff (x : List α) {n : Nat} : x.take n = x ↔ x.length ≤ n := + ⟨fun h ↦ by rw [← h]; simp; omega, List.take_of_length_le⟩ + +theorem exists_rightShift_iff_exists_leftShift {l : List α} (p : List α → Prop) : + (∃ (n : Nat), p (rightShift l n)) ↔ ∃ (n : Nat), p (leftShift l n) := by + simp [leftShift, rightShift] + constructor + · intro h + obtain ⟨n, hn⟩ := h + exists (l.length - n) + · intro h + obtain ⟨n, hn⟩ := h + by_cases n < l.length + · exists (l.length - n) + have : l.length - (l.length - n) = n := by omega + simp [this] + exact hn + · exists 0 + simp + rename_i h + simp at h + have := List.drop_eq_nil_iff (l := l) (i := n) + simp [this.mpr h] at hn + have := List.take_eq_self_iff l (n := n) + simp [this.mpr h] at hn + exact hn + def isBreakPoint (l : List Int) (pos : Nat) (h : pos < l.length) := if h:pos + 1 < l.length then @@ -164,9 +158,9 @@ def isBreakPoint (l : List Int) (pos : Nat) (h : pos < l.length) := then 0 else 1 else - if l[pos] > l[0] - then 1 - else 0 + if l[0] > l[pos] + then 0 + else 1 def countBreakPoints (l : List Int) : Nat := if l.length < 2 @@ -175,21 +169,74 @@ def countBreakPoints (l : List Int) : Nat := ((List.range l.length).attach.map (fun ⟨x,h⟩ => isBreakPoint l x (by simp at h; assumption))).sum +theorem ne_nil_of_two_ge {l : List α} (h : 2 ≤ l.length) : l ≠ [] := by + cases l with + | nil => simp at h + | cons hd tl => simp + +theorem sorted_of_countBreakPoints_eq_zero {l : List Int} (h : countBreakPoints l = 0): + ∀ (i : Nat) (hi : i + 1 < l.length), l[i] < l[i+1] := by + simp [countBreakPoints] at h + cases l with + | nil => simp + | cons hd tl => + cases tl with + | nil => simp + | cons hd' tl' => + simp[List.sum_eq_zero, isBreakPoint] at h + simp + intro i hi + specialize h i (by omega) + simp [hi] at h + exact h + + +theorem head_lt_getLast_of_sorted_of_ge_2 {l : List Int} (hl : l.length ≥ 2) + (sorted : ∀ (i : Nat) (hi : i + 1 < l.length), l[i] < l[i+1]) : + l[0]'(by omega) < l[l.length - 1] := by + induction l with + | nil => simp at hl + | cons hd tl ih => + simp + by_cases h : tl.length ≥ 2 + · specialize ih h + have htl : tl ≠ [] := ne_nil_of_two_ge h + have h₁ : hd < tl.head htl := by + sorry + have h₂ : tl.head htl < tl.getLast htl := by + sorry + have := Nat.lt_trans h₁ h₂ + + + theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ l.length < 2 := by - simp [countBreakPoints, List.sum_eq_zero] constructor · intro h + have sorted := sorted_of_countBreakPoints_eq_zero h false_or_by_contra rename_i hl simp at hl - specialize h hl cases l with | nil => simp at hl | cons hd tl => cases tl with | nil => simp at hl | cons hd' tl' => - sorry + have h₁ : hd < (hd' :: tl')[tl'.length] := by + have := head_lt_getLast_of_sorted_of_ge_2 (l := hd :: hd' :: tl') + simp at this + apply this trivial + simp at sorted + exact sorted + have h₂ : (hd :: tl')[tl'.length] < hd := by + simp [countBreakPoints, List.sum_eq_zero, isBreakPoint] at h + specialize h (tl'.length + 1) + simp at h + + + + + · omega @@ -203,7 +250,9 @@ theorem testCase4 : move_one_ball [3,5,4,1,2] = False := by native_decide theorem testCase5 : move_one_ball [] = True := by native_decide theorem move_one_ball_correct {l : List Int} : - move_one_ball l = true ↔ ∃ (n : Nat), List.Pairwise (fun (a b : Int) => a < b) (rightShift l n) := by + move_one_ball l = true ↔ + ∃ (n : Nat), ∀ (i : Nat) (hi : i + 1 < l.length), + (rightShift l n)[i]'(by simp; omega) < (rightShift l n)[i +1]'(by simpa) := by by_cases hl : l.length < 2 · simp [move_one_ball, hl, countBreakPoints] exists 0 @@ -221,16 +270,49 @@ theorem move_one_ball_correct {l : List Int} : rw [Nat.lt_two_iff] at h cases h with | inl h => - sorry + rw [countBreakPoints_eq_zero_iff] at h + contradiction | inr h => simp [countBreakPoints, hl, List.sum_eq_one_iff] at h + have := exists_rightShift_iff_exists_leftShift (l:= l) (p := fun (l : List Int) => + ∀ (i : Nat) (hi : i + 1 < l.length), l[i]'(by omega) < l[i + 1]) + simp at this + rw [this] rcases h with ⟨i, hi1, hi2⟩ - exists i - apply List.Pairwise_lt_of_forall_neighbor + exists (i + 1) + rcases hi1 with ⟨hi, hi1⟩ intro j hj - simp [rightShift] - sorry - · sorry + simp [leftShift] + simp [List.getElem_append] + simp [isBreakPoint] at hi2 + split + · split + · specialize hi2 (i + 1 + j) (by omega) + have : ¬ i = i + 1 + j := by omega + simp [this] at hi2 + have : i + 1 + j + 1 < l.length := by omega + simp [this] at hi2 + apply hi2 + · specialize hi2 (i + 1 + j) (by omega) + have : ¬ i = i + 1 + j := by omega + simp [this] at hi2 + have : ¬ i + 1 + j + 1 < l.length := by sorry + simp [this] at hi2 + have : j + 1 - (l.length - (i + 1)) = 0 := by sorry + simp [this] + exact hi2 + · split + · specialize hi2 0 (by omega) + have : ¬ i = 0 := by omega + simp [this] at hi2 + have : 1 < l.length := by omega + simp [this] at hi2 + omega + · sorry + · false_or_by_contra + rename_i h h' + + /-! ## Prompt From 9ef0e36841b686c56786f22437f7da42f7713ade Mon Sep 17 00:00:00 2001 From: jt0202 Date: Fri, 16 May 2025 19:16:08 +0200 Subject: [PATCH 06/14] Finish zero case --- HumanEvalLean/HumanEval109.lean | 176 ++++++++++++++++++++++++++------ 1 file changed, 146 insertions(+), 30 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 31c0b23..931cf8e 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -99,6 +99,82 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i simp at h apply h hj hkj +theorem List.sum_ge_two_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length), l[i] ≤ 1) : + l.sum ≥ 2 ↔ ∃ (i j : Nat) (hij : i ≠ j) (hi : i < l.length) (hj : j < l.length), + l[i] = 1 ∧ l[j] = 1 := by + induction l with + | nil => simp + | cons hd tl ih => + simp + cases hd with + | zero => + simp + simp at ih + rw [ih] + · constructor + · intro h + rcases h with ⟨i, hi, j, hj⟩ + exists (i+1) + simp [hi] + exists (j + 1) + simp [hj] + · intro h + rcases h with ⟨i, hi, j, hj⟩ + cases i with + | zero => simp at hi + | succ m => + exists m + simp at hi + simp [hi] + cases j with + | zero => simp at hj + | succ n => + exists n + simp at hj + simp [hj] + · intro i hi + specialize h (i+1) + simp at h + exact h hi + | succ k => + cases k with + | zero => + have : 2 ≤ 1 + tl.sum ↔ 1 ≤ tl.sum := by omega + simp [this, Nat.le_iff_lt_or_eq] + constructor + · intro h' + cases h' with + | inl h' => + simp [Nat.lt_iff_add_one_le] at h' + simp at ih + rw [ih] at h' + · rcases h' with ⟨i, hi, j, hij, hj⟩ + exists (i+1) + simp + exists hi + exists (j+1) + simp [hij, hj] + · intro i hi + simp at h + specialize h (i+1) + simp at h + exact h hi + | inr h' => + exists 0 + simp + rw [Eq.comm, sum_eq_one_iff] at h' + rcases h' with ⟨j, hj, htl⟩ + exists (j+1) + simp + exists hj + simp [htl] + · intro h' + sorry + + | succ l => + specialize h 0 + simp at h + end helper @@ -119,6 +195,12 @@ theorem length_rightShift {l : List α} {n : Nat} : def leftShift (l : List α) (n : Nat) := l.drop n ++ l.take n +@[simp] +theorem length_leftShift {l : List α} {n : Nat} : + (leftShift l n).length = l.length := by + simp [leftShift] + omega + theorem leftShiftExample1 : leftShift [3,4,5,1,2] 2 = [5,1,2,3,4] := by native_decide theorem leftShiftExample2 : leftShift [3,4,5,1,2] 3 = [1,2,3,4,5] := by native_decide @@ -190,24 +272,58 @@ theorem sorted_of_countBreakPoints_eq_zero {l : List Int} (h : countBreakPoints simp [hi] at h exact h - -theorem head_lt_getLast_of_sorted_of_ge_2 {l : List Int} (hl : l.length ≥ 2) +theorem pairwise_sorted_of_sorted {l : List Int} {i j : Nat} + (hj: j > 0) (hij : i + j < l.length) (sorted : ∀ (i : Nat) (hi : i + 1 < l.length), l[i] < l[i+1]) : - l[0]'(by omega) < l[l.length - 1] := by - induction l with - | nil => simp at hl + l[i]'(by omega) < l[i + j] := by + induction l generalizing i j with + | nil => simp at hij | cons hd tl ih => - simp - by_cases h : tl.length ≥ 2 - · specialize ih h - have htl : tl ≠ [] := ne_nil_of_two_ge h - have h₁ : hd < tl.head htl := by - sorry - have h₂ : tl.head htl < tl.getLast htl := by - sorry - have := Nat.lt_trans h₁ h₂ - - + cases i with + | zero => + simp + simp [Nat.lt_iff_add_one_le] at hj + cases j with + | zero => simp at hj + | succ k => + cases k with + | zero => + simp + specialize sorted 0 + simp at sorted + apply sorted + simp at hij + assumption + | succ m => + simp + have : m + 1 > 0 := by omega + have ih' := ih (i:= 0) (j := m+1) + specialize ih' this + simp at ih' + simp at hij + specialize ih' hij + apply Int.lt_trans (b := tl[0]) + · specialize sorted 0 + simp at sorted + apply sorted + apply Nat.lt_trans (m:= m + 1) + · simp + · exact hij + · apply ih' + intro i hi + specialize sorted (i+1) + simp at sorted + apply sorted hi + | succ n => + simp + have : n + 1 + j = (n + j).succ := by omega + simp [this] + apply ih + · exact hj + · intro i hi + specialize sorted (i+1) + simp at sorted + apply sorted hi theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ l.length < 2 := by constructor @@ -223,21 +339,20 @@ theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ | nil => simp at hl | cons hd' tl' => have h₁ : hd < (hd' :: tl')[tl'.length] := by - have := head_lt_getLast_of_sorted_of_ge_2 (l := hd :: hd' :: tl') - simp at this - apply this trivial - simp at sorted - exact sorted - have h₂ : (hd :: tl')[tl'.length] < hd := by + have head_lt_getLast := pairwise_sorted_of_sorted (l := hd :: hd' :: tl') (i := 0) + (j := tl'.length + 1) (by simp) (by simp) sorted + simp at head_lt_getLast + exact head_lt_getLast + have h₂ : (hd' :: tl')[tl'.length] < hd := by simp [countBreakPoints, List.sum_eq_zero, isBreakPoint] at h specialize h (tl'.length + 1) simp at h - - - - - - · omega + apply h + trivial + have := Int.lt_trans h₁ h₂ + simp at this + · intro h + simp [countBreakPoints, h] def move_one_ball (l : List Int) : Bool := @@ -296,9 +411,9 @@ theorem move_one_ball_correct {l : List Int} : · specialize hi2 (i + 1 + j) (by omega) have : ¬ i = i + 1 + j := by omega simp [this] at hi2 - have : ¬ i + 1 + j + 1 < l.length := by sorry + have : ¬ i + 1 + j + 1 < l.length := by omega simp [this] at hi2 - have : j + 1 - (l.length - (i + 1)) = 0 := by sorry + have : j + 1 - (l.length - (i + 1)) = 0 := by omega simp [this] exact hi2 · split @@ -313,6 +428,7 @@ theorem move_one_ball_correct {l : List Int} : rename_i h h' + /-! ## Prompt From 2d36a1f180d4eb374fc8fbe1b8e37239695c0e10 Mon Sep 17 00:00:00 2001 From: jt0202 Date: Sat, 17 May 2025 11:35:34 +0200 Subject: [PATCH 07/14] Finish one case --- HumanEvalLean/HumanEval109.lean | 39 +++++++++++++++++++++------------ 1 file changed, 25 insertions(+), 14 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 931cf8e..42c2c3c 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -66,7 +66,6 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i simp rcases h with ⟨_, h⟩ apply h - simp · intro h rcases h with ⟨i, hi, h⟩ cases i with @@ -76,12 +75,10 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i simp [hi] rw [List.sum_eq_zero] intro x hx - rw [List.mem_iff_getElem] at hx - rcases hx with ⟨k, hk, tlk⟩ - specialize h (k + 1) + specialize h (x+1) simp at h - rw [← tlk] - apply h hk + apply h + exact hx | succ k => simp at hi left @@ -169,14 +166,25 @@ theorem List.sum_ge_two_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length exists hj simp [htl] · intro h' - sorry - + by_cases hsum: 1 = tl.sum + · simp [hsum] + · simp [hsum, Nat.lt_iff_add_one_le] + simp at ih + rw [ih] + · sorry + · intro i hi + specialize h (i+1) + simp at h + exact h hi | succ l => specialize h 0 simp at h -end helper +-- from mathlib +@[simp] theorem List.take_eq_self_iff (x : List α) {n : Nat} : x.take n = x ↔ x.length ≤ n := + ⟨fun h ↦ by rw [← h]; simp; omega, List.take_of_length_le⟩ +end helper def rightShift (l : List α) (n : Nat) := l.drop (l.length - n) ++ l.take (l.length - n) @@ -205,10 +213,6 @@ theorem leftShiftExample1 : leftShift [3,4,5,1,2] 2 = [5,1,2,3,4] := by native_d theorem leftShiftExample2 : leftShift [3,4,5,1,2] 3 = [1,2,3,4,5] := by native_decide --- from mathlib -@[simp] theorem List.take_eq_self_iff (x : List α) {n : Nat} : x.take n = x ↔ x.length ≤ n := - ⟨fun h ↦ by rw [← h]; simp; omega, List.take_of_length_le⟩ - theorem exists_rightShift_iff_exists_leftShift {l : List α} (p : List α → Prop) : (∃ (n : Nat), p (rightShift l n)) ↔ ∃ (n : Nat), p (leftShift l n) := by simp [leftShift, rightShift] @@ -423,9 +427,16 @@ theorem move_one_ball_correct {l : List Int} : have : 1 < l.length := by omega simp [this] at hi2 omega - · sorry + · rename_i h₁ h₂ + specialize hi2 (j - (l.length - (i + 1))) (by omega) (by omega) + have : j - (l.length - (i + 1)) + 1 < l.length := by omega + simp [this] at hi2 + have : j - (l.length - (i + 1)) + 1 = j + 1 - (l.length - (i + 1)) := by omega + simp [this] at hi2 + exact hi2 · false_or_by_contra rename_i h h' + sorry From aaf504918ec60d3a40d7bebde6130717132c5b20 Mon Sep 17 00:00:00 2001 From: jt0202 Date: Sat, 17 May 2025 12:15:36 +0200 Subject: [PATCH 08/14] Sketch of main theorem --- HumanEvalLean/HumanEval109.lean | 49 +++++++++++++++++++++++++++++---- 1 file changed, 44 insertions(+), 5 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 42c2c3c..25035db 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -96,8 +96,8 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i simp at h apply h hj hkj -theorem List.sum_ge_two_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length), l[i] ≤ 1) : - l.sum ≥ 2 ↔ ∃ (i j : Nat) (hij : i ≠ j) (hi : i < l.length) (hj : j < l.length), +theorem List.two_le_sum_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length), l[i] ≤ 1) : + 2 ≤ l.sum ↔ ∃ (i j : Nat) (hij : i ≠ j) (hi : i < l.length) (hj : j < l.length), l[i] = 1 ∧ l[j] = 1 := by induction l with | nil => simp @@ -213,6 +213,10 @@ theorem leftShiftExample1 : leftShift [3,4,5,1,2] 2 = [5,1,2,3,4] := by native_d theorem leftShiftExample2 : leftShift [3,4,5,1,2] 3 = [1,2,3,4,5] := by native_decide +theorem List.sum_leftShift_eq_sum {l : List Int} {n : Nat} : + (leftShift l n).sum = l.sum := by + sorry + theorem exists_rightShift_iff_exists_leftShift {l : List α} (p : List α → Prop) : (∃ (n : Nat), p (rightShift l n)) ↔ ∃ (n : Nat), p (leftShift l n) := by simp [leftShift, rightShift] @@ -359,6 +363,33 @@ theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ simp [countBreakPoints, h] +theorem not_sorted_of_countBreakPoints_ge_two {l : List Int} (h : countBreakPoints l ≥ 2) : + ∀ (n : Nat), ∃ (i : Nat) (hi : i + 1 < (leftShift l n).length), + (leftShift l n)[i] ≥ (leftShift l n)[i+1] := by + simp [countBreakPoints] at h + split at h + · simp at h + · rw [List.two_le_sum_iff] at h + rcases h with ⟨i, j, hij, hi, hj, h⟩ + simp at h + intro n + by_cases hin : i = n + · simp [leftShift] + simp at hi + simp at hj + rw [Nat.ne_iff_lt_or_gt] at hij + cases hij with + | inl hij => + exists (j - i) + simp [hin, List.getElem_append] + have : j - n + 1 < l.length - n + min n l.length := by + simp [← hin] + rw [Nat.min_eq_left] + · rw [Nat.sub_add_eq_max, Nat.max_eq_left] + · omega + · omega + + def move_one_ball (l : List Int) : Bool := countBreakPoints l < 2 @@ -436,9 +467,17 @@ theorem move_one_ball_correct {l : List Int} : exact hi2 · false_or_by_contra rename_i h h' - sorry - - + simp at h' + have := exists_rightShift_iff_exists_leftShift (l:= l) (p := fun (l : List Int) => + ∀ (i : Nat) (hi : i + 1 < l.length), l[i]'(by omega) < l[i + 1]) + simp at this + rw [this] at h + have := not_sorted_of_countBreakPoints_ge_two (l := l) (by simpa) + rcases h with ⟨n,h⟩ + specialize this n + rcases this with ⟨i, hi, this⟩ + specialize h i (by simp at hi; exact hi) + omega /-! ## Prompt From 7553f73b04b98e5f90ae583182df55ee6609a2ff Mon Sep 17 00:00:00 2001 From: jt0202 Date: Sat, 17 May 2025 12:54:19 +0200 Subject: [PATCH 09/14] Different try --- HumanEvalLean/HumanEval109.lean | 61 +++++++++++++++++++++------------ 1 file changed, 39 insertions(+), 22 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 25035db..32dd63c 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -213,9 +213,18 @@ theorem leftShiftExample1 : leftShift [3,4,5,1,2] 2 = [5,1,2,3,4] := by native_d theorem leftShiftExample2 : leftShift [3,4,5,1,2] 3 = [1,2,3,4,5] := by native_decide +theorem List.sum_append {l₁ l₂ : List Int} : + (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by + induction l₁ with + | nil => simp + | cons hd tl ih => + simp [ih] + omega + theorem List.sum_leftShift_eq_sum {l : List Int} {n : Nat} : (leftShift l n).sum = l.sum := by - sorry + simp [leftShift] + rw [List.sum_append, Int.add_comm, ← List.sum_append, take_append_drop] theorem exists_rightShift_iff_exists_leftShift {l : List α} (p : List α → Prop) : (∃ (n : Nat), p (rightShift l n)) ↔ ∃ (n : Nat), p (leftShift l n) := by @@ -362,33 +371,42 @@ theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ · intro h simp [countBreakPoints, h] +theorem countBreakPoints_leftShift_eq_countBreakPoints {l : List Int} {n : Nat} : + countBreakPoints (leftShift l n) = countBreakPoints l := by + simp [countBreakPoints] + by_cases h: l.length < 2 + · simp [h] + · simp [h] + have : List.range (leftShift l n).length = List.range l.length := by + sorry + simp [this] theorem not_sorted_of_countBreakPoints_ge_two {l : List Int} (h : countBreakPoints l ≥ 2) : - ∀ (n : Nat), ∃ (i : Nat) (hi : i + 1 < (leftShift l n).length), - (leftShift l n)[i] ≥ (leftShift l n)[i+1] := by + ∃ (i : Nat) (hi : i + 1 < l.length), + l[i] ≥ l[i+1] := by simp [countBreakPoints] at h split at h · simp at h · rw [List.two_le_sum_iff] at h - rcases h with ⟨i, j, hij, hi, hj, h⟩ - simp at h - intro n - by_cases hin : i = n - · simp [leftShift] + · rcases h with ⟨i, j, hij, hi, hj, h⟩ + simp[isBreakPoint] at h simp at hi simp at hj - rw [Nat.ne_iff_lt_or_gt] at hij - cases hij with - | inl hij => - exists (j - i) - simp [hin, List.getElem_append] - have : j - n + 1 < l.length - n + min n l.length := by - simp [← hin] - rw [Nat.min_eq_left] - · rw [Nat.sub_add_eq_max, Nat.max_eq_left] - · omega - · omega - + have : i + 1 < l.length ∨ j + 1 < l.length := by omega + cases this with + | inl this => + simp [this] at h + exists i + exists this + simp [h] + | inr this => + simp [this] at h + exists j + exists this + simp [h] + · simp [isBreakPoint] + intro _ _ + split <;> split ; all_goals simp def move_one_ball (l : List Int) : Bool := countBreakPoints l < 2 @@ -472,9 +490,8 @@ theorem move_one_ball_correct {l : List Int} : ∀ (i : Nat) (hi : i + 1 < l.length), l[i]'(by omega) < l[i + 1]) simp at this rw [this] at h - have := not_sorted_of_countBreakPoints_ge_two (l := l) (by simpa) rcases h with ⟨n,h⟩ - specialize this n + have := not_sorted_of_countBreakPoints_ge_two (l := leftShift l n) rcases this with ⟨i, hi, this⟩ specialize h i (by simp at hi; exact hi) omega From abf05c6d08e29048c98b89f06811905a3ec27168 Mon Sep 17 00:00:00 2001 From: jt0202 Date: Sat, 17 May 2025 14:24:48 +0200 Subject: [PATCH 10/14] Case for ge 2 --- HumanEvalLean/HumanEval109.lean | 143 ++++++++++++++++++++++++-------- 1 file changed, 110 insertions(+), 33 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 32dd63c..589e96f 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -1,4 +1,4 @@ -variable {α : Type _} +variable {α : Type u} {β : Type v} section helper @@ -184,6 +184,14 @@ theorem List.two_le_sum_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length @[simp] theorem List.take_eq_self_iff (x : List α) {n : Nat} : x.take n = x ↔ x.length ≤ n := ⟨fun h ↦ by rw [← h]; simp; omega, List.take_of_length_le⟩ +theorem List.sum_append {l₁ l₂ : List Nat} : + (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by + induction l₁ with + | nil => simp + | cons hd tl ih => + simp [ih] + omega + end helper def rightShift (l : List α) (n : Nat) := @@ -213,18 +221,10 @@ theorem leftShiftExample1 : leftShift [3,4,5,1,2] 2 = [5,1,2,3,4] := by native_d theorem leftShiftExample2 : leftShift [3,4,5,1,2] 3 = [1,2,3,4,5] := by native_decide -theorem List.sum_append {l₁ l₂ : List Int} : - (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by - induction l₁ with - | nil => simp - | cons hd tl ih => - simp [ih] - omega - -theorem List.sum_leftShift_eq_sum {l : List Int} {n : Nat} : +theorem List.sum_leftShift_eq_sum {l : List Nat} {n : Nat} : (leftShift l n).sum = l.sum := by simp [leftShift] - rw [List.sum_append, Int.add_comm, ← List.sum_append, take_append_drop] + rw [List.sum_append, Nat.add_comm, ← List.sum_append, take_append_drop] theorem exists_rightShift_iff_exists_leftShift {l : List α} (p : List α → Prop) : (∃ (n : Nat), p (rightShift l n)) ↔ ∃ (n : Nat), p (leftShift l n) := by @@ -250,23 +250,25 @@ theorem exists_rightShift_iff_exists_leftShift {l : List α} (p : List α → Pr simp [this.mpr h] at hn exact hn -def isBreakPoint (l : List Int) (pos : Nat) (h : pos < l.length) := - if h:pos + 1 < l.length +def isBreakPoint (l : List Int) (pos : Nat) := + if h:pos < l.length then - if l[pos] < l[pos + 1] - then 0 - else 1 - else - if l[0] > l[pos] - then 0 - else 1 + if h':pos + 1 < l.length + then + if l[pos] < l[pos + 1] + then 0 + else 1 + else + if l[0] > l[pos] + then 0 + else 1 + else 0 def countBreakPoints (l : List Int) : Nat := if l.length < 2 then 0 else - ((List.range l.length).attach.map (fun ⟨x,h⟩ => - isBreakPoint l x (by simp at h; assumption))).sum + ((List.range l.length).map (fun x => isBreakPoint l x)).sum theorem ne_nil_of_two_ge {l : List α} (h : 2 ≤ l.length) : l ≠ [] := by cases l with @@ -287,7 +289,8 @@ theorem sorted_of_countBreakPoints_eq_zero {l : List Int} (h : countBreakPoints intro i hi specialize h i (by omega) simp [hi] at h - exact h + apply h + omega theorem pairwise_sorted_of_sorted {l : List Int} {i j : Nat} (hj: j > 0) (hij : i + j < l.length) @@ -365,7 +368,8 @@ theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ specialize h (tl'.length + 1) simp at h apply h - trivial + · trivial + · trivial have := Int.lt_trans h₁ h₂ simp at this · intro h @@ -376,10 +380,76 @@ theorem countBreakPoints_leftShift_eq_countBreakPoints {l : List Int} {n : Nat} simp [countBreakPoints] by_cases h: l.length < 2 · simp [h] - · simp [h] - have : List.range (leftShift l n).length = List.range l.length := by - sorry - simp [this] + · by_cases hn: n < l.length + · simp [h] + have : List.map (fun x => isBreakPoint (leftShift l n) x) (List.range l.length) = + leftShift (List.map (fun x => isBreakPoint l x) (List.range l.length)) n := by + apply List.ext_get + · simp + · simp + intro m h₁ _ + conv => + rhs + simp [leftShift] + rw [List.getElem_append] + simp + split + · simp [isBreakPoint, h₁] + split + · have : n + m < l.length := by omega + simp [this] + by_cases hnm : n + m +1 < l.length + · simp [hnm, leftShift, List.getElem_append] + simp [*] + have : m + 1 < l.length - n := by omega + simp [this] + rfl + · simp [hnm, leftShift, List.getElem_append] + simp [*] + have : ¬ m + 1 < l.length - n := by omega + simp [this] + have : m + 1 - (l.length - n) = 0 := by omega + simp [this] + · have : n + m < l.length := by omega + simp [this] + by_cases hnm : n + m +1 < l.length + · omega + · simp [hnm, leftShift, List.getElem_append] + simp [*] + have : 0 < l.length -n := by omega + simp [this] + have : n = 0 := by omega + simp [this] + · rename_i hnm + simp [isBreakPoint, h₁] + by_cases h₂ : m + 1 < l.length + · simp [h₂] + have : m - (l.length - n) < l.length := by omega + simp [this] + have : m - (l.length - n) + 1 < l.length := by omega + simp [this, leftShift, List.getElem_append] + simp [hnm] + have : ¬ m + 1 < l.length - n := by omega + simp [this] + congr + omega + · simp [h₂] + have : m - (l.length - n) < l.length := by omega + simp [this] + have : m - (l.length - n) + 1 < l.length := by omega + simp [this, leftShift, List.getElem_append, hnm] + have : 0 < l.length - n := by omega + simp [this] + congr + omega + simp [this] + rw [List.sum_leftShift_eq_sum (n:= n) (l:= (List.map (fun x => isBreakPoint l x) (List.range l.length)))] + · congr + funext + congr + simp at hn + simp [leftShift, List.drop_eq_nil_iff.mpr, hn] + theorem not_sorted_of_countBreakPoints_ge_two {l : List Int} (h : countBreakPoints l ≥ 2) : ∃ (i : Nat) (hi : i + 1 < l.length), @@ -398,15 +468,17 @@ theorem not_sorted_of_countBreakPoints_ge_two {l : List Int} (h : countBreakPoin simp [this] at h exists i exists this + simp [hi] at h simp [h] | inr this => simp [this] at h exists j exists this + simp [hj] at h simp [h] · simp [isBreakPoint] intro _ _ - split <;> split ; all_goals simp + split <;> split <;> split <;> simp def move_one_ball (l : List Int) : Bool := countBreakPoints l < 2 @@ -448,11 +520,11 @@ theorem move_one_ball_correct {l : List Int} : rw [this] rcases h with ⟨i, hi1, hi2⟩ exists (i + 1) - rcases hi1 with ⟨hi, hi1⟩ intro j hj simp [leftShift] simp [List.getElem_append] simp [isBreakPoint] at hi2 + rcases hi2 with ⟨hi, hi2⟩ split · split · specialize hi2 (i + 1 + j) (by omega) @@ -461,6 +533,7 @@ theorem move_one_ball_correct {l : List Int} : have : i + 1 + j + 1 < l.length := by omega simp [this] at hi2 apply hi2 + omega · specialize hi2 (i + 1 + j) (by omega) have : ¬ i = i + 1 + j := by omega simp [this] at hi2 @@ -468,7 +541,8 @@ theorem move_one_ball_correct {l : List Int} : simp [this] at hi2 have : j + 1 - (l.length - (i + 1)) = 0 := by omega simp [this] - exact hi2 + apply hi2 + omega · split · specialize hi2 0 (by omega) have : ¬ i = 0 := by omega @@ -482,7 +556,8 @@ theorem move_one_ball_correct {l : List Int} : simp [this] at hi2 have : j - (l.length - (i + 1)) + 1 = j + 1 - (l.length - (i + 1)) := by omega simp [this] at hi2 - exact hi2 + apply hi2 + omega · false_or_by_contra rename_i h h' simp at h' @@ -492,8 +567,10 @@ theorem move_one_ball_correct {l : List Int} : rw [this] at h rcases h with ⟨n,h⟩ have := not_sorted_of_countBreakPoints_ge_two (l := leftShift l n) + rw [countBreakPoints_leftShift_eq_countBreakPoints] at this + simp [h'] at this rcases this with ⟨i, hi, this⟩ - specialize h i (by simp at hi; exact hi) + specialize h i hi omega /-! From 5b03220ed9e5cf209420b6b7ed3ce14ef4579652 Mon Sep 17 00:00:00 2001 From: jt0202 Date: Sat, 17 May 2025 14:53:37 +0200 Subject: [PATCH 11/14] Finished --- HumanEvalLean/HumanEval109.lean | 161 ++++++++++++++++++-------------- 1 file changed, 89 insertions(+), 72 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 589e96f..a3dd413 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -1,4 +1,4 @@ -variable {α : Type u} {β : Type v} +variable {α : Type _} section helper @@ -97,88 +97,105 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i apply h hj hkj theorem List.two_le_sum_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length), l[i] ≤ 1) : - 2 ≤ l.sum ↔ ∃ (i j : Nat) (hij : i ≠ j) (hi : i < l.length) (hj : j < l.length), + 2 ≤ l.sum ↔ ∃ (i j : Nat) (_hij : i ≠ j) (hi : i < l.length) (hj : j < l.length), l[i] = 1 ∧ l[j] = 1 := by induction l with | nil => simp | cons hd tl ih => simp - cases hd with - | zero => - simp - simp at ih - rw [ih] - · constructor - · intro h - rcases h with ⟨i, hi, j, hj⟩ - exists (i+1) - simp [hi] - exists (j + 1) - simp [hj] - · intro h - rcases h with ⟨i, hi, j, hj⟩ - cases i with - | zero => simp at hi - | succ m => - exists m - simp at hi - simp [hi] - cases j with - | zero => simp at hj - | succ n => - exists n - simp at hj - simp [hj] + by_cases h' : 2 ≤ tl.sum + · have : 2 ≤ hd + tl.sum := by omega + rw [ih] at h' + · simp [this] + rcases h' with ⟨i, j, hij, hi, hj, h'⟩ + exists (i+1) + simp + constructor + · exists hi + simp [h'] + · exists (j+1) + simp [hij] + exists hj + simp [h'] · intro i hi specialize h (i+1) simp at h - exact h hi - | succ k => - cases k with + apply h hi + · simp at h' + cases htl : tl.sum with | zero => - have : 2 ≤ 1 + tl.sum ↔ 1 ≤ tl.sum := by omega - simp [this, Nat.le_iff_lt_or_eq] - constructor - · intro h' - cases h' with - | inl h' => - simp [Nat.lt_iff_add_one_le] at h' - simp at ih - rw [ih] at h' - · rcases h' with ⟨i, hi, j, hij, hj⟩ - exists (i+1) - simp - exists hi - exists (j+1) - simp [hij, hj] - · intro i hi - simp at h - specialize h (i+1) - simp at h - exact h hi - | inr h' => - exists 0 + simp + have hhd : ¬ 2 ≤ hd := by + intro h' + specialize h 0 + simp at h + omega + rw [List.sum_eq_zero] at htl + simp [hhd] + intro i hi hi' j hij hj + cases i with + | zero => + simp at hi' + cases j with + | zero => contradiction + | succ k => simp - rw [Eq.comm, sum_eq_one_iff] at h' - rcases h' with ⟨j, hj, htl⟩ - exists (j+1) + intro hk + specialize htl k + have : k < tl.length := by omega + specialize htl this + rw [hk] at htl + simp at htl + | succ k => + simp at hi' + specialize htl k + have : k < tl.length := by omega + specialize htl this + rw [hi'] at htl + simp at htl + | succ k => + have hk : k = 0 := by omega + simp [hk] + constructor + · intro h₁ + exists 0 + simp + constructor + · specialize h 0 + simp at h + omega + · simp [hk] at htl + rw [List.sum_eq_one_iff] at htl + rcases htl with ⟨i, hi,hi', _⟩ + exists (i+1) simp - exists hj - simp [htl] - · intro h' - by_cases hsum: 1 = tl.sum - · simp [hsum] - · simp [hsum, Nat.lt_iff_add_one_le] - simp at ih - rw [ih] - · sorry - · intro i hi - specialize h (i+1) - simp at h - exact h hi - | succ l => - specialize h 0 - simp at h + exists hi + · intro h₁ + simp [hk] at htl + rw [List.sum_eq_one_iff] at htl + rcases htl with ⟨i, hi,hi', htl⟩ + rcases h₁ with ⟨j, hj, k, hjk, hk⟩ + cases j with + | zero => + simp at hj + simp [hj] + | succ l => + simp at hj + cases k with + | zero => + simp at hk + simp [hk] + | succ m => + simp at hk + by_cases hil : i = l + · specialize htl m + rcases hk with ⟨hm, hm'⟩ + specialize htl hm + omega + · rcases hj with ⟨hl, hl'⟩ + specialize htl l hl + omega + -- from mathlib @[simp] theorem List.take_eq_self_iff (x : List α) {n : Nat} : x.take n = x ↔ x.length ≤ n := From 28419b9834487319b7e2c0cd88581f497ba8ee9e Mon Sep 17 00:00:00 2001 From: jt0202 Date: Sat, 17 May 2025 15:03:54 +0200 Subject: [PATCH 12/14] simp -> simp only --- HumanEvalLean/HumanEval109.lean | 280 ++++++++++++++++++-------------- 1 file changed, 156 insertions(+), 124 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index a3dd413..64319ab 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -15,13 +15,13 @@ theorem List.sum_eq_zero {l : List Nat} : l.sum = 0 ↔ induction l with | nil => simp | cons hd tl ih => - simp [ih] + simp only [sum_cons, Nat.add_eq_zero, ih, length_cons] constructor · intro h i hi cases i with | zero => simp [h] | succ m => - simp + simp only [getElem_cons_succ] apply And.right h · intro h constructor @@ -34,7 +34,7 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i induction l with | nil => simp | cons hd tl ih => - simp [Nat.add_eq_one_iff] + simp only [sum_cons, Nat.add_eq_one_iff, length_cons, ne_eq, exists_and_right] constructor · intro h cases h with @@ -43,7 +43,7 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i rw [ih] at hr rcases hr with ⟨i, hi, h⟩ exists (i + 1) - simp + simp only [getElem_cons_succ, Nat.add_lt_add_iff_right] constructor · exists hi simp [h] @@ -51,19 +51,19 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i cases j with | zero => simp[hl] | succ k => - simp + simp only [getElem_cons_succ] apply (And.right h) - simp at hij + simp only [Nat.add_right_cancel_iff] at hij assumption | inr h => exists 0 - simp [h] + simp only [h, getElem_cons_zero, Nat.zero_lt_succ, exists_const, true_and] rw [sum_eq_zero] at h intro j hj hij cases j with | zero => simp at hij | succ k => - simp + simp only [getElem_cons_succ] rcases h with ⟨_, h⟩ apply h · intro h @@ -71,29 +71,31 @@ theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i cases i with | zero => right - simp at hi - simp [hi] + simp only [getElem_cons_zero, Nat.zero_lt_succ, exists_const] at hi + simp only [hi, true_and] rw [List.sum_eq_zero] intro x hx specialize h (x+1) - simp at h + simp only [Nat.add_lt_add_iff_right, Nat.right_eq_add, Nat.add_eq_zero, Nat.succ_ne_self, + and_false, not_false_eq_true, getElem_cons_succ, forall_const] at h apply h exact hx | succ k => - simp at hi + simp only [getElem_cons_succ, Nat.add_lt_add_iff_right] at hi left constructor · specialize h 0 - simp at h + simp only [Nat.zero_lt_succ, Nat.add_eq_zero, Nat.succ_ne_self, and_false, + not_false_eq_true, getElem_cons_zero, forall_const] at h assumption · rw [ih] exists k rcases hi with ⟨hk, tlk⟩ exists hk - simp [tlk] + simp only [tlk, ne_eq, true_and] intro j hj hkj specialize h (j + 1) - simp at h + simp only [Nat.add_lt_add_iff_right, Nat.add_right_cancel_iff, getElem_cons_succ] at h apply h hj hkj theorem List.two_le_sum_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length), l[i] ≤ 1) : @@ -102,52 +104,53 @@ theorem List.two_le_sum_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length induction l with | nil => simp | cons hd tl ih => - simp + simp only [sum_cons, length_cons, exists_and_left, exists_and_right, ne_eq, exists_prop] by_cases h' : 2 ≤ tl.sum · have : 2 ≤ hd + tl.sum := by omega rw [ih] at h' - · simp [this] + · simp only [this, true_iff] rcases h' with ⟨i, j, hij, hi, hj, h'⟩ exists (i+1) - simp + simp only [getElem_cons_succ, Nat.add_lt_add_iff_right] constructor · exists hi simp [h'] · exists (j+1) - simp [hij] + simp only [Nat.add_right_cancel_iff, hij, not_false_eq_true, getElem_cons_succ, + Nat.add_lt_add_iff_right, true_and] exists hj simp [h'] · intro i hi specialize h (i+1) - simp at h + simp only [length_cons, Nat.add_lt_add_iff_right, getElem_cons_succ] at h apply h hi - · simp at h' + · simp only [Nat.not_le] at h' cases htl : tl.sum with | zero => - simp + simp only [Nat.add_zero] have hhd : ¬ 2 ≤ hd := by intro h' specialize h 0 - simp at h + simp only [length_cons, Nat.zero_lt_succ, getElem_cons_zero, forall_const] at h omega rw [List.sum_eq_zero] at htl - simp [hhd] + simp only [hhd, false_iff, not_exists, not_and, forall_exists_index] intro i hi hi' j hij hj cases i with | zero => - simp at hi' + simp only [getElem_cons_zero] at hi' cases j with | zero => contradiction | succ k => - simp + simp only [getElem_cons_succ] intro hk specialize htl k have : k < tl.length := by omega specialize htl this rw [hk] at htl - simp at htl + simp only [Nat.succ_ne_self] at htl | succ k => - simp at hi' + simp only [getElem_cons_succ] at hi' specialize htl k have : k < tl.length := by omega specialize htl this @@ -155,38 +158,39 @@ theorem List.two_le_sum_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length simp at htl | succ k => have hk : k = 0 := by omega - simp [hk] + simp only [hk, Nat.zero_add, Nat.reduceLeDiff] constructor · intro h₁ exists 0 - simp + simp only [getElem_cons_zero, Nat.zero_lt_succ, exists_const] constructor · specialize h 0 - simp at h + simp only [length_cons, Nat.zero_lt_succ, getElem_cons_zero, forall_const] at h omega - · simp [hk] at htl + · simp only [hk, Nat.zero_add] at htl rw [List.sum_eq_one_iff] at htl rcases htl with ⟨i, hi,hi', _⟩ exists (i+1) - simp + simp only [Nat.right_eq_add, Nat.add_eq_zero, 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₁ - simp [hk] at htl + simp only [hk, Nat.zero_add] at htl rw [List.sum_eq_one_iff] at htl rcases htl with ⟨i, hi,hi', htl⟩ rcases h₁ with ⟨j, hj, k, hjk, hk⟩ cases j with | zero => - simp at hj + simp only [getElem_cons_zero, Nat.zero_lt_succ, exists_const] at hj simp [hj] | succ l => - simp at hj + simp only [getElem_cons_succ, Nat.add_lt_add_iff_right] at hj cases k with | zero => - simp at hk + simp only [getElem_cons_zero, Nat.zero_lt_succ, exists_const] at hk simp [hk] | succ m => - simp at hk + simp only [getElem_cons_succ, Nat.add_lt_add_iff_right] at hk by_cases hil : i = l · specialize htl m rcases hk with ⟨hm, hm'⟩ @@ -199,14 +203,14 @@ theorem List.two_le_sum_iff {l : List Nat} (h : ∀ (i : Nat) (hi : i < l.length -- from mathlib @[simp] theorem List.take_eq_self_iff (x : List α) {n : Nat} : x.take n = x ↔ x.length ≤ n := - ⟨fun h ↦ by rw [← h]; simp; omega, List.take_of_length_le⟩ + ⟨fun h ↦ by rw [← h]; simp only [length_take]; omega, List.take_of_length_le⟩ theorem List.sum_append {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by induction l₁ with | nil => simp | cons hd tl ih => - simp [ih] + simp only [cons_append, sum_cons, ih] omega end helper @@ -245,7 +249,7 @@ theorem List.sum_leftShift_eq_sum {l : List Nat} {n : Nat} : theorem exists_rightShift_iff_exists_leftShift {l : List α} (p : List α → Prop) : (∃ (n : Nat), p (rightShift l n)) ↔ ∃ (n : Nat), p (leftShift l n) := by - simp [leftShift, rightShift] + simp only [rightShift, leftShift] constructor · intro h obtain ⟨n, hn⟩ := h @@ -255,16 +259,16 @@ theorem exists_rightShift_iff_exists_leftShift {l : List α} (p : List α → Pr by_cases n < l.length · exists (l.length - n) have : l.length - (l.length - n) = n := by omega - simp [this] + simp only [this] exact hn · exists 0 - simp + simp only [Nat.sub_zero, List.drop_length, List.take_length, List.nil_append] rename_i h - simp at h + simp only [Nat.not_lt] at h have := List.drop_eq_nil_iff (l := l) (i := n) - simp [this.mpr h] at hn + simp only [this.mpr h, List.nil_append] at hn have := List.take_eq_self_iff l (n := n) - simp [this.mpr h] at hn + simp only [this.mpr h] at hn exact hn def isBreakPoint (l : List Int) (pos : Nat) := @@ -301,11 +305,15 @@ theorem sorted_of_countBreakPoints_eq_zero {l : List Int} (h : countBreakPoints cases tl with | nil => simp | cons hd' tl' => - simp[List.sum_eq_zero, isBreakPoint] at h - simp + simp only [List.length_cons, Nat.le_add_left, isBreakPoint, Nat.add_lt_add_iff_right, + List.getElem_cons_succ, List.getElem_cons_zero, gt_iff_lt, List.sum_eq_zero, + List.length_map, List.length_range, List.getElem_map, List.getElem_range, dite_eq_right_iff, + forall_const] at h + simp only [List.length_cons, Nat.add_lt_add_iff_right, List.getElem_cons_succ] intro i hi specialize h i (by omega) - simp [hi] at h + simp only [hi, ↓reduceDIte, ite_eq_left_iff, Int.not_lt, Nat.succ_ne_self, imp_false, + Int.not_le] at h apply h omega @@ -318,30 +326,32 @@ theorem pairwise_sorted_of_sorted {l : List Int} {i j : Nat} | cons hd tl ih => cases i with | zero => - simp - simp [Nat.lt_iff_add_one_le] at hj + simp only [List.getElem_cons_zero, Nat.zero_add] + simp only [gt_iff_lt, Nat.lt_iff_add_one_le, Nat.zero_add] at hj cases j with | zero => simp at hj | succ k => cases k with | zero => - simp + simp only [Nat.zero_add, List.getElem_cons_succ] specialize sorted 0 - simp at sorted + simp only [Nat.zero_add, List.length_cons, Nat.lt_add_left_iff_pos, + List.getElem_cons_zero, List.getElem_cons_succ] at sorted apply sorted - simp at hij + simp only [Nat.zero_add, List.length_cons, Nat.lt_add_left_iff_pos] at hij assumption | succ m => - simp + simp only [List.getElem_cons_succ] have : m + 1 > 0 := by omega have ih' := ih (i:= 0) (j := m+1) specialize ih' this - simp at ih' - simp at hij + simp only [Nat.zero_add] at ih' + simp only [Nat.zero_add, List.length_cons, Nat.add_lt_add_iff_right] at hij specialize ih' hij apply Int.lt_trans (b := tl[0]) · specialize sorted 0 - simp at sorted + simp only [Nat.zero_add, List.length_cons, Nat.lt_add_left_iff_pos, + List.getElem_cons_zero, List.getElem_cons_succ] at sorted apply sorted apply Nat.lt_trans (m:= m + 1) · simp @@ -349,17 +359,17 @@ theorem pairwise_sorted_of_sorted {l : List Int} {i j : Nat} · apply ih' intro i hi specialize sorted (i+1) - simp at sorted + simp only [List.length_cons, Nat.add_lt_add_iff_right, List.getElem_cons_succ] at sorted apply sorted hi | succ n => - simp + simp only [List.getElem_cons_succ] have : n + 1 + j = (n + j).succ := by omega - simp [this] + simp only [this, Nat.succ_eq_add_one, List.getElem_cons_succ, gt_iff_lt] apply ih · exact hj · intro i hi specialize sorted (i+1) - simp at sorted + simp only [List.length_cons, Nat.add_lt_add_iff_right, List.getElem_cons_succ] at sorted apply sorted hi theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ l.length < 2 := by @@ -368,7 +378,7 @@ theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ have sorted := sorted_of_countBreakPoints_eq_zero h false_or_by_contra rename_i hl - simp at hl + simp only [gt_iff_lt, Nat.not_lt] at hl cases l with | nil => simp at hl | cons hd tl => @@ -378,12 +388,17 @@ theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ have h₁ : hd < (hd' :: tl')[tl'.length] := by have head_lt_getLast := pairwise_sorted_of_sorted (l := hd :: hd' :: tl') (i := 0) (j := tl'.length + 1) (by simp) (by simp) sorted - simp at head_lt_getLast + simp only [List.getElem_cons_zero, Nat.zero_add, + List.getElem_cons_succ] at head_lt_getLast exact head_lt_getLast have h₂ : (hd' :: tl')[tl'.length] < hd := by - simp [countBreakPoints, List.sum_eq_zero, isBreakPoint] at h + simp only [countBreakPoints, List.length_cons, isBreakPoint, Nat.add_lt_add_iff_right, + List.getElem_cons_succ, List.getElem_cons_zero, gt_iff_lt, ite_eq_left_iff, Nat.not_lt, + Nat.le_add_left, List.sum_eq_zero, List.length_map, List.length_range, List.getElem_map, + List.getElem_range, dite_eq_right_iff, forall_const] at h specialize h (tl'.length + 1) - simp at h + simp only [Nat.lt_add_one, Nat.lt_irrefl, ↓reduceDIte, List.getElem_cons_succ, + ite_eq_left_iff, Int.not_lt, Nat.succ_ne_self, imp_false, Int.not_le] at h apply h · trivial · trivial @@ -394,106 +409,114 @@ theorem countBreakPoints_eq_zero_iff {l : List Int} : countBreakPoints l = 0 ↔ theorem countBreakPoints_leftShift_eq_countBreakPoints {l : List Int} {n : Nat} : countBreakPoints (leftShift l n) = countBreakPoints l := by - simp [countBreakPoints] + simp only [countBreakPoints, length_leftShift] by_cases h: l.length < 2 · simp [h] · by_cases hn: n < l.length - · simp [h] + · simp only [h, ↓reduceIte] have : List.map (fun x => isBreakPoint (leftShift l n) x) (List.range l.length) = leftShift (List.map (fun x => isBreakPoint l x) (List.range l.length)) n := by apply List.ext_get · simp - · simp + · simp only [List.length_map, List.length_range, length_leftShift, List.get_eq_getElem, + List.getElem_map, List.getElem_range] intro m h₁ _ conv => rhs - simp [leftShift] + simp only [leftShift] rw [List.getElem_append] simp split - · simp [isBreakPoint, h₁] + · simp only [isBreakPoint, length_leftShift, h₁, ↓reduceDIte, gt_iff_lt] split · have : n + m < l.length := by omega - simp [this] + simp only [this, ↓reduceDIte] by_cases hnm : n + m +1 < l.length - · simp [hnm, leftShift, List.getElem_append] - simp [*] + · simp only [leftShift, List.getElem_append, List.length_drop, List.getElem_drop, + List.getElem_take, hnm, ↓reduceDIte] + simp only [↓reduceDIte, *] have : m + 1 < l.length - n := by omega - simp [this] + simp only [this, ↓reduceDIte] rfl - · simp [hnm, leftShift, List.getElem_append] - simp [*] + · simp only [leftShift, List.getElem_append, List.length_drop, List.getElem_drop, + List.getElem_take, hnm, ↓reduceDIte] + simp only [↓reduceDIte, *] have : ¬ m + 1 < l.length - n := by omega - simp [this] + simp only [this, ↓reduceDIte] have : m + 1 - (l.length - n) = 0 := by omega simp [this] · have : n + m < l.length := by omega - simp [this] + simp only [this, ↓reduceDIte] by_cases hnm : n + m +1 < l.length · omega - · simp [hnm, leftShift, List.getElem_append] - simp [*] + · simp only [leftShift, List.getElem_append, List.length_drop, List.getElem_drop, + List.getElem_take, Nat.add_zero, Nat.zero_le, Nat.sub_eq_zero_of_le, hnm, + ↓reduceDIte] + simp only [↓reduceDIte, *] have : 0 < l.length -n := by omega - simp [this] + simp only [this, ↓reduceDIte] have : n = 0 := by omega simp [this] · rename_i hnm - simp [isBreakPoint, h₁] + simp only [isBreakPoint, length_leftShift, h₁, ↓reduceDIte, gt_iff_lt] by_cases h₂ : m + 1 < l.length - · simp [h₂] + · simp only [h₂, ↓reduceDIte] have : m - (l.length - n) < l.length := by omega - simp [this] + simp only [this, ↓reduceDIte] have : m - (l.length - n) + 1 < l.length := by omega - simp [this, leftShift, List.getElem_append] - simp [hnm] + simp only [leftShift, List.getElem_append, List.length_drop, List.getElem_drop, + List.getElem_take, this, ↓reduceDIte, hnm] have : ¬ m + 1 < l.length - n := by omega - simp [this] + simp only [this, ↓reduceDIte] congr omega - · simp [h₂] + · simp only [h₂, ↓reduceDIte] have : m - (l.length - n) < l.length := by omega - simp [this] + simp only [this, ↓reduceDIte] have : m - (l.length - n) + 1 < l.length := by omega - simp [this, leftShift, List.getElem_append, hnm] + simp only [leftShift, List.getElem_append, List.length_drop, hnm, ↓reduceDIte, + List.getElem_take, List.getElem_drop, Nat.add_zero, Nat.zero_le, + Nat.sub_eq_zero_of_le, this] have : 0 < l.length - n := by omega - simp [this] + simp only [this, ↓reduceDIte] congr omega - simp [this] + simp only [this] rw [List.sum_leftShift_eq_sum (n:= n) (l:= (List.map (fun x => isBreakPoint l x) (List.range l.length)))] · congr funext congr - simp at hn + simp only [Nat.not_lt] at hn simp [leftShift, List.drop_eq_nil_iff.mpr, hn] theorem not_sorted_of_countBreakPoints_ge_two {l : List Int} (h : countBreakPoints l ≥ 2) : ∃ (i : Nat) (hi : i + 1 < l.length), l[i] ≥ l[i+1] := by - simp [countBreakPoints] at h + simp only [countBreakPoints, ge_iff_le] at h split at h · simp at h · rw [List.two_le_sum_iff] at h · rcases h with ⟨i, j, hij, hi, hj, h⟩ - simp[isBreakPoint] at h - simp at hi - simp at hj + simp only [isBreakPoint, gt_iff_lt, List.getElem_map, List.getElem_range] at h + simp only [List.length_map, List.length_range] at hi + simp only [List.length_map, List.length_range] at hj have : i + 1 < l.length ∨ j + 1 < l.length := by omega cases this with | inl this => - simp [this] at h + simp only [this, ↓reduceDIte] at h exists i exists this - simp [hi] at h + simp only [hi, ↓reduceDIte, ite_eq_right_iff, Nat.zero_ne_one, imp_false, Int.not_lt] at h simp [h] | inr this => - simp [this] at h + simp only [this, ↓reduceDIte] at h exists j exists this - simp [hj] at h + simp only [hj, ↓reduceDIte, ite_eq_right_iff, Nat.zero_ne_one, imp_false, Int.not_lt] at h simp [h] - · simp [isBreakPoint] + · simp only [isBreakPoint, gt_iff_lt, List.length_map, List.length_range, List.getElem_map, + List.getElem_range] intro _ _ split <;> split <;> split <;> simp @@ -509,9 +532,11 @@ theorem testCase5 : move_one_ball [] = True := by native_decide theorem move_one_ball_correct {l : List Int} : move_one_ball l = true ↔ ∃ (n : Nat), ∀ (i : Nat) (hi : i + 1 < l.length), - (rightShift l n)[i]'(by simp; omega) < (rightShift l n)[i +1]'(by simpa) := by + (rightShift l n)[i]'(by simp only [length_rightShift]; omega) < + (rightShift l n)[i +1]'(by simpa) := by by_cases hl : l.length < 2 - · simp [move_one_ball, hl, countBreakPoints] + · simp only [move_one_ball, countBreakPoints, hl, ↓reduceIte, Nat.zero_lt_succ, decide_true, + true_iff] exists 0 cases l with | nil => simp @@ -519,9 +544,9 @@ theorem move_one_ball_correct {l : List Int} : cases tl with | nil => simp | cons hd' tl' => - simp at hl + simp only [List.length_cons] at hl omega - · simp [move_one_ball] + · simp only [move_one_ball, decide_eq_true_eq] constructor · intro h rw [Nat.lt_two_iff] at h @@ -530,62 +555,69 @@ theorem move_one_ball_correct {l : List Int} : rw [countBreakPoints_eq_zero_iff] at h contradiction | inr h => - simp [countBreakPoints, hl, List.sum_eq_one_iff] at h + simp only [countBreakPoints, hl, ↓reduceIte, List.sum_eq_one_iff, List.getElem_map, + List.getElem_range, List.length_map, List.length_range, ne_eq, exists_and_left, + exists_prop] at h have := exists_rightShift_iff_exists_leftShift (l:= l) (p := fun (l : List Int) => ∀ (i : Nat) (hi : i + 1 < l.length), l[i]'(by omega) < l[i + 1]) - simp at this + simp only [length_rightShift, length_leftShift] at this rw [this] rcases h with ⟨i, hi1, hi2⟩ exists (i + 1) intro j hj - simp [leftShift] - simp [List.getElem_append] - simp [isBreakPoint] at hi2 + simp only [leftShift] + simp only [List.getElem_append, List.length_drop, List.getElem_drop, List.getElem_take] + simp only [isBreakPoint, gt_iff_lt, dite_eq_right_iff] at hi2 rcases hi2 with ⟨hi, hi2⟩ split · split · specialize hi2 (i + 1 + j) (by omega) have : ¬ i = i + 1 + j := by omega - simp [this] at hi2 + simp only [this, not_false_eq_true, forall_const] at hi2 have : i + 1 + j + 1 < l.length := by omega - simp [this] at hi2 + simp only [this, ↓reduceDIte, ite_eq_left_iff, Int.not_lt, Nat.succ_ne_self, imp_false, + Int.not_le] at hi2 apply hi2 omega · specialize hi2 (i + 1 + j) (by omega) have : ¬ i = i + 1 + j := by omega - simp [this] at hi2 + simp only [this, not_false_eq_true, forall_const] at hi2 have : ¬ i + 1 + j + 1 < l.length := by omega - simp [this] at hi2 + simp only [this, ↓reduceDIte, ite_eq_left_iff, Int.not_lt, Nat.succ_ne_self, imp_false, + Int.not_le] at hi2 have : j + 1 - (l.length - (i + 1)) = 0 := by omega - simp [this] + simp only [this, gt_iff_lt] apply hi2 omega · split · specialize hi2 0 (by omega) have : ¬ i = 0 := by omega - simp [this] at hi2 + simp only [this, not_false_eq_true, Nat.zero_add, Int.lt_irrefl, ↓reduceIte, + forall_const] at hi2 have : 1 < l.length := by omega - simp [this] at hi2 + simp only [this, ↓reduceDIte, ite_eq_left_iff, Int.not_lt, Nat.succ_ne_self, imp_false, + Int.not_le] at hi2 omega · rename_i h₁ h₂ specialize hi2 (j - (l.length - (i + 1))) (by omega) (by omega) have : j - (l.length - (i + 1)) + 1 < l.length := by omega - simp [this] at hi2 + simp only [this, ↓reduceDIte, ite_eq_left_iff, Int.not_lt, Nat.succ_ne_self, imp_false, + Int.not_le] at hi2 have : j - (l.length - (i + 1)) + 1 = j + 1 - (l.length - (i + 1)) := by omega - simp [this] at hi2 + simp only [this] at hi2 apply hi2 omega · false_or_by_contra rename_i h h' - simp at h' + simp only [Nat.not_lt] at h' have := exists_rightShift_iff_exists_leftShift (l:= l) (p := fun (l : List Int) => ∀ (i : Nat) (hi : i + 1 < l.length), l[i]'(by omega) < l[i + 1]) - simp at this + simp only [length_rightShift, length_leftShift] at this rw [this] at h rcases h with ⟨n,h⟩ have := not_sorted_of_countBreakPoints_ge_two (l := leftShift l n) rw [countBreakPoints_leftShift_eq_countBreakPoints] at this - simp [h'] at this + simp only [ge_iff_le, h', length_leftShift, forall_const] at this rcases this with ⟨i, hi, this⟩ specialize h i hi omega From 58bdd17c0f9ac0153aa8c203619d3de7db7c0894 Mon Sep 17 00:00:00 2001 From: jt0202 Date: Mon, 2 Jun 2025 17:24:01 +0200 Subject: [PATCH 13/14] Update to stable release --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 6625aac..5e48589 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.20.0-rc4 +leanprover/lean4:v4.20.0 \ No newline at end of file From a8d293515b8d249e3f3dbed6f112a59bbb95dbfa Mon Sep 17 00:00:00 2001 From: jt0202 Date: Thu, 5 Jun 2025 17:33:15 +0200 Subject: [PATCH 14/14] Suggestions from review --- HumanEvalLean/HumanEval109.lean | 35 +++++++++++---------------------- lean-toolchain | 2 +- 2 files changed, 12 insertions(+), 25 deletions(-) diff --git a/HumanEvalLean/HumanEval109.lean b/HumanEvalLean/HumanEval109.lean index 64319ab..c8b6d4e 100644 --- a/HumanEvalLean/HumanEval109.lean +++ b/HumanEvalLean/HumanEval109.lean @@ -3,31 +3,18 @@ variable {α : Type _} section helper theorem Nat.lt_two_iff {n : Nat} : n < 2 ↔ n = 0 ∨ n = 1 := by - cases n with - | zero => simp - | succ m => - cases m with - | zero => simp - | succ o => simp + omega + +theorem List.exists_mem_and {P : α → Prop} {l : List α} : + (∃ a, a ∈ l ∧ P a) ↔ (∃ (n : Nat), ∃ h, P (l[n]'h)) := by + refine ⟨fun ⟨a, h, h'⟩ => ?_, fun ⟨n, h, h'⟩ => ⟨l[n], by simp, h'⟩⟩ + obtain ⟨i, h'', rfl⟩ := List.getElem_of_mem h + exact ⟨_, _, h'⟩ theorem List.sum_eq_zero {l : List Nat} : l.sum = 0 ↔ - ∀ (i : Nat) (hi : i < l.length), l[i]'hi = 0 := by - induction l with - | nil => simp - | cons hd tl ih => - simp only [sum_cons, Nat.add_eq_zero, ih, length_cons] - constructor - · intro h i hi - cases i with - | zero => simp [h] - | succ m => - simp only [getElem_cons_succ] - apply And.right h - · intro h - constructor - · apply h 0 (by simp) - · intro i hi - apply h (i + 1) (by omega) + ∀ (i : Nat) (hi : i < l.length), l[i]'hi = 0 := by + rw [← Decidable.not_iff_not] + simp [← Nat.pos_iff_ne_zero, Nat.sum_pos_iff_exists_pos, List.exists_mem_and] theorem List.sum_eq_one_iff {l : List Nat} : l.sum = 1 ↔ ∃ (i : Nat) (hi : i < l.length), l[i] = 1 ∧ ∀ (j : Nat) (hj : j < l.length), i ≠ j → l[j] = 0 := by @@ -244,7 +231,7 @@ theorem leftShiftExample2 : leftShift [3,4,5,1,2] 3 = [1,2,3,4,5] := by native_d theorem List.sum_leftShift_eq_sum {l : List Nat} {n : Nat} : (leftShift l n).sum = l.sum := by - simp [leftShift] + simp only [leftShift] rw [List.sum_append, Nat.add_comm, ← List.sum_append, take_append_drop] theorem exists_rightShift_iff_exists_leftShift {l : List α} (p : List α → Prop) : diff --git a/lean-toolchain b/lean-toolchain index 5e48589..67499a5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.20.0 \ No newline at end of file +leanprover/lean4:v4.20.1 \ No newline at end of file