Skip to content

Commit 8371c12

Browse files
kim-emclaude
kim-em
and
claude
committed
feat(Query): query complexity framework with sorting lower bound
Add a framework for proving upper and lower bounds on query complexity of comparison-based algorithms, using `Prog` (free monad over query types) with oracle-parametric evaluation and structural query counting. Results: - Insertion sort: correctness + O(n²) upper bound - Merge sort: correctness + n·⌈log₂ n⌉ upper bound - Lower bound: any correct comparison sort on an infinite type needs ≥ ⌈log₂(n!)⌉ queries (via adversarial pigeonhole on QueryTree depth) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 11957b8 commit 8371c12

File tree

12 files changed

+1245
-0
lines changed

12 files changed

+1245
-0
lines changed

‎Cslib.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,17 @@
11
module -- shake: keep-all
22

33
public import Cslib.Algorithms.Lean.MergeSort.MergeSort
4+
public import Cslib.Algorithms.Lean.Query.Bounds
5+
public import Cslib.Algorithms.Lean.Query.Prog
6+
public import Cslib.Algorithms.Lean.Query.QueryTree
7+
public import Cslib.Algorithms.Lean.Query.Sort.Insertion.Defs
8+
public import Cslib.Algorithms.Lean.Query.Sort.Insertion.Lemmas
9+
public import Cslib.Algorithms.Lean.Query.Sort.IsSort
10+
public import Cslib.Algorithms.Lean.Query.Sort.LEQuery
11+
public import Cslib.Algorithms.Lean.Query.Sort.LowerBound
12+
public import Cslib.Algorithms.Lean.Query.Sort.Merge.Defs
13+
public import Cslib.Algorithms.Lean.Query.Sort.Merge.Lemmas
14+
public import Cslib.Algorithms.Lean.Query.Sort.QueryTree
415
public import Cslib.Algorithms.Lean.TimeM
516
public import Cslib.Computability.Automata.Acceptors.Acceptor
617
public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor

‎Cslib/Algorithms/Lean/Query/Bounds.lean‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
/-
2+
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kim Morrison, Sebastian Graf
5+
-/
6+
module
7+
8+
public import Cslib.Algorithms.Lean.Query.Prog
9+
10+
/-! # Upper and Lower Bounds for Query Complexity
11+
12+
Definitions of upper and lower bounds on the number of queries a program makes,
13+
quantified over oracles.
14+
-/
15+
16+
open Cslib.Query
17+
18+
public section
19+
20+
namespace Cslib.Query
21+
22+
/-- Upper bound: for all oracles, inputs of size ≤ n make at most `bound n` queries. -/
23+
@[expose] def UpperBound (prog : α → Prog Q β)
24+
(size : α → Nat) (bound : Nat → Nat) : Prop :=
25+
∀ (oracle : {ι : Type} → Q ι → ι) (n : Nat) (x : α),
26+
size x ≤ n → (prog x).queriesOn oracle ≤ bound n
27+
28+
/-- Lower bound: for every size n, there exists an input and oracle
29+
making the program perform ≥ `bound n` queries. -/
30+
@[expose] def LowerBound (prog : α → Prog Q β)
31+
(size : α → Nat) (bound : Nat → Nat) : Prop :=
32+
∀ (n : Nat), ∃ (x : α), size x ≤ n ∧
33+
∃ (oracle : {ι : Type} → Q ι → ι), bound n ≤ (prog x).queriesOn oracle
34+
35+
end Cslib.Query
36+
37+
end -- public section

