feat(Query): query complexity framework with sorting examples - #401

Open

kim-em wants to merge 99 commits into

leanprover:mainfrom

kim-em:combined-query-complexity

Commits on Feb 26, 2026

Big PR
Shreyas4991
committed
8be8d07
Fixed worst case statement
Shreyas4991
committed
e50c8b0
Linarith
Shreyas4991
committed
79d77de
More review fixes
Shreyas4991
committed
c1e3323
More review fixes
Shreyas4991
committed
ddab6f0
More review fixes
Shreyas4991
committed
08decfa
More review fixes
Shreyas4991
committed
a2b4782
More review fixes
Shreyas4991
committed
54bb351
More review fixes
Shreyas4991
committed
7ee16a0
More review fixes
Shreyas4991
committed
cc806f0
Fix test file imports
Shreyas4991
committed
a732ed8
More review fixes
Shreyas4991
committed
2cee489

Commits on Feb 27, 2026

Commits on Feb 28, 2026

Suggested name change. Additionally add co-author list:

committed
9f3df4d
Merge branch 'main' of github.com:leanprover/cslib into query-final-squash
Shreyas4991
committed
6db1fde
Fix lake shake issues
Shreyas4991
committed
a9485da
Done
Shreyas4991
committed
6fef51f

Commits on Mar 2, 2026

Switch to bool
Shreyas4991
committed
f479c93
Lower bound
Shreyas4991
committed
5e2a2f6
GPT generated lower bound
Shreyas4991
committed
6b78316
Added module
Shreyas4991
committed
4fab097
exe mk_all
Shreyas4991
committed
8097c61
Minimize imports
Shreyas4991
committed
87e7ded
Done
Shreyas4991
committed
3f71048
GPT finished the proof for lists with nodup
Shreyas4991
committed
57856b7
Got it for infinite types as well
Shreyas4991
committed
53c2ef3

Commits on Mar 3, 2026

remove deicsion tree proofs
Shreyas4991
committed
b712d16

Commits on Mar 8, 2026

Merge branch 'main' of github.com:leanprover/cslib into query-final-squash
Shreyas4991
committed
1eeb2d8

Commits on Mar 11, 2026

Merge branch 'main' of github.com:leanprover/cslib into query-final-squash
Shreyas4991
committed
7370fc6

Commits on Mar 16, 2026

Merge branch 'main' of github.com:leanprover/cslib into query-final-squash
Shreyas4991
committed
df70978
Merge upstream main
Shreyas4991
committed
275d827

Commits on Mar 17, 2026

Remove accidental file
Shreyas4991
committed
e9cb648
Initialize clean up of lower bound proof
Shreyas4991
committed
7f4010e
Include the model parametric style lower bound in the lower bound file
Shreyas4991
committed
d04ca73
Clean up
Shreyas4991
committed
e7c8bde
Clean up a bit
Shreyas4991
committed
a8e9f3d
Merge branch 'main' into query-final-squash
Shreyas4991
authored
4ca216d
Remove Prop from structure
Shreyas4991
committed
30cf281
docstring
Shreyas4991
committed
a145ded
Merge branch 'query-final-squash' of github.com:Shreyas4991/cslib into query-final-squash
Shreyas4991
committed
6761169
Where did prop typed structures sneak in. Purge them
Shreyas4991
committed
c6e1add
Where did prop typed structures sneak in. Purge them
Shreyas4991
committed
e07de01

Commits on Mar 18, 2026

Fix lint
Shreyas4991
committed
cf9f1f5

Commits on Mar 19, 2026

Fix documentation for listLinearSearch evaluation
Shreyas4991
authored
56c98a5

Commits on Apr 16, 2026

Update ListComparisonSort.lean

Shreyas4991
and
Arleee1
authored
1fb24e1

Commits on Apr 22, 2026

Merge #372 (query complexity, attempt 1) for attribution
kim-em
committed
3fc5afd
feat(Query): query complexity framework with sorting lower bound

committed
7ece1dd
feat(Query): add Prog.cost and complex multiplication example

committed
883edfd
docs(Query/Arith): clarify these are toy examples of parametrized costs

committed
7327006

Commits on Apr 28, 2026

refactor(Query): replace Prog with FreeM directly

kim-em
and
claude
committed
de06cdf
refactor(Query): replace QueryTree with generalised FreeM lower bound

