feat: add 12 CS algorithm implementations with correctness proofs by brando90 · Pull Request #383 · leanprover/cslib

brando90 · 2026-03-02T06:32:36Z

Summary

Adds 12 formally verified CS algorithm implementations ported from the VeriBench benchmark to CSLiB format. All proofs are complete (zero sorry), all tests use decide (not native_decide). All files pass lake build, lint-style, and mk_all.

Sorting (6 files)

InsertionSort: sorted, permutation, length proofs
BubbleSort: permutation, length, fixed-point proofs
SelectionSort: sorted, permutation, length proofs
QuickSort: sorted, permutation, length proofs (fuel-based with partition)
CountingSort: sorted, permutation, length proofs (via count characterization)
HeapSort: permutation, length proofs (fuel-based with findLargest/heapify)

Graph (3 files)

DFS: reachability soundness and completeness proofs
BFS: shortest-path soundness proof
Dijkstra: self-distance theorem, weighted path definition

Search (1 file)

BinarySearch: found-element soundness proof

Dynamic Programming (2 files)

LCS: sublist proofs, length bounds, self-LCS
EditDistance: reflexivity, nil cases, upper bound

Test plan

All 12 files compile with lake build
All decide tests pass
lake exe lint-style passes
lake exe mk_all --module succeeds

🤖 Generated with Claude Code

…eteness proofs Add depth-first search on directed adjacency-list graphs with: - `dfsAux`/`dfs` implementation with fuel-based termination - `Reachable` inductive predicate for graph reachability - `dfs_soundness`: dfs returns true → target is reachable - `ReachableAvoiding` + `dfsAux_complete_avoiding`: completeness for simple paths - Unit tests on small graphs verified via `decide` Adapted from the VeriBench benchmark. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Add breadth-first search on directed adjacency-list graphs with: - `bfsAux`/`bfs` returning shortest distance as `Option Nat` - `IsPath` inductive predicate for directed walks with path list - `IsPath.trans`/`IsPath.snoc` for path composition - `bfs_soundness`: BFS returns `some d` → a path of length `d` exists - Queue invariant `QueueInv` tracking path witnesses through BFS loop - Unit tests verified via `decide` Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

- `binarySearchAux`/`binarySearch` with fuel-based termination - `binarySearch_found`: returned index points to target element - `binarySearch_bounds`: returned index is within array bounds - Unit tests verified via `decide` Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…oofs Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Proves sorted output, permutation preservation, and length preservation via extractMin properties (minimum bound, permutation, length decrease). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Proves sorted output, permutation preservation, and length preservation via partition properties (element bounds, permutation, length). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Proves sorted output, permutation preservation (via count equality), and length preservation using buildSorted and findMax properties. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Proves sublist of both inputs, length bounds, and self-LCS identity via fuel-based induction on the LCS computation. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Proves reflexivity (self-distance is 0), empty list properties, and upper bound (distance ≤ sum of lengths) via fuel-based induction. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…oofs Implements fuel-based Dijkstra's algorithm on weighted adjacency-list graphs. Includes extractMin, dijkstraAux, dijkstra, IsWeightedPath inductive definition, weighted_path_refl, and dijkstra_start_self theorem. All proofs complete (no sorry). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Implements fuel-based heap sort on lists of natural numbers with findLargest, heapify, buildMaxHeap, and heapSortAux. Proves swap_perm via count_set, heapSort_perm and heapSort_length. All proofs complete (no sorry). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

jt0202 · 2026-03-03T10:44:31Z

It would be better to split the PR into multiple PRs and have one for every single algorithm so that it is easier to review.

jt0202 · 2026-03-03T10:46:01Z

Cslib/Algorithms/Graph/DFS.lean

+def dfs (g : Graph) (start target : Nat) : Bool :=
+  dfsAux g start target [] (g.length + 1)


I think a better definition would not have a target as dfs would also be of interest in further algorithms like finding connected components where one does not really search for a specific vertex.

jt0202 · 2026-03-03T10:49:40Z

Cslib/Algorithms/Graph/Dijkstra.lean

+`g[i]` is the list of `(neighbor, weight)` pairs for node `i`. -/
+abbrev Graph := List (List (Nat × Nat))
+
+/-- Extract the minimum-distance entry from a priority queue (list of (distance, node) pairs).


