Skip to content

fix: do not redefine clog2 #322

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
chenson2018 merged 2 commits into from
Feb 5, 2026
Merged

fix: do not redefine clog2 #322

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c27d491
Do not redefine clog2
eric-wieser Feb 5, 2026
b16b640
merge conflict
chenson2018 Feb 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 15 additions & 23 deletions Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,48 +130,40 @@ def timeMergeSortRec : ℕ → ℕ
| 1 => 0
| n@(_+2) => timeMergeSortRec (n/2) + timeMergeSortRec ((n-1)/2 + 1) + n

/-- The ceiling of Nat.log 2 -/
@[grind =]
def clog2 (n : ℕ) : ℕ :=
if n ≤ 1 then 0 else Nat.log 2 (n - 1) + 1
open Nat (clog)

/-- Key Lemma: ⌈log2 ⌈n/2⌉⌉ ≤ ⌈log2 n⌉ - 1 for n > 1 -/
@[grind →]
lemma clog2_half_le (n : ℕ) (h : n > 1) : clog2 ((n + 1) / 2) ≤ clog2 n - 1 := by
have := Nat.sub_mul_div (n + 1) 2 1
grind [Nat.log_eq_zero_iff, Nat.log_div_base]
lemma clog2_half_le (n : ℕ) (h : n > 1) : clog 2 ((n + 1) / 2) ≤ clog 2 n - 1 := by
rw [Nat.clog_of_one_lt one_lt_two h]
grind

/-- Same logic for the floor half: ⌈log2 ⌊n/2⌋⌉ ≤ ⌈log2 n⌉ - 1 -/
@[grind →]
lemma clog2_floor_half_le (n : ℕ) (h : n > 1) : clog2 (n / 2) ≤ clog2 n - 1 := by
lemma clog2_floor_half_le (n : ℕ) (h : n > 1) : clog 2 (n / 2) ≤ clog 2 n - 1 := by
apply Nat.le_trans _ (clog2_half_le n h)
simp only [clog2]
split_ifs
· grind
· grind
· grind
· grw [Nat.log_mono_right]
grind
apply Nat.clog_monotone
grind

private lemma some_algebra (n : ℕ) :
(n / 2 + 1) * clog2 (n / 2 + 1) + ((n + 1) / 2 + 1) * clog2 ((n + 1) / 2 + 1) + (n + 2) ≤
(n + 2) * clog2 (n + 2) := by
(n / 2 + 1) * clog 2 (n / 2 + 1) + ((n + 1) / 2 + 1) * clog 2 ((n + 1) / 2 + 1) + (n + 2) ≤
(n + 2) * clog 2 (n + 2) := by
-- 1. Substitution: Let N = n_1 + 2 to clean up the expression
let N := n + 2
have hN : N ≥ 2 := by omega
-- 2. Rewrite the terms using N
have t1 : n / 2 + 1 = N / 2 := by omega
have t2 : (n + 1) / 2 + 1 = (N + 1) / 2 := by omega
have t3 : n + 1 + 1 = N := by omega
let k := clog2 N
have h_bound_l : clog2 (N / 2) ≤ k - 1 := clog2_floor_half_le N hN
have h_bound_r : clog2 ((N + 1) / 2) ≤ k - 1 := clog2_half_le N hN
let k := clog 2 N
have h_bound_l : clog 2 (N / 2) ≤ k - 1 := clog2_floor_half_le N hN
have h_bound_r : clog 2 ((N + 1) / 2) ≤ k - 1 := clog2_half_le N hN
have h_split : N / 2 + (N + 1) / 2 = N := by omega
grw [t1, t2, t3, h_bound_l, h_bound_r, ←Nat.add_mul, h_split]
exact Nat.le_refl (N * (k - 1) + N)

/-- Upper bound function for merge sort time complexity: `T(n) = n * ⌈log₂ n⌉` -/
abbrev T (n : ℕ) : ℕ := n * clog2 n
abbrev T (n : ℕ) : ℕ := n * clog 2 n

/-- Solve the recurrence -/
theorem timeMergeSortRec_le (n : ℕ) : timeMergeSortRec n ≤ T n := by
Expand Down Expand Up @@ -216,8 +208,8 @@ theorem mergeSort_time_le (xs : List α) :

/-- Time complexity of mergeSort -/
theorem mergeSort_time (xs : List α) :
let n := xs.length
(mergeSort xs).time ≤ n * clog2 n := by
let n := xs.length
(mergeSort xs).time ≤ n * clog 2 n := by
grind [mergeSort_time_le, timeMergeSortRec_le]

end TimeComplexity
Expand Down