‎Cslib/Algorithms/Lean/Query/Prog.lean‎

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
/-
2+
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Sorrachai Yingchareonthawornchai, Kim Morrison, Sebastian Graf, Shreyas Srinivas
5+
-/
6+
module
7+
8+
public import Cslib.Foundations.Control.Monad.Free
9+
10+
/-! # Prog: Programs as Free Monads over Query Types
11+
12+
`Prog Q α` is an alias for `FreeM Q α`, representing a program that makes queries of type `Q`
13+
and returns a result of type `α`. A query type `Q : Type → Type` maps each query to its
14+
response type.
15+
16+
The key operations are:
17+
- `Prog.eval oracle p`: evaluate `p` by answering each query using `oracle`
18+
- `Prog.queriesOn oracle p`: count the queries along the oracle-determined path
19+
20+
Because the oracle is supplied *after* the program produces its query plan (the `Prog` tree),
21+
a sound implementation of `prog` has no way to "guess" what the oracle would respond.
22+
This is the foundation of the anti-cheating guarantee for both upper and lower bounds.
23+
24+
This provides an alternative to the `TimeM`-based cost analysis in
25+
`Cslib.Algorithms.Lean.MergeSort`: here query counting is structural (derived from the
26+
`Prog` tree) rather than annotation-based.
27+
-/
28+
29+
open Cslib
30+
31+
public section
32+
33+
namespace Cslib.Query
34+
35+
/-- A program that makes queries of type `Q` and returns a result of type `α`.
36+
This is `FreeM Q α`, the free monad over the query type. -/
37+
abbrev Prog (Q : Type → Type) (α : Type) := FreeM Q α
38+
39+
namespace Prog
40+
41+
variable {Q : Type → Type} {α β : Type}
42+
43+
/-- Evaluate a program by answering each query using `oracle`. -/
44+
@[expose] def eval (oracle : {ι : Type} → Q ι → ι) : Prog Q α → α
45+
| .pure a => a
46+
| .liftBind op cont => eval oracle (cont (oracle op))
47+
48+
/-- Count the number of queries along the path determined by `oracle`. -/
49+
@[expose] def queriesOn (oracle : {ι : Type} → Q ι → ι) : Prog Q α → Nat
50+
| .pure _ => 0
51+
| .liftBind op cont => 1 + queriesOn oracle (cont (oracle op))
52+
53+
-- Simp lemmas for eval
54+
55+
@[simp] theorem eval_pure (oracle : {ι : Type} → Q ι → ι) (a : α) :
56+
eval oracle (.pure a : Prog Q α) = a := rfl
57+
58+
@[simp] theorem eval_liftBind (oracle : {ι : Type} → Q ι → ι)
59+
{ι : Type} (op : Q ι) (cont : ι → Prog Q α) :
60+
eval oracle (.liftBind op cont) = eval oracle (cont (oracle op)) := rfl
61+
62+
@[simp] theorem eval_bind (oracle : {ι : Type} → Q ι → ι)
63+
(t : Prog Q α) (f : α → Prog Q β) :
64+
eval oracle (t.bind f) = eval oracle (f (eval oracle t)) := by
65+
induction t with
66+
| pure a => rfl
67+
| liftBind op cont ih => exact ih (oracle op)
68+
69+
-- Simp lemmas for queriesOn
70+
71+
@[simp] theorem queriesOn_pure (oracle : {ι : Type} → Q ι → ι) (a : α) :
72+
queriesOn oracle (.pure a : Prog Q α) = 0 := rfl
73+
74+
@[simp] theorem queriesOn_liftBind (oracle : {ι : Type} → Q ι → ι)
75+
{ι : Type} (op : Q ι) (cont : ι → Prog Q α) :
76+
queriesOn oracle (.liftBind op cont) = 1 + queriesOn oracle (cont (oracle op)) := rfl
77+
78+
@[simp] theorem queriesOn_bind (oracle : {ι : Type} → Q ι → ι)
79+
(t : Prog Q α) (f : α → Prog Q β) :
80+
queriesOn oracle (t.bind f) =
81+
queriesOn oracle t + queriesOn oracle (f (eval oracle t)) := by
82+
induction t with
83+
| pure a => simp [FreeM.bind]
84+
| liftBind op cont ih =>
85+
simp only [FreeM.bind, queriesOn_liftBind, eval_liftBind, ih (oracle op)]
86+
omega
87+
88+
end Prog
89+
90+
end Cslib.Query
91+
92+
end -- public section

‎Cslib/Algorithms/Lean/Query/QueryTree.lean‎