kim-em
and
claude
committed
b46a156
docs(Query/Arith): fix off-by-strictness in Gauss/naive crossover comment

kim-em
and
claude
committed
3bf2acb
refactor(Query/FreeM): route eval, cost, and queriesOn through FreeM.liftM

kim-em
and
claude
committed
3b93bad
docs(Query/FreeM): add field docstrings to Tally to satisfy docBlame linter

kim-em
and
claude
committed
2dc7d9f

Commits on Apr 29, 2026

drop Tally
eric-wieser
committed
391cab0

Commits on Aug 27, 2026

refactor(Query): address review feedback
kim-em
committed
6fdf909
Merge remote-tracking branch 'origin/main' into combined-query-complexity
kim-em
committed
c3067db
fix(Query): adapt to Lean 4.34
kim-em
committed
40ea780
docs(Query): update FreeM simp description
kim-em
committed
79c29f8
refactor(Query): polish docs and merge sort
kim-em
committed
f257485
refactor(Query): apply second-opinion review
kim-em
committed
1cc3324

Commits on Sep 1, 2026

refactor(Query): apply review suggestions

kim-em
and
claude
committed
36e098c
refactor(Query): make FreeM query interpreters universe polymorphic

kim-em
and
claude
committed
2a83ed9
chore: golf proofs
eric-wieser
committed
a2e9050
refactor: simplify InfinitePermOrder
eric-wieser
committed
8727846

Commits on Sep 2, 2026

refactor(Query): make mergeSort agree with List.mergeSort

kim-em
and
claude
committed
57b1c35
refactor: `Infinite` is a distraction in most of the proof
eric-wieser
committed
46d7d92
Merge branch 'combined-query-complexity' of github.com:kim-em/cslib into combined-query-complexity
eric-wieser
committed
693c2c5
feat(Query): UpperBound.of_pointwise and LowerBound.le_upperBound

kim-em
and
claude
committed
cd51b93
docs(Query): FreeM setup recipe and countQueries design note

kim-em
and
claude
committed
901c0ce
feat(Query): tighten insertion sort bound to n * (n - 1) / 2

kim-em
and
claude
committed
877cf1a
refactor(Query): merge sort count lemma in simp normal form

kim-em
and
claude
committed
239b7ad
feat(Query): IsSort.eval_eq uniqueness lemma

kim-em
and
claude
committed
398c22b
chore(Query): mark declarations proposed upstream to Mathlib private

kim-em
and
claude
committed
8547036
feat(Query): combined bounds for mergeSort

kim-em
and
claude
committed
09c565a
test(Query): executable and API checks for the query framework

kim-em
and
claude
committed
6a904b2
refactor(Query): mirror upstream List.mergeSort_append

kim-em
and
claude
committed
aee6621
chore(Query): drop unused imports

kim-em
and
claude
committed
dad82a1
refactor(Query): single cardinal bound in the lower-bound theorem

kim-em
and
claude
committed
0bd0e2a

Commits on Sep 3, 2026

Add monad-generic versions first
eric-wieser
committed
b5e94ca

Commits on Sep 5, 2026

test(Query): naturality of the monad-generic sorts

kim-em
and
claude
committed
f6d8269

Commits on Sep 9, 2026

chore(Query): mirror the generalized upstream extend lemma

kim-em
and
claude
committed
b2d2b4f
Merge remote-tracking branch 'upstream/main' into combined-query-complexity
kim-em
committed
0b9e74f

Commits on Sep 10, 2026

Merge remote-tracking branch 'origin/main' into combined-query-complexity
eric-wieser
committed
0e0a1cd
deduplicate insertionSort
eric-wieser
committed
5f8b6c4
Deduplicate List.mergeM
eric-wieser
committed
fa632a0
deduplicate
eric-wieser
committed
f40241d

Commits on Sep 13, 2026

Merge branch 'main' into combined-query-complexity
eric-wieser
authored
5f470fb
Remove dead code
eric-wieser
committed
fbb2723
Drop a theorem dropped upstream
eric-wieser
committed
38a3d9c

Commits on Sep 14, 2026

Merge remote-tracking branch 'origin/main' into combined-query-complexity
eric-wieser
committed
062250a
Delete upstreamed lemma
eric-wieser
committed
8c44899
golf
eric-wieser
committed
f145d4b
simpnf
eric-wieser
committed
77b81ed
ite helper lemma
eric-wieser
committed
2466ded