Query model example - #75
Open
felipponn wants to merge 20 commits into
Open
Conversation
Add a self-contained query model (free monad `Prog` + `Model` + `eval`) as an alternative to `TimeM` for measuring algorithm complexity, so the two approaches can be compared in practice. The query model of query-model-tutorial.md lives in CSLib PR #372, which is still open and not present at the pinned cslib revision, so it is vendored here as `Fad.QueryModel`: - `Prog Q R`: a program as a tree of queries (a free monad); cost is assigned afterwards by a `Model`, never carried by the algorithm (no cheating). - `Model.evalQuery`/`Model.cost`, `Prog.eval : Prog Q R → Model Q Cost → R × Cost`. - `eval_bind`/`runtime_bind`/`result_bind`: the query-model analogues of `TimeM.time_of_bind`/`ret_bind`, driving the complexity proofs. - `UpperBound`/`LowerBound` predicates. `Fad.Chapter2Query` reimplements the running-time examples of `Fad.Chapter2` (`append`, `concat₁`, `concat₂`) in the query model, with the analogous complexity theorems (`concat₁_runtime`: Θ(m·n); `concat₂_runtime`: Θ(m²·n)), and `#eval`s that measure the same program under several cost models — the thing `TimeM` cannot do without rewriting the algorithm. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AbkMyCwYRAiUy3NFwn9M4f
Under the current Lean/Mathlib toolchain, `simp only [..., decide_eq_true_eq, <proj-lemmas>]` no longer strips `decide P = true` to `P` when projection rfl-lemmas (`residue`/`count`/`value_add`/`weight_add`) are unfolded in the same call: `decide_eq_true_eq` is reported unused and the goal stays wrapped in `decide (…) = true`, so the following `constructor` / `calc` / `⟨_, _⟩` steps fail (no `And` constructor; `calc` type mismatch; `Eq.refl` given 2 fields). Fix: strip the `decide` in its own `simp only [_, decide_eq_true_eq]` pass first, then unfold the projections in a second step. Three sites across the two `key_fact` theorems (coin-change and knapsack). No statements changed; the whole `Fad` library builds again (8696 jobs, 0 errors). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AbkMyCwYRAiUy3NFwn9M4f
…red copy Replace the self-contained Fad/QueryModel.lean with the real query-complexity framework from CSLib PR leanprover/cslib#401 (kim-em:combined-query-complexity): FreeM-based programs with eval / cost / queriesOn interpreters and the UpperBound/LowerBound predicates. - lakefile.toml: point cslib at the PR branch (pinned rev 391cab00) - lean-toolchain: v4.33.0-rc1 -> v4.30.0-rc2 (required by that cslib/mathlib pin) - lake-manifest.json: regenerated for the new pins - Fad/QueryModel.lean: removed (no longer vendored) - Fad/Chapter2-Query.lean: rewritten against the FreeM API (append, concat1, concat2); same programs measured under a fixed oracle with varying weights - Fad/Chapter2-Amortized.lean: new — binary counter showing amortized O(1) via the potential method (Phi = number of 1-bits), a natural fit for queriesOn - Fad/Chapter3.lean: List.toAssocList' (top-level in v4.30, was Lean.List.* in v4.33) — collateral fix for the toolchain downgrade Full `lake build` green (8347 jobs); remaining warnings are pre-existing sorries. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AbkMyCwYRAiUy3NFwn9M4f
Second amortized example alongside the binary counter, mirroring the book's "two examples" of §2.4. `build p = foldr insert []` with `insert x xs = x : dropWhile (p x) xs`, formalized in the query model with the predicate `p x y` as the cost-bearing query. Uses the book's uniform potential method (eq. 2.3) in subtraction-free form: S = length, A = 2, proving the *inequality* C + S(after) <= S(before) + 2 per step (contrast the counter's exact equality) and telescoping to the O(n) total bound `build_queriesOn_le : (build xs).queriesOn o <= 2 * xs.length`. Includes the book's own example verbatim: `build (==) [4,4,2,1,1,2,5] = [4,2,1,2,5]` (8 predicate evals, bound 14). Full `lake build` green (8347 jobs). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AbkMyCwYRAiUy3NFwn9M4f
Member
|
This PR needs to be split; I can't accept it as-is. It should not include the commits from #69. Here, we will include only the Chapter02 examples using the query model from leanprover/cslib#401 |
Contributor
|
why not leanprover/cslib#685? It is both the origin of the idea and the right way to justify using query models. Also the code needs to be licensed properly. For Apache 2.0 code this means pasting the original copyright notice. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This pull request adds a new file,
Chapter2-Amortized.lean, with a formal amortized analysis of a binary counter in the query model, and updates imports accordingly.These changes collectively provide a framework for reasoning about and measuring computational cost in Lean, and demonstrate its application to classic algorithms and amortized analysis.