Lines changed: 139 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,139 @@
1+
/-
2+
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kim Morrison, Sebastian Graf
5+
-/
6+
module
7+
8+
public import Mathlib.Data.Nat.Log
9+
public import Mathlib.Data.Fintype.Card
10+
11+
/-! # QueryTree: Decision Trees for Query Complexity Lower Bounds
12+
13+
`QueryTree Q R α` is a free monad specialized to a single query type: queries take
14+
input `Q` and return `R`, with final results of type `α`. It reifies an algorithm's
15+
query pattern as an explicit decision tree.
16+
17+
The key advantage over `Prog`/`FreeM` for lower bound proofs is that `R` is a fixed type
18+
parameter (not existentially quantified per query), making structural induction with
19+
pigeonhole arguments straightforward.
20+
21+
## Main Definitions
22+
23+
- `QueryTree Q R α` — the decision tree type
24+
- `QueryTree.ask` — the canonical single-query tree
25+
- `QueryTree.eval` — evaluate with a specific oracle
26+
- `QueryTree.queriesOn` — count queries along an oracle-determined path
27+
-/
28+
29+
public section
30+
31+
namespace Cslib.Query
32+
33+
/-- A decision tree over queries of type `Q → R`, with results of type `α`.
34+
35+
This is the free monad specialized to a single fixed-type operation, used to reify
36+
algorithms as explicit trees for query complexity lower bounds. -/
37+
inductive QueryTree (Q : Type) (R : Type) (α : Type) where
38+
/-- A completed computation returning value `a`. -/
39+
| pure (a : α) : QueryTree Q R α
40+
/-- A query node: asks query `q`, then continues based on the response. -/
41+
| query (q : Q) (cont : R → QueryTree Q R α) : QueryTree Q R α
42+
43+
namespace QueryTree
44+
45+
variable {Q R α β γ : Type}
46+
47+
/-- Lift a single query into the tree. -/
48+
@[expose] def ask (q : Q) : QueryTree Q R R := .query q .pure
49+
50+
/-- Monadic bind for query trees. -/
51+
@[expose] protected def bind : QueryTree Q R α → (α → QueryTree Q R β) → QueryTree Q R β
52+
| .pure a, f => f a
53+
| .query q cont, f => .query q (fun r => (cont r).bind f)
54+
55+
/-- Functorial map for query trees. -/
56+
@[expose] protected def map (f : α → β) : QueryTree Q R α → QueryTree Q R β
57+
| .pure a => .pure (f a)
58+
| .query q cont => .query q (fun r => (cont r).map f)
59+
60+
protected theorem bind_pure : ∀ (x : QueryTree Q R α), x.bind .pure = x
61+
| .pure _ => rfl
62+
| .query _ cont => by simp [QueryTree.bind, QueryTree.bind_pure]
63+
64+
protected theorem bind_assoc :
65+
∀ (x : QueryTree Q R α) (f : α → QueryTree Q R β) (g : β → QueryTree Q R γ),
66+
(x.bind f).bind g = x.bind (fun a => (f a).bind g)
67+
| .pure _, _, _ => rfl
68+
| .query _ cont, f, g => by simp [QueryTree.bind, QueryTree.bind_assoc]
69+
70+
protected theorem bind_pure_comp (f : α → β) :
71+
∀ (x : QueryTree Q R α), x.bind (.pure ∘ f) = x.map f
72+
| .pure _ => rfl
73+
| .query _ cont => by simp [QueryTree.bind, QueryTree.map, QueryTree.bind_pure_comp]
74+
75+
protected theorem id_map : ∀ (x : QueryTree Q R α), x.map id = x
76+
| .pure _ => rfl
77+
| .query _ cont => by simp [QueryTree.map, QueryTree.id_map]
78+
79+
instance : Monad (QueryTree Q R) where
80+
pure := .pure
81+
bind := .bind
82+
83+
instance : LawfulMonad (QueryTree Q R) := LawfulMonad.mk'
84+
(bind_pure_comp := fun _ _ => rfl)
85+
(id_map := QueryTree.bind_pure)
86+
(pure_bind := fun _ _ => rfl)
87+
(bind_assoc := QueryTree.bind_assoc)
88+
89+
-- Core operations
90+
91+
/-- Evaluate a query tree with a specific oracle, returning the final result. -/
92+
@[expose] def eval (oracle : Q → R) : QueryTree Q R α → α
93+
| .pure a => a
94+
| .query q cont => eval oracle (cont (oracle q))
95+
96+
/-- Count the number of queries along the path determined by `oracle`. -/
97+
@[expose] def queriesOn (oracle : Q → R) : QueryTree Q R α → Nat
98+
| .pure _ => 0
99+
| .query q cont => 1 + queriesOn oracle (cont (oracle q))
100+
101+
-- Simp lemmas
102+
103+
@[simp] theorem eval_pure' (oracle : Q → R) (a : α) :
104+
(QueryTree.pure a : QueryTree Q R α).eval oracle = a := rfl
105+
106+
@[simp] theorem eval_query (oracle : Q → R) (q : Q) (cont : R → QueryTree Q R α) :
107+
(QueryTree.query q cont).eval oracle = (cont (oracle q)).eval oracle := rfl
108+
109+
@[simp] theorem eval_bind (oracle : Q → R) (t : QueryTree Q R α) (f : α → QueryTree Q R β) :
110+
(t.bind f).eval oracle = (f (t.eval oracle)).eval oracle := by
111+
induction t with
112+
| pure a => rfl
113+
| query q cont ih => exact ih (oracle q)
114+
115+
@[simp] theorem queriesOn_pure' (oracle : Q → R) (a : α) :
116+
(QueryTree.pure a : QueryTree Q R α).queriesOn oracle = 0 := rfl
117+
118+
@[simp] theorem queriesOn_query (oracle : Q → R) (q : Q) (cont : R → QueryTree Q R α) :
119+
(QueryTree.query q cont).queriesOn oracle = 1 + (cont (oracle q)).queriesOn oracle := rfl
120+
121+
/-- Queries of `t.bind f` = queries of `t` + queries of the continuation. -/
122+
@[simp] theorem queriesOn_bind (oracle : Q → R) (t : QueryTree Q R α) (f : α → QueryTree Q R β) :
123+
(t.bind f).queriesOn oracle =
124+
t.queriesOn oracle + (f (t.eval oracle)).queriesOn oracle := by
125+
induction t with
126+
| pure a => simp [QueryTree.bind, queriesOn, eval]
127+
| query q cont ih => simp only [QueryTree.bind, queriesOn_query, eval_query, ih (oracle q)]; omega
128+
129+
@[simp] theorem queriesOn_ask (oracle : Q → R) (q : Q) :
130+
(ask q : QueryTree Q R R).queriesOn oracle = 1 := rfl
131+
132+
@[simp] theorem eval_ask (oracle : Q → R) (q : Q) :
133+
(ask q : QueryTree Q R R).eval oracle = oracle q := rfl
134+
135+
end QueryTree
136+
137+
end Cslib.Query
138+
139+
end -- public section

