While loop - #184
Draft
crei wants to merge 24 commits into
Draft
While loop#184crei wants to merge 24 commits into
crei wants to merge 24 commits into
Conversation
Bump `mathlib` dependency to [e06eff5](leanprover-community/mathlib4@e06eff5): chore(Data): move some files to Basic (#43176) (2026-08-31) Previously at: [0fa18d4](leanprover-community/mathlib4@0fa18d4): refactor: change the default value of `Measure.map` to a Dirac mass (#42322) (2026-08-26) Closes leanprover#847 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/33406502145/artifacts/9763801315) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`e06eff5`) so you can reproduce and fix the incompatibility locally by checking out this branch. _Opened automatically by [downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports) via [this workflow run](https://github.com/leanprover/cslib/actions/runs/33434556067)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Document a couple of heavy `grind` uses flagged by [the weekly `mergeWithGrind` report](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Weekly.20linting.20log/near/620201866).
Drop an `obtain` that the following `grind` does not need, as flagged by [the weekly `mergeWithGrind` report](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Weekly.20linting.20log/near/620201866).
…eanprover#851) Golf a heavy proof that was recently flagged as such (in leanprover#850) by splitting `all_goals` into bullets and doing the work.
Restructure the complexity definitions and add the scaffolding for the loop combinators of multi-tape Turing machines. Deterministic.lean: * rework the hierarchy of computability definitions into three layers: `ComputesFunInTimeAndSpace` (behaviour of a given machine, generic alphabet), `ComputableInTimeAndSpace` (existence of a finite machine over `Bool`) and `ComputableInTimeAndSpaceOfLength` (bounds depending only on the input length), with all bounds depending on the input rather than on its length * add `Function.Embedding.listMap`, the `mono` lemmas and `ComputableInTimeAndSpace.congr`, which reads a computation as a computation of a different function at different encodings Combinators: * `Loop`: the loop with a fused body `α → Option α`, its partial function `loopFunction` and the statement of its complexity * `While`: the loop with an explicit condition, characterised by `WhileRel` and by the iterates of its body, with its complexity derived from the loop by fusing the condition into the body * `Ite`, `Comp`: the complexity of a conditional and of a composition Encodings: * requirements on encodings instead of fixed encodings, starting with `IsOptionEncoding` and the canonical `encOption` Plumbing: * the machine-level constructions the combinators are built from: sequential composition (proved), running a machine on other tapes, the clean-halting normal form, tape contents and redirecting the input and output of a machine to work tapes The constructions themselves are still missing; the files state their results as `proof_wanted` and both new directories have a README describing the plan. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Prove `computableInTimeAndSpace_loopFunction` modulo the plumbing, which is
stated as `sorry`ed theorems. `Loop.lean` itself contains no `sorry`.
`proof_wanted` emits a private declaration and its `❰…❱` reference syntax
resolves only within one file, so the plumbing results a combinator builds on
have to be real declarations. The ones the loop needs are therefore stated as
theorems with a `sorry` body; `lake build --wfail` fails on them until they are
filled in.
Words.lean (new): the interface the combinators use.
* `TapesHold` and `TransformsTapes`: `TransformsCfg` restricted to
configurations in which every work tape holds a word, with the input head
normalised to position `1` and the output preserved. Untouched tapes are
described by the postcondition rather than by a set of tape indices, so
`Cfg.AgreesOutside` never appears in a combinator.
* scratch tapes are hidden behind `∃ m c, ∀ k i o keep, …`, so a caller names
an input tape, an output tape and the tapes to keep, and never an embedding.
* `exists_transformsTapes_repeat`: the loop-back that `seq` cannot express.
`seq` sends the halting state of one machine to the initial state of the
*next* one; a loop sends it back to the initial state of the *same* one.
This was missing from the plan and is the only reason the loop combinator
needs the machine level at all.
* `exists_transformsTapes_branch` is family-indexed. Since the bounds of
`TransformsCfg` are numbers, a specification whose bounds depend on the input
is a family over one fixed machine, which the unindexed `exists_branchOnTape`
cannot provide.
* `exists_transformsTapes_ofComputable` and its input-tape variant fold together
the clean normal form, `onTape` and `liftTapes`.
Loop:
* `mem_loopFunction_iff` and the lemmas on `loopIterate` it rests on, relating
the function the loop computes to the iterates the machine runs through
(proved, and free of `sorry`).
* `computableInTimeAndSpace_loopFunction`: the machine copies its input onto
`T1`, runs the body into `T3`, and then repeats "compute the flag on `T4`;
either stop or clear `T4`, clear `T1`, destruct `T3` onto `T1`, clear `T3`
and run the body again", finally emitting `T1`. The loop invariant is keyed
on the current value rather than on the round index, so one round is a single
`TransformsTapes` statement per input.
Deterministic:
* `length_output_runFrom_le` and `ComputableInTimeAndSpace.length_encOut_le`:
a machine emits at most one symbol per step. This is the only bound available
on the length of an intermediate result, since a machine can produce an output
much longer than the space it uses; the loop needs it to bound
`(encOpt (some x)).length`, which `hsize` does not bound.
Encodings/Option:
* `computableInTimeAndSpace_isNone` is proved: it is `Option.isNone` being
constant outside `{none}`.
Comp:
* `computableInTimeAndSpace_id`, the streaming copy, used to move the input of
the loop onto a work tape.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`ite` is not primitive in Lean: `ite c t e` is `Decidable.casesOn`, the recursor
of the two-constructor inductive `Decidable c`, whose constructors carry only
proofs. `Prop` is erased, so the computational content of a conditional is
exactly the recursor of `Bool`, and the `Decidable` layer contributes nothing
beyond a computable Boolean test. `Combinators/Ite.lean` is restructured around
that primitive.
* `computableInTimeAndSpace_cond` is the primitive, the recursor of `Bool`. This
is the previous `computableInTimeAndSpace_ite` renamed; its statement is
unchanged, since its condition was already `α → Bool`.
* `computableInTimeAndSpace_ite` is now Lean's `ite`, for a decidable predicate,
and is derived from the primitive through `decide`. For a language the test it
asks for is `DecidableInTimeAndSpace`.
* `computableInTimeAndSpace_casesOn` is a `match` on a finite type, derived by
nesting the primitive once per constructor. Only the branch that is taken is
executed and the number of tests is a constant of the type, so the branches
contribute their supremum and the tests are absorbed into the constant factor.
* `computableInTimeAndSpace_match` is the same from a computable scrutinee,
which is the form to use: the tests come for free, since deciding which value
the scrutinee has is a function on a finite type and hence computable in
constant time.
Only `computableInTimeAndSpace_cond` remains a `sorry`; everything else in the
file is proved from it.
The module docstring records why this cannot be reduced to composition.
`cond` viewed as a function `Bool × β × β → β` is perfectly computable — it
reads a tag and streams out the component it selects — but
fun a => if c a then f a else g a = cond ∘ (fun a => (c a, f a, g a))
computes both branches. That costs `tf + tg` rather than `max tf tg`, stores
both encoded results on work tapes, and, worst, evaluates `2 ^ n` branches for
`n` nested conditionals instead of `n`. The content of a case analysis is that
the branch not taken is never run, and that laziness is not expressible by
composing total functions: the machine has to choose before it runs. So this is
a combinator with a machine-level branch behind it, not a consequence of
`computableInTimeAndSpace_comp`.
The docstring of `computableInTimeAndSpace_casesOn` also records where the
analogy stops: for a *recursive* inductive type the recursor is a fold, not a
case analysis, and its combinator is the loop of `Combinators/Loop.lean` with an
iteration bound.
`Comp`: `computableInTimeAndSpace_comp` becomes a `sorry`ed theorem, since
`computableInTimeAndSpace_match` composes the constructor test with the
scrutinee.
`CslibTests/Complexity/Combinators.lean`: worked examples of a conditional on a
decidable predicate and of a `match` on a three-constructor enumeration, the
latter needing nothing of the type beyond `Fintype`.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A non-recursive inductive type is a finite sum of finite products, so its constructors and its eliminator are the introduction rule of a finite product and the elimination rule of a finite coproduct. `Combinators/Ite.lean` is the second; this is the first. The two are built the same way, by nesting the binary case once per field resp. per constructor: * the eliminator nests `computableInTimeAndSpace_cond`, and the branches contribute their supremum, since only the branch that is taken runs; * the constructor nests `computableInTimeAndSpace_concat`, and the fields contribute their sum, since every field is computed. Combinators/Tuple.lean (new): * `computableInTimeAndSpace_flatten`: finitely many computations, concatenated. Proved by induction on the number of fields; the base case is `computableInTimeAndSpace_of_const`, since a constructor with no fields is a constant. * `computableInTimeAndSpace_ctor`: the same read as a constructor, for any encoding that is the concatenation of the encoded fields. The pair constructor is the two-field instance. Nothing is asked of the encoding beyond that syntactic factorisation. Building a value needs no computability assumption on its encoding, unlike taking one apart, which is why the destructors of a type are collected as requirements in `Encodings/` while the constructors are not. The arity has to be a constant of the type: each nesting costs one rewind of the input tape, so `k` fields cost `k` times the input length in time, which is absorbed into the existential constant only because `k` is fixed. A structure with a variable number of components is not a finite product and needs the loop with an iteration bound instead — the same boundary as for the eliminator, where a recursive type needs a fold rather than a case analysis. Combinators/Concat.lean (new): the concatenation of two computations, as a `sorry`ed theorem in the style of the other machine-level combinators on this branch, together with `computableInTimeAndSpace_pair` derived from it. It is proved against the plumbing of the `samschles/tm-04-rewind` chain, which is an independent development from the one here — the two share filenames for `Deterministic`, `Plumbing/Basic` and `Plumbing/Sequential` but differ by around a hundred lines in each, off a merge base five commits before either — so the proof cannot be carried over without merging the chains. Only the statement is duplicated, so the sorried file can be replaced wholesale once they meet. CslibTests/Complexity/Combinators.lean, worked examples on Lean's own types: * `Ordering`, for the `match` on a finite type, replacing an invented enumeration; * `Option.some` at the canonical `encOption` of `Encodings/Option.lean`, showing that a tagged constructor is built by treating the tag as a field computed by a constant function; * a subtype constructor, which costs nothing at all: the proof field is erased, so the encoding of the constructed value is the encoding of the data field and the constructor is a change of coordinates, `ComputableInTimeAndSpace.congr`, with no combinator involved; * a three-field heterogeneous tuple encoded flat rather than as nested pairs, which is where `computableInTimeAndSpace_flatten` is the form to use, since the index family of `computableInTimeAndSpace_ctor` is dependent and awkward to instantiate when the fields have different types. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`computableInTimeAndSpace_pair` assumed the encoding of a pair *is* the concatenation of the encoded components. That is a condition on the shape of the encoded string, of a different kind from the hypotheses of the eliminator, which are all of the form "this function is computable"; and it rules out interleaved, repackaged or otherwise non-concatenated layouts. Encodings/Pair.lean (new) replaces it with complexity requirements, at the bounds a machine can actually meet — linear time and constant space, i.e. by streaming with only the finite control: * `pack`: the components, one after the other, can be turned into the encoded pair; * `fst_computable`, `snd_computable`: the components can be read back. Zero space, which is what `Encodings/Option.lean` asks, is too strong here: a single tag bit can be dropped while streaming, but finding where a component ends may need the control to keep count. One field is not a complexity. `cat_injective` says the components laid out one after the other determine the pair. It is not a condition on the pair's encoding — it says nothing about it — but on the component encodings: the first has to be self-delimiting in front of the second. It is unavoidable, since without it "the components one after the other" is not an encoding and `pack` cannot be stated; and it is exactly what a parenthesis- or escape-based encoding is built to have. `computableInTimeAndSpace_pair_of_isPairEncoding` derives the pair from the requirements: run the two machines one after the other, which produces the components in order, then pack. The encoded components appear in both bounds because the concatenation is handed to the packing machine as its input and `computableInTimeAndSpace_comp` parks an intermediate result on a work tape; the shape-assuming `computableInTimeAndSpace_pair` avoids that step and keeps the sharper bounds, so both are kept, labelled. Producing and consuming stay asymmetric, and that is not an artifact: with a concatenation-style layout `pack` is free — a machine emitting the components in order has already produced the pair — while reading a component back is not, since the boundary has to be found. Concatenating is easier than parsing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`Shape` has only one constructor of arity two, so the tag never has to distinguish alternatives with the same payload shape. `Span` does: its two alternatives both carry two natural numbers and are told apart by the tag alone. * `span_ctor`: either alternative built from the tag and the two fields, the construction shared between them since only the tag and the constructor differ. * a function into `Span` that chooses between the alternatives, which is `computableInTimeAndSpace_cond` over two instances of that construction. Only the branch that is taken is built, so the field bounds appear once rather than twice. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`computableInTimeAndSpace_cond` was the sorried primitive and the finite case analysis was built from it by nesting once per constructor. That is the wrong way round. A machine does not nest: deciding among `n` cases is one machine reading a scrutinee of constant length and dispatching from its finite control, which is no harder than deciding among two. The nested construction therefore decomposed nothing — it replayed the same argument `n - 1` times, and since each replay multiplies the constants, the bounds had to be renormalised into a fixed shape at every step for the induction to go through. `computableInTimeAndSpace_match` is now the primitive, for a scrutinee in any finite type, and carries the `hagree` weakening. `cond`, `ite` and the new `dite` are its instances at `Bool`. The two forms are interderivable at constant cost — the tag gives every test by one composition with a function on a finite type, the tests give the tag by running all of them — so nothing is lost, and `computableInTimeAndSpace_casesOn`, which consumed per-case tests, is dropped rather than restated. The file loses the induction, the renormalisation, the empty-scrutinee case and the manufacturing of tests inside `_match`: 282 lines to 191, of which the arithmetic is now two `Finset.sup_le`s at `Bool`. `dite` is what the `hagree` weakening was for. Its branches are not functions of the input alone, so neither can be asked to be computable as it stands; what is asked instead is a computable total function agreeing with the branch where that branch is taken. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`computableInTimeAndSpace_match` took a bound for the scrutinee and a family of bounds for the branches, and concluded with their sum-of-suprema. Since those only ever appear added together in the conclusion, a single pair of bounds covering all of them says the same thing: given separate bounds, weaken each to their supremum and apply the collapsed form, and the old conclusion comes back verbatim. So the two are interderivable and `Finset.sup` leaves the statement. `Fintype ι` weakens to `Finite ι` with it, which is the honest hypothesis. `computableInTimeAndSpace_flatten` and `_ctor` collapse the same way, which also retires the claim that the eliminator's supremum and the constructor's sum were the interesting difference between them. They are not: the number of branches and the number of fields are both constants of the type, so sum and supremum differ by a constant factor, and an implementation running *every* branch would meet either bound. What does distinguish them is that no time bound appears in the case analysis' space bound — a machine computing all the branches has to park their encoded outputs on work tapes, and an output's length is bounded only by the time that produced it. The sum/supremum distinction becomes real only for a variable number of items, which is the loop. `flatten` loses its `key` helper entirely: with the bounds no longer indexed by the field, the induction runs directly on the statement. Also gone from the tests: the `Fin.sum_univ_*` and `Matrix.cons_val_*` normalisation at every call site, and with it the `Lean.Expr.appArg!` simproc panic that the three-field example was tripping. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`f` carries no information: it is `fun a => br (sel a) a` up to `funext`, and stating the conclusion for that function directly is equivalent. Keeping it costs a `fun _ => rfl` where the two agree definitionally, and saves the caller a `ComputableInTimeAndSpace.congr` where they do not — which is the case the combinator exists for, since a caller's goal is a `match` and not an application of the branch family. What made it look expensive was applying the theorem with `obtain`, where there is no expected type to infer `f` from and `hagree` fixes it to the wrong function. With `exact` or `refine` it is inferred, so the explicit `(f := …)` in `cond` and in the `Shape` example goes away and the latter drops from six lines to one. Said so in the docstring. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`Span` was only exercised on the constructor side, and the one eliminator example, on `Shape`, went as far as the tag and no further — so the case the `hagree` weakening exists for had never been checked. Two examples now do. `Span` is the easy half: both alternatives carry two naturals, so `Span.fst` and `Span.snd` are total and the branches read them with nothing invented. The destructuring is entirely in `hagree`, which is `rfl` once the scrutinee is case split, since the projections agree with the pattern variables by definition. `Shape` is the half that needs the weakening. Its arities are zero, one and two, so `Shape.r` has to return something on a `rect` and `Shape.w` on a `circle`, and the value is arbitrary. Each branch reads that junk nowhere, because it is only run where its own alternative holds; a combinator demanding the branches equal the `match` everywhere could not be applied at all. Both go through unchanged. What is left over in each is `hbr`, which asks that a branch be computable as a function of the input rather than of the payload — that is a computable destructor per field plus pairing, which are requirements on the encoding and not further combinators. One trap recorded in the docstring: the branch family has to be written `fun a => ![…] i` rather than `![…] i` with the input abstracted inside each entry. The two are equal by `funext`, but `cases` cannot generalise the scrutinee under a binder, and with the second spelling `hagree` is not `rfl`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The destructuring example carried an input type and a `sel : α → Span` in front of the match, which is a composition the theorem already handles and which the `Shape` examples already show. Taking the input to be `Span` leaves the eliminator of the type and nothing else: the branches take the payload rather than the input alongside it, and what the type has to supply is visible as two hypotheses — that the alternative can be read off the encoding, and that a branch is computable as a function of the value being matched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every inductive type comes with `ctorIdx`, generated from `casesOn`, which is exactly the hand-written tag: `Span.ctorIdx` is `fun x => Span.casesOn x (fun _ _ => 0) fun _ _ => 1`. It lands in `ℕ`, so `[Finite ι]` barred it. That hypothesis was stronger than the machine needs. What the machine needs is finitely many possible contents of the work tape holding the encoded scrutinee, which is `(Set.range sel).Finite`, and for a finite type that is `Set.toFinite _`. Branches outside the range are correspondingly no longer asked to be computable — with an `ℕ`-indexed family all but finitely many of them are junk, and quantifying over all of `ℕ` would make the hypothesis unsatisfiable for any nonconstant bound. This matters for mechanising the combinator rather than for using it by hand, where a `Bool` or `Fin n` tag is still pleasanter: a tactic cannot invent a bespoke tag type for an arbitrary inductive, but `ctorIdx` is always there, and both side conditions — finite range, and the branches agreeing — are discharged by case analysis on the scrutinee. An example on `Span` does exactly that. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The step-gluing in `computableInTimeAndSpace_loopFunction` was repetitive
because the plumbing leaves were not of the right form: `clear` returned
`ws' i = [] ∧ ∀ l ≠ i, ws' l = ws l`, `ofComputable` a four-way conjunction,
and every seam between two machines re-proved the frame — which tapes survived —
by a case analysis per tape.
Under their own preconditions those postconditions are each a single equality of
the whole vector. `ofComputable` changes exactly one word: tape `i` and the
`keep` tapes are untouched and the scratch tapes were blank before, so ending
blank is *unchanged*. Hence:
* `exists_transformsTapes_clear`: `ws' = Function.update ws i []`
* `exists_transformsTapes_ofComputable`, `_ofComputableInput`:
`ws' = Function.update ws o (encOut (g a))`
In the loop proof, the bespoke predicates `Both`/`Only1`/`Only3`/`InvMid`
become one sealed vector family `V w1 w3 w4` with projection, blankness and
`Function.update` equations proved once; each of the eight step-gluings is then
one or two `rw`s instead of an unpack-repack of frame conditions, and the
composite of the five-machine round is taken apart by `rfl`-patterns.
The net line count is flat (748 → 757): the vector family and its nine
single-purpose lemmas cost up front what the seams used to pay severally. What
changes is that the per-seam content is now only what is specific to that seam.
The other half of the proof's bulk — the `A₁…A₇`/`B₁…B₅` renormalisations of
each machine's bound into `a`-units — is untouched: it is not a statement
problem but the price of charging round-`x` costs to the loop input `a`, which
the repeat combinator's uniform per-round bounds force.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two pieces of `computableInTimeAndSpace_loopFunction` were self-contained and are now file-level declarations: * `loopIterate_succ_of_lt` (public): as long as the loop has not stopped, each iterate comes from the previous one by a successful call of the body. This was `hnext`, and it is pure recursion theory with no machine in it. * the `tapeWords` algebra (private): the vector of words holding three values on three named tapes, with its projection, blankness and `Function.update` equations. This was the sealed `V` family inside the proof; as named lemmas the equations are stated once, independently checkable, and the proof's gluing rewrites name what they use. Also drops `nat_bound_sum`, which nothing used. The theorem's proof shrinks from ~560 to ~475 lines; the file grows to 800 because the extracted pieces carry their own documentation. The remaining monolith is deliberate: the round machines (`hExit`/`hCont`/`hRound`) share the obtains of the five component machines and the `W`-renormalisation, so extracting them as lemmas would cost each a ~40-line hypothesis list restating the machine specifications and the bound facts — more text than the ~90-line proof bodies they would remove. The `###` section comments inside the proof mark the honest module boundaries. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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
2 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.
No description provided.