From 83416213ced79e4c92c45e5c45d91f7f8da902cc Mon Sep 17 00:00:00 2001 From: Sorrachai Yingchareonthawornchai Date: Mon, 9 Nov 2026 19:36:38 +0100 Subject: [PATCH 1/2] docs: explain installing and importing AlgoLib --- README.md | 156 +++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 132 insertions(+), 24 deletions(-) diff --git a/README.md b/README.md index c3a42db..ba399af 100644 --- a/README.md +++ b/README.md @@ -1,22 +1,143 @@ # AlgoLib -A [Lean 4](https://lean-lang.org/) library for **algorithms**, built on top of [Mathlib](https://github.com/leanprover-community/mathlib4). AlgoLib aims to provide machine-checked definitions, theorems, and algorithm implementations covering the standard undergraduate-through-graduate curriculum on algorithms. +A [Lean 4](https://lean-lang.org/) library for **algorithms**, built on top of +[Mathlib](https://github.com/leanprover-community/mathlib4) and +[CSLib](https://github.com/leanprover/cslib). AlgoLib aims to provide machine-checked +definitions, theorems, and algorithm implementations covering the standard +undergraduate-through-graduate curriculum on algorithms. -Since we focus on computable definitions and algorithms, we introduce new definitions for concepts already formalized in Mathlib (e.g., out definition of graphs). Our primarly goals is to provide a concise formalization of algorithms that stays close to their textbook formulation without compromising on generality. +We focus on computable definitions and algorithms. Where needed, we introduce +definitions for concepts already formalized in Mathlib, such as graphs. Our goal +is to stay close to textbook formulations without compromising on generality. + +## Using AlgoLib in your project + +### Prerequisites + +Install [Lean and its editor support](https://lean-lang.org/install/) and +[Git](https://git-scm.com/downloads). The Lean installation includes `elan`, the +toolchain manager, and `lake`, the build tool and package manager. + +Use the Lean version specified by AlgoLib's [`lean-toolchain`](lean-toolchain) +at the revision you depend on. The current version is: + +```text +leanprover/lean4:v4.30.0-rc2 +``` + +For an existing project, its `lean-toolchain` must match this version, and any +direct Mathlib or CSLib dependencies must be compatible with AlgoLib's +[`lakefile.toml`](lakefile.toml) and [`lake-manifest.json`](lake-manifest.json). +When you run Lake, `elan` downloads the specified Lean toolchain if needed. + +### Add the dependency + +Add the following to your project's `lakefile.toml`: + +```toml +[[require]] +name = "AlgoLib" +git = "https://github.com/cslib-community/AlgoLib" +rev = "main" +``` + +Alternatively, if your project uses `lakefile.lean`, add: + +```lean +require AlgoLib from git + "https://github.com/cslib-community/AlgoLib" @ "main" +``` + +Use the configuration format your project already uses. The package name is +case-sensitive: `AlgoLib`. + +From your project's root directory, fetch the dependency and the Mathlib cache: + +```sh +lake update AlgoLib +lake exe cache get +``` + +The cache command downloads precompiled Mathlib dependencies to reduce the first +build's work. AlgoLib's dependencies are fetched automatically. + +### Import and build + +Import the modules you need in your Lean files. For example: + +```lean +import AlgoLib.Theory.Graph.Basic + +#check AlgoLib.Graph +#check AlgoLib.SimpleGraph +#check AlgoLib.DiGraph +``` + +You can also import the modules collected in the library's root file with: + +```lean +import AlgoLib +``` + +Run `lake build` after adding the import to one of your project's build targets. +For a standalone file named `Example.lean` in the project root, use: + +```sh +lake build AlgoLib +lake env lean Example.lean +``` + +Open the project root in VS Code so the Lean extension uses the project's +toolchain and dependencies. + +### Pinning a revision + +The examples above follow `main` when you run `lake update AlgoLib`. For a +reproducible project, replace `main` with the full commit hash of a revision you +have tested, and commit the generated `lake-manifest.json`. Use the +`lean-toolchain` from that same AlgoLib revision. + +## Building AlgoLib locally + +To work on AlgoLib itself, clone the repository and build it: + +```sh +git clone https://github.com/cslib-community/AlgoLib.git +cd AlgoLib +lake exe cache get +lake build +``` + +The checkout includes its toolchain and dependency manifest. Keep these files +when reproducing a build. See the [contribution guide](.github/CONTRIBUTING.md) +before making changes. + +## Repository layout + +```text +AlgoLib.lean # imports the library's modules +AlgoLib/ +├── Theory/ # graph definitions and mathematical results +├── Algorithms/ # algorithms and correctness proofs +├── DataStructures/ # binary trees, splay trees, union-find, … +└── Util/ # supporting lemmas and utilities +blueprint/ # mathematical exposition +website/ # website sources +``` ## Roadmap — v1 -### Theory +The following topics describe our goals for the library. -Among others: +### Theory -- **Walks & connectivity.** Walks, paths, cycles, Eulerian walks, components. +- **Walks and connectivity.** Walks, paths, cycles, Eulerian walks, components. - **Trees.** Trees and forests, Cayley's theorem on the number of labeled trees. -- **Spectral graph theory.** Laplacian, Cheeger's inequality (upper and lower bounds), expansion / expander graphs. +- **Spectral graph theory.** Laplacians, Cheeger's inequality, expansion and expander graphs. - **Matchings.** Matchings, augmenting paths, Hall's theorem, König's theorem. - **Colorings.** Proper vertex and edge colorings, chromatic number, basic bounds. -- **Contractions, minors, topological minors.** Edge/vertex contractions and the minor and topological-minor relations. -- **Embeddings & planarity.** Planar graphs, Euler's formula, Kuratowski's theorem, toroidal graphs. +- **Contractions and minors.** Edge and vertex contractions, minors and topological minors. +- **Embeddings and planarity.** Planar graphs, Euler's formula, Kuratowski's theorem, toroidal graphs. ### Algorithms @@ -27,21 +148,8 @@ Among others: - **Strongly connected components.** Tarjan / Kosaraju. - **Union–Find.** Disjoint-set forests with union-by-rank and path compression. -Every algorithm comes with a proof of correctness and a proof of runtime. - -## Repository layout - -``` -AlgoLib/ -├── Basic/ -- core graph structures (Graph, SimpleGraph, DiGraph, SimpleDiGraph) -├── Theory/ -- mathematical results (walks, trees, spectral, matching, …) -└── Algorithms/ -- algorithm implementations and correctness proofs -``` - -## Building +We aim to accompany each algorithm with proofs of correctness and runtime. -``` -lake build -``` +## License -Requires the Lean toolchain pinned in `lean-toolchain`. `elan` will install it automatically. +AlgoLib is released under the [Apache License 2.0](LICENSE). From fee4f48dfb9df57be44042e6947b837a43d61d30 Mon Sep 17 00:00:00 2001 From: Sorrachai Yingchareonthawornchai Date: Mon, 9 Nov 2026 23:33:04 +0100 Subject: [PATCH 2/2] feat: upgrade AlgoLib to Lean 4.35.0 --- .github/workflows/push.yml | 9 +- AlgoLib.lean | 164 +++++++++--------- .../Algorithms/Graph/Connectivity/Basic.lean | 12 +- AlgoLib/Algorithms/Graph/Flow/Basic.lean | 2 +- AlgoLib/Algorithms/Graph/MST/Basic.lean | 2 +- AlgoLib/Algorithms/Graph/SCC/Basic.lean | 2 +- AlgoLib/Algorithms/Graph/Search/Basic.lean | 2 +- .../Algorithms/Graph/ShortestPath/Basic.lean | 2 +- AlgoLib/Algorithms/Graph/Traversal/BFS.lean | 8 +- AlgoLib/Algorithms/Graph/Traversal/Basic.lean | 4 +- AlgoLib/DataStructures/BinaryTree/Basic.lean | 1 + .../DataStructures/BinaryTree/BinaryTree.lean | 134 +++++++------- AlgoLib/DataStructures/SplayTree/BSTAPI.lean | 14 +- AlgoLib/DataStructures/SplayTree/Basic.lean | 100 ++++++----- .../DataStructures/SplayTree/Complexity.lean | 108 ++++++------ .../DataStructures/SplayTree/Correctness.lean | 58 ++++--- .../SplayTree/StaticOptimality.lean | 47 ++--- .../DataStructures/SplayTree/Weighted.lean | 121 +++++++------ AlgoLib/DataStructures/UnionFind/Basic.lean | 1 + AlgoLib/Theory/Graph/Adjacency.lean | 6 +- AlgoLib/Theory/Graph/Basic'.lean | 8 +- AlgoLib/Theory/Graph/Basic.lean | 6 +- AlgoLib/Theory/Graph/Coloring/Basic.lean | 2 +- AlgoLib/Theory/Graph/Connectivity/Basic.lean | 12 +- .../Theory/Graph/Connectivity/Components.lean | 8 +- .../Graph/Connectivity/Connectivity.lean | 10 +- AlgoLib/Theory/Graph/Connectivity/Cuts.lean | 6 +- .../Theory/Graph/Connectivity/Directed.lean | 11 +- .../Theory/Graph/Connectivity/Reachable.lean | 8 +- AlgoLib/Theory/Graph/Decidable.lean | 12 +- AlgoLib/Theory/Graph/Degree.lean | 10 +- AlgoLib/Theory/Graph/Delete.lean | 16 +- AlgoLib/Theory/Graph/Embeddings/Basic.lean | 2 +- AlgoLib/Theory/Graph/Finite.lean | 22 ++- AlgoLib/Theory/Graph/Graphs.lean | 1 + AlgoLib/Theory/Graph/Matching/Basic.lean | 1 + AlgoLib/Theory/Graph/Minors/Basic.lean | 1 + AlgoLib/Theory/Graph/Spectral/Basic.lean | 1 + AlgoLib/Theory/Graph/Spectral/Cheeger_LB.lean | 6 +- AlgoLib/Theory/Graph/Spectral/Cuts.lean | 16 +- AlgoLib/Theory/Graph/Spectral/Expansion.lean | 16 +- AlgoLib/Theory/Graph/Spectral/Helper.lean | 10 +- AlgoLib/Theory/Graph/Structures/Basic.lean | 2 + AlgoLib/Theory/Graph/Structures/Cycle.lean | 1 + AlgoLib/Theory/Graph/Structures/Eulerian.lean | 10 +- AlgoLib/Theory/Graph/Structures/Forest.lean | 6 +- .../Theory/Graph/Structures/Hamiltonian.lean | 10 +- AlgoLib/Theory/Graph/Structures/InGraph.lean | 1 + .../Graph/Structures/InSimpleDiGraph.lean | 10 +- .../Graph/Structures/InSimpleGraph.lean | 10 +- .../Graph/Structures/InSimpleGraph/Cycle.lean | 10 +- .../Graph/Structures/InSimpleGraph/Path.lean | 10 +- .../Structures/InSimpleGraph/VertexSeq.lean | 10 +- .../Graph/Structures/InSimpleGraph/Walk.lean | 8 +- AlgoLib/Theory/Graph/Structures/Path.lean | 1 + .../Theory/Graph/Structures/SimpleCycle.lean | 49 +++--- .../SimpleGraph_only/Bipartite.lean | 8 +- .../Structures/SimpleGraph_only/Girth.lean | 14 +- .../SimpleGraph_only/MooreBound.lean | 12 +- .../SimpleGraph_only/MooreBound/Bounds.lean | 6 +- .../SimpleGraph_only/MooreBound/Core.lean | 8 +- .../SimpleGraph_only/MooreBound/Counting.lean | 14 +- .../MooreBound/HalfLayers.lean | 11 +- .../MooreBound/RootedLayers.lean | 14 +- .../Theory/Graph/Structures/SimplePath.lean | 6 +- .../Theory/Graph/Structures/SimpleWalk.lean | 10 +- AlgoLib/Theory/Graph/Structures/Trail.lean | 1 + AlgoLib/Theory/Graph/Structures/Tree.lean | 8 +- .../Theory/Graph/Structures/Trees/Basic.lean | 2 +- .../Theory/Graph/Structures/VertexSeq.lean | 20 ++- .../Graph/Structures/VertexSeq/Append.lean | 6 +- .../Graph/Structures/VertexSeq/Basic.lean | 6 +- .../Structures/VertexSeq/CommonPrefix.lean | 6 +- .../Graph/Structures/VertexSeq/Edges.lean | 8 +- .../Graph/Structures/VertexSeq/Erase.lean | 6 +- .../Graph/Structures/VertexSeq/Index.lean | 6 +- .../Graph/Structures/VertexSeq/MapZip.lean | 6 +- .../Structures/VertexSeq/Predicates.lean | 6 +- .../Graph/Structures/VertexSeq/Subseq.lean | 6 +- AlgoLib/Theory/Graph/Structures/Walk.lean | 10 +- AlgoLib/Theory/Graph/Subgraph.lean | 6 +- AlgoLib/Util/Decidable.lean | 10 +- AlgoLib/Util/Finset.lean | 12 +- README.md | 30 +++- lake-manifest.json | 38 ++-- lakefile.toml | 6 +- lean-toolchain | 2 +- tests/Import.lean | 21 +++ 88 files changed, 880 insertions(+), 565 deletions(-) create mode 100644 tests/Import.lean diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 7b08a1b..3e24181 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -25,7 +25,7 @@ jobs: - name: Don't 'import Mathlib', use precise imports if: always() run: | - ! (find AlgoLib -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$') + ! (find AlgoLib -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^(public )?(meta )?import Mathlib$') build: name: Build project @@ -40,6 +40,11 @@ jobs: id: build-lean uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # v1.2.0 + - name: Check public imports and declaration checker + run: | + lake env lean tests/Import.lean + lake build checkdecls + - name: File dependencies if: github.ref == 'refs/heads/main' run: | @@ -56,4 +61,4 @@ jobs: homepage: "website" # website/ is plain static HTML, not a Jekyll site. The action still copies # the API docs and blueprint into website/, then uploads that folder directly. - build-page: false \ No newline at end of file + build-page: false diff --git a/AlgoLib.lean b/AlgoLib.lean index 0e407dc..13cc924 100644 --- a/AlgoLib.lean +++ b/AlgoLib.lean @@ -1,88 +1,90 @@ +module + -- Theory -import AlgoLib.Theory.Graph.Adjacency -import AlgoLib.Theory.Graph.Basic -import AlgoLib.Theory.Graph.Basic' -import AlgoLib.Theory.Graph.Coloring.Basic -import AlgoLib.Theory.Graph.Connectivity.Basic -import AlgoLib.Theory.Graph.Connectivity.Components -import AlgoLib.Theory.Graph.Connectivity.Connectivity -import AlgoLib.Theory.Graph.Connectivity.Cuts -import AlgoLib.Theory.Graph.Connectivity.Directed -import AlgoLib.Theory.Graph.Connectivity.Reachable -import AlgoLib.Theory.Graph.Decidable -import AlgoLib.Theory.Graph.Degree -import AlgoLib.Theory.Graph.Delete -import AlgoLib.Theory.Graph.Embeddings.Basic -import AlgoLib.Theory.Graph.Finite -import AlgoLib.Theory.Graph.Graphs -import AlgoLib.Theory.Graph.Matching.Basic -import AlgoLib.Theory.Graph.Minors.Basic -import AlgoLib.Theory.Graph.Spectral.Basic -import AlgoLib.Theory.Graph.Spectral.Cheeger_LB -import AlgoLib.Theory.Graph.Spectral.Cuts -import AlgoLib.Theory.Graph.Spectral.Expansion -import AlgoLib.Theory.Graph.Spectral.Helper -import AlgoLib.Theory.Graph.Structures.Basic -import AlgoLib.Theory.Graph.Structures.Cycle -import AlgoLib.Theory.Graph.Structures.Eulerian -import AlgoLib.Theory.Graph.Structures.Forest -import AlgoLib.Theory.Graph.Structures.Hamiltonian -import AlgoLib.Theory.Graph.Structures.InGraph -import AlgoLib.Theory.Graph.Structures.InSimpleDiGraph -import AlgoLib.Theory.Graph.Structures.InSimpleGraph -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Cycle -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Path -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.VertexSeq -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Walk -import AlgoLib.Theory.Graph.Structures.Path -import AlgoLib.Theory.Graph.Structures.SimpleCycle -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Bipartite -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Girth -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Bounds -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Core -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Counting -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.HalfLayers -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.RootedLayers -import AlgoLib.Theory.Graph.Structures.SimplePath -import AlgoLib.Theory.Graph.Structures.SimpleWalk -import AlgoLib.Theory.Graph.Structures.Trail -import AlgoLib.Theory.Graph.Structures.Tree -import AlgoLib.Theory.Graph.Structures.Trees.Basic -import AlgoLib.Theory.Graph.Structures.VertexSeq -import AlgoLib.Theory.Graph.Structures.VertexSeq.Append -import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic -import AlgoLib.Theory.Graph.Structures.VertexSeq.CommonPrefix -import AlgoLib.Theory.Graph.Structures.VertexSeq.Edges -import AlgoLib.Theory.Graph.Structures.VertexSeq.Erase -import AlgoLib.Theory.Graph.Structures.VertexSeq.Index -import AlgoLib.Theory.Graph.Structures.VertexSeq.MapZip -import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates -import AlgoLib.Theory.Graph.Structures.VertexSeq.Subseq -import AlgoLib.Theory.Graph.Structures.Walk -import AlgoLib.Theory.Graph.Subgraph +public import AlgoLib.Theory.Graph.Adjacency +public import AlgoLib.Theory.Graph.Basic +public import AlgoLib.Theory.Graph.Basic' +public import AlgoLib.Theory.Graph.Coloring.Basic +public import AlgoLib.Theory.Graph.Connectivity.Basic +public import AlgoLib.Theory.Graph.Connectivity.Components +public import AlgoLib.Theory.Graph.Connectivity.Connectivity +public import AlgoLib.Theory.Graph.Connectivity.Cuts +public import AlgoLib.Theory.Graph.Connectivity.Directed +public import AlgoLib.Theory.Graph.Connectivity.Reachable +public import AlgoLib.Theory.Graph.Decidable +public import AlgoLib.Theory.Graph.Degree +public import AlgoLib.Theory.Graph.Delete +public import AlgoLib.Theory.Graph.Embeddings.Basic +public import AlgoLib.Theory.Graph.Finite +public import AlgoLib.Theory.Graph.Graphs +public import AlgoLib.Theory.Graph.Matching.Basic +public import AlgoLib.Theory.Graph.Minors.Basic +public import AlgoLib.Theory.Graph.Spectral.Basic +public import AlgoLib.Theory.Graph.Spectral.Cheeger_LB +public import AlgoLib.Theory.Graph.Spectral.Cuts +public import AlgoLib.Theory.Graph.Spectral.Expansion +public import AlgoLib.Theory.Graph.Spectral.Helper +public import AlgoLib.Theory.Graph.Structures.Basic +public import AlgoLib.Theory.Graph.Structures.Cycle +public import AlgoLib.Theory.Graph.Structures.Eulerian +public import AlgoLib.Theory.Graph.Structures.Forest +public import AlgoLib.Theory.Graph.Structures.Hamiltonian +public import AlgoLib.Theory.Graph.Structures.InGraph +public import AlgoLib.Theory.Graph.Structures.InSimpleDiGraph +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Cycle +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Path +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.VertexSeq +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Walk +public import AlgoLib.Theory.Graph.Structures.Path +public import AlgoLib.Theory.Graph.Structures.SimpleCycle +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Bipartite +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Girth +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Bounds +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Core +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Counting +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.HalfLayers +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.RootedLayers +public import AlgoLib.Theory.Graph.Structures.SimplePath +public import AlgoLib.Theory.Graph.Structures.SimpleWalk +public import AlgoLib.Theory.Graph.Structures.Trail +public import AlgoLib.Theory.Graph.Structures.Tree +public import AlgoLib.Theory.Graph.Structures.Trees.Basic +public import AlgoLib.Theory.Graph.Structures.VertexSeq +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Append +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic +public import AlgoLib.Theory.Graph.Structures.VertexSeq.CommonPrefix +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Edges +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Erase +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Index +public import AlgoLib.Theory.Graph.Structures.VertexSeq.MapZip +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Subseq +public import AlgoLib.Theory.Graph.Structures.Walk +public import AlgoLib.Theory.Graph.Subgraph -- Algorithms -import AlgoLib.Algorithms.Graph.Connectivity.Basic -import AlgoLib.Algorithms.Graph.Flow.Basic -import AlgoLib.Algorithms.Graph.MST.Basic -import AlgoLib.Algorithms.Graph.SCC.Basic -import AlgoLib.Algorithms.Graph.Search.Basic -import AlgoLib.Algorithms.Graph.ShortestPath.Basic -import AlgoLib.Algorithms.Graph.Traversal.BFS -import AlgoLib.Algorithms.Graph.Traversal.Basic +public import AlgoLib.Algorithms.Graph.Connectivity.Basic +public import AlgoLib.Algorithms.Graph.Flow.Basic +public import AlgoLib.Algorithms.Graph.MST.Basic +public import AlgoLib.Algorithms.Graph.SCC.Basic +public import AlgoLib.Algorithms.Graph.Search.Basic +public import AlgoLib.Algorithms.Graph.ShortestPath.Basic +public import AlgoLib.Algorithms.Graph.Traversal.BFS +public import AlgoLib.Algorithms.Graph.Traversal.Basic -- Data structures -import AlgoLib.DataStructures.BinaryTree.Basic -import AlgoLib.DataStructures.BinaryTree.BinaryTree -import AlgoLib.DataStructures.SplayTree.BSTAPI -import AlgoLib.DataStructures.SplayTree.Basic -import AlgoLib.DataStructures.SplayTree.Complexity -import AlgoLib.DataStructures.SplayTree.Correctness -import AlgoLib.DataStructures.SplayTree.StaticOptimality -import AlgoLib.DataStructures.SplayTree.Weighted -import AlgoLib.DataStructures.UnionFind.Basic +public import AlgoLib.DataStructures.BinaryTree.Basic +public import AlgoLib.DataStructures.BinaryTree.BinaryTree +public import AlgoLib.DataStructures.SplayTree.BSTAPI +public import AlgoLib.DataStructures.SplayTree.Basic +public import AlgoLib.DataStructures.SplayTree.Complexity +public import AlgoLib.DataStructures.SplayTree.Correctness +public import AlgoLib.DataStructures.SplayTree.StaticOptimality +public import AlgoLib.DataStructures.SplayTree.Weighted +public import AlgoLib.DataStructures.UnionFind.Basic -- Utilities -import AlgoLib.Util.Decidable -import AlgoLib.Util.Finset +public import AlgoLib.Util.Decidable +public import AlgoLib.Util.Finset diff --git a/AlgoLib/Algorithms/Graph/Connectivity/Basic.lean b/AlgoLib/Algorithms/Graph/Connectivity/Basic.lean index 6d9006b..7eab333 100644 --- a/AlgoLib/Algorithms/Graph/Connectivity/Basic.lean +++ b/AlgoLib/Algorithms/Graph/Connectivity/Basic.lean @@ -3,10 +3,12 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Decidable -import AlgoLib.Theory.Graph.Connectivity.Connectivity -import AlgoLib.Algorithms.Graph.Traversal.BFS -import AlgoLib.Util.Finset +module + +public import AlgoLib.Theory.Graph.Decidable +public import AlgoLib.Theory.Graph.Connectivity.Connectivity +public import AlgoLib.Algorithms.Graph.Traversal.BFS +public import AlgoLib.Util.Finset /-! # The computable connectivity layer @@ -70,6 +72,8 @@ never imports the algorithms tree. algorithm: `decide` is realistic up to about six vertices. -/ +@[expose] public section + namespace AlgoLib variable {α : Type*} diff --git a/AlgoLib/Algorithms/Graph/Flow/Basic.lean b/AlgoLib/Algorithms/Graph/Flow/Basic.lean index 8b13789..0cca093 100644 --- a/AlgoLib/Algorithms/Graph/Flow/Basic.lean +++ b/AlgoLib/Algorithms/Graph/Flow/Basic.lean @@ -1 +1 @@ - +module diff --git a/AlgoLib/Algorithms/Graph/MST/Basic.lean b/AlgoLib/Algorithms/Graph/MST/Basic.lean index 8b13789..0cca093 100644 --- a/AlgoLib/Algorithms/Graph/MST/Basic.lean +++ b/AlgoLib/Algorithms/Graph/MST/Basic.lean @@ -1 +1 @@ - +module diff --git a/AlgoLib/Algorithms/Graph/SCC/Basic.lean b/AlgoLib/Algorithms/Graph/SCC/Basic.lean index 8b13789..0cca093 100644 --- a/AlgoLib/Algorithms/Graph/SCC/Basic.lean +++ b/AlgoLib/Algorithms/Graph/SCC/Basic.lean @@ -1 +1 @@ - +module diff --git a/AlgoLib/Algorithms/Graph/Search/Basic.lean b/AlgoLib/Algorithms/Graph/Search/Basic.lean index 8b13789..0cca093 100644 --- a/AlgoLib/Algorithms/Graph/Search/Basic.lean +++ b/AlgoLib/Algorithms/Graph/Search/Basic.lean @@ -1 +1 @@ - +module diff --git a/AlgoLib/Algorithms/Graph/ShortestPath/Basic.lean b/AlgoLib/Algorithms/Graph/ShortestPath/Basic.lean index 8b13789..0cca093 100644 --- a/AlgoLib/Algorithms/Graph/ShortestPath/Basic.lean +++ b/AlgoLib/Algorithms/Graph/ShortestPath/Basic.lean @@ -1 +1 @@ - +module diff --git a/AlgoLib/Algorithms/Graph/Traversal/BFS.lean b/AlgoLib/Algorithms/Graph/Traversal/BFS.lean index e20df68..38e18b0 100644 --- a/AlgoLib/Algorithms/Graph/Traversal/BFS.lean +++ b/AlgoLib/Algorithms/Graph/Traversal/BFS.lean @@ -3,8 +3,10 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Fable 5.1) -/ -import AlgoLib.Theory.Graph.Decidable -import AlgoLib.Theory.Graph.Connectivity.Directed +module + +public import AlgoLib.Theory.Graph.Decidable +public import AlgoLib.Theory.Graph.Connectivity.Directed /-! # Breadth-first search @@ -73,6 +75,8 @@ arcs have decidable membership, and proves it correct against the specifications `V(G)` reaches anything, and `Reachable s s ↔ s ∈ V(G)` is reproduced exactly. -/ +@[expose] public section + namespace AlgoLib variable {α : Type*} diff --git a/AlgoLib/Algorithms/Graph/Traversal/Basic.lean b/AlgoLib/Algorithms/Graph/Traversal/Basic.lean index f1007e3..e2bb0c5 100644 --- a/AlgoLib/Algorithms/Graph/Traversal/Basic.lean +++ b/AlgoLib/Algorithms/Graph/Traversal/Basic.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Fable 5.1) -/ -import AlgoLib.Algorithms.Graph.Traversal.BFS +module + +public import AlgoLib.Algorithms.Graph.Traversal.BFS /-! # `AlgoLib.Algorithms.Graph.Traversal` diff --git a/AlgoLib/DataStructures/BinaryTree/Basic.lean b/AlgoLib/DataStructures/BinaryTree/Basic.lean index e69de29..0cca093 100644 --- a/AlgoLib/DataStructures/BinaryTree/Basic.lean +++ b/AlgoLib/DataStructures/BinaryTree/Basic.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/DataStructures/BinaryTree/BinaryTree.lean b/AlgoLib/DataStructures/BinaryTree/BinaryTree.lean index 83d88f7..8fa6789 100644 --- a/AlgoLib/DataStructures/BinaryTree/BinaryTree.lean +++ b/AlgoLib/DataStructures/BinaryTree/BinaryTree.lean @@ -18,54 +18,54 @@ set_option linter.style.header false /-! # Binary Tree -In this file we introduce the `Tree` data structure and its basic operations. +In this file we introduce the `BinaryTree` data structure and its basic operations. -/ variable {α : Type} /-- A tree node -/ -notation:65 l:66 " △[" v "] " r:66 => Tree.node v l r +notation:65 l:66 " △[" v "] " r:66 => BinaryTree.node v l r -namespace Tree +namespace BinaryTree /-! ### Core Definitions -/ section CoreDefs -theorem non_empty_exist (s : Tree α) (h : s ≠ .nil) : +theorem non_empty_exist (s : BinaryTree α) (h : s ≠ .nil) : ∃ A k B, s = A △[k] B := by induction s <;> grind -def num_nodes : Tree α → ℕ +def num_nodes : BinaryTree α → ℕ | .nil => 0 | .node _ l r => 1 + num_nodes l + num_nodes r -@[simp] lemma num_nodes_empty : num_nodes (nil : Tree α) = 0 := rfl +@[simp] lemma num_nodes_empty : num_nodes (nil : BinaryTree α) = 0 := rfl -@[simp] lemma num_nodes_node (l : Tree α) (k : α) (r : Tree α) : +@[simp] lemma num_nodes_node (l : BinaryTree α) (k : α) (r : BinaryTree α) : (l △[k] r).num_nodes = 1 + l.num_nodes + r.num_nodes := rfl /-- In-order traversal as a list of keys. -/ -def toKeyList : Tree α → List α +def toKeyList : BinaryTree α → List α | .nil => [] | l △[k] r => l.toKeyList ++ [k] ++ r.toKeyList -@[simp] lemma toKeyList_empty : toKeyList (nil : Tree α) = [] := rfl +@[simp] lemma toKeyList_empty : toKeyList (nil : BinaryTree α) = [] := rfl -@[simp] lemma toKeyList_node (l : Tree α) (k : α) (r : Tree α) : +@[simp] lemma toKeyList_node (l : BinaryTree α) (k : α) (r : BinaryTree α) : (l △[k] r).toKeyList = l.toKeyList ++ [k] ++ r.toKeyList := rfl -lemma eq_nil_of_toKeyList_eq_nil {t : Tree α} (h : toKeyList t = []) : t = nil := by +lemma eq_nil_of_toKeyList_eq_nil {t : BinaryTree α} (h : toKeyList t = []) : t = nil := by cases t <;> simp_all -lemma num_nodes_eq_length_toKeyList (t : Tree α) : t.num_nodes = t.toKeyList.length := by +lemma num_nodes_eq_length_toKeyList (t : BinaryTree α) : t.num_nodes = t.toKeyList.length := by induction t <;> simp_all; omega /-- Number of nodes on the search path for `q` in `t`. Zero on the empty tree; on a node this counts the root plus (if `q ≠ k`) the search path length in the appropriate subtree. -/ -def search_path_len [LinearOrder α] (t : Tree α) (q : α) : ℕ := +def search_path_len [LinearOrder α] (t : BinaryTree α) (q : α) : ℕ := match t with - | nil => 0 + | .nil => 0 | l △[key] r => if q < key then 1 + l.search_path_len q @@ -74,7 +74,7 @@ def search_path_len [LinearOrder α] (t : Tree α) (q : α) : ℕ := else 1 -lemma search_path_len_le_num_nodes [LinearOrder α] (t : Tree α) (q : α) : +lemma search_path_len_le_num_nodes [LinearOrder α] (t : BinaryTree α) (q : α) : search_path_len t q ≤ t.num_nodes := by induction t <;> simp [search_path_len]; split_ifs <;> omega @@ -87,9 +87,9 @@ If `contains t q` is true, then `q` is in `t`; but the converse need not necessarily hold true. The converse is true for a binary search tree. Hence the name of it. -/ -def BST_contains [LinearOrder α] (t : Tree α) (q : α) : Prop := +def BST_contains [LinearOrder α] (t : BinaryTree α) (q : α) : Prop := match t with - | nil => False + | .nil => False | l △[key] r => if q < key then l.BST_contains q @@ -105,19 +105,19 @@ end CoreDefs section Membership /-- Inductive membership relation on binary trees, modelled on `List.Mem`. -/ -inductive Mem (a : α) : Tree α → Prop where +inductive Mem (a : α) : BinaryTree α → Prop where /-- `a` is the key at the root. -/ - | here {l r : Tree α} : Mem a (l △[a] r) + | here {l r : BinaryTree α} : Mem a (l △[a] r) /-- `a` lies in the left subtree. -/ - | left {k : α} {l r : Tree α} : Mem a l → Mem a (l △[k] r) + | left {k : α} {l r : BinaryTree α} : Mem a l → Mem a (l △[k] r) /-- `a` lies in the right subtree. -/ - | right {k : α} {l r : Tree α} : Mem a r → Mem a (l △[k] r) + | right {k : α} {l r : BinaryTree α} : Mem a r → Mem a (l △[k] r) -instance : Membership α (Tree α) := ⟨fun t a => Mem a t⟩ +instance : Membership α (BinaryTree α) := ⟨fun t a => Mem a t⟩ -@[simp] lemma not_mem_nil (a : α) : a ∉ (nil : Tree α) := nofun +@[simp] lemma not_mem_nil (a : α) : a ∉ (nil : BinaryTree α) := nofun -@[simp] lemma mem_node_iff {a k : α} {l r : Tree α} : +@[simp] lemma mem_node_iff {a k : α} {l r : BinaryTree α} : a ∈ (l △[k] r) ↔ a = k ∨ a ∈ l ∨ a ∈ r := by refine ⟨fun h => ?_, fun h => ?_⟩ · cases h with @@ -130,7 +130,7 @@ instance : Membership α (Tree α) := ⟨fun t a => Mem a t⟩ · exact .right h /-- Membership agrees with membership in the in-order key list. -/ -theorem mem_iff_mem_toKeyList {a : α} {t : Tree α} : +theorem mem_iff_mem_toKeyList {a : α} {t : BinaryTree α} : a ∈ t ↔ a ∈ t.toKeyList := by induction t with | nil => simp @@ -139,7 +139,7 @@ theorem mem_iff_mem_toKeyList {a : α} {t : Tree α} : simp only [List.mem_append, List.mem_singleton, ihl, ihr] tauto -instance decidableMem [DecidableEq α] (a : α) : ∀ t : Tree α, Decidable (a ∈ t) +instance decidableMem [DecidableEq α] (a : α) : ∀ t : BinaryTree α, Decidable (a ∈ t) | .nil => isFalse nofun | l △[k] r => haveI : Decidable (a ∈ l) := decidableMem a l @@ -148,7 +148,7 @@ instance decidableMem [DecidableEq α] (a : α) : ∀ t : Tree α, Decidable (a /-- The search-path `contains` implies membership. The converse needs the BST invariant. -/ -theorem contains_imp_mem [LinearOrder α] {t : Tree α} {q : α} : +theorem contains_imp_mem [LinearOrder α] {t : BinaryTree α} {q : α} : t.BST_contains q → q ∈ t := by induction t with | nil => simp [BST_contains] @@ -167,49 +167,49 @@ end Membership /-! ### Rotations and Mirroring -/ section Transformations -def rotateRight : Tree α → Tree α +def rotateRight : BinaryTree α → BinaryTree α | (a △[x] b) △[y] c => a △[x] (b △[y] c) | t => t -def rotateLeft : Tree α → Tree α +def rotateLeft : BinaryTree α → BinaryTree α | a △[x] (b △[y] c) => (a △[x] b) △[y] c | t => t /-- Mirror a binary tree: swap every left and right subtree. -/ -def mirror : Tree α → Tree α +def mirror : BinaryTree α → BinaryTree α | .nil => .nil | l △[k] r => r.mirror △[k] l.mirror -@[simp] lemma mirror_empty : (nil : Tree α).mirror = nil := rfl +@[simp] lemma mirror_empty : (nil : BinaryTree α).mirror = nil := rfl -@[simp] lemma mirror_node (l : Tree α) (k : α) (r : Tree α) : +@[simp] lemma mirror_node (l : BinaryTree α) (k : α) (r : BinaryTree α) : (l △[k] r).mirror = r.mirror △[k] l.mirror := rfl -@[simp] lemma mirror_mirror (t : Tree α) : t.mirror.mirror = t := by +@[simp] lemma mirror_mirror (t : BinaryTree α) : t.mirror.mirror = t := by induction t <;> simp_all -@[simp] lemma num_nodes_mirror (t : Tree α) : t.mirror.num_nodes = t.num_nodes := by +@[simp] lemma num_nodes_mirror (t : BinaryTree α) : t.mirror.num_nodes = t.num_nodes := by induction t <;> simp_all [num_nodes]; omega -@[simp] lemma toKeyList_mirror (t : Tree α) : t.mirror.toKeyList = t.toKeyList.reverse := by +@[simp] lemma toKeyList_mirror (t : BinaryTree α) : t.mirror.toKeyList = t.toKeyList.reverse := by induction t <;> simp_all [toKeyList] -@[simp] lemma mirror_rotateRight (t : Tree α) : +@[simp] lemma mirror_rotateRight (t : BinaryTree α) : (rotateRight t).mirror = rotateLeft t.mirror := by rcases t with _ | ⟨k, (_ | ⟨lk, ll, lr⟩), r⟩ <;> simp [rotateRight, rotateLeft, mirror] -@[simp] lemma mirror_rotateLeft (t : Tree α) : +@[simp] lemma mirror_rotateLeft (t : BinaryTree α) : (rotateLeft t).mirror = rotateRight t.mirror := by rcases t with _ | ⟨k, l, (_ | ⟨rk, rl, rr⟩)⟩ <;> simp [rotateRight, rotateLeft, mirror] -@[simp] theorem num_nodes_rotateRight (t : Tree α) : +@[simp] theorem num_nodes_rotateRight (t : BinaryTree α) : (rotateRight t).num_nodes = t.num_nodes := by rcases t with _ | ⟨k, (_ | ⟨lk, ll, lr⟩), r⟩ <;> simp [rotateRight]; omega -@[simp] theorem num_nodes_rotateLeft (t : Tree α) : +@[simp] theorem num_nodes_rotateLeft (t : BinaryTree α) : (rotateLeft t).num_nodes = t.num_nodes := by have h := num_nodes_rotateRight t.mirror simp only [← mirror_rotateLeft, num_nodes_mirror] at h; exact h @@ -221,20 +221,20 @@ end Transformations section ContainsLemmas @[simp] lemma not_contains_empty [LinearOrder α] (q : α) : - ¬ (nil : Tree α).BST_contains q := nofun + ¬ (nil : BinaryTree α).BST_contains q := nofun -@[simp] lemma contains_node_lt [LinearOrder α] {l : Tree α} {k q : α} - {r : Tree α} (h : q < k) : +@[simp] lemma contains_node_lt [LinearOrder α] {l : BinaryTree α} {k q : α} + {r : BinaryTree α} (h : q < k) : (l △[k] r).BST_contains q ↔ l.BST_contains q := by simp [BST_contains, h] -@[simp] lemma contains_node_gt [LinearOrder α] {l : Tree α} {k q : α} - {r : Tree α} (h : k < q) : +@[simp] lemma contains_node_gt [LinearOrder α] {l : BinaryTree α} {k q : α} + {r : BinaryTree α} (h : k < q) : (l △[k] r).BST_contains q ↔ r.BST_contains q := by simp [BST_contains, h, not_lt_of_gt h] @[simp] lemma contains_node_not_eq_not_lt [LinearOrder α] - {l : Tree α} {k q : α} {r : Tree α} + {l : BinaryTree α} {k q : α} {r : BinaryTree α} (h1 : ¬ q = k) (h2 : ¬ q < k) : (l △[k] r).BST_contains q ↔ r.BST_contains q := by have hgt : k < q := lt_of_le_of_ne (Std.not_lt.mp h2) (Ne.symm (Ne.intro h1)) @@ -243,22 +243,22 @@ section ContainsLemmas end ContainsLemmas -/-! ### Tree Invariants and BST Properties -/ +/-! ### BinaryTree Invariants and BST Properties -/ section Invariants /-- BST invariant parameterised by optional lower/upper key bounds. `IsBSTAux t lb ub` holds iff every key in `t` lies strictly in `(lb, ub)` (absent bound = ±∞) and children satisfy the BST property recursively. -/ -inductive IsBSTAux [LinearOrder α] : Tree α → Option α → Option α → Prop where +inductive IsBSTAux [LinearOrder α] : BinaryTree α → Option α → Option α → Prop where | nil (lb ub : Option α) : IsBSTAux .nil lb ub - | node {l r : Tree α} {k : α} {lb ub : Option α} + | node {l r : BinaryTree α} {k : α} {lb ub : Option α} (hlb : lb.elim True (· < k)) (hub : ub.elim True (k < ·)) (hl : IsBSTAux l lb (some k)) (hr : IsBSTAux r (some k) ub) : IsBSTAux (l △[k] r) lb ub -def IsBST [LinearOrder α] (t : Tree α) : Prop := t.IsBSTAux none none +def IsBST [LinearOrder α] (t : BinaryTree α) : Prop := t.IsBSTAux none none end Invariants @@ -266,9 +266,9 @@ end Invariants section IsBSTAccessors @[simp] lemma IsBSTAux_nil [LinearOrder α] (lb ub : Option α) : - IsBSTAux (.nil : Tree α) lb ub := .nil lb ub + IsBSTAux (.nil : BinaryTree α) lb ub := .nil lb ub -@[simp] lemma IsBSTAux_node [LinearOrder α] (l : Tree α) (k : α) (r : Tree α) +@[simp] lemma IsBSTAux_node [LinearOrder α] (l : BinaryTree α) (k : α) (r : BinaryTree α) (lb ub : Option α) : IsBSTAux (l △[k] r) lb ub ↔ lb.elim True (· < k) ∧ ub.elim True (k < ·) ∧ @@ -276,19 +276,19 @@ section IsBSTAccessors ⟨fun h => by cases h with | node hlb hub hl hr => exact ⟨hlb, hub, hl, hr⟩, fun ⟨h1, h2, h3, h4⟩ => .node h1 h2 h3 h4⟩ -@[simp] lemma IsBST_node [LinearOrder α] (l : Tree α) (k : α) (r : Tree α) : +@[simp] lemma IsBST_node [LinearOrder α] (l : BinaryTree α) (k : α) (r : BinaryTree α) : IsBST (l △[k] r) ↔ IsBSTAux l none (some k) ∧ IsBSTAux r (some k) none := by simp [IsBST, IsBSTAux_node] -private lemma IsBSTAux_children_none [LinearOrder α] {t : Tree α} {x y : Option α} +private lemma IsBSTAux_children_none [LinearOrder α] {t : BinaryTree α} {x y : Option α} (h : IsBSTAux t x y) : IsBSTAux t none y ∧ IsBSTAux t x none := by induction h <;> simp_all -theorem IsBST_left_of_IsBST [LinearOrder α] {k : α} {l r : Tree α} +theorem IsBST_left_of_IsBST [LinearOrder α] {k : α} {l r : BinaryTree α} (hbst : IsBST (l △[k] r)) : IsBST l := (IsBSTAux_children_none ((IsBST_node l k r).mp hbst).1).2 -theorem IsBST_right_of_IsBST [LinearOrder α] {k : α} {l r : Tree α} +theorem IsBST_right_of_IsBST [LinearOrder α] {k : α} {l r : BinaryTree α} (hbst : IsBST (l △[k] r)) : IsBST r := (IsBSTAux_children_none ((IsBST_node l k r).mp hbst).2).1 @@ -299,7 +299,7 @@ end IsBSTAccessors section BSTMembership /-- In a BST subtree with upper bound `some ub`, every member is `< ub`. -/ -private lemma IsBSTAux.lt_of_mem_ub [LinearOrder α] {t : Tree α} {q ub : α} +private lemma IsBSTAux.lt_of_mem_ub [LinearOrder α] {t : BinaryTree α} {q ub : α} {lb : Option α} (h : IsBSTAux t lb (some ub)) (hmem : q ∈ t) : q < ub := by induction t generalizing lb ub with | nil => simp at hmem @@ -311,7 +311,7 @@ private lemma IsBSTAux.lt_of_mem_ub [LinearOrder α] {t : Tree α} {q ub : α} · exact ihr hr hmr /-- In a BST subtree with lower bound `some lb`, every member is `> lb`. -/ -private lemma IsBSTAux.gt_of_mem_lb [LinearOrder α] {t : Tree α} {q lb : α} +private lemma IsBSTAux.gt_of_mem_lb [LinearOrder α] {t : BinaryTree α} {q lb : α} {ub : Option α} (h : IsBSTAux t (some lb) ub) (hmem : q ∈ t) : lb < q := by induction t generalizing lb ub with | nil => simp at hmem @@ -324,7 +324,7 @@ private lemma IsBSTAux.gt_of_mem_lb [LinearOrder α] {t : Tree α} {q lb : α} /-- Membership implies the BST search path finds the key, for any bound configuration. -/ -private theorem IsBSTAux.mem_imp_contains [LinearOrder α] {t : Tree α} {q : α} +private theorem IsBSTAux.mem_imp_contains [LinearOrder α] {t : BinaryTree α} {q : α} {lb ub : Option α} (h : IsBSTAux t lb ub) (hmem : q ∈ t) : t.BST_contains q := by induction t generalizing lb ub with | nil => simp at hmem @@ -341,40 +341,40 @@ private theorem IsBSTAux.mem_imp_contains [LinearOrder α] {t : Tree α} {q : α /-- Converse of `contains_imp_mem` for BSTs: membership implies the search-path `contains` succeeds. -/ -theorem mem_imp_contains [LinearOrder α] {t : Tree α} (hbst : IsBST t) +theorem mem_imp_contains [LinearOrder α] {t : BinaryTree α} (hbst : IsBST t) {q : α} (hmem : q ∈ t) : t.BST_contains q := IsBSTAux.mem_imp_contains hbst hmem /-- For BSTs, the search-path `contains` coincides with membership. -/ -theorem contains_iff_mem [LinearOrder α] {t : Tree α} (hbst : IsBST t) {q : α} : +theorem contains_iff_mem [LinearOrder α] {t : BinaryTree α} (hbst : IsBST t) {q : α} : t.BST_contains q ↔ q ∈ t := ⟨contains_imp_mem, mem_imp_contains hbst⟩ /-- For BSTs, all keys in the left subtree are smaller than the root key. -/ -theorem lt_of_IsBST_left [LinearOrder α] (l : Tree α) (k : α) (r : Tree α) +theorem lt_of_IsBST_left [LinearOrder α] (l : BinaryTree α) (k : α) (r : BinaryTree α) (hbst : IsBST (l △[k] r)) {q : α} (hql : q ∈ l) : q < k := IsBSTAux.lt_of_mem_ub ((IsBST_node l k r).mp hbst).1 hql /-- For BSTs, all keys in the right subtree are greater than the root key. -/ -theorem gt_of_IsBST_right [LinearOrder α] (l : Tree α) (k : α) (r : Tree α) +theorem gt_of_IsBST_right [LinearOrder α] (l : BinaryTree α) (k : α) (r : BinaryTree α) (hbst : IsBST (l △[k] r)) {q : α} (hqr : q ∈ r) : k < q := IsBSTAux.gt_of_mem_lb ((IsBST_node l k r).mp hbst).2 hqr /-- A tree that contains something is not nil. -/ -theorem ne_nil_of_mem {t : Tree α} (q : α) (hq : q ∈ t) : t ≠ nil := by +theorem ne_nil_of_mem {t : BinaryTree α} (q : α) (hq : q ∈ t) : t ≠ nil := by rintro rfl; exact not_mem_nil q hq end BSTMembership -end Tree +end BinaryTree /-! ### BST Structure -/ section BSTStructure -/-- A binary search tree: a `Tree` bundled with a proof of the `IsBST` invariant. -/ +/-- A binary search tree: a `BinaryTree` bundled with a proof of the `IsBST` invariant. -/ structure BST (α : Type) [LinearOrder α] where - tree : Tree α - hBST : Tree.IsBST tree + tree : BinaryTree α + hBST : BinaryTree.IsBST tree namespace BST diff --git a/AlgoLib/DataStructures/SplayTree/BSTAPI.lean b/AlgoLib/DataStructures/SplayTree/BSTAPI.lean index c00d2e9..ae2b141 100644 --- a/AlgoLib/DataStructures/SplayTree/BSTAPI.lean +++ b/AlgoLib/DataStructures/SplayTree/BSTAPI.lean @@ -5,25 +5,29 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche, Sorrachai Yingchareonthawornchai -/ -import AlgoLib.DataStructures.SplayTree.Complexity -import AlgoLib.DataStructures.SplayTree.Correctness -import AlgoLib.DataStructures.SplayTree.StaticOptimality +module + +public import AlgoLib.DataStructures.SplayTree.Complexity +public import AlgoLib.DataStructures.SplayTree.Correctness +public import AlgoLib.DataStructures.SplayTree.StaticOptimality /-! # Splay Tree API for BST This module provides a high-level API for splaying directly on the `BST` type. -It encapsulates the raw `Tree` operations and their associated invariant +It encapsulates the raw `BinaryTree` operations and their associated invariant proofs, allowing users to safely and cleanly manipulate BSTs without manually re-proving the `IsBST` invariant after every rotation. -/ +@[expose] public section + variable {α : Type} [LinearOrder α] namespace SplayTree.BSTAPI open SplayTree -open Tree +open BinaryTree /-! ### Core Operation -/ diff --git a/AlgoLib/DataStructures/SplayTree/Basic.lean b/AlgoLib/DataStructures/SplayTree/Basic.lean index 3ee7983..22bca82 100644 --- a/AlgoLib/DataStructures/SplayTree/Basic.lean +++ b/AlgoLib/DataStructures/SplayTree/Basic.lean @@ -5,8 +5,10 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche, Sorrachai Yingchareonthawornchai -/ -import AlgoLib.DataStructures.BinaryTree.BinaryTree -import Mathlib.Data.List.Sort +module + +public import AlgoLib.DataStructures.BinaryTree.BinaryTree +public import Mathlib.Data.List.Sort /-! # Splay Tree Basic Definitions @@ -16,11 +18,13 @@ rotation primitives, path frames, and the `splay` and `splayUp` functions. It also provides fundamental structural lemmas regarding tree size and descent paths. -/ +@[expose] public section + variable {α : Type} namespace SplayTree -open Tree +open BinaryTree /-! ### Definitions -/ section Definitions @@ -41,22 +45,24 @@ def Dir.flip : Dir → Dir /-- Single primitive rotation that brings the `d`-child of the root up one level. `L` ↦ `rotateRight`, `R` ↦ `rotateLeft`. -/ -def Dir.bringUp : Dir → Tree α → Tree α +def Dir.bringUp : Dir → BinaryTree α → BinaryTree α | .L => rotateRight | .R => rotateLeft -lemma Dir.bringUp_ne_nil_of_ne_nil (d : Dir) (t : Tree α) (ht : t ≠ nil) : d.bringUp t ≠ nil := by +lemma Dir.bringUp_ne_nil_of_ne_nil (d : Dir) (t : BinaryTree α) (ht : t ≠ nil) : + d.bringUp t ≠ nil := by cases d <;> simp only [Dir.bringUp, rotateLeft, rotateRight] <;> split <;> simp [ht] /-- Apply `op` to the `d`-child of the root, leaving everything else fixed. -/ -def applyChild (d : Dir) (op : Tree α → Tree α) : Tree α → Tree α +def applyChild (d : Dir) (op : BinaryTree α → BinaryTree α) : BinaryTree α → BinaryTree α | l △[k] r => match d with | .L => (op l) △[k] r | .R => l △[k] (op r) | .nil => .nil -lemma applyChild_ne_nil_of_ne_nil (d : Dir) (op : Tree α → Tree α) (t : Tree α) (ht : t ≠ nil) : +lemma applyChild_ne_nil_of_ne_nil (d : Dir) (op : BinaryTree α → BinaryTree α) + (t : BinaryTree α) (ht : t ≠ nil) : applyChild d op t ≠ nil := by cases t <;> cases d <;> simp_all [applyChild] @@ -65,15 +71,15 @@ its key, and the subtree we did *not* descend into. -/ structure Frame α where dir : Dir key : α - sibling : Tree α + sibling : BinaryTree α /-- Re-attach a subtree `c` below the ancestor described by `f`. -/ -def Frame.attach (c : Tree α) (f : Frame α) : Tree α := +def Frame.attach (c : BinaryTree α) (f : Frame α) : BinaryTree α := match f.dir with | .L => c △[f.key] f.sibling | .R => f.sibling △[f.key] c -@[simp] lemma mirror_bringUp (d : Dir) (t : Tree α) : +@[simp] lemma mirror_bringUp (d : Dir) (t : BinaryTree α) : (d.bringUp t).mirror = d.flip.bringUp t.mirror := by cases d <;> simp [Dir.bringUp, Dir.flip] @@ -81,13 +87,13 @@ def Frame.attach (c : Tree α) (f : Frame α) : Tree α := def Frame.flip (f : Frame α) : Frame α := { dir := f.dir.flip, key := f.key, sibling := f.sibling.mirror } -@[simp] lemma mirror_attach (c : Tree α) (f : Frame α) : +@[simp] lemma mirror_attach (c : BinaryTree α) (f : Frame α) : (f.attach c).mirror = f.flip.attach c.mirror := by cases f with | mk d k s => cases d <;> simp [Frame.attach, Frame.flip, Dir.flip] @[simp] lemma mirror_applyChild_bringUp (d₁ d₂ : Dir) - (t : Tree α) : + (t : BinaryTree α) : (applyChild d₁ d₂.bringUp t).mirror = applyChild d₁.flip d₂.flip.bringUp t.mirror := by rcases t with _ | ⟨k, l, r⟩ @@ -97,16 +103,16 @@ def Frame.flip (f : Frame α) : Frame α := mirror_node] <;> congr 1 <;> first | exact mirror_rotateRight _ | exact mirror_rotateLeft _ -lemma Frame.attach_ne_nil (c : Tree α) (f : Frame α) : f.attach c ≠ nil := by +lemma Frame.attach_ne_nil (c : BinaryTree α) (f : Frame α) : f.attach c ≠ nil := by unfold attach; cases f.dir <;> simp /-- Descend from `t` toward `q`, returning the subtree reached (either the matching node or `.nil` if `q` is absent) and the path above it. The head of the returned list is the deepest frame (parent of the returned subtree). -/ -def descend [LinearOrder α] (t : Tree α) (q : α) : Tree α × List (Frame α) := +def descend [LinearOrder α] (t : BinaryTree α) (q : α) : BinaryTree α × List (Frame α) := go t [] where - go : Tree α → List (Frame α) → Tree α × List (Frame α) + go : BinaryTree α → List (Frame α) → BinaryTree α × List (Frame α) | .nil, acc => (.nil, acc) | l △[k] r, acc => if q = k then (l △[k] r, acc) @@ -121,7 +127,7 @@ up. Each double step (parent `f1`, grandparent `f2`) is: `f2.dir`-child (in direction `f1.dir`), then one outer rotation (in direction `f2.dir`). A leftover single frame is a plain zig/zag. -/ -def splayUp : Tree α → List (Frame α) → Tree α +def splayUp : BinaryTree α → List (Frame α) → BinaryTree α | c, [] => c | c, [f] => f.dir.bringUp (f.attach c) | c, f1 :: f2 :: rest => @@ -135,7 +141,7 @@ def splayUp : Tree α → List (Frame α) → Tree α /-- Bottom-up splay: the "textbook" splay analysed by Tarjan, Sundar, and Elmasry. If `q` is absent the last visited ancestor is splayed to the root. -/ -def splay [LinearOrder α] (t : Tree α) (q : α) : Tree α := +def splay [LinearOrder α] (t : BinaryTree α) (q : α) : BinaryTree α := match descend t q with | (.nil, []) => .nil | (.nil, f :: rest) => splayUp (f.attach .nil) rest @@ -143,12 +149,12 @@ def splay [LinearOrder α] (t : Tree α) (q : α) : Tree α := /-- Reassemble a subtree `c` with its ancestral path `path` (deepest frame first) back into the original tree. -/ -def reassemble (c : Tree α) (path : List (Frame α)) : Tree α := +def reassemble (c : BinaryTree α) (path : List (Frame α)) : BinaryTree α := path.foldl (fun c' f => f.attach c') c -@[simp] lemma reassemble_nil (c : Tree α) : reassemble c [] = c := rfl +@[simp] lemma reassemble_nil (c : BinaryTree α) : reassemble c [] = c := rfl -@[simp] lemma reassemble_cons (c : Tree α) (f : Frame α) (rest : List (Frame α)) : +@[simp] lemma reassemble_cons (c : BinaryTree α) (f : Frame α) (rest : List (Frame α)) : reassemble c (f :: rest) = reassemble (f.attach c) rest := rfl /-- Number of nodes a single frame contributes when re-attached: the @@ -166,12 +172,12 @@ end Definitions /-! ### Unfolding and Induction Lemmas for `splayUp` -/ section SplayUpInduction -@[simp] theorem splayUp_nil (c : Tree α) : splayUp c [] = c := rfl +@[simp] theorem splayUp_nil (c : BinaryTree α) : splayUp c [] = c := rfl -@[simp] theorem splayUp_singleton (c : Tree α) (f : Frame α) : +@[simp] theorem splayUp_singleton (c : BinaryTree α) (f : Frame α) : splayUp c [f] = f.dir.bringUp (f.attach c) := rfl -theorem splayUp_cons_cons (c : Tree α) (f1 f2 : Frame α) (rest : List (Frame α)) : +theorem splayUp_cons_cons (c : BinaryTree α) (f1 f2 : Frame α) (rest : List (Frame α)) : splayUp c (f1 :: f2 :: rest) = splayUp (if f1.dir = f2.dir then @@ -181,13 +187,13 @@ theorem splayUp_cons_cons (c : Tree α) (f1 f2 : Frame α) (rest : List (Frame (f2.attach (f1.attach c)))) rest := rfl -theorem splayUp_cons_cons_same (c : Tree α) (f1 f2 : Frame α) +theorem splayUp_cons_cons_same (c : BinaryTree α) (f1 f2 : Frame α) (rest : List (Frame α)) (h : f1.dir = f2.dir) : splayUp c (f1 :: f2 :: rest) = splayUp (f2.dir.bringUp (f2.dir.bringUp (f2.attach (f1.attach c)))) rest := by rw [splayUp_cons_cons]; simp [h] -theorem splayUp_cons_cons_opp (c : Tree α) (f1 f2 : Frame α) +theorem splayUp_cons_cons_opp (c : BinaryTree α) (f1 f2 : Frame α) (rest : List (Frame α)) (h : f1.dir ≠ f2.dir) : splayUp c (f1 :: f2 :: rest) = splayUp (f2.dir.bringUp @@ -198,12 +204,12 @@ theorem splayUp_cons_cons_opp (c : Tree α) (f1 f2 : Frame α) singleton frame, and the general pair-cons step. The tree `c` is generalised automatically. -/ theorem splayUp_induction - {motive : Tree α → List (Frame α) → Prop} + {motive : BinaryTree α → List (Frame α) → Prop} (nil : ∀ c, motive c []) (single : ∀ c f, motive c [f]) (step : ∀ c f1 f2 rest, (∀ c', motive c' rest) → motive c (f1 :: f2 :: rest)) - (c : Tree α) (path : List (Frame α)) : motive c path := by + (c : BinaryTree α) (path : List (Frame α)) : motive c path := by induction path using List.twoStepInduction generalizing c with | nil => exact nil c | singleton f => exact single c f @@ -221,19 +227,19 @@ section NodeCount pathNodes (f :: rest) = f.nodes + pathNodes rest := rfl @[simp] -theorem num_nodes_Frame_attach (c : Tree α) (f : Frame α) : +theorem num_nodes_Frame_attach (c : BinaryTree α) (f : Frame α) : (f.attach c).num_nodes = c.num_nodes + f.nodes := by unfold Frame.attach Frame.nodes cases f.dir <;> simp <;> omega @[simp] -theorem num_nodes_bringUp (d : Dir) (t : Tree α) : +theorem num_nodes_bringUp (d : Dir) (t : BinaryTree α) : (d.bringUp t).num_nodes = t.num_nodes := by cases d <;> simp [Dir.bringUp] @[simp] -theorem num_nodes_applyChild (d : Dir) (op : Tree α → Tree α) - (hop : ∀ s, (op s).num_nodes = s.num_nodes) (t : Tree α) : +theorem num_nodes_applyChild (d : Dir) (op : BinaryTree α → BinaryTree α) + (hop : ∀ s, (op s).num_nodes = s.num_nodes) (t : BinaryTree α) : (applyChild d op t).num_nodes = t.num_nodes := by cases t with | nil => rfl @@ -241,12 +247,12 @@ theorem num_nodes_applyChild (d : Dir) (op : Tree α → Tree α) cases d <;> simp [applyChild, hop] @[simp] -theorem num_nodes_applyChild_bringUp (d₁ d₂ : Dir) (t : Tree α) : +theorem num_nodes_applyChild_bringUp (d₁ d₂ : Dir) (t : BinaryTree α) : (applyChild d₁ d₂.bringUp t).num_nodes = t.num_nodes := num_nodes_applyChild _ _ (num_nodes_bringUp _) _ @[simp] -theorem num_nodes_splayUp (c : Tree α) (path : List (Frame α)) : +theorem num_nodes_splayUp (c : BinaryTree α) (path : List (Frame α)) : (splayUp c path).num_nodes = c.num_nodes + pathNodes path := by induction path using List.twoStepInduction generalizing c with | nil => simp [splayUp] @@ -257,7 +263,7 @@ theorem num_nodes_splayUp (c : Tree α) (path : List (Frame α)) : · rw [ih]; simp [Frame.nodes, pathNodes_cons]; omega · rw [ih]; simp [Frame.nodes, pathNodes_cons]; omega -theorem num_nodes_descend_go [LinearOrder α] (t : Tree α) (q : α) (acc : List (Frame α)) : +theorem num_nodes_descend_go [LinearOrder α] (t : BinaryTree α) (q : α) (acc : List (Frame α)) : let r := descend.go q t acc r.1.num_nodes + pathNodes r.2 = t.num_nodes + pathNodes acc := by induction t generalizing acc with @@ -271,13 +277,13 @@ theorem num_nodes_descend_go [LinearOrder α] (t : Tree α) (q : α) (acc : List · have := ihr (acc := ⟨.R, k, l⟩ :: acc) simp [Frame.nodes] at this ⊢; omega -theorem num_nodes_descend [LinearOrder α] (t : Tree α) (q : α) : +theorem num_nodes_descend [LinearOrder α] (t : BinaryTree α) (q : α) : (descend t q).1.num_nodes + pathNodes (descend t q).2 = t.num_nodes := by have := num_nodes_descend_go t q [] simpa [descend] using this @[simp] -theorem num_nodes_splay [LinearOrder α] (t : Tree α) (q : α) : +theorem num_nodes_splay [LinearOrder α] (t : BinaryTree α) (q : α) : (splay t q).num_nodes = t.num_nodes := by unfold splay have hd := num_nodes_descend t q @@ -304,7 +310,7 @@ section DescendLemmas @[simp] lemma descend_empty [LinearOrder α] (q : α) : descend .nil q = (.nil, []) := rfl -lemma descend_go_append [LinearOrder α] (q : α) (t : Tree α) (acc : List (Frame α)) : +lemma descend_go_append [LinearOrder α] (q : α) (t : BinaryTree α) (acc : List (Frame α)) : descend.go q t acc = ((descend.go q t []).1, (descend.go q t []).2 ++ acc) := by induction t generalizing acc with @@ -318,15 +324,15 @@ lemma descend_go_append [LinearOrder α] (q : α) (t : Tree α) (acc : List (Fra · rw [ihr (acc := ⟨.R, k, l⟩ :: acc), ihr (acc := [⟨.R, k, l⟩])]; simp -lemma descend_node_eq [LinearOrder α] (l : Tree α) (k : α) (r : Tree α) : +lemma descend_node_eq [LinearOrder α] (l : BinaryTree α) (k : α) (r : BinaryTree α) : descend (l △[k] r) k = (l △[k] r, []) := by simp [descend, descend.go] -lemma descend_eq_descend_go [LinearOrder α] (t : Tree α) (q : α) : +lemma descend_eq_descend_go [LinearOrder α] (t : BinaryTree α) (q : α) : descend t q = descend.go q t [] := rfl -lemma descend_node_lt [LinearOrder α] {l : Tree α} {k : α} - {r : Tree α} {q : α} (h : q < k) : +lemma descend_node_lt [LinearOrder α] {l : BinaryTree α} {k : α} + {r : BinaryTree α} {q : α} (h : q < k) : descend (l △[k] r) q = ((descend l q).1, (descend l q).2 ++ [⟨.L, k, r⟩]) := by @@ -335,8 +341,8 @@ lemma descend_node_lt [LinearOrder α] {l : Tree α} {k : α} unfold descend.go rw [if_neg hne, if_pos h, descend_go_append q l [⟨.L, k, r⟩]]; rfl -lemma descend_node_gt [LinearOrder α] {l : Tree α} {k : α} - {r : Tree α} {q : α} (h : k < q) : +lemma descend_node_gt [LinearOrder α] {l : BinaryTree α} {k : α} + {r : BinaryTree α} {q : α} (h : k < q) : descend (l △[k] r) q = ((descend r q).1, (descend r q).2 ++ [⟨.R, k, l⟩]) := by @@ -346,11 +352,11 @@ lemma descend_node_gt [LinearOrder α] {l : Tree α} {k : α} rw [if_neg hne, if_neg (not_lt.mpr h.le), descend_go_append q r [⟨.R, k, l⟩]]; rfl -lemma reassemble_append (c : Tree α) (p1 p2 : List (Frame α)) : +lemma reassemble_append (c : BinaryTree α) (p1 p2 : List (Frame α)) : reassemble c (p1 ++ p2) = reassemble (reassemble c p1) p2 := by simp [reassemble, List.foldl_append] -theorem descend_go_preserves_tree [LinearOrder α] (t : Tree α) +theorem descend_go_preserves_tree [LinearOrder α] (t : BinaryTree α) (q : α) (acc : List (Frame α)) : reassemble (descend.go q t acc).1 (descend.go q t acc).2 = reassemble t acc := by @@ -363,12 +369,12 @@ theorem descend_go_preserves_tree [LinearOrder α] (t : Tree α) · exact ihl (acc := ⟨.L, k, r⟩ :: acc) · exact ihr (acc := ⟨.R, k, l⟩ :: acc) -theorem descend_preserves_tree [LinearOrder α] (t : Tree α) (q : α) : +theorem descend_preserves_tree [LinearOrder α] (t : BinaryTree α) (q : α) : reassemble (descend t q).1 (descend t q).2 = t := by have := descend_go_preserves_tree t q [] simpa [descend] using this -lemma descend_go_length_le [LinearOrder α] (q : α) (t : Tree α) (acc : List (Frame α)) : +lemma descend_go_length_le [LinearOrder α] (q : α) (t : BinaryTree α) (acc : List (Frame α)) : acc.length ≤ (descend.go q t acc).2.length := by induction t generalizing acc with | nil => simp [descend.go] diff --git a/AlgoLib/DataStructures/SplayTree/Complexity.lean b/AlgoLib/DataStructures/SplayTree/Complexity.lean index 361913b..2f0d35f 100644 --- a/AlgoLib/DataStructures/SplayTree/Complexity.lean +++ b/AlgoLib/DataStructures/SplayTree/Complexity.lean @@ -5,9 +5,11 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche, Sorrachai Yingchareonthawornchai -/ -import AlgoLib.DataStructures.SplayTree.Basic -import Mathlib.Data.Real.Basic -import Mathlib.Analysis.SpecialFunctions.Log.Base +module + +public import AlgoLib.DataStructures.SplayTree.Basic +public import Mathlib.Data.Real.Basic +public import Mathlib.Analysis.SpecialFunctions.Log.Base /-! # Amortized Complexity of Splay Trees @@ -21,11 +23,13 @@ the classical O(m log n + n log n) total cost bound for a sequence of splay operations. -/ +@[expose] public section + variable {α : Type} namespace SplayTree -open Tree +open BinaryTree /-! ### Cost and Search-Path Length -/ section CostAndSearchPath @@ -34,19 +38,19 @@ section CostAndSearchPath Caution: If the search fails, we do not rotate (as currently defined in splay) the empty leaf and start to rotate from its ancestor, so the cost is path.length - 1. -/ -def splay.cost [LinearOrder α] (t : Tree α) (q : α) : ℝ := +def splay.cost [LinearOrder α] (t : BinaryTree α) (q : α) : ℝ := match descend t q with | (.nil, []) => 0 | (.nil, _ :: rest) => rest.length | (.node _ _ _, path) => path.length -theorem splay_cost_nonneg [LinearOrder α] (t : Tree α) (q : α) : +theorem splay_cost_nonneg [LinearOrder α] (t : BinaryTree α) (q : α) : 0 ≤ splay.cost t q := by unfold splay.cost split <;> simp /-- Subtrees have positive search path length. -/ -lemma search_path_len_node_pos [LinearOrder α] (l : Tree α) (k : α) (r : Tree α) +lemma search_path_len_node_pos [LinearOrder α] (l : BinaryTree α) (k : α) (r : BinaryTree α) (q : α) : 1 ≤ (l △[k] r).search_path_len q := by unfold search_path_len split_ifs <;> omega @@ -54,7 +58,7 @@ lemma search_path_len_node_pos [LinearOrder α] (l : Tree α) (k : α) (r : Tree /-- Relation between `search_path_len` and the length of the path produced by `descend`. When `descend` reaches a node, the search path is one link longer; when it reaches `.nil`, the two are equal. -/ -theorem search_path_len_eq_descend_length [LinearOrder α] (t : Tree α) (q : α) : +theorem search_path_len_eq_descend_length [LinearOrder α] (t : BinaryTree α) (q : α) : t.search_path_len q = (descend t q).2.length + (match (descend t q).1 with | .nil => 0 | .node _ _ _ => 1) := by @@ -89,11 +93,11 @@ path to give the O(log n) amortized bound. noncomputable section PotentialMethod /-- Rank of a tree: `log_2(num_nodes)`, or 0 for the empty tree. -/ -def rank (t : Tree α) : ℝ := +def rank (t : BinaryTree α) : ℝ := if t.num_nodes = 0 then 0 else Real.logb 2 t.num_nodes /-- Potential of a tree: sum of ranks over all subtrees (including itself). -/ -def φ : Tree α → ℝ +def φ : BinaryTree α → ℝ | .nil => 0 | s@(l △[_] r) => rank s + φ l + φ r @@ -127,25 +131,25 @@ theorem log_sum_le {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) /-! #### Basic rank and potential lemmas -/ -@[simp] lemma rank_empty : rank (.nil : Tree α) = 0 := by simp [rank] +@[simp] lemma rank_empty : rank (.nil : BinaryTree α) = 0 := by simp [rank] -lemma rank_nonneg (t : Tree α) : 0 ≤ rank t := by +lemma rank_nonneg (t : BinaryTree α) : 0 ≤ rank t := by simp only [rank]; split_ifs with h · rfl · exact Real.logb_nonneg (by grind) (by exact_mod_cast Nat.one_le_iff_ne_zero.mpr h) -@[simp] lemma φ_empty : φ (.nil : Tree α) = 0 := rfl +@[simp] lemma φ_empty : φ (.nil : BinaryTree α) = 0 := rfl -@[simp] lemma φ_node (l : Tree α) (k : α) (r : Tree α) : +@[simp] lemma φ_node (l : BinaryTree α) (k : α) (r : BinaryTree α) : φ (l △[k] r) = rank (l △[k] r) + φ l + φ r := rfl -lemma φ_nonneg : ∀ t : Tree α, 0 ≤ φ t +lemma φ_nonneg : ∀ t : BinaryTree α, 0 ≤ φ t | .nil => le_refl _ | l △[k] r => by simp [φ]; linarith [rank_nonneg (l △[k] r), φ_nonneg l, φ_nonneg r] -lemma rank_le_of_num_nodes_le {s t : Tree α} +lemma rank_le_of_num_nodes_le {s t : BinaryTree α} (h : s.num_nodes ≤ t.num_nodes) : rank s ≤ rank t := by simp only [rank] split_ifs with hs ht ht @@ -157,21 +161,21 @@ lemma rank_le_of_num_nodes_le {s t : Tree α} (by exact_mod_cast Nat.one_le_iff_ne_zero.mpr hs) (by simp_all only [Nat.cast_le]) -lemma rank_eq_of_num_nodes_eq {s t : Tree α} +lemma rank_eq_of_num_nodes_eq {s t : BinaryTree α} (h : s.num_nodes = t.num_nodes) : rank s = rank t := by exact le_antisymm (rank_le_of_num_nodes_le (le_of_eq h)) (rank_le_of_num_nodes_le (le_of_eq h.symm)) -@[simp] lemma rank_splay [LinearOrder α] (t : Tree α) (q : α) : +@[simp] lemma rank_splay [LinearOrder α] (t : BinaryTree α) (q : α) : rank (splay t q) = rank t := rank_eq_of_num_nodes_eq (num_nodes_splay t q) /-! #### Mirror preserves rank and potential -/ -lemma rank_mirror (t : Tree α) : rank t.mirror = rank t := by +lemma rank_mirror (t : BinaryTree α) : rank t.mirror = rank t := by simp [rank] -lemma φ_mirror : ∀ t : Tree α, φ t.mirror = φ t +lemma φ_mirror : ∀ t : BinaryTree α, φ t.mirror = φ t | .nil => rfl | l △[k] r => by change rank (r.mirror △[k] l.mirror) + φ r.mirror + φ l.mirror = @@ -184,7 +188,7 @@ lemma φ_mirror : ∀ t : Tree α, φ t.mirror = φ t /-- Transfer a potential-step inequality from mirrored trees to the originals. -/ private lemma φ_transfer_mirror - {step s c step' s' : Tree α} + {step s c step' s' : BinaryTree α} (hstep : step.mirror = step') (hs : s.mirror = s') (h : φ step' - φ s' + 2 ≤ @@ -214,28 +218,28 @@ private lemma one_le_logb {x : ℝ} (hx : 2 ≤ x) : /-! #### Potential of subtrees versus the whole tree -/ -theorem φ_subtree_le_left (l : Tree α) (k : α) (r : Tree α) : +theorem φ_subtree_le_left (l : BinaryTree α) (k : α) (r : BinaryTree α) : φ l ≤ φ (l △[k] r) := by simp [φ]; linarith [rank_nonneg (l △[k] r), φ_nonneg r] -theorem φ_subtree_le_right (l : Tree α) (k : α) (r : Tree α) : +theorem φ_subtree_le_right (l : BinaryTree α) (k : α) (r : BinaryTree α) : φ r ≤ φ (l △[k] r) := by simp [φ]; linarith [rank_nonneg (l △[k] r), φ_nonneg l] -theorem φ_le_attach (c : Tree α) (f : Frame α) : +theorem φ_le_attach (c : BinaryTree α) (f : Frame α) : φ c ≤ φ (f.attach c) := by cases f with | mk d k s => cases d <;> simp [Frame.attach, φ_node] <;> linarith [rank_nonneg (c △[k] s), rank_nonneg (s △[k] c), φ_nonneg c, φ_nonneg s] -theorem φ_le_reassemble (c : Tree α) (path : List (Frame α)) : +theorem φ_le_reassemble (c : BinaryTree α) (path : List (Frame α)) : φ c ≤ φ (reassemble c path) := by induction path generalizing c with | nil => simp | cons f rest ih => simp only [reassemble_cons]; exact le_trans (φ_le_attach c f) (ih _) -theorem φ_descend_subtree_le [LinearOrder α] (t : Tree α) (q : α) : +theorem φ_descend_subtree_le [LinearOrder α] (t : BinaryTree α) (q : α) : φ (descend t q).1 ≤ φ t := by have h := descend_preserves_tree t q calc φ (descend t q).1 @@ -243,15 +247,15 @@ theorem φ_descend_subtree_le [LinearOrder α] (t : Tree α) (q : α) : φ_le_reassemble _ _ _ = φ t := by rw [h] -theorem φ_attach_base_le [LinearOrder α] (t : Tree α) (q : α) +theorem φ_attach_base_le [LinearOrder α] (t : BinaryTree α) (q : α) (f : Frame α) (rest : List (Frame α)) (hd : descend t q = (.nil, f :: rest)) : φ (f.attach .nil) ≤ φ t := by have h := descend_preserves_tree t q rw [hd] at h; simp only at h; rw [← h] exact φ_le_reassemble (f.attach .nil) rest -theorem φ_descend_node_le [LinearOrder α] (t : Tree α) (q : α) - (l : Tree α) (k : α) (r : Tree α) (path : List (Frame α)) +theorem φ_descend_node_le [LinearOrder α] (t : BinaryTree α) (q : α) + (l : BinaryTree α) (k : α) (r : BinaryTree α) (path : List (Frame α)) (hd : descend t q = (l △[k] r, path)) : φ (l △[k] r) ≤ φ t := by have h := descend_preserves_tree t q rw [hd] at h; simp_all only [φ_node, ge_iff_le]; rw [← h] @@ -259,7 +263,7 @@ theorem φ_descend_node_le [LinearOrder α] (t : Tree α) (q : α) /-! #### Splay step potential bounds -/ -theorem φ_zig (c : Tree α) (f : Frame α) : +theorem φ_zig (c : BinaryTree α) (f : Frame α) : φ (f.dir.bringUp (f.attach c)) - φ (f.attach c) ≤ rank (f.dir.bringUp (f.attach c)) - rank c := by rcases f with ⟨d, key, sib⟩ @@ -279,8 +283,8 @@ theorem φ_zig (c : Tree α) (f : Frame α) : by simp; omega)] /-- Zig-zig, left–left direction only. -/ -private theorem φ_zigzig_left (c : Tree α) - (k1 : α) (n1 : Tree α) (k2 : α) (n2 : Tree α) : +private theorem φ_zigzig_left (c : BinaryTree α) + (k1 : α) (n1 : BinaryTree α) (k2 : α) (n2 : BinaryTree α) : let s := (Frame.mk .L k2 n2).attach ((Frame.mk .L k1 n1).attach c) let step := rotateRight (rotateRight s) φ step - φ s + 2 ≤ 3 * (rank step - rank c) := by @@ -314,7 +318,7 @@ private theorem φ_zigzig_left (c : Tree α) logb_mono (show (0 : ℝ) < 1 + a + b by linarith) (show 1 + a + b ≤ 2 + a + b + nn1 by linarith)] -theorem φ_zigzig (c : Tree α) (f1 f2 : Frame α) +theorem φ_zigzig (c : BinaryTree α) (f1 f2 : Frame α) (heq : f1.dir = f2.dir) : let s := f2.attach (f1.attach c) let step := f2.dir.bringUp (f2.dir.bringUp s) @@ -327,8 +331,8 @@ theorem φ_zigzig (c : Tree α) (f1 f2 : Frame α) exact φ_transfer_mirror (by simp [mirror_rotateLeft]) (by simp) h /-- Zig-zag, left–right direction only. -/ -private theorem φ_zigzag_left (c : Tree α) - (k1 : α) (n1 : Tree α) (k2 : α) (n2 : Tree α) : +private theorem φ_zigzag_left (c : BinaryTree α) + (k1 : α) (n1 : BinaryTree α) (k2 : α) (n2 : BinaryTree α) : let f1 : Frame α := ⟨.L, k1, n1⟩ let f2 : Frame α := ⟨.R, k2, n2⟩ let s := f2.attach (f1.attach c) @@ -369,7 +373,7 @@ private theorem φ_zigzag_left (c : Tree α) logb_mono (show (0 : ℝ) < 1 + a + b by linarith) (show 1 + a + b ≤ 3 + nn2 + a + b + nn1 by linarith)] -theorem φ_zigzag (c : Tree α) (f1 f2 : Frame α) +theorem φ_zigzag (c : BinaryTree α) (f1 f2 : Frame α) (hne : f1.dir ≠ f2.dir) : let s := f2.attach (f1.attach c) let step := f2.dir.bringUp (applyChild f2.dir f1.dir.bringUp s) @@ -384,14 +388,14 @@ theorem φ_zigzag (c : Tree α) (f1 f2 : Frame α) /-! #### Telescoping: potential change along the full splayUp -/ -lemma φ_attach_congr {s s' : Tree α} (f : Frame α) +lemma φ_attach_congr {s s' : BinaryTree α} (f : Frame α) (h : s.num_nodes = s'.num_nodes) : φ (f.attach s') - φ (f.attach s) = φ s' - φ s := by cases f with | mk d k sib => cases d <;> simp only [Frame.attach, φ_node, add_sub_add_right_eq_sub] <;> (unfold rank; simp [h]) -lemma φ_reassemble_congr {s s' : Tree α} (path : List (Frame α)) +lemma φ_reassemble_congr {s s' : BinaryTree α} (path : List (Frame α)) (h : s.num_nodes = s'.num_nodes) : φ (reassemble s' path) - φ (reassemble s path) = φ s' - φ s := by induction path generalizing s s' with @@ -403,7 +407,7 @@ lemma φ_reassemble_congr {s s' : Tree α} (path : List (Frame α)) /-- The total potential change of splayUp plus the path length is at most 3 × the rank increase + 1. -/ -theorem φ_splayUp (c : Tree α) (path : List (Frame α)) : +theorem φ_splayUp (c : BinaryTree α) (path : List (Frame α)) : φ (splayUp c path) - φ (reassemble c path) + path.length ≤ 3 * (rank (splayUp c path) - rank c) + 1 := by induction c, path using splayUp_induction with @@ -436,14 +440,14 @@ theorem φ_splayUp (c : Tree α) (path : List (Frame α)) : /-! #### The main O(log n) amortized bound -/ -private lemma rank_eq_logb {t : Tree α} +private lemma rank_eq_logb {t : BinaryTree α} (h : t.num_nodes ≠ 0) : rank t = Real.logb 2 t.num_nodes := by simp [rank, h] private lemma num_nodes_pos_of_descend_nonempty_path - [LinearOrder α] {t : Tree α} {q : α} - {reached : Tree α} {path : List (Frame α)} + [LinearOrder α] {t : BinaryTree α} {q : α} + {reached : BinaryTree α} {path : List (Frame α)} (hdecomp : descend t q = (reached, path)) (hpath : path ≠ []) : t.num_nodes ≠ 0 := by intro h0 @@ -454,7 +458,7 @@ private lemma num_nodes_pos_of_descend_nonempty_path · simp [pathNodes, Frame.nodes] at hd; omega theorem splay_amortized_bound [LinearOrder α] - (t : Tree α) (q : α) : + (t : BinaryTree α) (q : α) : φ (splay t q) - φ t + splay.cost t q ≤ 3 * Real.logb 2 t.num_nodes + 1 := by rcases hdecomp : descend t q with ⟨reached, path⟩ @@ -479,7 +483,7 @@ theorem splay_amortized_bound [LinearOrder α] rw [h_cost] have h_eq : splay t q = splayUp (f.attach .nil) rest := by simp [splay, hdecomp] rw [h_eq] - set base := f.attach (.nil : Tree α) + set base := f.attach (.nil : BinaryTree α) have hpres' : reassemble base rest = t := by rw [← hpres]; simp [reassemble, base] have hφ := φ_splayUp base rest rw [hpres'] at hφ @@ -515,27 +519,27 @@ section SequenceCost /-! #### Splay Sequence -/ /-- A clean sequence generator for a series of splays. -/ -def splaySeq [LinearOrder α] {m : ℕ} (init : Tree α) -(X : Fin m → α) : Fin (m + 1) → Tree α := +def splaySeq [LinearOrder α] {m : ℕ} (init : BinaryTree α) +(X : Fin m → α) : Fin (m + 1) → BinaryTree α := fun i => Nat.recOn i.val init (fun j acc => if h : j < m then splay acc (X ⟨j, h⟩) else acc) /-- The total cost is defined as the sum of actual rotations performed across the generated sequence. -/ -def splay.sequence_cost [LinearOrder α] {m : ℕ} (init : Tree α) (X : Fin m → α) : ℝ := +def splay.sequence_cost [LinearOrder α] {m : ℕ} (init : BinaryTree α) (X : Fin m → α) : ℝ := ∑ i : Fin m, splay.cost (splaySeq init X i.castSucc) (X i) /-- The tree at step `i+1` is exactly the result of splaying the target key on the tree at step `i`. -/ lemma splaySeq_succ [LinearOrder α] {m : ℕ} -(init : Tree α) (X : Fin m → α) (i : Fin m) : +(init : BinaryTree α) (X : Fin m → α) (i : Fin m) : splaySeq init X i.succ = splay (splaySeq init X i.castSucc) (X i) := by unfold splaySeq simp only [Fin.val_succ, Fin.val_castSucc, Fin.is_lt, ↓reduceDIte] /-- Splaying preserves the number of nodes across the entire sequence. -/ lemma splaySeq_num_nodes [LinearOrder α] {m : ℕ} -(init : Tree α) (X : Fin m → α) (i : Fin (m + 1)) : +(init : BinaryTree α) (X : Fin m → α) (i : Fin (m + 1)) : (splaySeq init X i).num_nodes = init.num_nodes := by unfold splaySeq generalize i.val = j @@ -561,7 +565,7 @@ private lemma nat_log_le (a b : ℕ) (hab : a ≤ b) : exact mul_le_mul_of_nonneg_left h_log ha_nonneg /-- Bound the maximum possible potential of any initial tree: Φ ≤ n log₂ n. -/ -lemma φ_le_n_log_n [LinearOrder α] (init : Tree α) : +lemma φ_le_n_log_n [LinearOrder α] (init : BinaryTree α) : φ init ≤ init.num_nodes * Real.logb 2 init.num_nodes := by induction init with | nil => simp [φ] @@ -614,7 +618,7 @@ theorem amortized_cost_bound' {S : Type*} (m : ℕ) hΦ_nonneg (s (Fin.last m))] theorem splay_total_cost [LinearOrder α] (m : ℕ) - (t : Fin (m + 1) → Tree α) + (t : Fin (m + 1) → BinaryTree α) (q : Fin m → α) (n : ℕ) (hseq : ∀ i : Fin m, t i.succ = splay (t i.castSucc) (q i)) @@ -647,7 +651,7 @@ theorem splay_total_cost [LinearOrder α] (m : ℕ) /-! #### The Main Total Cost Bound Theorem -/ theorem nlogn_cost [LinearOrder α] (n m : ℕ) (X : Fin m → α) - (init : Tree α) (h_size : init.num_nodes = n) : + (init : BinaryTree α) (h_size : init.num_nodes = n) : splay.sequence_cost init X ≤ m * (3 * Real.logb 2 n + 1) + n * Real.logb 2 n := by have h_amortized := splay_total_cost m (splaySeq init X) X n (splaySeq_succ init X) diff --git a/AlgoLib/DataStructures/SplayTree/Correctness.lean b/AlgoLib/DataStructures/SplayTree/Correctness.lean index 13a7f91..a6f4186 100644 --- a/AlgoLib/DataStructures/SplayTree/Correctness.lean +++ b/AlgoLib/DataStructures/SplayTree/Correctness.lean @@ -5,7 +5,9 @@ Authors: Anton Kovsharov, Antoine du Fresne von Hohenesche, Sorrachai Yingchareonthawornchai -/ -import AlgoLib.DataStructures.SplayTree.Basic +module + +public import AlgoLib.DataStructures.SplayTree.Basic /-! # Splay Tree Correctness @@ -15,44 +17,46 @@ It establishes that splaying preserves the binary search tree (BST) invariant and guarantees that querying an existing key successfully rotates it to the root. -/ +@[expose] public section + variable {α : Type} namespace SplayTree -open Tree +open BinaryTree /-! ### `toKeyList` Preservation -/ section ToKeyListPreservation -@[simp] theorem toKeyList_rotateRight (t : Tree α) : +@[simp] theorem toKeyList_rotateRight (t : BinaryTree α) : (rotateRight t).toKeyList = t.toKeyList := by cases t; · rfl rename_i k l r cases l <;> simp [rotateRight, toKeyList] -@[simp] theorem toKeyList_rotateLeft (t : Tree α) : +@[simp] theorem toKeyList_rotateLeft (t : BinaryTree α) : (rotateLeft t).toKeyList = t.toKeyList := by cases t; · rfl rename_i k l r cases r <;> simp [rotateLeft, toKeyList] -@[simp] theorem toKeyList_bringUp (d : Dir) (t : Tree α) : +@[simp] theorem toKeyList_bringUp (d : Dir) (t : BinaryTree α) : (d.bringUp t).toKeyList = t.toKeyList := by cases d <;> simp [Dir.bringUp] -@[simp] theorem toKeyList_applyChild (d : Dir) (op : Tree α → Tree α) - (hop : ∀ s, (op s).toKeyList = s.toKeyList) (t : Tree α) : +@[simp] theorem toKeyList_applyChild (d : Dir) (op : BinaryTree α → BinaryTree α) + (hop : ∀ s, (op s).toKeyList = s.toKeyList) (t : BinaryTree α) : (applyChild d op t).toKeyList = t.toKeyList := by cases t with | nil => rfl | node k l r => cases d <;> simp [applyChild, toKeyList, hop] @[simp] -theorem toKeyList_applyChild_bringUp (d₁ d₂ : Dir) (t : Tree α) : +theorem toKeyList_applyChild_bringUp (d₁ d₂ : Dir) (t : BinaryTree α) : (applyChild d₁ d₂.bringUp t).toKeyList = t.toKeyList := toKeyList_applyChild _ _ (toKeyList_bringUp _) _ -@[simp] theorem toKeyList_Frame_attach (c : Tree α) (f : Frame α) : +@[simp] theorem toKeyList_Frame_attach (c : BinaryTree α) (f : Frame α) : (f.attach c).toKeyList = (match f.dir with | .L => c.toKeyList ++ [f.key] ++ f.sibling.toKeyList @@ -60,7 +64,7 @@ theorem toKeyList_applyChild_bringUp (d₁ d₂ : Dir) (t : Tree α) : unfold Frame.attach cases f.dir <;> simp [toKeyList] -lemma reassemble_toKeyList_congr {c1 c2 : Tree α} (path : List (Frame α)) +lemma reassemble_toKeyList_congr {c1 c2 : BinaryTree α} (path : List (Frame α)) (h : c1.toKeyList = c2.toKeyList) : (reassemble c1 path).toKeyList = (reassemble c2 path).toKeyList := by induction path generalizing c1 c2 with @@ -70,7 +74,7 @@ lemma reassemble_toKeyList_congr {c1 c2 : Tree α} (path : List (Frame α)) simp [h] @[simp] -theorem toKeyList_splayUp (c : Tree α) (path : List (Frame α)) : +theorem toKeyList_splayUp (c : BinaryTree α) (path : List (Frame α)) : (splayUp c path).toKeyList = (reassemble c path).toKeyList := by induction c, path using splayUp_induction with | nil c => simp @@ -81,7 +85,7 @@ theorem toKeyList_splayUp (c : Tree α) (path : List (Frame α)) : (rw [ih]; apply reassemble_toKeyList_congr; simp) @[simp] -theorem toKeyList_splay [LinearOrder α] (t : Tree α) (q : α) : +theorem toKeyList_splay [LinearOrder α] (t : BinaryTree α) (q : α) : (splay t q).toKeyList = t.toKeyList := by unfold splay have hpres := descend_preserves_tree t q @@ -98,7 +102,7 @@ theorem toKeyList_splay [LinearOrder α] (t : Tree α) (q : α) : rw [h] at hpres rw [toKeyList_splayUp, ← hpres] -theorem splay_empty_iff [LinearOrder α] (t : Tree α) (q : α) : +theorem splay_empty_iff [LinearOrder α] (t : BinaryTree α) (q : α) : splay t q = .nil ↔ t = .nil := by constructor · intro h @@ -118,7 +122,7 @@ section BSTPreservation /-- Helper: `IsBSTAux t lb ub` is equivalent to the key list being bounded and sorted. Proved by induction on `t`. -/ -private lemma IsBSTAux_iff_bounded_sorted (t : Tree α) [LinearOrder α] : +private lemma IsBSTAux_iff_bounded_sorted (t : BinaryTree α) [LinearOrder α] : ∀ lb ub : Option α, IsBSTAux t lb ub ↔ (∀ x ∈ t.toKeyList, lb.elim True (· < x)) ∧ @@ -135,34 +139,34 @@ private lemma IsBSTAux_iff_bounded_sorted (t : Tree α) [LinearOrder α] : /-- A tree is a BST iff its in-order traversal is strictly sorted (pairwise `<`). Reduces every BST-preservation question to "does the operation preserve `toKeyList`?". -/ -theorem IsBST_iff_toKeyList_sorted [LinearOrder α] (t : Tree α) : +theorem IsBST_iff_toKeyList_sorted [LinearOrder α] (t : BinaryTree α) : IsBST t ↔ t.toKeyList.Pairwise (· < ·) := by simp only [IsBST, IsBSTAux_iff_bounded_sorted t none none, Option.elim] exact ⟨fun ⟨_, _, h⟩ => h, fun h => ⟨fun _ _ => trivial, fun _ _ => trivial, h⟩⟩ /-- Transfer BST-ness between trees with the same in-order traversal. -/ -lemma IsBST_of_toKeyList_eq [LinearOrder α] {t t' : Tree α} +lemma IsBST_of_toKeyList_eq [LinearOrder α] {t t' : BinaryTree α} (h : t'.toKeyList = t.toKeyList) (hbst : IsBST t) : IsBST t' := by rw [IsBST_iff_toKeyList_sorted] at hbst ⊢; rwa [h] /-- Bottom-up splay preserves the BST invariant. -/ -theorem IsBST_splay [LinearOrder α] (t : Tree α) (q : α) (h : IsBST t) : +theorem IsBST_splay [LinearOrder α] (t : BinaryTree α) (q : α) (h : IsBST t) : IsBST (splay t q) := IsBST_of_toKeyList_eq (toKeyList_splay t q) h /-- Each primitive rotation preserves the BST invariant. -/ -theorem IsBST_bringUp [LinearOrder α] (d : Dir) (t : Tree α) (h : IsBST t) : +theorem IsBST_bringUp [LinearOrder α] (d : Dir) (t : BinaryTree α) (h : IsBST t) : IsBST (d.bringUp t) := IsBST_of_toKeyList_eq (toKeyList_bringUp d t) h -theorem IsBST_applyChild [LinearOrder α] (d : Dir) (op : Tree α → Tree α) +theorem IsBST_applyChild [LinearOrder α] (d : Dir) (op : BinaryTree α → BinaryTree α) (hop_keys : ∀ s, (op s).toKeyList = s.toKeyList) - (t : Tree α) (h : IsBST t) : + (t : BinaryTree α) (h : IsBST t) : IsBST (applyChild d op t) := IsBST_of_toKeyList_eq (toKeyList_applyChild d op hop_keys t) h /-- Any frame-wise splay-up preserves BST-ness of the reassembled tree. -/ -theorem IsBST_splayUp [LinearOrder α] (c : Tree α) (path : List (Frame α)) +theorem IsBST_splayUp [LinearOrder α] (c : BinaryTree α) (path : List (Frame α)) (h : IsBST (reassemble c path)) : IsBST (splayUp c path) := IsBST_of_toKeyList_eq (toKeyList_splayUp c path) h @@ -173,9 +177,9 @@ end BSTPreservation section RootOfContainedKey /-- If `t.contains q`, the subtree reached by `descend` is a node whose key -equals `q`. Mirrors how `descend` and `Tree.contains` follow the same +equals `q`. Mirrors how `descend` and `BinaryTree.contains` follow the same comparison path. -/ -theorem descend_contains [LinearOrder α] (t : Tree α) (q : α) (h : t.BST_contains q) : +theorem descend_contains [LinearOrder α] (t : BinaryTree α) (q : α) (h : t.BST_contains q) : ∃ l r, (descend t q).1 = l △[q] r := by induction t with | nil => simp [BST_contains] at h @@ -195,7 +199,7 @@ theorem descend_contains [LinearOrder α] (t : Tree α) (q : α) (h : t.BST_cont /-- Membership-style variant of `descend_contains`: in a BST, if `q ∈ t` then `descend` reaches the node with key `q`. -/ -theorem descend_contains' [LinearOrder α] (t : Tree α) (q : α) (hbst : IsBST t) +theorem descend_contains' [LinearOrder α] (t : BinaryTree α) (q : α) (hbst : IsBST t) (h : q ∈ t) : ∃ l r, (descend t q).1 = l △[q] r := descend_contains t q (mem_imp_contains hbst h) @@ -203,7 +207,7 @@ theorem descend_contains' [LinearOrder α] (t : Tree α) (q : α) (hbst : IsBST whose root key is still `k`. Each rotation step brings `c` one level higher without changing its root key. -/ theorem splayUp_root_key_of_node : - ∀ (path : List (Frame α)) (l : Tree α) (k : α) (r : Tree α), + ∀ (path : List (Frame α)) (l : BinaryTree α) (k : α) (r : BinaryTree α), ∃ l' r', splayUp (l △[k] r) path = l' △[k] r' := by intro path induction path using List.twoStepInduction with @@ -223,7 +227,7 @@ theorem splayUp_root_key_of_node : rotateRight, rotateLeft] /-- If `t.contains q`, the bottom-up splay of `t` at `q` has `q` at the root. -/ -theorem splay_root_of_contains [LinearOrder α] (t : Tree α) (q : α) +theorem splay_root_of_contains [LinearOrder α] (t : BinaryTree α) (q : α) (hc : t.BST_contains q) : ∃ l r, splay t q = l △[q] r := by obtain ⟨lr, rr, hd⟩ := descend_contains t q hc unfold splay @@ -234,7 +238,7 @@ theorem splay_root_of_contains [LinearOrder α] (t : Tree α) (q : α) /-- Membership-style variant of `splay_root_of_contains`: in a BST, if `q ∈ t` then splaying brings `q` to the root. -/ -theorem splay_root_of_contains' [LinearOrder α] (t : Tree α) (q : α) +theorem splay_root_of_contains' [LinearOrder α] (t : BinaryTree α) (q : α) (hbst : IsBST t) (h : q ∈ t) : ∃ l r, splay t q = l △[q] r := splay_root_of_contains t q (mem_imp_contains hbst h) diff --git a/AlgoLib/DataStructures/SplayTree/StaticOptimality.lean b/AlgoLib/DataStructures/SplayTree/StaticOptimality.lean index 8b14b4e..a2f8278 100644 --- a/AlgoLib/DataStructures/SplayTree/StaticOptimality.lean +++ b/AlgoLib/DataStructures/SplayTree/StaticOptimality.lean @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Benjamin Aram Berendsohn, Antoine du Fresne von Hohenesche -/ -import AlgoLib.DataStructures.SplayTree.Weighted +module + +public import AlgoLib.DataStructures.SplayTree.Weighted /-! # Static optimality of Splay Trees @@ -13,40 +15,43 @@ Formalizes static optimality of splay trees with an O(n²) overall overhead, as analysis (https://11011110.github.io/blog/2008/02/07/static-optimality-for.html). -/ +@[expose] public section + variable {α : Type} namespace SplayTree namespace Weighted -open Tree +open BinaryTree /-- Total cost of a sequence of accesses in the static tree `t`: the sum of the search path lengths of the accessed keys. -/ -def staticCost {m : ℕ} [LinearOrder α] (t : Tree α) (X : Fin m → α) : ℕ := +def staticCost {m : ℕ} [LinearOrder α] (t : BinaryTree α) (X : Fin m → α) : ℕ := ∑ i, search_path_len t (X i) -private noncomputable def staticWeight [LinearOrder α] (s : Tree α) (q : α) : ℝ := +private noncomputable def staticWeight [LinearOrder α] (s : BinaryTree α) (q : α) : ℝ := 3 ^ (s.num_nodes - search_path_len s q : ℝ) -private lemma staticWeight_ge_one [LinearOrder α] (s : Tree α) (q : α) : +private lemma staticWeight_ge_one [LinearOrder α] (s : BinaryTree α) (q : α) : staticWeight s q ≥ 1 := Real.one_le_rpow (by norm_num) (sub_nonneg.mpr (mod_cast search_path_len_le_num_nodes s q)) -private lemma staticWeight_pos [LinearOrder α] (s : Tree α) (q : α) : staticWeight s q > 0 := +private lemma staticWeight_pos [LinearOrder α] (s : BinaryTree α) (q : α) : staticWeight s q > 0 := FnPos_of_FnLbOne (staticWeight_ge_one s) q /-- If two weight functions differ by a constant factor on the keys of `t`, so do the sizes. -/ -private lemma size_eq_mul_size {w w' : α → ℝ} {c : ℝ} {t : Tree α} +private lemma size_eq_mul_size {w w' : α → ℝ} {c : ℝ} {t : BinaryTree α} (h : ∀ x ∈ t.toKeyList, w x = c * w' x) : size w t = c * size w' t := by rw [size_from_toKeyList, size_from_toKeyList, ← List.sum_map_mul_left] exact congrArg List.sum (List.map_congr_left h) -private lemma search_path_len_left [LinearOrder α] (v : α) (l r : Tree α) (q : α) (hqv : q < v) : +private lemma search_path_len_left [LinearOrder α] (v : α) (l r : BinaryTree α) + (q : α) (hqv : q < v) : search_path_len (node v l r) q = 1 + search_path_len l q := by simp [search_path_len, hqv] -private lemma staticWeight_left [LinearOrder α] (v : α) (l r : Tree α) (q : α) (hqv : q < v) : +private lemma staticWeight_left [LinearOrder α] (v : α) (l r : BinaryTree α) (q : α) (hqv : q < v) : let s := node v l r staticWeight s q = 3 ^ (s.num_nodes - l.num_nodes - 1 : ℝ) * staticWeight l q := by simp only [staticWeight, num_nodes_node, Nat.cast_add, Nat.cast_one] @@ -55,7 +60,7 @@ private lemma staticWeight_left [LinearOrder α] (v : α) (l r : Tree α) (q : simp [search_path_len_left v l r q hqv]; linarith private lemma staticWeight_size_left [LinearOrder α] - {v : α} {l r : Tree α} (hbst : (node v l r).IsBST) : + {v : α} {l r : BinaryTree α} (hbst : (node v l r).IsBST) : let s := node v l r size (staticWeight s) l = 3 ^ (s.num_nodes - l.num_nodes - 1 : ℝ) * size (staticWeight l) l := by @@ -64,11 +69,13 @@ private lemma staticWeight_size_left [LinearOrder α] intro x hx exact staticWeight_left v l r x (lt_of_IsBST_left l v r hbst (mem_iff_mem_toKeyList.mpr hx)) -private lemma search_path_len_right [LinearOrder α] (v : α) (l r : Tree α) (q : α) (hqv : v < q) : +private lemma search_path_len_right [LinearOrder α] (v : α) (l r : BinaryTree α) + (q : α) (hqv : v < q) : search_path_len (node v l r) q = 1 + search_path_len r q := by simp [search_path_len, hqv, lt_asymm hqv] -private lemma staticWeight_right [LinearOrder α] (v : α) (l r : Tree α) (q : α) (hqv : v < q) : +private lemma staticWeight_right [LinearOrder α] (v : α) (l r : BinaryTree α) + (q : α) (hqv : v < q) : let s := node v l r staticWeight s q = 3 ^ (s.num_nodes - r.num_nodes - 1 : ℝ) * staticWeight r q := by simp only [staticWeight, num_nodes_node, Nat.cast_add, Nat.cast_one] @@ -77,7 +84,7 @@ private lemma staticWeight_right [LinearOrder α] (v : α) (l r : Tree α) (q : simp [search_path_len_right v l r q hqv]; linarith private lemma staticWeight_size_right [LinearOrder α] - {v : α} {l r : Tree α} (hbst : (node v l r).IsBST) : + {v : α} {l r : BinaryTree α} (hbst : (node v l r).IsBST) : let s := node v l r size (staticWeight s) r = 3 ^ (s.num_nodes - r.num_nodes - 1 : ℝ) * size (staticWeight r) r := by @@ -86,7 +93,7 @@ private lemma staticWeight_size_right [LinearOrder α] intro x hx exact staticWeight_right v l r x (gt_of_IsBST_right l v r hbst (mem_iff_mem_toKeyList.mpr hx)) -private lemma staticWeight_size_self_ub [LinearOrder α] (s : Tree α) (hbst : s.IsBST) : +private lemma staticWeight_size_self_ub [LinearOrder α] (s : BinaryTree α) (hbst : s.IsBST) : size (staticWeight s) s ≤ 3 ^ s.num_nodes := by induction s with | nil => simp @@ -123,13 +130,13 @@ private lemma staticWeight_size_self_ub [LinearOrder α] (s : Tree α) (hbst : s simp only [this]; apply mul_comm linarith -private lemma staticWeight_size_ub [LinearOrder α] (s t : Tree α) +private lemma staticWeight_size_ub [LinearOrder α] (s t : BinaryTree α) (hst : t.toKeyList.Sublist s.toKeyList) (hbst : s.IsBST) : size (staticWeight s) t ≤ 3 ^ s.num_nodes := (size_le_size_of_toKeyList_Sublist (FnNonneg_of_FnPos (staticWeight_pos s)) hst).trans (staticWeight_size_self_ub s hbst) -private lemma staticWeight_rank_ub [LinearOrder α] (s t : Tree α) +private lemma staticWeight_rank_ub [LinearOrder α] (s t : BinaryTree α) (hst : t.toKeyList.Sublist s.toKeyList) (hbst : s.IsBST) : rank (staticWeight s) t ≤ s.num_nodes * Real.logb 2 3 := by unfold rank; cases t with @@ -143,7 +150,7 @@ private lemma staticWeight_rank_ub [LinearOrder α] (s t : Tree α) simp · exact staticWeight_size_ub s _ hst hbst -private lemma staticWeight_φ_ub_aux [LinearOrder α] (s t : Tree α) +private lemma staticWeight_φ_ub_aux [LinearOrder α] (s t : BinaryTree α) (hst : t.toKeyList.Sublist s.toKeyList) (hbst : s.IsBST) : φ (staticWeight s) t ≤ s.num_nodes * t.num_nodes * Real.logb 2 3 := by induction t with @@ -161,7 +168,7 @@ private lemma staticWeight_φ_ub_aux [LinearOrder α] (s t : Tree α) have := staticWeight_rank_ub s (node v l r) hst hbst linarith -private lemma staticWeight_φ_ub [LinearOrder α] (s t : Tree α) +private lemma staticWeight_φ_ub [LinearOrder α] (s t : BinaryTree α) (hst : s.toKeyList = t.toKeyList) (hbst : s.IsBST) : φ (staticWeight s) t ≤ s.num_nodes ^ 2 * Real.logb 2 3 := by calc φ (staticWeight s) t ≤ s.num_nodes * t.num_nodes * Real.logb 2 3 := by @@ -179,13 +186,13 @@ and an O(n²) additive term. Assumes that all queries are successful. -/ theorem splay_tree_static_optimality [LinearOrder α] (m : ℕ) - (init s : Tree α) (hkeys : s.toKeyList = init.toKeyList) + (init s : BinaryTree α) (hkeys : s.toKeyList = init.toKeyList) (hinitbst : init.IsBST) (X : Fin m → α) (hX : ∀ i, X i ∈ init) : let n := s.num_nodes splay.sequence_cost init X ≤ m + (Real.logb 2 3) * (3 * staticCost s X + n ^ 2) := by have hsbst : s.IsBST := IsBST_of_toKeyList_eq hkeys hinitbst - have hφ_ub : (∀ (t : Tree α), t.toKeyList = init.toKeyList + have hφ_ub : (∀ (t : BinaryTree α), t.toKeyList = init.toKeyList → φ (staticWeight s) t ≤ ↑s.num_nodes ^ 2 * Real.logb 2 3) := by intro t h; apply staticWeight_φ_ub · simp [h, hkeys] diff --git a/AlgoLib/DataStructures/SplayTree/Weighted.lean b/AlgoLib/DataStructures/SplayTree/Weighted.lean index 24b900d..eac6fdd 100644 --- a/AlgoLib/DataStructures/SplayTree/Weighted.lean +++ b/AlgoLib/DataStructures/SplayTree/Weighted.lean @@ -4,11 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Benjamin Aram Berendsohn, Antoine du Fresne von Hohenesche -/ -import Mathlib.Data.Real.Basic -import Mathlib.Tactic.Linarith +module -import AlgoLib.DataStructures.SplayTree.Complexity -- Required for some lemmas -import AlgoLib.DataStructures.SplayTree.Correctness -- Required for some lemmas +public import Mathlib.Data.Real.Basic +public import Mathlib.Tactic.Linarith + +public import AlgoLib.DataStructures.SplayTree.Complexity -- Required for some lemmas +public import AlgoLib.DataStructures.SplayTree.Correctness -- Required for some lemmas /-! # Weighted Bounds for Splay Trees @@ -22,13 +24,15 @@ the splay tree. The weight function is defined simply as a function `w : α → `α`. -/ +@[expose] public section + variable {α : Type} namespace SplayTree namespace Weighted -open Tree +open BinaryTree /-! ## Definitions for weighted potential analysis -/ section WeightedPotentialMethod @@ -54,18 +58,18 @@ lemma FnNonneg_of_FnLbOne {w : α → ℝ} (h : FnLbOne w) : (FnNonneg w) := by intro x; linarith [h x] /-- Size of a tree: total weight of all nodes. -/ -def size (w : α → ℝ) : Tree α → ℝ +def size (w : α → ℝ) : BinaryTree α → ℝ | nil => (0 : ℝ) | node b l r => w b + size w l + size w r /-- Rank of a tree: logarithm of the size, or 0 for the empty tree. -/ -noncomputable def rank (w : α → ℝ) (t : Tree α) : ℝ := +noncomputable def rank (w : α → ℝ) (t : BinaryTree α) : ℝ := match t with | nil => 0 | _ => Real.logb 2 (size w t) /-- Potential of a tree: sum of ranks over all subtrees (including itself). -/ -noncomputable def φ (w : α → ℝ) : Tree α → ℝ +noncomputable def φ (w : α → ℝ) : BinaryTree α → ℝ | .nil => 0 | s@(l △[_] r) => rank w s + φ w l + φ w r @@ -76,56 +80,57 @@ variable {w : α → ℝ} /-! #### Basic size lemmas -/ -@[simp] lemma size_empty : size w (.nil : Tree α) = 0 := rfl -@[simp] lemma size_node {v : α} {l r : Tree α} : size w (node v l r) = w v + size w l + size w r := +@[simp] lemma size_empty : size w (.nil : BinaryTree α) = 0 := rfl +@[simp] lemma size_node {v : α} {l r : BinaryTree α} : + size w (node v l r) = w v + size w l + size w r := rfl -@[simp] theorem size_rotateRight (t : Tree α) : +@[simp] theorem size_rotateRight (t : BinaryTree α) : size w (rotateRight t) = size w t := by rcases t with _ | ⟨k, (_ | ⟨lk, ll, lr⟩), r⟩ <;> simp [rotateRight]; linarith -@[simp] theorem size_rotateLeft (t : Tree α) : +@[simp] theorem size_rotateLeft (t : BinaryTree α) : size w (rotateLeft t) = size w t := by rcases t with _ | ⟨k, l, (_ | ⟨rk, rl, rr⟩)⟩ <;> simp [rotateLeft]; linarith -lemma size_nonneg (hw : FnNonneg w) (t : Tree α) : 0 ≤ size w t := by +lemma size_nonneg (hw : FnNonneg w) (t : BinaryTree α) : 0 ≤ size w t := by induction t with | nil => rfl | node v l r ihl ihr => exact add_nonneg (add_nonneg (hw v) ihl) ihr -private lemma size_nonneg' (hw : FnPos w) (t : Tree α) : 0 ≤ size w t := +private lemma size_nonneg' (hw : FnPos w) (t : BinaryTree α) : 0 ≤ size w t := size_nonneg (FnNonneg_of_FnPos hw) t -private lemma size_nonneg'' (hw : FnLbOne w) (t : Tree α) : 0 ≤ size w t := +private lemma size_nonneg'' (hw : FnLbOne w) (t : BinaryTree α) : 0 ≤ size w t := size_nonneg (FnNonneg_of_FnLbOne hw) t -lemma size_ge_root_value (hw : FnNonneg w) (v : α) (l r : Tree α) : +lemma size_ge_root_value (hw : FnNonneg w) (v : α) (l r : BinaryTree α) : w v ≤ size w (node v l r) := le_add_of_le_of_nonneg (le_add_of_nonneg_right (size_nonneg hw l)) (size_nonneg hw r) -lemma size_ge_left_child (hw : FnNonneg w) (v : α) (l r : Tree α) : +lemma size_ge_left_child (hw : FnNonneg w) (v : α) (l r : BinaryTree α) : size w l ≤ size w (node v l r) := by simp [size_node]; linarith [hw v, size_nonneg hw r] -lemma size_ge_right_child (hw : FnNonneg w) (v : α) (l r : Tree α) : +lemma size_ge_right_child (hw : FnNonneg w) (v : α) (l r : BinaryTree α) : size w r ≤ size w (node v l r) := by simp [size_node]; linarith [hw v, size_nonneg hw l] -lemma size_pos_of_non_nil (hw : FnPos w) (t : Tree α) (h : t ≠ nil) : 0 < size w t := by +lemma size_pos_of_non_nil (hw : FnPos w) (t : BinaryTree α) (h : t ≠ nil) : 0 < size w t := by obtain ⟨l, v, r, rfl⟩ := non_empty_exist t h exact (hw v).trans_le (size_ge_root_value (FnNonneg_of_FnPos hw) v l r) -lemma size_from_toKeyList (t : Tree α) : +lemma size_from_toKeyList (t : BinaryTree α) : size w t = (t.toKeyList.map w).sum := by induction t <;> simp [*]; ring -lemma size_zero_iff_empty (hw : FnPos w) (t : Tree α) : size w t = 0 ↔ t = nil := +lemma size_zero_iff_empty (hw : FnPos w) (t : BinaryTree α) : size w t = 0 ↔ t = nil := ⟨not_imp_not.mp fun ht => (size_pos_of_non_nil hw t ht).ne', fun h => h ▸ rfl⟩ lemma size_le_size_of_toKeyList_Sublist (hw : FnNonneg w) - {s t : Tree α} (h : s.toKeyList.Sublist t.toKeyList) : + {s t : BinaryTree α} (h : s.toKeyList.Sublist t.toKeyList) : size w s ≤ size w t := by rw [size_from_toKeyList, size_from_toKeyList] exact (h.map w).sum_le_sum (List.forall_mem_map.mpr fun x _ => hw x) @@ -133,64 +138,65 @@ lemma size_le_size_of_toKeyList_Sublist (hw : FnNonneg w) /-! #### Splay-tree-related size lemmas -/ @[simp] -theorem size_bringUp (d : Dir) (t : Tree α) : +theorem size_bringUp (d : Dir) (t : BinaryTree α) : size w (d.bringUp t) = size w t := by cases d <;> simp [Dir.bringUp] @[simp] -theorem size_applyChild (d : Dir) (op : Tree α → Tree α) - (hop : ∀ s, size w (op s) = size w s) (t : Tree α) : +theorem size_applyChild (d : Dir) (op : BinaryTree α → BinaryTree α) + (hop : ∀ s, size w (op s) = size w s) (t : BinaryTree α) : size w (applyChild d op t) = size w t := by cases t <;> cases d <;> simp [applyChild, hop] -lemma size_Frame_attach (s : Tree α) (f : Frame α) : +lemma size_Frame_attach (s : BinaryTree α) (f : Frame α) : size w (f.attach s) = size w s + w f.key + size w f.sibling := by rcases f with ⟨_ | _, k, sib⟩ <;> simp only [Frame.attach, size_node] <;> ring -@[simp] lemma size_splay [LinearOrder α] (s : Tree α) (q : α) : size w (splay s q) = size w s := by +@[simp] lemma size_splay [LinearOrder α] (s : BinaryTree α) (q : α) : + size w (splay s q) = size w s := by rw [size_from_toKeyList, size_from_toKeyList]; rw [toKeyList_splay] /-! #### Basic rank lemmas -/ -@[simp] lemma rank_empty : rank w (.nil : Tree α) = 0 := rfl +@[simp] lemma rank_empty : rank w (.nil : BinaryTree α) = 0 := rfl -lemma rank_nonneg (hw : FnLbOne w) (t : Tree α) : 0 ≤ rank w t := by +lemma rank_nonneg (hw : FnLbOne w) (t : BinaryTree α) : 0 ≤ rank w t := by cases t with | nil => rfl | node v l r => exact Real.logb_nonneg one_lt_two ((hw v).trans (size_ge_root_value (FnNonneg_of_FnLbOne hw) v l r)) -private lemma rank_eq_logb_size (t : Tree α) : rank w t = Real.logb 2 (size w t) := by +private lemma rank_eq_logb_size (t : BinaryTree α) : rank w t = Real.logb 2 (size w t) := by cases t <;> simp [rank] -lemma rank_le_of_size_le (hw : FnLbOne w) (s t : Tree α) (h : size w s ≤ size w t) : +lemma rank_le_of_size_le (hw : FnLbOne w) (s t : BinaryTree α) (h : size w s ≤ size w t) : rank w s ≤ rank w t := by rcases eq_or_ne s nil with rfl | hs · exact rank_nonneg hw t · rw [rank_eq_logb_size, rank_eq_logb_size] exact Real.logb_le_logb_of_le one_lt_two (size_pos_of_non_nil (FnPos_of_FnLbOne hw) s hs) h -lemma rank_eq_of_toKeyList_eq {s t : Tree α} +lemma rank_eq_of_toKeyList_eq {s t : BinaryTree α} (h : s.toKeyList = t.toKeyList) : rank w s = rank w t := by rw [rank_eq_logb_size, rank_eq_logb_size, size_from_toKeyList, size_from_toKeyList, h] /-! #### Splay-related rank lemmas -/ -@[simp] lemma rank_splay [LinearOrder α] (w : α → ℝ) (t : Tree α) (q : α) : +@[simp] lemma rank_splay [LinearOrder α] (w : α → ℝ) (t : BinaryTree α) (q : α) : rank w (splay t q) = rank w t := rank_eq_of_toKeyList_eq (toKeyList_splay t q) /-! #### Basic potential lemmas -/ -@[simp] lemma φ_empty : φ w (.nil : Tree α) = 0 := rfl +@[simp] lemma φ_empty : φ w (.nil : BinaryTree α) = 0 := rfl -@[simp] lemma φ_node (l : Tree α) (k : α) (r : Tree α) : +@[simp] lemma φ_node (l : BinaryTree α) (k : α) (r : BinaryTree α) : φ w (l △[k] r) = rank w (l △[k] r) + φ w l + φ w r := rfl -lemma φ_nonneg (hw : FnLbOne w) (t : Tree α) : 0 ≤ φ w t := by +lemma φ_nonneg (hw : FnLbOne w) (t : BinaryTree α) : 0 ≤ φ w t := by induction t with | nil => rfl | node k l r ihl ihr => exact add_nonneg (add_nonneg (rank_nonneg hw _) ihl) ihr @@ -198,28 +204,28 @@ lemma φ_nonneg (hw : FnLbOne w) (t : Tree α) : 0 ≤ φ w t := by /-! #### Potential of subtrees versus the whole tree -/ -theorem φ_le_attach (hw : FnLbOne w) (c : Tree α) (f : Frame α) : +theorem φ_le_attach (hw : FnLbOne w) (c : BinaryTree α) (f : Frame α) : φ w c ≤ φ w (f.attach c) := by rcases f with ⟨_ | _, k, s⟩ <;> simp only [Frame.attach, φ_node] <;> linarith [rank_nonneg hw (c △[k] s), rank_nonneg hw (s △[k] c), φ_nonneg hw s] -theorem φ_le_reassemble (hw : FnLbOne w) (c : Tree α) (path : List (Frame α)) : +theorem φ_le_reassemble (hw : FnLbOne w) (c : BinaryTree α) (path : List (Frame α)) : φ w c ≤ φ w (reassemble c path) := by induction path generalizing c with | nil => rfl | cons f rest ih => exact (φ_le_attach hw c f).trans (ih _) -theorem φ_descend_subtree_le [LinearOrder α] (hw : FnLbOne w) (t : Tree α) (q : α) : +theorem φ_descend_subtree_le [LinearOrder α] (hw : FnLbOne w) (t : BinaryTree α) (q : α) : φ w (descend t q).1 ≤ φ w t := (φ_le_reassemble hw _ _).trans_eq (congrArg (φ w) (descend_preserves_tree t q)) /-! #### Mirror preserves rank and potential -/ -lemma rank_mirror (t : Tree α) : rank w t.mirror = rank w t := by +lemma rank_mirror (t : BinaryTree α) : rank w t.mirror = rank w t := by simp [rank_eq_logb_size, size_from_toKeyList] -lemma φ_mirror (t : Tree α) : φ w t.mirror = φ w t := by +lemma φ_mirror (t : BinaryTree α) : φ w t.mirror = φ w t := by induction t with | nil => rfl | node v l r => @@ -229,7 +235,7 @@ lemma φ_mirror (t : Tree α) : φ w t.mirror = φ w t := by /-! #### Splay step potential bounds -/ -theorem φ_zig (hw : FnLbOne w) (c : Tree α) (f : Frame α) : +theorem φ_zig (hw : FnLbOne w) (c : BinaryTree α) (f : Frame α) : φ w (f.dir.bringUp (f.attach c)) - φ w (f.attach c) ≤ rank w (f.dir.bringUp (f.attach c)) - rank w c := by rcases f with ⟨_ | _, key, sib⟩ <;> rcases c with _ | ⟨k, l, r⟩ <;> @@ -241,7 +247,7 @@ theorem φ_zig (hw : FnLbOne w) (c : Tree α) (f : Frame α) : (by simp; linarith [hw k, size_nonneg'' hw r])] private theorem φ_zigzig_left (hw : FnLbOne w) - (a b c : α) (t1 t2 t3 t4 : Tree α) : + (a b c : α) (t1 t2 t3 t4 : BinaryTree α) : let x := node a t1 t2 -- The node we're rotating let s := node c (node b x t3) t4 -- The initial tree let s' := rotateRight (rotateRight s) -- The resulting tree @@ -272,7 +278,7 @@ private theorem φ_zigzig_left (hw : FnLbOne w) · unfold s' rotateRight s x x'; simp; linarith [hw b] linarith -theorem φ_zigzig (hw : FnLbOne w) (a : α) (l r : Tree α) (f1 f2 : Frame α) +theorem φ_zigzig (hw : FnLbOne w) (a : α) (l r : BinaryTree α) (f1 f2 : Frame α) (heq : f1.dir = f2.dir) : let c := node a l r let s := f2.attach (f1.attach c) @@ -286,7 +292,7 @@ theorem φ_zigzig (hw : FnLbOne w) (a : α) (l r : Tree α) (f1 f2 : Frame α) simpa only [← mirror_node, φ_mirror, rank_mirror] using h private theorem φ_zigzag_left (hw : FnLbOne w) - (a b c : α) (t1 t2 t3 t4 : Tree α) : + (a b c : α) (t1 t2 t3 t4 : BinaryTree α) : let x := node b t2 t3 -- The node we're rotating let s := node a t1 (node c x t4) -- The initial tree let s' := rotateLeft (applyChild .R rotateRight s) -- The resulting tree @@ -321,7 +327,7 @@ private theorem φ_zigzag_left (hw : FnLbOne w) linarith -theorem φ_zigzag (hw : FnLbOne w) (a : α) (l r : Tree α) (f1 f2 : Frame α) +theorem φ_zigzag (hw : FnLbOne w) (a : α) (l r : BinaryTree α) (f1 f2 : Frame α) (hne : f1.dir ≠ f2.dir) : let c := node a l r let s := f2.attach (f1.attach c) @@ -337,12 +343,12 @@ theorem φ_zigzag (hw : FnLbOne w) (a : α) (l r : Tree α) (f1 f2 : Frame α) /-! #### Telescoping: potential change along the full splayUp -/ -lemma φ_attach_congr {s s' : Tree α} (f : Frame α) +lemma φ_attach_congr {s s' : BinaryTree α} (f : Frame α) (h : size w s = size w s') : φ w (f.attach s') - φ w (f.attach s) = φ w s' - φ w s := by rcases f with ⟨_ | _, k, sib⟩ <;> simp [Frame.attach, rank, h] -lemma φ_reassemble_congr {s s' : Tree α} (path : List (Frame α)) +lemma φ_reassemble_congr {s s' : BinaryTree α} (path : List (Frame α)) (h : size w s = size w s') : φ w (reassemble s' path) - φ w (reassemble s path) = φ w s' - φ w s := by induction path generalizing s s' with @@ -351,7 +357,7 @@ lemma φ_reassemble_congr {s s' : Tree α} (path : List (Frame α)) /-- The total potential change of splayUp plus the path length is at most 3 × the rank increase + 1. -/ -theorem φ_splayUp (hw : FnLbOne w) (c : Tree α) (hc : c ≠ nil) (path : List (Frame α)) : +theorem φ_splayUp (hw : FnLbOne w) (c : BinaryTree α) (hc : c ≠ nil) (path : List (Frame α)) : φ w (splayUp c path) - φ w (reassemble c path) + path.length ≤ 3 * (rank w (splayUp c path) - rank w c) + 1 := by induction c, path using splayUp_induction with @@ -401,7 +407,7 @@ theorem φ_splayUp (hw : FnLbOne w) (c : Tree α) (hc : c ≠ nil) (path : List /-- Slightly weaker version of Sleator and Tarjan's access lemma: Does not take into account the subtree rooted at q, only the weight of q itself; also requires weights at least one. -/ theorem splay_access_lemma [LinearOrder α] - (hw : FnLbOne w) (t : Tree α) (q : α) (hbst : IsBST t) (hq : q ∈ t) : + (hw : FnLbOne w) (t : BinaryTree α) (q : α) (hbst : IsBST t) (hq : q ∈ t) : φ w (splay t q) - φ w t + splay.cost t q ≤ 3 * Real.logb 2 (size w t / w q) + 1 := by rcases hdecomp : descend t q with ⟨reached, path⟩ @@ -462,7 +468,7 @@ theorem total_cost_bound {S : Type*} (m : ℕ) theorem splay_total_weighted_cost' [LinearOrder α] (hw : FnLbOne w) (m : ℕ) - (t : Fin (m + 1) → Tree α) + (t : Fin (m + 1) → BinaryTree α) (q : Fin m → α) (hseq : ∀ i : Fin m, t i.succ = splay (t i.castSucc) (q i)) (hbst : (t 0).IsBST) @@ -491,7 +497,7 @@ theorem splay_total_weighted_cost' [LinearOrder α] theorem splay_total_weighted_cost [LinearOrder α] (hw : FnLbOne w) (m : ℕ) - (init : Tree α) (hbst : init.IsBST) + (init : BinaryTree α) (hbst : init.IsBST) {φ_ub : ℝ} (hφ : ∀ t, t.toKeyList = init.toKeyList → φ w t ≤ φ_ub) (X : Fin m → α) (hcont : ∀ i, X i ∈ init) : splay.sequence_cost init X ≤ @@ -514,12 +520,13 @@ def FnLb (b : ℝ) (w : α → ℝ) : Prop := lemma FnPos_of_FnLb {w : α → ℝ} {b : ℝ} (h : FnLb b w) (hb : b > 0) : (FnPos w) := by intro x; linarith [h x] -private lemma size_mul_weight (c : ℝ) (t : Tree α) : +private lemma size_mul_weight (c : ℝ) (t : BinaryTree α) : let w' := fun x => c * (w x) size w' t = c * (size w t) := by simp [size_from_toKeyList, List.sum_map_mul_left] -private lemma rank_mul_weight (hw : FnPos w) (c : ℝ) (hc : c > 0) (t : Tree α) (ht : t ≠ nil) : +private lemma rank_mul_weight (hw : FnPos w) (c : ℝ) (hc : c > 0) + (t : BinaryTree α) (ht : t ≠ nil) : let w' := fun x => c * (w x) rank w' t = rank w t + Real.logb 2 c := by cases t with @@ -531,7 +538,7 @@ private lemma rank_mul_weight (hw : FnPos w) (c : ℝ) (hc : c > 0) (t : Tree α simp; linarith [hw v, size_nonneg' hw l, size_nonneg' hw r] unfold rank; simp only [w', size_mul_weight, Real.logb_mul hcnz hsize]; linarith -private lemma φ_mul_weight (hw : FnPos w) (c : ℝ) (hc : c > 0) (t : Tree α) : +private lemma φ_mul_weight (hw : FnPos w) (c : ℝ) (hc : c > 0) (t : BinaryTree α) : let w' := fun x => c * (w x) φ w' t = φ w t + t.num_nodes * (Real.logb 2 c) := by induction t with @@ -546,7 +553,7 @@ bound, not necessarily one. -/ theorem splay_total_weighted_cost_lb [LinearOrder α] {ε : ℝ} (hε : ε > 0) (hw : FnLb ε w) (m : ℕ) - (t : Fin (m + 1) → Tree α) + (t : Fin (m + 1) → BinaryTree α) (q : Fin m → α) (hseq : ∀ i : Fin m, t i.succ = splay (t i.castSucc) (q i)) (hbst : (t 0).IsBST) @@ -589,7 +596,7 @@ theorem FnLb_of_Finite_of_FnPos {w : α → ℝ} [Finite α] (hw : FnPos w) : theorem splay_total_weighted_cost_pos [LinearOrder α] [Finite α] (hw : FnPos w) (m : ℕ) - (t : Fin (m + 1) → Tree α) + (t : Fin (m + 1) → BinaryTree α) (q : Fin m → α) (hseq : ∀ i : Fin m, t i.succ = splay (t i.castSucc) (q i)) (hbst : (t 0).IsBST) diff --git a/AlgoLib/DataStructures/UnionFind/Basic.lean b/AlgoLib/DataStructures/UnionFind/Basic.lean index e69de29..0cca093 100644 --- a/AlgoLib/DataStructures/UnionFind/Basic.lean +++ b/AlgoLib/DataStructures/UnionFind/Basic.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/Theory/Graph/Adjacency.lean b/AlgoLib/Theory/Graph/Adjacency.lean index b84aff5..b216c69 100644 --- a/AlgoLib/Theory/Graph/Adjacency.lean +++ b/AlgoLib/Theory/Graph/Adjacency.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Basic +module + +public import AlgoLib.Theory.Graph.Basic /-! # Adjacency @@ -54,6 +56,8 @@ defined in terms of the same edge-membership conditions. target `v`; no `symm` lemma is provided for them. -/ +@[expose] public section + namespace AlgoLib variable {α β : Type*} diff --git a/AlgoLib/Theory/Graph/Basic'.lean b/AlgoLib/Theory/Graph/Basic'.lean index bb606e1..f3d9092 100644 --- a/AlgoLib/Theory/Graph/Basic'.lean +++ b/AlgoLib/Theory/Graph/Basic'.lean @@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai -/ -import Cslib.Foundations.Semantics.LTS.Basic -import Mathlib.Combinatorics.SimpleGraph.Basic -import Mathlib.Combinatorics.Graph.Basic +module + +public import Cslib.Foundations.Semantics.LTS.Basic +public import Mathlib.Combinatorics.SimpleGraph.Basic +public import Mathlib.Combinatorics.Graph.Basic @[expose] public section diff --git a/AlgoLib/Theory/Graph/Basic.lean b/AlgoLib/Theory/Graph/Basic.lean index 9200175..5032aae 100644 --- a/AlgoLib/Theory/Graph/Basic.lean +++ b/AlgoLib/Theory/Graph/Basic.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai -/ -import Mathlib.Data.Sym.Sym2 +module + +public import Mathlib.Data.Sym.Sym2 /-! # Graph structures @@ -61,6 +63,8 @@ The corresponding `Coe` instances are registered. coercion: an undirected graph should be viewed as directed only on purpose. -/ +@[expose] public section + namespace AlgoLib variable {α β : Type*} diff --git a/AlgoLib/Theory/Graph/Coloring/Basic.lean b/AlgoLib/Theory/Graph/Coloring/Basic.lean index 8b13789..0cca093 100644 --- a/AlgoLib/Theory/Graph/Coloring/Basic.lean +++ b/AlgoLib/Theory/Graph/Coloring/Basic.lean @@ -1 +1 @@ - +module diff --git a/AlgoLib/Theory/Graph/Connectivity/Basic.lean b/AlgoLib/Theory/Graph/Connectivity/Basic.lean index a49aba7..a2b4ea2 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Basic.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Basic.lean @@ -3,11 +3,13 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5), Basil Rohner, Sorrachai Yingchareonthawornchai -/ -import AlgoLib.Theory.Graph.Connectivity.Reachable -import AlgoLib.Theory.Graph.Connectivity.Directed -import AlgoLib.Theory.Graph.Connectivity.Components -import AlgoLib.Theory.Graph.Connectivity.Cuts -import AlgoLib.Theory.Graph.Connectivity.Connectivity +module + +public import AlgoLib.Theory.Graph.Connectivity.Reachable +public import AlgoLib.Theory.Graph.Connectivity.Directed +public import AlgoLib.Theory.Graph.Connectivity.Components +public import AlgoLib.Theory.Graph.Connectivity.Cuts +public import AlgoLib.Theory.Graph.Connectivity.Connectivity /-! # `AlgoLib.Theory.Graph.Connectivity` diff --git a/AlgoLib/Theory/Graph/Connectivity/Components.lean b/AlgoLib/Theory/Graph/Connectivity/Components.lean index ef3ad6d..cfa7d55 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Components.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Components.lean @@ -3,8 +3,10 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Connectivity.Reachable -import Mathlib.Data.Set.Card +module + +public import AlgoLib.Theory.Graph.Connectivity.Reachable +public import Mathlib.Data.Set.Card /-! # Connected components @@ -47,6 +49,8 @@ represents them as sets of vertices and collects the facts that make the reachability-level characterizations below, which avoid cardinals altogether. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Connectivity/Connectivity.lean b/AlgoLib/Theory/Graph/Connectivity/Connectivity.lean index 04fed1a..3f1e573 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Connectivity.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Connectivity.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Finite -import AlgoLib.Theory.Graph.Connectivity.Cuts -import Mathlib.Data.ENat.Lattice +module + +public import AlgoLib.Theory.Graph.Finite +public import AlgoLib.Theory.Graph.Connectivity.Cuts +public import Mathlib.Data.ENat.Lattice /-! # Vertex and edge connectivity @@ -51,6 +53,8 @@ edges, must be removed to destroy the connectivity of `G`. automatically. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Connectivity/Cuts.lean b/AlgoLib/Theory/Graph/Connectivity/Cuts.lean index ab3960e..9c0e65a 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Cuts.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Cuts.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Connectivity.Components +module + +public import AlgoLib.Theory.Graph.Connectivity.Components /-! # Cuts, separators and boundaries @@ -44,6 +46,8 @@ boundary of a vertex set. allowed to meet `A` and `B`, and a terminal inside the cut is simply no longer a vertex. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Connectivity/Directed.lean b/AlgoLib/Theory/Graph/Connectivity/Directed.lean index b6614f4..4d72678 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Directed.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Directed.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Fable 5.1) -/ -import AlgoLib.Theory.Graph.Structures.InSimpleDiGraph -import AlgoLib.Theory.Graph.Connectivity.Reachable -import Mathlib.Data.ENat.Lattice +module + +public import AlgoLib.Theory.Graph.Structures.InSimpleDiGraph +public import AlgoLib.Theory.Graph.Connectivity.Reachable +public import Mathlib.Data.ENat.Lattice /-! # Reachability and distance in a simple directed graph @@ -53,6 +55,8 @@ that definition usable. correctness proof serve both kinds of graph. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib @@ -134,6 +138,7 @@ theorem le_dist_iff {G : SimpleDiGraph α} {u v : α} {n : ℕ∞} : theorem dist_eq_top_iff {G : SimpleDiGraph α} {u v : α} : G.dist u v = ⊤ ↔ ¬ G.Reachable u v := by simp [dist, iInf_eq_top, Reachable] + exact ⟨fun h w hG hu hns => h w hns hG hu, fun h w hns hG hu => h w hG hu hns⟩ /-- `v` is reachable from `u` exactly when the distance is finite. -/ theorem reachable_iff_dist_ne_top {G : SimpleDiGraph α} {u v : α} : diff --git a/AlgoLib/Theory/Graph/Connectivity/Reachable.lean b/AlgoLib/Theory/Graph/Connectivity/Reachable.lean index 8ec29f1..0d03f4b 100644 --- a/AlgoLib/Theory/Graph/Connectivity/Reachable.lean +++ b/AlgoLib/Theory/Graph/Connectivity/Reachable.lean @@ -3,8 +3,10 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Delete -import AlgoLib.Theory.Graph.Structures.InSimpleGraph +module + +public import AlgoLib.Theory.Graph.Delete +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph /-! # Reachability in a simple graph @@ -47,6 +49,8 @@ is the failure of reachability after a deletion. connected component. `IsPreconnected` is the non-emptiness-free variant. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Decidable.lean b/AlgoLib/Theory/Graph/Decidable.lean index 14a7bb2..12549c8 100644 --- a/AlgoLib/Theory/Graph/Decidable.lean +++ b/AlgoLib/Theory/Graph/Decidable.lean @@ -3,10 +3,12 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Delete -import AlgoLib.Theory.Graph.Degree -import AlgoLib.Theory.Graph.Finite -import AlgoLib.Util.Decidable +module + +public import AlgoLib.Theory.Graph.Delete +public import AlgoLib.Theory.Graph.Degree +public import AlgoLib.Theory.Graph.Finite +public import AlgoLib.Util.Decidable /-! # Decidable graph predicates @@ -56,6 +58,8 @@ on top of what is here and of the breadth-first search in them explicitly keeps instance search from having to unfold structure literals. -/ +@[expose] public section + namespace AlgoLib variable {α : Type*} diff --git a/AlgoLib/Theory/Graph/Degree.lean b/AlgoLib/Theory/Graph/Degree.lean index 2ae6f75..53602ec 100644 --- a/AlgoLib/Theory/Graph/Degree.lean +++ b/AlgoLib/Theory/Graph/Degree.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner -/ -import AlgoLib.Theory.Graph.Adjacency -import Mathlib.Data.Set.Card -import Mathlib.Data.ENat.Lattice +module + +public import AlgoLib.Theory.Graph.Adjacency +public import Mathlib.Data.Set.Card +public import Mathlib.Data.ENat.Lattice /-! # Neighbourhoods and degrees @@ -50,6 +52,8 @@ and the minimum and maximum degree. `minDegree = ⊤` without per-definition finiteness hypotheses. -/ +@[expose] public section + namespace AlgoLib variable {α β : Type*} diff --git a/AlgoLib/Theory/Graph/Delete.lean b/AlgoLib/Theory/Graph/Delete.lean index f6e6f54..28fa338 100644 --- a/AlgoLib/Theory/Graph/Delete.lean +++ b/AlgoLib/Theory/Graph/Delete.lean @@ -3,8 +3,10 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Adjacency -import AlgoLib.Theory.Graph.Subgraph +module + +public import AlgoLib.Theory.Graph.Adjacency +public import AlgoLib.Theory.Graph.Subgraph /-! # Deleting vertices and edges @@ -37,6 +39,8 @@ a set of edges, or remove a set of vertices. endpoint pair?) that should not be settled here as a side effect. -/ +@[expose] public section + namespace AlgoLib variable {α : Type*} @@ -134,9 +138,9 @@ lemma SimpleGraph.deleteVertices_mono (G : SimpleGraph α) {S₁ S₂ : Set α} makes the `induce` API of `AlgoLib.Graph.Subgraph` available for `deleteVertices`. -/ lemma SimpleGraph.deleteVertices_eq_induce (G : SimpleGraph α) (S : Set α) : G.deleteVertices S = G.induce Sᶜ := by - cases G - simp only [SimpleGraph.deleteVertices, SimpleGraph.induce, SimpleGraph.mk.injEq] - refine ⟨?_, rfl⟩ - rw [Set.diff_eq, Set.inter_comm] + have hv : G.vertexSet \ S = Sᶜ ∩ G.vertexSet := by + ext v + exact and_comm + exact (SimpleGraph.mk.injEq ..).mpr ⟨hv, rfl⟩ end AlgoLib diff --git a/AlgoLib/Theory/Graph/Embeddings/Basic.lean b/AlgoLib/Theory/Graph/Embeddings/Basic.lean index 8b13789..0cca093 100644 --- a/AlgoLib/Theory/Graph/Embeddings/Basic.lean +++ b/AlgoLib/Theory/Graph/Embeddings/Basic.lean @@ -1 +1 @@ - +module diff --git a/AlgoLib/Theory/Graph/Finite.lean b/AlgoLib/Theory/Graph/Finite.lean index 048f915..ebb74d6 100644 --- a/AlgoLib/Theory/Graph/Finite.lean +++ b/AlgoLib/Theory/Graph/Finite.lean @@ -3,13 +3,15 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Huang.JiangYi (co/ Claude Opus 5) -/ -import Mathlib.Algebra.Group.Nat.Even -import Mathlib.Data.Nat.Choose.Basic -import Mathlib.Data.Set.Card -import Mathlib.Data.Set.Finite.Basic -import Mathlib.Data.Set.Finite.Range -import Mathlib.Data.Sym.Card -import AlgoLib.Theory.Graph.Basic +module + +public import Mathlib.Algebra.Group.Nat.Even +public import Mathlib.Data.Nat.Choose.Basic +public import Mathlib.Data.Set.Card +public import Mathlib.Data.Set.Finite.Basic +public import Mathlib.Data.Set.Finite.Range +public import Mathlib.Data.Sym.Card +public import AlgoLib.Theory.Graph.Basic /-! # Finiteness of graphs @@ -72,6 +74,8 @@ proved rather than assumed. `|E(G)| ≤ 2·C(|V(G)|, 2)`. -/ +@[expose] public section + namespace AlgoLib open scoped AlgoLib @@ -286,7 +290,7 @@ subtype. -/ private lemma SimpleGraph.vertexFinset_card_eq (G : SimpleGraph α) [Finite G.vertexSet] [Fintype G.vertexSet] : G.vertexFinset.card = Fintype.card G.vertexSet := by - simp [SimpleGraph.vertexFinset] + exact Set.toFinset_card G.vertexSet /-- Lift an edge of `G` to a non-diagonal `Sym2` on the vertex subtype. -/ private lemma SimpleGraph.edge_lift (G : SimpleGraph α) {e : Sym2 α} (he : e ∈ G.edgeSet) : @@ -334,7 +338,7 @@ theorem SimpleGraph.card_edgeFinset_le_card_choose_two private lemma SimpleDiGraph.vertexFinset_card_eq (G : SimpleDiGraph α) [Fintype G.vertexSet] : G.vertexFinset.card = Fintype.card G.vertexSet := by - simp [SimpleDiGraph.vertexFinset] + exact Set.toFinset_card G.vertexSet /-- The edge set of a simple directed graph has size at most `2·C(|V|, 2)`. The proof embeds `E(G)` into the off-diagonal of `V × V`. -/ diff --git a/AlgoLib/Theory/Graph/Graphs.lean b/AlgoLib/Theory/Graph/Graphs.lean index e69de29..0cca093 100644 --- a/AlgoLib/Theory/Graph/Graphs.lean +++ b/AlgoLib/Theory/Graph/Graphs.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/Theory/Graph/Matching/Basic.lean b/AlgoLib/Theory/Graph/Matching/Basic.lean index e69de29..0cca093 100644 --- a/AlgoLib/Theory/Graph/Matching/Basic.lean +++ b/AlgoLib/Theory/Graph/Matching/Basic.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/Theory/Graph/Minors/Basic.lean b/AlgoLib/Theory/Graph/Minors/Basic.lean index e69de29..0cca093 100644 --- a/AlgoLib/Theory/Graph/Minors/Basic.lean +++ b/AlgoLib/Theory/Graph/Minors/Basic.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/Theory/Graph/Spectral/Basic.lean b/AlgoLib/Theory/Graph/Spectral/Basic.lean index e69de29..0cca093 100644 --- a/AlgoLib/Theory/Graph/Spectral/Basic.lean +++ b/AlgoLib/Theory/Graph/Spectral/Basic.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/Theory/Graph/Spectral/Cheeger_LB.lean b/AlgoLib/Theory/Graph/Spectral/Cheeger_LB.lean index 7995377..8cd0fd1 100644 --- a/AlgoLib/Theory/Graph/Spectral/Cheeger_LB.lean +++ b/AlgoLib/Theory/Graph/Spectral/Cheeger_LB.lean @@ -1,4 +1,8 @@ -import AlgoLib.Theory.Graph.Spectral.Expansion +module + +public import AlgoLib.Theory.Graph.Spectral.Expansion + +@[expose] public section -- Cheeger's Lower Bound -- Authors: Weixuan Yuan, Yuchen Zhong diff --git a/AlgoLib/Theory/Graph/Spectral/Cuts.lean b/AlgoLib/Theory/Graph/Spectral/Cuts.lean index 3ac44a3..a996d52 100644 --- a/AlgoLib/Theory/Graph/Spectral/Cuts.lean +++ b/AlgoLib/Theory/Graph/Spectral/Cuts.lean @@ -1,10 +1,14 @@ -import Mathlib.Tactic -import Mathlib.Order.WithBot -import Mathlib.Data.Sym.Sym2 -import Mathlib.Data.Finset.Basic +module -import AlgoLib.Theory.Graph.Basic -import AlgoLib.Theory.Graph.Finite +public import Mathlib.Tactic +public import Mathlib.Order.WithBot +public import Mathlib.Data.Sym.Sym2 +public import Mathlib.Data.Finset.Basic + +public import AlgoLib.Theory.Graph.Basic +public import AlgoLib.Theory.Graph.Finite + +@[expose] public section -- Cuts (undirected simple) -- Authors: Weixuan Yuan diff --git a/AlgoLib/Theory/Graph/Spectral/Expansion.lean b/AlgoLib/Theory/Graph/Spectral/Expansion.lean index 8f94ca5..6dce675 100644 --- a/AlgoLib/Theory/Graph/Spectral/Expansion.lean +++ b/AlgoLib/Theory/Graph/Spectral/Expansion.lean @@ -1,10 +1,14 @@ -import Mathlib.Tactic +module -import AlgoLib.Theory.Graph.Basic -import AlgoLib.Theory.Graph.Finite -import AlgoLib.Theory.Graph.Degree -import AlgoLib.Theory.Graph.Spectral.Cuts -import AlgoLib.Theory.Graph.Spectral.Helper +public import Mathlib.Tactic + +public import AlgoLib.Theory.Graph.Basic +public import AlgoLib.Theory.Graph.Finite +public import AlgoLib.Theory.Graph.Degree +public import AlgoLib.Theory.Graph.Spectral.Cuts +public import AlgoLib.Theory.Graph.Spectral.Helper + +@[expose] public section -- Cuts and contractions (undirected simple) -- Authors: Yuchen Zhong, Weixuan Yuan diff --git a/AlgoLib/Theory/Graph/Spectral/Helper.lean b/AlgoLib/Theory/Graph/Spectral/Helper.lean index 0091ac0..a4959fc 100644 --- a/AlgoLib/Theory/Graph/Spectral/Helper.lean +++ b/AlgoLib/Theory/Graph/Spectral/Helper.lean @@ -1,6 +1,10 @@ -import Mathlib.Tactic -import AlgoLib.Theory.Graph.Basic -import AlgoLib.Theory.Graph.Finite +module + +public import Mathlib.Tactic +public import AlgoLib.Theory.Graph.Basic +public import AlgoLib.Theory.Graph.Finite + +@[expose] public section -- Arithmetic Helpers -- Authors: Weixuan Yuan, Yuchen Zhong diff --git a/AlgoLib/Theory/Graph/Structures/Basic.lean b/AlgoLib/Theory/Graph/Structures/Basic.lean index dbf77c5..6837427 100644 --- a/AlgoLib/Theory/Graph/Structures/Basic.lean +++ b/AlgoLib/Theory/Graph/Structures/Basic.lean @@ -1,3 +1,5 @@ +module + /- /- Copyright (c) 2026 Basil Rohner. All rights reserved. diff --git a/AlgoLib/Theory/Graph/Structures/Cycle.lean b/AlgoLib/Theory/Graph/Structures/Cycle.lean index e69de29..0cca093 100644 --- a/AlgoLib/Theory/Graph/Structures/Cycle.lean +++ b/AlgoLib/Theory/Graph/Structures/Cycle.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/Theory/Graph/Structures/Eulerian.lean b/AlgoLib/Theory/Graph/Structures/Eulerian.lean index 7cd3363..6bdf40e 100644 --- a/AlgoLib/Theory/Graph/Structures/Eulerian.lean +++ b/AlgoLib/Theory/Graph/Structures/Eulerian.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Basic -import AlgoLib.Theory.Graph.Structures.Walk -import AlgoLib.Theory.Graph.Structures.SimpleWalk +module + +public import AlgoLib.Theory.Graph.Basic +public import AlgoLib.Theory.Graph.Structures.Walk +public import AlgoLib.Theory.Graph.Structures.SimpleWalk /-! # Eulerian walks @@ -23,6 +25,8 @@ is open. * `SimpleWalk.IsEulerianCircuit G w` — Eulerian and closed. -/ +@[expose] public section + open AlgoLib variable {α ε : Type*} diff --git a/AlgoLib/Theory/Graph/Structures/Forest.lean b/AlgoLib/Theory/Graph/Structures/Forest.lean index b2ba0a6..8d69cf5 100644 --- a/AlgoLib/Theory/Graph/Structures/Forest.lean +++ b/AlgoLib/Theory/Graph/Structures/Forest.lean @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan, Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Structures.InSimpleGraph +module + +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph /-! # Forests @@ -29,6 +31,8 @@ hand that a walk's vertices and edges lie in `G`. That has been retired in favou `SimpleGraph.IsSimpleWalkIn.iff_edges`) and carries the whole closure API. -/ +@[expose] public section + open AlgoLib variable {α : Type*} diff --git a/AlgoLib/Theory/Graph/Structures/Hamiltonian.lean b/AlgoLib/Theory/Graph/Structures/Hamiltonian.lean index 943d67d..6051997 100644 --- a/AlgoLib/Theory/Graph/Structures/Hamiltonian.lean +++ b/AlgoLib/Theory/Graph/Structures/Hamiltonian.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Basic -import AlgoLib.Theory.Graph.Structures.Walk -import AlgoLib.Theory.Graph.Structures.SimpleWalk +module + +public import AlgoLib.Theory.Graph.Basic +public import AlgoLib.Theory.Graph.Structures.Walk +public import AlgoLib.Theory.Graph.Structures.SimpleWalk /-! # Hamiltonian walks @@ -23,6 +25,8 @@ Hamiltonian *path* is open (head ≠ tail in a simple graph); a Hamiltonian * `SimpleWalk.IsHamiltonianCycle G w` — Hamiltonian and closed. -/ +@[expose] public section + open AlgoLib variable {α ε : Type*} diff --git a/AlgoLib/Theory/Graph/Structures/InGraph.lean b/AlgoLib/Theory/Graph/Structures/InGraph.lean index e69de29..0cca093 100644 --- a/AlgoLib/Theory/Graph/Structures/InGraph.lean +++ b/AlgoLib/Theory/Graph/Structures/InGraph.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/Theory/Graph/Structures/InSimpleDiGraph.lean b/AlgoLib/Theory/Graph/Structures/InSimpleDiGraph.lean index 04f0057..2352fb3 100644 --- a/AlgoLib/Theory/Graph/Structures/InSimpleDiGraph.lean +++ b/AlgoLib/Theory/Graph/Structures/InSimpleDiGraph.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Adjacency -import AlgoLib.Theory.Graph.Subgraph -import AlgoLib.Theory.Graph.Structures.SimpleWalk +module + +public import AlgoLib.Theory.Graph.Adjacency +public import AlgoLib.Theory.Graph.Subgraph +public import AlgoLib.Theory.Graph.Structures.SimpleWalk /-! # Vertex sequences realized in a simple directed graph @@ -50,6 +52,8 @@ simple walks to a `SimpleDiGraph`. to the vertex sequence layer. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Structures/InSimpleGraph.lean b/AlgoLib/Theory/Graph/Structures/InSimpleGraph.lean index b5ae71d..40ae378 100644 --- a/AlgoLib/Theory/Graph/Structures/InSimpleGraph.lean +++ b/AlgoLib/Theory/Graph/Structures/InSimpleGraph.lean @@ -3,10 +3,12 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.VertexSeq -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Walk -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Path -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Cycle +module + +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.VertexSeq +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Walk +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Path +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Cycle /-! # Vertex sequences, walks, paths and cycles realized in a simple graph diff --git a/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Cycle.lean b/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Cycle.lean index 1686c66..917d8cf 100644 --- a/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Cycle.lean +++ b/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Cycle.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Path -import AlgoLib.Theory.Graph.Structures.SimpleCycle -import Mathlib.Data.Set.Card +module + +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Path +public import AlgoLib.Theory.Graph.Structures.SimpleCycle +public import Mathlib.Data.Set.Card /-! # Simple cycles realized in a simple graph @@ -31,6 +33,8 @@ Part of the `InSimpleGraph` folder; see the umbrella module * `SimpleGraph.isAcyclic_of_subgraph` — acyclicity passes from supergraphs to subgraphs. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Path.lean b/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Path.lean index 7697eab..1ff9462 100644 --- a/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Path.lean +++ b/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Path.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Walk -import AlgoLib.Theory.Graph.Structures.SimplePath -import Mathlib.Data.Set.Card +module + +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Walk +public import AlgoLib.Theory.Graph.Structures.SimplePath +public import Mathlib.Data.Set.Card /-! # Simple paths realized in a simple graph @@ -18,6 +20,8 @@ Part of the `InSimpleGraph` folder; see the umbrella module `AlgoLib.Theory.Structures.InSimpleGraph`. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Structures/InSimpleGraph/VertexSeq.lean b/AlgoLib/Theory/Graph/Structures/InSimpleGraph/VertexSeq.lean index 0d3779f..66272b9 100644 --- a/AlgoLib/Theory/Graph/Structures/InSimpleGraph/VertexSeq.lean +++ b/AlgoLib/Theory/Graph/Structures/InSimpleGraph/VertexSeq.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Adjacency -import AlgoLib.Theory.Graph.Subgraph -import AlgoLib.Theory.Graph.Structures.VertexSeq +module + +public import AlgoLib.Theory.Graph.Adjacency +public import AlgoLib.Theory.Graph.Subgraph +public import AlgoLib.Theory.Graph.Structures.VertexSeq /-! # Vertex sequences realized in a simple graph @@ -26,6 +28,8 @@ Part of the `InSimpleGraph` folder; see the umbrella module `AlgoLib.Theory.Structures.InSimpleGraph` for the overview. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Walk.lean b/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Walk.lean index 154c663..9d2e7b1 100644 --- a/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Walk.lean +++ b/AlgoLib/Theory/Graph/Structures/InSimpleGraph/Walk.lean @@ -3,8 +3,10 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.InSimpleGraph.VertexSeq -import AlgoLib.Theory.Graph.Structures.SimpleWalk +module + +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.VertexSeq +public import AlgoLib.Theory.Graph.Structures.SimpleWalk /-! # Simple walks realized in a simple graph @@ -18,6 +20,8 @@ Part of the `InSimpleGraph` folder; see the umbrella module `AlgoLib.Theory.Structures.InSimpleGraph`. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Structures/Path.lean b/AlgoLib/Theory/Graph/Structures/Path.lean index e69de29..0cca093 100644 --- a/AlgoLib/Theory/Graph/Structures/Path.lean +++ b/AlgoLib/Theory/Graph/Structures/Path.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/Theory/Graph/Structures/SimpleCycle.lean b/AlgoLib/Theory/Graph/Structures/SimpleCycle.lean index 9e92b5d..24c4270 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleCycle.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleCycle.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.SimplePath +module + +public import AlgoLib.Theory.Graph.Structures.SimplePath /-! # Simple cycles @@ -34,6 +36,8 @@ API here only reflects a chosen traversal orientation and is not canonical. * `SimpleCycle.edges_ofTwoPaths_subset` — every selected edge comes from an input path. -/ +@[expose] public section + variable {α : Type*} namespace SimpleWalk @@ -112,7 +116,7 @@ attribute [simp, grind] SimpleCycle.val SimpleCycle.vertices SimpleCycle.support /-- The simple walk obtained by appending the starting vertex to a path of length at least two. -/ -private def walkOfPathClosing (p : SimplePath α) (hlen : 2 ≤ p.vertices.length) : +def walkOfPathClosing (p : SimplePath α) (hlen : 2 ≤ p.vertices.length) : SimpleWalk α := ⟨VertexSeq.cons p.vertices p.head, ⟨p.val.nonstalling, fun h => by have hzero := VertexSeq.length_zero_of_nodup_closed p.vertices p.nodup @@ -120,15 +124,16 @@ private def walkOfPathClosing (p : SimplePath α) (hlen : 2 ≤ p.vertices.lengt omega⟩⟩ /-- Closing a path of length at least two satisfies the cycle conditions. -/ -private lemma isCycle_ofPathClosing (p : SimplePath α) +lemma isCycle_ofPathClosing (p : SimplePath α) (hlen : 2 ≤ p.vertices.length) : SimpleWalk.IsCycle (walkOfPathClosing p hlen) := by change 3 ≤ (VertexSeq.cons p.vertices p.head).length ∧ (VertexSeq.cons p.vertices p.head).closed ∧ (VertexSeq.cons p.vertices p.head).dropTail.nodup - refine ⟨?_, by simp [VertexSeq.closed], by simpa using p.nodup⟩ - simp [VertexSeq.length] at hlen ⊢ - omega + refine ⟨?_, by simp [VertexSeq.closed], ?_⟩ + · simp [VertexSeq.length] at hlen ⊢ + omega + · simpa only [VertexSeq.dropTail] using p.nodup /-- Close a simple path by adding an edge from its tail back to its head. -/ def ofPathClosing (p : SimplePath α) @@ -139,13 +144,13 @@ def ofPathClosing (p : SimplePath α) /-! ### ofInternallyDisjointPaths -/ /-- Two paths with the same tail can be glued after reversing the second one. -/ -private lemma tail_eq_head_reverse_of_tail_eq (P Q : SimplePath α) +lemma tail_eq_head_reverse_of_tail_eq (P Q : SimplePath α) (htail : P.tail = Q.tail) : P.val.tail = Q.val.reverse.head := by simpa using htail /-- The walk obtained by following two internally disjoint paths in opposite directions is a simple cycle. -/ -private lemma isCycle_ofInternallyDisjointPaths (P Q : SimplePath α) +lemma isCycle_ofInternallyDisjointPaths (P Q : SimplePath α) (hhead : P.head = Q.head) (htail : P.tail = Q.tail) (hab : P.head ≠ P.tail) (hint : ∀ z, z ∈ P.vertices → z ∈ Q.vertices → @@ -258,7 +263,7 @@ longest common prefix of their vertex lists. Defined via `List.commonPrefix`, so no index arithmetic is involved. Compare the earlier `findIdx`-on-`zip` definition, which forced every downstream lemma to carry dependent `getElem` bounds. -/ -private def divergenceVertex [DecidableEq α] (p q : SimplePath α) +def divergenceVertex [DecidableEq α] (p q : SimplePath α) (hhead : p.head = q.head) : α := (List.commonPrefix p.vertices.toList q.vertices.toList).getLast (List.commonPrefix_ne_nil (x := p.head) (by grind) (by grind)) @@ -266,7 +271,7 @@ private def divergenceVertex [DecidableEq α] (p q : SimplePath α) /-- The three facts that make the divergence vertex what it is: the two suffixes from it end together, it is not that common endpoint, and the two paths take different next steps out of it. -/ -private lemma divergenceVertex_core [DecidableEq α] (p q : SimplePath α) +lemma divergenceVertex_core [DecidableEq α] (p q : SimplePath α) (hhead : p.head = q.head) (htail : p.tail = q.tail) (hne : p.vertices ≠ q.vertices) : let a := divergenceVertex p q hhead @@ -332,7 +337,7 @@ private lemma divergenceVertex_core [DecidableEq α] (p q : SimplePath α) /-- The full divergence specification used by `buildOfTwoPaths`. The four extra components are routine consequences of `divergenceVertex_core`. -/ -private lemma divergenceVertex_spec [DecidableEq α] (p q : SimplePath α) +lemma divergenceVertex_spec [DecidableEq α] (p q : SimplePath α) (hhead : p.head = q.head) (htail : p.tail = q.tail) (hne : p.vertices ≠ q.vertices) : let a := divergenceVertex p q hhead @@ -346,23 +351,23 @@ private lemma divergenceVertex_spec [DecidableEq α] (p q : SimplePath α) refine ⟨hap, haq, ?_, ?_, htaileq, ?_, ?_, hane, hsecond⟩ <;> grind [VertexSeq.head_suffixFrom] -private lemma divergenceVertex_mem_left [DecidableEq α] (p q : SimplePath α) +lemma divergenceVertex_mem_left [DecidableEq α] (p q : SimplePath α) (hhead : p.head = q.head) (htail : p.tail = q.tail) (hne : p.vertices ≠ q.vertices) : divergenceVertex p q hhead ∈ p.vertices := (divergenceVertex_core p q hhead htail hne).1 -private lemma divergenceVertex_mem_right [DecidableEq α] (p q : SimplePath α) +lemma divergenceVertex_mem_right [DecidableEq α] (p q : SimplePath α) (hhead : p.head = q.head) (htail : p.tail = q.tail) (hne : p.vertices ≠ q.vertices) : divergenceVertex p q hhead ∈ q.vertices := (divergenceVertex_core p q hhead htail hne).2.1 -private def firstRejoinVertex [DecidableEq α] (a : α) (p q : SimplePath α) +def firstRejoinVertex [DecidableEq α] (a : α) (p q : SimplePath α) (hwit : ∃ z ∈ p.vertices.toList, ¬(z = a ∨ z ∉ q.vertices)) : α := (p.vertices.dropWhile (fun z => z = a ∨ z ∉ q.vertices) hwit).head -private lemma firstRejoinVertex_spec [DecidableEq α] (a : α) (p q : SimplePath α) +lemma firstRejoinVertex_spec [DecidableEq α] (a : α) (p q : SimplePath α) (hpa : p.head = a) (hqa : q.head = a) (hsecond : p.vertices.dropHead.head ≠ q.vertices.dropHead.head) (hwit : ∃ z ∈ p.vertices.toList, ¬(z = a ∨ z ∉ q.vertices)) : @@ -398,7 +403,7 @@ private lemma firstRejoinVertex_spec [DecidableEq α] (a : α) (p q : SimplePath · intro z hzP hzQ have hzQ' : z ∈ q.vertices := VertexSeq.prefixUntil_subset q.vertices b hbQ z hzQ have hzFirst := VertexSeq.eq_head_dropWhile_or_pred_of_mem_prefixUntil - p.vertices pred hwit (z := z) (by simpa [P, b, r, pred] using hzP) + p.vertices pred hwit (z := z) (by simpa [P, b, r, pred, firstRejoinVertex] using hzP) rcases hzFirst with hzb | hza | hznot · exact Or.inr (hzb.trans hPtail.symm) · exact Or.inl (hza.trans hPhead.symm) @@ -411,14 +416,14 @@ private lemma firstRejoinVertex_spec [DecidableEq α] (a : α) (p q : SimplePath ((VertexSeq.head_dropHead_prefixUntil_of_length_one p.vertices b hbP hP1).trans (VertexSeq.head_dropHead_prefixUntil_of_length_one q.vertices b hbQ hQ1).symm) -private lemma firstRejoinVertex_mem_left [DecidableEq α] (a : α) +lemma firstRejoinVertex_mem_left [DecidableEq α] (a : α) (p q : SimplePath α) (hwit : ∃ z ∈ p.vertices.toList, ¬(z = a ∨ z ∉ q.vertices)) : firstRejoinVertex a p q hwit ∈ p.vertices := by exact VertexSeq.dropWhile_subset p.vertices (fun z => z = a ∨ z ∉ q.vertices) hwit _ (VertexSeq.head_mem _) -private lemma firstRejoinVertex_mem_right [DecidableEq α] (a : α) +lemma firstRejoinVertex_mem_right [DecidableEq α] (a : α) (p q : SimplePath α) (hwit : ∃ z ∈ p.vertices.toList, ¬(z = a ∨ z ∉ q.vertices)) : firstRejoinVertex a p q hwit ∈ q.vertices := by @@ -427,13 +432,13 @@ private lemma firstRejoinVertex_mem_right [DecidableEq α] (a : α) by_contra h exact hnot (Or.inr h) -private structure OfTwoPathsData (p q : SimplePath α) where +structure OfTwoPathsData (p q : SimplePath α) where cycle : SimpleCycle α length_le : cycle.length ≤ p.length + q.length head_mem_left : cycle.head ∈ p.vertices edges_subset : ∀ e ∈ cycle.edges, e ∈ p.edges ∨ e ∈ q.edges -private def buildOfTwoPaths [DecidableEq α] (p q : SimplePath α) +def buildOfTwoPaths [DecidableEq α] (p q : SimplePath α) (hhead : p.head = q.head) (htail : p.tail = q.tail) (hne : p.vertices ≠ q.vertices) : OfTwoPathsData p q := by let a := divergenceVertex p q hhead @@ -522,14 +527,14 @@ lemma edges_ofTwoPaths_subset [DecidableEq α] (p q : SimplePath α) /-! ## reroot -/ /-- The suffix rooted at a cycle vertex can be glued to the preceding prefix. -/ -private lemma tail_suffixFrom_eq_head_prefixUntil [DecidableEq α] (c : SimpleCycle α) +lemma tail_suffixFrom_eq_head_prefixUntil [DecidableEq α] (c : SimpleCycle α) (u : α) (hu : u ∈ vertices c) : (c.val.suffixFrom u hu).val.tail = (c.val.prefixUntil u hu).val.head := by simpa using (closed c).symm /-- Re-rooting the underlying walk of a simple cycle at a non-head vertex preserves the cycle property. -/ -private lemma isCycle_reroot_glue [DecidableEq α] (c : SimpleCycle α) (u : α) +lemma isCycle_reroot_glue [DecidableEq α] (c : SimpleCycle α) (u : α) (hu : u ∈ vertices c) (hhead : u ≠ head c) : SimpleWalk.IsCycle ((c.val.suffixFrom u hu).glue (c.val.prefixUntil u hu) diff --git a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/Bipartite.lean b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/Bipartite.lean index 2e2b884..cdb355d 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/Bipartite.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/Bipartite.lean @@ -3,8 +3,10 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.InSimpleGraph -import Mathlib.Algebra.Group.Nat.Even +module + +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph +public import Mathlib.Algebra.Group.Nat.Even /-! # Bipartite simple graphs @@ -42,6 +44,8 @@ corollaries of it, and live in the `IsBipartite` namespace because that is the predicate they assume. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/Girth.lean b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/Girth.lean index d154457..01b507b 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/Girth.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/Girth.lean @@ -3,11 +3,13 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Degree -import AlgoLib.Theory.Graph.Structures.InSimpleGraph -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Bipartite -import Mathlib.Data.ENat.Lattice -import Mathlib.Data.Set.Card +module + +public import AlgoLib.Theory.Graph.Degree +public import AlgoLib.Theory.Graph.Structures.InSimpleGraph +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Bipartite +public import Mathlib.Data.ENat.Lattice +public import Mathlib.Data.Set.Card /-! # Girth @@ -42,6 +44,8 @@ automatically, and the infimum API (`le_iInf`, `iInf₂_le`) drives the basic lemmas below; see `girth.ge_iff` for the workhorse characterization. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound.lean b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound.lean index cd303a3..64d82f8 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound.lean @@ -3,11 +3,13 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Counting -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Core -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.RootedLayers -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.HalfLayers -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Bounds +module + +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Counting +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Core +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.RootedLayers +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.HalfLayers +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Bounds /-! # Moore bounds for simple graphs diff --git a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Bounds.lean b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Bounds.lean index 6f74bcc..3e59e53 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Bounds.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Bounds.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.HalfLayers +module + +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.HalfLayers /-! # The Moore bounds @@ -13,6 +15,8 @@ files of the `MooreBound` folder; see the umbrella module `AlgoLib.Theory.Structures.SimpleGraph_only.MooreBound`. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Core.lean b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Core.lean index 19dc557..2cf4060 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Core.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Core.lean @@ -3,8 +3,10 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Girth -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Counting +module + +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Girth +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Counting /-! # Moore bounds: fresh neighbours and the shared counting core @@ -18,6 +20,8 @@ Part of the `MooreBound` folder; see the umbrella module `AlgoLib.Theory.Structures.SimpleGraph_only.MooreBound`. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib diff --git a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Counting.lean b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Counting.lean index dd61e4a..70e0159 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Counting.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/Counting.lean @@ -3,11 +3,13 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Weixuan Yuan -/ -import Mathlib.Algebra.BigOperators.Group.Finset.Basic -import Mathlib.Algebra.Order.BigOperators.Group.Finset -import Mathlib.Algebra.BigOperators.Ring.Finset -import Mathlib.Algebra.BigOperators.Finprod -import Mathlib.Data.Set.Card.Arithmetic +module + +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Algebra.Order.BigOperators.Group.Finset +public import Mathlib.Algebra.BigOperators.Ring.Finset +public import Mathlib.Algebra.BigOperators.Finprod +public import Mathlib.Data.Set.Card.Arithmetic /-! # Counting lemmas for the Moore bounds @@ -24,6 +26,8 @@ so that the graph development can stay free of ad-hoc cardinality reasoning. elements of `N`, and distinct elements own disjoint sets, then `k * |L| ≤ |N|`. -/ +@[expose] public section + namespace Set lemma ncard_biUnion_finset_eq_sum {ι β : Type*} (s : Finset ι) diff --git a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/HalfLayers.lean b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/HalfLayers.lean index d2dc177..8ec1a4a 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/HalfLayers.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/HalfLayers.lean @@ -3,7 +3,11 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.RootedLayers +module + +import Mathlib.Tactic.NormNum + +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.RootedLayers /-! # Moore bounds: the half-layers around a central edge @@ -16,6 +20,8 @@ Part of the `MooreBound` folder; see the umbrella module `AlgoLib.Theory.Structures.SimpleGraph_only.MooreBound`. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib @@ -224,7 +230,8 @@ lemma mul_ncard_halfLayer_le_succ_of_lt_girth (G : SimpleGraph α) intro v hv simp only [hFdef, dif_pos hv] have hgirth' : (2 * (((i + 1 : ℕ) : ℕ∞) + 1)) < G.girth := by - push_cast; convert hgirth using 2 + convert hgirth using 2 + norm_num [Nat.cast_add, add_assoc] refine Set.mul_ncard_le_ncard_of_children (F := F) hLfin hNfin ?_ ?_ ?_ · -- children lie in the next half-layer: a child cannot be the banned endpoint, -- since that would close a cycle shorter than the girth diff --git a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/RootedLayers.lean b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/RootedLayers.lean index 9543c63..668f0a8 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/RootedLayers.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleGraph_only/MooreBound/RootedLayers.lean @@ -3,7 +3,11 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Core +module + +import Mathlib.Tactic.NormNum + +public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Core /-! # Moore bounds: the rooted layers @@ -17,6 +21,8 @@ Part of the `MooreBound` folder; see the umbrella module `AlgoLib.Theory.Structures.SimpleGraph_only.MooreBound`. -/ +@[expose] public section + variable {α : Type*} namespace AlgoLib @@ -185,7 +191,8 @@ lemma mul_ncard_rootLayer_le_succ_of_lt_girth (G : SimpleGraph α) F v = freshNeighborSet G hv.path := by intro v hv; simp only [hFdef, dif_pos hv] have hgirth' : (2 * (((i + 1 : ℕ) : ℕ∞) + 1)) < G.girth := by - push_cast; convert hgirth using 2 + convert hgirth using 2 + norm_num [Nat.cast_add, add_assoc] refine Set.mul_ncard_le_ncard_of_children (F := F) hLfin hNfin ?_ ?_ ?_ · -- children lie in the next layer intro v hv u hu @@ -232,7 +239,8 @@ lemma le_ncard_rootLayer_succ (G : SimpleGraph α) (hV : V(G).Finite) have hprev : δ * (δ - 1) ^ i ≤ (rootLayer G x (i + 1)).ncard := ih hgirthPrev have hgirthGrowth : (2 * (i + 2) : ℕ∞) < G.girth := by - simpa [Nat.add_assoc] using hgirth + convert hgirth using 2 + norm_num [Nat.cast_add, add_assoc] have hgrowth := mul_ncard_rootLayer_le_succ_of_lt_girth G hV (δ := δ) (i := i) (x := x) hmin hgirthGrowth diff --git a/AlgoLib/Theory/Graph/Structures/SimplePath.lean b/AlgoLib/Theory/Graph/Structures/SimplePath.lean index 219add5..a2a3d81 100644 --- a/AlgoLib/Theory/Graph/Structures/SimplePath.lean +++ b/AlgoLib/Theory/Graph/Structures/SimplePath.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.SimpleWalk +module + +public import AlgoLib.Theory.Graph.Structures.SimpleWalk /-! # Simple paths @@ -29,6 +31,8 @@ where a simple walk is expected. Every operation is the `SimpleWalk` one plus a proof that `nodup` survives. -/ +@[expose] public section + variable {α : Type*} namespace SimpleWalk diff --git a/AlgoLib/Theory/Graph/Structures/SimpleWalk.lean b/AlgoLib/Theory/Graph/Structures/SimpleWalk.lean index 4406646..504a241 100644 --- a/AlgoLib/Theory/Graph/Structures/SimpleWalk.lean +++ b/AlgoLib/Theory/Graph/Structures/SimpleWalk.lean @@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan, Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Basic -import AlgoLib.Theory.Graph.Structures.VertexSeq +module + +public import AlgoLib.Theory.Graph.Basic +public import AlgoLib.Theory.Graph.Structures.VertexSeq /-! # Simple walks @@ -31,10 +33,12 @@ Every operation is the `VertexSeq` one plus a proof that non-stalling survives, and every lemma below is a thin wrapper around its `VertexSeq` counterpart. -/ +@[expose] public section + variable {α : Type*} /-- A simple walk: a `VertexSeq` with no two consecutive vertices equal. -/ -def SimpleWalk (α : Type*) := { w : VertexSeq α // w.nonstalling } +abbrev SimpleWalk (α : Type*) := { w : VertexSeq α // w.nonstalling } -- `VertexSeq.edges` and `VertexSeq.arcs` (the traversed edges/arcs) live in -- `VertexSeq/Edges.lean`, since they are purely combinatorial. diff --git a/AlgoLib/Theory/Graph/Structures/Trail.lean b/AlgoLib/Theory/Graph/Structures/Trail.lean index e69de29..0cca093 100644 --- a/AlgoLib/Theory/Graph/Structures/Trail.lean +++ b/AlgoLib/Theory/Graph/Structures/Trail.lean @@ -0,0 +1 @@ +module diff --git a/AlgoLib/Theory/Graph/Structures/Tree.lean b/AlgoLib/Theory/Graph/Structures/Tree.lean index ccf19e4..dd30778 100644 --- a/AlgoLib/Theory/Graph/Structures/Tree.lean +++ b/AlgoLib/Theory/Graph/Structures/Tree.lean @@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan, Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Connectivity.Reachable -import AlgoLib.Theory.Graph.Structures.Forest +module + +public import AlgoLib.Theory.Graph.Connectivity.Reachable +public import AlgoLib.Theory.Graph.Structures.Forest /-! # Trees @@ -27,6 +29,8 @@ carried a second, standalone definition of `IsConnected` phrased over the now-re there is a single notion of connectedness in the library. -/ +@[expose] public section + open AlgoLib variable {α : Type*} diff --git a/AlgoLib/Theory/Graph/Structures/Trees/Basic.lean b/AlgoLib/Theory/Graph/Structures/Trees/Basic.lean index 8b13789..0cca093 100644 --- a/AlgoLib/Theory/Graph/Structures/Trees/Basic.lean +++ b/AlgoLib/Theory/Graph/Structures/Trees/Basic.lean @@ -1 +1 @@ - +module diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq.lean index 3cf98fc..47538fe 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq.lean @@ -3,15 +3,17 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic -import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates -import AlgoLib.Theory.Graph.Structures.VertexSeq.Append -import AlgoLib.Theory.Graph.Structures.VertexSeq.MapZip -import AlgoLib.Theory.Graph.Structures.VertexSeq.Subseq -import AlgoLib.Theory.Graph.Structures.VertexSeq.Erase -import AlgoLib.Theory.Graph.Structures.VertexSeq.Edges -import AlgoLib.Theory.Graph.Structures.VertexSeq.Index -import AlgoLib.Theory.Graph.Structures.VertexSeq.CommonPrefix +module + +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Append +public import AlgoLib.Theory.Graph.Structures.VertexSeq.MapZip +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Subseq +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Erase +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Edges +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Index +public import AlgoLib.Theory.Graph.Structures.VertexSeq.CommonPrefix /-! # Vertex sequences diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq/Append.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq/Append.lean index 1bdaaea..367508f 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq/Append.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq/Append.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates +module + +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates /-! # Vertex sequences: append and reverse @@ -18,6 +20,8 @@ laws, associativity and involutivity, and the preservation of `nodup` and * `VertexSeq.reverse` — reversal, swapping head and tail. -/ +@[expose] public section + variable {α : Type*} namespace VertexSeq diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq/Basic.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq/Basic.lean index 5e0d04f..f1bd66d 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq/Basic.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq/Basic.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import Mathlib.Data.List.Basic +module + +public import Mathlib.Data.List.Basic /-! # Vertex sequences: carrier and basic accessors @@ -25,6 +27,8 @@ instances, and the endpoint-dropping operations `dropHead`/`dropTail`. * `VertexSeq.dropHead`, `VertexSeq.dropTail` — drop the first or last vertex. -/ +@[expose] public section + variable {α : Type*} /-- A type that admits a right-extension operation. -/ diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq/CommonPrefix.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq/CommonPrefix.lean index 4e8f25a..e977759 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq/CommonPrefix.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq/CommonPrefix.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import Mathlib.Data.List.Basic +module + +public import Mathlib.Data.List.Basic /-! # Longest common prefix of two lists @@ -28,6 +30,8 @@ The file lives under `VertexSeq/` only because the library has no general-purpos entries after the cut differ. -/ +@[expose] public section + variable {α : Type*} namespace List diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq/Edges.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq/Edges.lean index 56b01d5..e5eb487 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq/Edges.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq/Edges.lean @@ -3,8 +3,10 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import Mathlib.Data.Sym.Sym2 -import AlgoLib.Theory.Graph.Structures.VertexSeq.Erase +module + +public import Mathlib.Data.Sym.Sym2 +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Erase /-! # Vertex sequences: traversed edges and arcs @@ -25,6 +27,8 @@ multiplicity are retained (needed for trails/Eulerian walks), and a graph's * `VertexSeq.arcs` — the list of directed arcs traversed. -/ +@[expose] public section + variable {α : Type*} namespace VertexSeq diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq/Erase.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq/Erase.lean index e97998b..18c4be4 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq/Erase.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq/Erase.lean @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan, Huang.JiangYi (co/ Claude Opus 5) -/ -import AlgoLib.Theory.Graph.Structures.VertexSeq.Subseq +module + +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Subseq /-! # Vertex sequences: erasure operations @@ -21,6 +23,8 @@ Two ways to remove redundancy from a vertex sequence: * `VertexSeq.loopErase`, `VertexSeq.cycleErase`. -/ +@[expose] public section + variable {α : Type*} namespace VertexSeq diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq/Index.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq/Index.lean index eba27d6..545c1c4 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq/Index.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq/Index.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic +module + +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic /-! # Vertex sequences: indexing and insertion @@ -20,6 +22,8 @@ of a vertex at a given index. one positional *editing* operation the carrier is expected to offer. -/ +@[expose] public section + variable {α : Type*} namespace VertexSeq diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq/MapZip.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq/MapZip.lean index 1fa2941..a19ac48 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq/MapZip.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq/MapZip.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates +module + +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates /-! # Vertex sequences: map, fold, zip @@ -24,6 +26,8 @@ a colouring pass) reaches for first. * `VertexSeq.any`, `VertexSeq.all` — existential/universal predicates. -/ +@[expose] public section + variable {α : Type*} namespace VertexSeq diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq/Predicates.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq/Predicates.lean index 81fb850..eb05aba 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq/Predicates.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq/Predicates.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic +module + +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic /-! # Vertex sequences: structural predicates @@ -24,6 +26,8 @@ operations in their own files. * `VertexSeq.nodup`, `VertexSeq.nonstalling`, `VertexSeq.closed`. -/ +@[expose] public section + variable {α : Type*} namespace VertexSeq diff --git a/AlgoLib/Theory/Graph/Structures/VertexSeq/Subseq.lean b/AlgoLib/Theory/Graph/Structures/VertexSeq/Subseq.lean index 59867c5..9e0d84d 100644 --- a/AlgoLib/Theory/Graph/Structures/VertexSeq/Subseq.lean +++ b/AlgoLib/Theory/Graph/Structures/VertexSeq/Subseq.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan -/ -import AlgoLib.Theory.Graph.Structures.VertexSeq.Append +module + +public import AlgoLib.Theory.Graph.Structures.VertexSeq.Append /-! # Vertex sequences: subsequence operations @@ -21,6 +23,8 @@ with their head/tail/length/subset laws and the preservation of `nodup` and * `VertexSeq.splitAt` — split into pieces at every occurrence of a vertex. -/ +@[expose] public section + variable {α : Type*} namespace VertexSeq diff --git a/AlgoLib/Theory/Graph/Structures/Walk.lean b/AlgoLib/Theory/Graph/Structures/Walk.lean index 1cf14b9..e6d41a3 100644 --- a/AlgoLib/Theory/Graph/Structures/Walk.lean +++ b/AlgoLib/Theory/Graph/Structures/Walk.lean @@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan, Huang.JiangYi (co/ Claude Opus 5) -/ -import Mathlib.Data.Sym.Sym2 -import AlgoLib.Theory.Graph.Basic -import AlgoLib.Theory.Graph.Structures.VertexSeq +module + +public import Mathlib.Data.Sym.Sym2 +public import AlgoLib.Theory.Graph.Basic +public import AlgoLib.Theory.Graph.Structures.VertexSeq /-! # Walks @@ -20,6 +22,8 @@ This file mirrors the API of `VertexSeq` lemma-for-lemma, with the additional edge list `toEdgeList` and edge-aware membership. -/ +@[expose] public section + variable {α ε : Type*} /-- A non-empty inductive sequence of vertices interleaved with edges. diff --git a/AlgoLib/Theory/Graph/Subgraph.lean b/AlgoLib/Theory/Graph/Subgraph.lean index f2f6a57..2ead0c2 100644 --- a/AlgoLib/Theory/Graph/Subgraph.lean +++ b/AlgoLib/Theory/Graph/Subgraph.lean @@ -3,7 +3,9 @@ Copyright (c) 2026 Basil Rohner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Basil Rohner, Sorrachai Yingchareonthawornchai -/ -import AlgoLib.Theory.Graph.Basic +module + +public import AlgoLib.Theory.Graph.Basic /-! # Subgraphs and induced subgraphs @@ -49,6 +51,8 @@ with a subgraph predicate and an induced-subgraph constructor. `G`; no separate looplessness obligation appears. -/ +@[expose] public section + namespace AlgoLib variable {α β : Type*} diff --git a/AlgoLib/Util/Decidable.lean b/AlgoLib/Util/Decidable.lean index 163abe2..d2c09cf 100644 --- a/AlgoLib/Util/Decidable.lean +++ b/AlgoLib/Util/Decidable.lean @@ -3,9 +3,11 @@ Copyright (c) 2026 GraphLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ -import Mathlib.Data.Sym.Sym2 -import Mathlib.Data.Set.Finite.Basic -import Mathlib.Data.Fintype.Sets +module + +public import Mathlib.Data.Sym.Sym2 +public import Mathlib.Data.Set.Finite.Basic +public import Mathlib.Data.Fintype.Sets /-! # Decidability helpers for `Sym2` and `Set` @@ -32,6 +34,8 @@ candidates for upstreaming. instance actually evaluates: `Set.toFinset` needs only `[Fintype ↥s]` and computes. -/ +@[expose] public section + variable {α : Type*} /-! ## `Sym2` -/ diff --git a/AlgoLib/Util/Finset.lean b/AlgoLib/Util/Finset.lean index afb22a2..c84f4be 100644 --- a/AlgoLib/Util/Finset.lean +++ b/AlgoLib/Util/Finset.lean @@ -3,10 +3,12 @@ Copyright (c) 2026 GraphLib working group. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Huang.JiangYi (co/ Claude Opus 5) -/ -import Mathlib.Data.Finset.Powerset -import Mathlib.Data.Set.Card -import Mathlib.Data.ENat.Lattice -import AlgoLib.Util.Decidable +module + +public import Mathlib.Data.Finset.Powerset +public import Mathlib.Data.Set.Card +public import Mathlib.Data.ENat.Lattice +public import AlgoLib.Util.Decidable /-! # Finite iteration and bounded infima @@ -52,6 +54,8 @@ once here rather than four times over in the connectivity development. visible at every call site. -/ +@[expose] public section + variable {β : Type*} namespace Finset diff --git a/README.md b/README.md index ba399af..9f75602 100644 --- a/README.md +++ b/README.md @@ -18,11 +18,18 @@ Install [Lean and its editor support](https://lean-lang.org/install/) and [Git](https://git-scm.com/downloads). The Lean installation includes `elan`, the toolchain manager, and `lake`, the build tool and package manager. +To start a new project with the supported Lean version: + +```sh +lake +leanprover/lean4:v4.35.0 new my_algolib_project lib +cd my_algolib_project +``` + Use the Lean version specified by AlgoLib's [`lean-toolchain`](lean-toolchain) at the revision you depend on. The current version is: ```text -leanprover/lean4:v4.30.0-rc2 +leanprover/lean4:v4.35.0 ``` For an existing project, its `lean-toolchain` must match this version, and any @@ -59,13 +66,17 @@ lake exe cache get ``` The cache command downloads precompiled Mathlib dependencies to reduce the first -build's work. AlgoLib's dependencies are fetched automatically. +build's work. AlgoLib's dependencies are fetched automatically, including Mathlib +and CSLib pinned to `v4.35.0`. ### Import and build -Import the modules you need in your Lean files. For example: +AlgoLib uses Lean's module system. A new Lean file can import the modules it +needs as follows: ```lean +module + import AlgoLib.Theory.Graph.Basic #check AlgoLib.Graph @@ -76,6 +87,8 @@ import AlgoLib.Theory.Graph.Basic You can also import the modules collected in the library's root file with: ```lean +module + import AlgoLib ``` @@ -97,6 +110,17 @@ reproducible project, replace `main` with the full commit hash of a revision you have tested, and commit the generated `lake-manifest.json`. Use the `lean-toolchain` from that same AlgoLib revision. +### Upgrading an existing project + +Set your project's `lean-toolchain` to `leanprover/lean4:v4.35.0`, then run the +dependency and build commands above. If you require Mathlib or CSLib directly, +align those requirements with their `v4.35.0` releases. + +Mathlib renamed `Tree` to `BinaryTree`. AlgoLib's binary-tree API now uses the +`BinaryTree` namespace too: update `Tree α`, `open Tree`, and qualified names +such as `Tree.num_nodes` to `BinaryTree α`, `open BinaryTree`, and +`BinaryTree.num_nodes`. The module import paths are unchanged. + ## Building AlgoLib locally To work on AlgoLib itself, clone the repository and build it: diff --git a/lake-manifest.json b/lake-manifest.json index b7b3234..b61c0d2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,14 +1,14 @@ -{"version": "1.2.0", +{"version": "1.3.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d802ffd29db1f5dc5a29206b1a8af62bfcc234a3", + "rev": "56a005855ea17e0b0958f73ec801ae140b0a1679", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.35.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls", @@ -18,24 +18,24 @@ "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", "name": "checkdecls", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/cslib", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "608cbe1b629a276abd3f2081f9b42dc766d8fd78", + "rev": "5b56df99362532c46e1175381fbbdd755bd56030", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.35.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "293af9b2a383eed4d04d66b898d608d0a44b750f", + "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef", + "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,50 +65,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", + "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.98", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", + "rev": "4a174c490d8707121c4a9290800489f105d85e07", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", + "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.35.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "AlgoLib", diff --git a/lakefile.toml b/lakefile.toml index d41ec61..7044a63 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -14,16 +14,18 @@ maxSynthPendingDepth = 3 [[require]] name = "cslib" scope = "leanprover" +rev = "v4.35.0" [[require]] name = "checkdecls" scope = "PatrickMassot" -rev = "master" +rev = "3d425859e73fcfbef85b9638c2a91708ef4a22d4" [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.30.0-rc2" +rev = "v4.35.0" [[lean_lib]] name = "AlgoLib" +requiresModuleSystem = true diff --git a/lean-toolchain b/lean-toolchain index 635bb95..a6aff06 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc2 \ No newline at end of file +leanprover/lean4:v4.35.0 diff --git a/tests/Import.lean b/tests/Import.lean new file mode 100644 index 0000000..9438456 --- /dev/null +++ b/tests/Import.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2026 AlgoLib contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ + +module + +import AlgoLib + +/-! Check that a module-system consumer can use the public graph and tree APIs. -/ + +example : Type := AlgoLib.Graph Nat Unit + +example : Type := AlgoLib.SimpleGraph Nat + +example (G : AlgoLib.SimpleDiGraph Nat) [Fintype G.vertexSet] + [DecidablePred (· ∈ G.edgeSet)] (s : Nat) : Finset Nat := + G.bfsReachableFinset s + +example (t : BinaryTree Nat) (q : Nat) : (SplayTree.splay t q).num_nodes = t.num_nodes := + SplayTree.num_nodes_splay t q