For Dijkstra a class offering the extract and update functions might be preferable so that you can use the same algorithm with arrays, heaps and search trees.

Shreyas4991 · 2026-03-03T17:26:57Z

Cslib/Algorithms/DynamicProgramming/EditDistance.lean

@@ -0,0 +1,132 @@
+/-


Several major points with this PR, hence offering the review here:

Please use Mathlib graph definitions as a baseline.

Please make separate PRs for the 20 algorithms

This PR duplicates insertion sort and LCS with other PRs.

Please space out these PRs. Dealing with a tonne of AI generated PRs is infeasible for any maintainer team of any OSS project.

The pure Levenshtein distance already exists in mathlib. Please use this version for correctness.

brando90 · 2026-03-05T21:48:42Z

It would be better to split the PR into multiple PRs and have one for every single algorithm so that it is easier to review.

yes I can seperate them latter with @patternscientist who is helping.

brando90 · 2026-03-05T21:50:05Z

It would be better to split the PR into multiple PRs and have one for every single algorithm so that it is easier to review.

@jt0202 also, I saw this: https://github.com/leanprover/cslib/blob/main/Cslib/Languages/Boole/README.md but it's empty. I anecdotally heard it's the language for CSLiB that has been already developed...when will it be pushed? So I don't have to redo the work in this PR.

brando90 requested review from chenson2018 and fmontesi as code owners March 2, 2026 06:32

brando90 and others added 11 commits March 1, 2026 23:31

feat(Algorithms): add insertion sort with sorted and permutation proofs

d34ed69

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat(Algorithms): add bubble sort with permutation and fixed-point pr…

fff016e

…oofs Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat(Algorithms): add selection sort with full correctness proofs

cc63d55

Proves sorted output, permutation preservation, and length preservation via extractMin properties (minimum bound, permutation, length decrease). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat(Algorithms): add quick sort with full correctness proofs

de74fca

Proves sorted output, permutation preservation, and length preservation via partition properties (element bounds, permutation, length). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat(Algorithms): add counting sort with full correctness proofs

06b1506

Proves sorted output, permutation preservation (via count equality), and length preservation using buildSorted and findMax properties. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat(Algorithms): add longest common subsequence with correctness proofs

bf718dd

Proves sublist of both inputs, length bounds, and self-LCS identity via fuel-based induction on the LCS computation. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat(Algorithms): add edit distance with correctness proofs

08d6c8e

Proves reflexivity (self-distance is 0), empty list properties, and upper bound (distance ≤ sum of lengths) via fuel-based induction. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

brando90 changed the title ~~feat(Algorithms): add DFS graph reachability with soundness and completeness proofs~~ feat: add 12 CS algorithm implementations with correctness proofs Mar 2, 2026

jt0202 reviewed Mar 3, 2026

View reviewed changes

Shreyas4991 suggested changes Mar 3, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add 12 CS algorithm implementations with correctness proofs#383

feat: add 12 CS algorithm implementations with correctness proofs#383
brando90 wants to merge 12 commits intoleanprover:mainfrom
brando90:feat/graph-dfs

brando90 commented Mar 2, 2026 •

edited

Loading

Uh oh!

jt0202 commented Mar 3, 2026

Uh oh!

jt0202 Mar 3, 2026

Uh oh!

jt0202 Mar 3, 2026

Uh oh!

Shreyas4991 Mar 3, 2026 •

edited

Loading

Uh oh!

brando90 commented Mar 5, 2026

Uh oh!

brando90 commented Mar 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		def dfs (g : Graph) (start target : Nat) : Bool :=
		dfsAux g start target [] (g.length + 1)

Conversation

brando90 commented Mar 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Sorting (6 files)

Graph (3 files)

Search (1 file)

Dynamic Programming (2 files)

Test plan

Uh oh!

jt0202 commented Mar 3, 2026

Uh oh!

jt0202 Mar 3, 2026

Choose a reason for hiding this comment

Uh oh!

jt0202 Mar 3, 2026

Choose a reason for hiding this comment

Uh oh!

Shreyas4991 Mar 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

brando90 commented Mar 5, 2026

Uh oh!

brando90 commented Mar 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

brando90 commented Mar 2, 2026 •

edited

Loading

Shreyas4991 Mar 3, 2026 •

edited

Loading