From ac846a1b9f1d3465682c1a2395e0d04c689290b1 Mon Sep 17 00:00:00 2001 From: Abhirup Date: Fri, 8 May 2026 10:12:00 +0530 Subject: [PATCH] Added new feat MinList --- Cslib.lean | 1 + .../Algorithms/Lean/MergeSort/MergeSort.lean | 12 ++ Cslib/Algorithms/Lean/MinList/MinList.lean | 119 ++++++++++++++++++ 3 files changed, 132 insertions(+) create mode 100644 Cslib/Algorithms/Lean/MinList/MinList.lean diff --git a/Cslib.lean b/Cslib.lean index 92a251cdf..03d7fc5d7 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -1,6 +1,7 @@ module -- shake: keep-all public import Cslib.Algorithms.Lean.MergeSort.MergeSort +public import Cslib.Algorithms.Lean.MinList.MinList public import Cslib.Algorithms.Lean.TimeM public import Cslib.Computability.Automata.Acceptors.Acceptor public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean index 6de2ca6e6..12f0eea1a 100644 --- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean +++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean @@ -21,6 +21,7 @@ over the list `TimeM ℕ (List α)`. The time complexity of `mergeSort` is the n ## Main results - `mergeSort_correct`: `mergeSort` permutes the list into a sorted one. +- `mergeSort_idempotent`: sorting the sorted output does not change it. - `mergeSort_time`: The number of comparisons of `mergeSort` is at most `n*⌈log₂ n⌉`. -/ @@ -110,6 +111,17 @@ theorem mergeSort_perm (xs : List α) : ⟪mergeSort xs⟫ ~ xs := by theorem mergeSort_correct (xs : List α) : IsSorted ⟪mergeSort xs⟫ ∧ ⟪mergeSort xs⟫ ~ xs := ⟨mergeSort_sorted xs, mergeSort_perm xs⟩ +/-- MergeSort is idempotent on values: sorting the sorted output does not change it. -/ +theorem mergeSort_idempotent (xs : List α) : + ⟪mergeSort ⟪mergeSort xs⟫⟫ = ⟪mergeSort xs⟫ := by + -- Both sides are sorted and permutations of each other. + have hperm : ⟪mergeSort ⟪mergeSort xs⟫⟫ ~ ⟪mergeSort xs⟫ := by + simpa using (mergeSort_perm (xs := ⟪mergeSort xs⟫)) + have hsorted₁ : IsSorted ⟪mergeSort ⟪mergeSort xs⟫⟫ := mergeSort_sorted (xs := ⟪mergeSort xs⟫) + have hsorted₂ : IsSorted ⟪mergeSort xs⟫ := mergeSort_sorted (xs := xs) + -- Mathlib: a sorted permutation is unique. + simpa using List.eq_of_perm_of_sorted hperm hsorted₁ hsorted₂ + end Correctness section TimeComplexity diff --git a/Cslib/Algorithms/Lean/MinList/MinList.lean b/Cslib/Algorithms/Lean/MinList/MinList.lean new file mode 100644 index 000000000..38d0ed55e --- /dev/null +++ b/Cslib/Algorithms/Lean/MinList/MinList.lean @@ -0,0 +1,119 @@ +module + +public import Cslib.Algorithms.Lean.TimeM +public import Mathlib.Tactic + +/-! +# Minimum of a list (linear scan) + +We implement a simple linear scan algorithm that returns the minimum element of a list, +counting comparisons as time cost. + +We return an `Option α` to handle the empty list. + +## Main results + +- `minScan_correct`: if the output is `some m`, then `m` is an element of the list and is + below every element of the list. +- `minScan_time_le`: the number of comparisons is at most the list length. +-/ + +@[expose] public section + +set_option autoImplicit false + +namespace Cslib.Algorithms.Lean.TimeM + +open List + +variable {α : Type} [LinearOrder α] + +/-- `m` is a minimum element of `xs` if it is below every element of `xs`. -/ +abbrev MinOfList (m : α) (xs : List α) : Prop := ∀ z ∈ xs, m ≤ z + +/-- Compute the minimum of a list by scanning from the right, counting comparisons. + +Cost model: each comparison (`x ≤ m`) costs one tick. -/ +def minScan : List α → TimeM ℕ (Option α) + | [] => return none + | x :: xs => do + let r ← minScan xs + match r with + | none => return some x + | some m => do + ✓ + if x ≤ m then + return some x + else + return some m + +section Correctness + +/-- Correctness for `minScan`. + +If `minScan xs` returns `some m`, then `m ∈ xs` and `m` is a minimum element of `xs`. +If it returns `none`, then `xs` is empty. -/ +theorem minScan_correct (xs : List α) : + match ⟪minScan xs⟫ with + | none => xs = [] + | some m => m ∈ xs ∧ MinOfList m xs := by + induction xs with + | nil => + simp [minScan] + | cons x xs ih => + cases h : ⟪minScan xs⟫ with + | none => + have hxsempty : xs = [] := by + simpa [h] using ih + subst hxsempty + simp [minScan, h] + | some m => + have ihm : m ∈ xs ∧ MinOfList m xs := by + simpa [h] using ih + by_cases hxm : x ≤ m + · -- choose `x` + refine ?_ + simp [minScan, h, hxm, ihm] + intro z hz + rcases hz with rfl | hz + · exact le_rfl + · exact le_trans hxm (ihm.2 z hz) + · -- choose `m` + have hmx : m ≤ x := by + have ht := le_total m x + cases ht with + | inl hmx => exact hmx + | inr hcontr => exact False.elim (hxm hcontr) + refine ?_ + simp [minScan, h, hxm, ihm] + intro z hz + rcases hz with rfl | hz + · exact hmx + · exact ihm.2 z hz + +end Correctness + +section TimeComplexity + +/-- The scan does at most one comparison per element. -/ +theorem minScan_time_le (xs : List α) : (minScan xs).time ≤ xs.length := by + induction xs with + | nil => + simp [minScan] + | cons x xs ih => + -- Split on whether the recursive call found a minimum. + cases h : ⟪minScan xs⟫ with + | none => + -- No comparison performed at this step. + have : (minScan xs).time ≤ xs.length + 1 := le_trans ih (Nat.le_succ _) + simpa [minScan, time_bind, h, Nat.succ_eq_add_one, Nat.add_assoc, Nat.add_comm, + Nat.add_left_comm] using this + | some m => + -- One comparison performed at this step. + have : (minScan xs).time + 1 ≤ xs.length + 1 := Nat.add_le_add_right ih 1 + simpa [minScan, time_bind, h, Nat.succ_eq_add_one, Nat.add_assoc, Nat.add_comm, + Nat.add_left_comm] using this + +end TimeComplexity + +end Cslib.Algorithms.Lean.TimeM