From 9a815c966b800589bd7deb257a66a1b5a2a01863 Mon Sep 17 00:00:00 2001 From: "Christopher J. R. Lloyd" Date: Sat, 11 Apr 2026 22:04:36 -0400 Subject: [PATCH 1/4] Time Complexity of List.Length --- Cslib.lean | 1 + Cslib/Foundations/Data/List/Basic.lean | 52 ++++++++++++++++++++++++++ 2 files changed, 53 insertions(+) create mode 100644 Cslib/Foundations/Data/List/Basic.lean diff --git a/Cslib.lean b/Cslib.lean index 3e5977af2..c82e5d3c2 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -43,6 +43,7 @@ public import Cslib.Foundations.Control.Monad.Free.Fold public import Cslib.Foundations.Data.BiTape public import Cslib.Foundations.Data.FinFun public import Cslib.Foundations.Data.HasFresh +public import Cslib.Foundations.Data.List.Basic public import Cslib.Foundations.Data.Nat.Segment public import Cslib.Foundations.Data.OmegaSequence.Defs public import Cslib.Foundations.Data.OmegaSequence.Flatten diff --git a/Cslib/Foundations/Data/List/Basic.lean b/Cslib/Foundations/Data/List/Basic.lean new file mode 100644 index 000000000..ca4b12115 --- /dev/null +++ b/Cslib/Foundations/Data/List/Basic.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2026 Christopher J. R. Lloyd. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christopher J. R. Lloyd +-/ +module + +public import Cslib.Algorithms.Lean.TimeM + + +/-! +# List Algorithms + +In this file we prove `List.length` runs in eaxctly n steps using the +time monad over the list `TimeM Nat Nat`. The time complexity of +`List.length` is the length of the List. + +-- +## Main results + +- `List.length_time`: `List.length` runs in exactly n steps + +-/ + +namespace Cslib.Foundations.Data + +open Cslib.Algorithms.Lean +open Cslib.Algorithms.Lean.TimeM + +/-- List.Length with TimeM Monad. -/ +public def List.length : List α → TimeM Nat Nat + | .nil => return 0 + | .cons _ as => do ✓ (Functor.map (fun x => x + 1) (List.length as)) + +section Correctness + +/-- List.Length matches List.length in Batteries. -/ +theorem ret_list_length : ∀ xs : List α, ⟪List.length xs⟫ = _root_.List.length xs := by + intros + fun_induction List.length with grind [List.length] + +end Correctness + +section TimeComplexity + +/-- The recursive list length algorithm runs in `n` steps for a list of length `n`. -/ +public theorem List.length_time (xs : List α) : (List.length xs).time = _root_.List.length xs := by + fun_induction List.length with grind [List.length] + +end TimeComplexity + +end Cslib.Foundations.Data From 3c1c889fe5aa6bfa8687acf063be206773fdb707 Mon Sep 17 00:00:00 2001 From: "Christopher J. R. Lloyd" Date: Sun, 12 Apr 2026 12:20:09 -0400 Subject: [PATCH 2/4] Move to Cslib.Algorithms.Lean.ListLength namespace --- .../Data/List => Algorithms/Lean/ListLength}/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) rename Cslib/{Foundations/Data/List => Algorithms/Lean/ListLength}/Basic.lean (94%) diff --git a/Cslib/Foundations/Data/List/Basic.lean b/Cslib/Algorithms/Lean/ListLength/Basic.lean similarity index 94% rename from Cslib/Foundations/Data/List/Basic.lean rename to Cslib/Algorithms/Lean/ListLength/Basic.lean index ca4b12115..0e7dfc4e5 100644 --- a/Cslib/Foundations/Data/List/Basic.lean +++ b/Cslib/Algorithms/Lean/ListLength/Basic.lean @@ -22,7 +22,7 @@ time monad over the list `TimeM Nat Nat`. The time complexity of -/ -namespace Cslib.Foundations.Data +namespace Cslib.Algorithms.Lean.ListLength open Cslib.Algorithms.Lean open Cslib.Algorithms.Lean.TimeM @@ -49,4 +49,4 @@ public theorem List.length_time (xs : List α) : (List.length xs).time = _root_. end TimeComplexity -end Cslib.Foundations.Data +end Cslib.Algorithms.Lean.ListLength From 7f3cb3e181b76f45ee5c57c1cc5783d3185e875f Mon Sep 17 00:00:00 2001 From: Chris Lloyd Date: Mon, 13 Apr 2026 23:03:29 -0400 Subject: [PATCH 3/4] Update Basic.lean Co-authored-by: Eric Wieser --- Cslib/Algorithms/Lean/ListLength/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Algorithms/Lean/ListLength/Basic.lean b/Cslib/Algorithms/Lean/ListLength/Basic.lean index 0e7dfc4e5..89ea08903 100644 --- a/Cslib/Algorithms/Lean/ListLength/Basic.lean +++ b/Cslib/Algorithms/Lean/ListLength/Basic.lean @@ -30,7 +30,7 @@ open Cslib.Algorithms.Lean.TimeM /-- List.Length with TimeM Monad. -/ public def List.length : List α → TimeM Nat Nat | .nil => return 0 - | .cons _ as => do ✓ (Functor.map (fun x => x + 1) (List.length as)) + | .cons _ as => do ✓ ((fun x => x + 1) <$> (List.length as)) section Correctness From 77dc1bb935d3e5bc84c2565924d03d286d31e371 Mon Sep 17 00:00:00 2001 From: "Christopher J. R. Lloyd" Date: Tue, 14 Apr 2026 21:49:07 -0400 Subject: [PATCH 4/4] Update to Eric's Second suggestion --- Cslib/Algorithms/Lean/ListLength/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Algorithms/Lean/ListLength/Basic.lean b/Cslib/Algorithms/Lean/ListLength/Basic.lean index 89ea08903..9f2321555 100644 --- a/Cslib/Algorithms/Lean/ListLength/Basic.lean +++ b/Cslib/Algorithms/Lean/ListLength/Basic.lean @@ -30,7 +30,7 @@ open Cslib.Algorithms.Lean.TimeM /-- List.Length with TimeM Monad. -/ public def List.length : List α → TimeM Nat Nat | .nil => return 0 - | .cons _ as => do ✓ ((fun x => x + 1) <$> (List.length as)) + | .cons _ as => do ✓ return (← List.length as) + 1 section Correctness