‎Cslib/Algorithms/Lean/Query/Sort/Insertion/Defs.lean‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
/-
2+
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kim Morrison
5+
-/
6+
module
7+
8+
public import Cslib.Algorithms.Lean.Query.Sort.LEQuery
9+
10+
/-! # Insertion Sort as a Query Program
11+
12+
Insertion sort implemented as a `Prog (LEQuery α)`, making all comparison queries explicit.
13+
-/
14+
15+
open Cslib.Query
16+
17+
public section
18+
19+
namespace Cslib.Query
20+
21+
/-- Insert `x` into a sorted list using comparison queries. -/
22+
@[expose] def orderedInsert (x : α) : List α → Prog (LEQuery α) (List α)
23+
| [] => pure [x]
24+
| y :: ys => do
25+
let le ← LEQuery.ask x y
26+
if le then
27+
pure (x :: y :: ys)
28+
else do
29+
let rest ← orderedInsert x ys
30+
pure (y :: rest)
31+
32+
/-- Sort a list using insertion sort with comparison queries. -/
33+
@[expose] def insertionSort : List α → Prog (LEQuery α) (List α)
34+
| [] => pure []
35+
| x :: xs => do
36+
let sorted ← insertionSort xs
37+
orderedInsert x sorted
38+
39+
end Cslib.Query
40+
41+
end -- public section

0 commit comments

Comments
 (0)