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

Open

brando90 wants to merge 12 commits intoleanprover:mainfrom

brando90:feat/graph-dfs

Commits on Mar 2, 2026

feat(Algorithms): add DFS graph reachability with soundness and completeness proofs

brando90
and
claude
committed
feat(Algorithms): add BFS shortest-path with soundness proof

brando90
and
claude
committed
feat(Algorithms): add binary search with found-element soundness proof

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

brando90
and
claude
committed
feat(Algorithms): add bubble sort with permutation and fixed-point proofs

brando90
and
claude
committed
feat(Algorithms): add selection sort with full correctness proofs

brando90
and
claude
committed
feat(Algorithms): add quick sort with full correctness proofs

brando90
and
claude
committed
feat(Algorithms): add counting sort with full correctness proofs

brando90
and
claude
committed
feat(Algorithms): add longest common subsequence with correctness proofs

brando90
and
claude
committed
feat(Algorithms): add edit distance with correctness proofs

brando90
and
claude
committed
feat: add Dijkstra's shortest path algorithm with full correctness proofs

brando90
and
claude
committed
feat: add heap sort with permutation and length preservation proofs

brando90
and
claude
committed