[Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for `Seq` by vasnesterov · Pull Request #34311 · leanprover-community/mathlib4

vasnesterov · 2026-01-23T13:02:31Z

This PR develops a theory that justifies corecursive definitions of the form

def foo (x : X) := hd x :: f (foo (tlArg x))

where f : Seq α → Seq α is a friendly operation.

This is a part of the compute_asymptotics tactic (#28291).

github-actions · 2026-01-23T13:03:40Z

PR summary b87448799e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic	2909	2922	+13 (+0.45%)

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	13
`Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion` (new file)	1652

Declarations diff

+ FriendlyOperation
+ FriendlyOperation.comp
+ FriendlyOperation.const
+ FriendlyOperation.dist_le
+ FriendlyOperation.exists_fixed_point
+ FriendlyOperation.id
+ FriendlyOperation.ite
+ FriendlyOperationClass
+ FriendlyOperationClass.comp
+ Stream'.dist_le_one
+ boundedSpace
+ dist_cons_cons
+ dist_cons_cons_eq_one
+ dist_cons_nil
+ dist_eq_half_of_head
+ dist_eq_one_of_head
+ dist_eq_two_inv_pow
+ dist_nil_cons
+ exists_fixed_point_of_contractible
+ gcorec
+ gcorec_nil
+ gcorec_some
++ dist_le_one
+++ foo

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

ocfnash · 2026-01-29T10:50:05Z

Thanks, this is very nice work! Just to check my own understanding, is the reason corecursion is useful here because:

We need to regard the RHS of expansions like $1 / (1 - x) = 1 + x + x^2 + \cdots$ as a formal multiseries with an infinite basis (that is $1$, $x$, $x^2$, ...). We want these bases to be ordered lists (thus necessarily possibly infinite) whose head is the leading term, which we use to compute the limit.
We want to compute lazily with these lists, partly for performance reasons, and partly because we might not know how far down an expansion we need to remember if we were to truncate (e.g., if we multiply by a large power of $x$ later on in the calculation).

Have I got that about right? If so this does indeed seem to be a strong case for your design.

vasnesterov · 2026-02-02T21:43:52Z

@ocfnash Thanks! Yes, we want to work with series as lazy possibly infinite lists, because we can’t know in advance how many terms we’ll need. It’s also easier to work with infinite series mathematically than with their truncations, I guess.

But "basis" in the context of this tactic means something different (and it is always finite). A basis is just a list of real functions ordered by their growth rate. The main object we work with is a so-called multiseries -- a multivariate formal series with monomials of the form b₁^e₁ * ... * bₙ^eₙ, where [b₁, ..., bₙ] is our basis and e₁, ..., eₙ are real numbers.

We need corecursion to define the operations on multiseries: addition, multiplication, etc. Some operations (multiplication and powser) cannot be expressed directly using Seq.corec. That’s why we need to develop some theory of non-primitive corecursion.

I’ve written a short description of how the tactic works to give reviewers more context: https://vasnesterov.github.io/compute_asymptotics. Feel free to ask/suggest anything.

eric-wieser · 2026-02-06T18:43:13Z

+/-- Metric space structure on `Stream' α` considering `α` as a discrete metric space. -/
+noncomputable local instance : MetricSpace (Stream' α) :=
+  @PiNat.metricSpace (fun _ ↦ α) (fun _ ↦ ⊥) (fun _ ↦ discreteTopology_bot _)


Should this be a global instance on Stream, but with a [DiscreteTopology α] assumption?

I don't think anything here should be global. I see this file as an ad hoc implementation of a very limited construction - just enough for the tactic.

It's possible to generalize this to arbitrary coinductive type and support a more powerful form of corecursion, but I think we need to wait until QPF is done and ready to use before doing that.

Do you think this metric space structure is useful for other applications?

eric-wieser · 2026-02-06T20:50:55Z

+```
+(where hd and tlArg are arbitrary functions) can be encoded via the corecursor `Seq.corec`.
+
+It is not enough, however, to define multiplication and powser operation for multiseries.


Suggested change

It is not enough, however, to define multiplication and powser operation for multiseries.

It is not enough, however, to define multiplication and power operations for multiseries.

It's the powser operation (https://vasnesterov.github.io/compute_asymptotics#lazyseries-and-powser-operation) -- the substitution of a multiseries into a power series. This is what Eberl calls it in his tactic. But I'm happy to rename it if you have a better suggestion!

jcommelin

Thanks 🎉

bors merge

…n for `Seq` (#34311) This PR develops a theory that justifies corecursive definitions of the form ```lean def foo (x : X) := hd x :: f (foo (tlArg x)) ``` where `f : Seq α → Seq α` is a friendly operation.

mathlib-bors · 2026-02-10T07:21:51Z

Pull request successfully merged into master.

Build succeeded:

…n for `Seq` (leanprover-community#34311) This PR develops a theory that justifies corecursive definitions of the form ```lean def foo (x : X) := hd x :: f (foo (tlArg x)) ``` where `f : Seq α → Seq α` is a friendly operation.

…n for `Seq`: `FriendlyOperation` API (#35072) This is a continuation of #34311. This PR adds more API about friendly operations: * Basic friendly operations constructions * `FriendlyOperation.destruct`: a "coinductive destructor" for `FriendlyOperation`

…n for `Seq`: `FriendlyOperation` API (leanprover-community#35072) This is a continuation of leanprover-community#34311. This PR adds more API about friendly operations: * Basic friendly operations constructions * `FriendlyOperation.destruct`: a "coinductive destructor" for `FriendlyOperation`

init

55619ca

vasnesterov added the t-data Data (lists, quotients, numbers, etc) label Jan 23, 2026

vasnesterov mentioned this pull request Jan 23, 2026

feat(Tactic): tactic for computing asymptotics of real functions #28291

Open

12 tasks

plp127 reviewed Jan 23, 2026

View reviewed changes

Comment thread Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean

Comment thread Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean

vasnesterov added 6 commits January 23, 2026 16:24

resolve TODO

9188d17

fix references

bb0c37c

add comment

3529fbf

namespace

a498e90

corecursion: halve

f05ccfa

docs

9a2d1c7

grunweg changed the title ~~feat(Tactic/ComputeAsymptotics/Multiseries): Non-primitive corecursion for Seq~~ feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq Jan 27, 2026

joneugster assigned ocfnash Jan 30, 2026

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2026

vasnesterov removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 2, 2026

eric-wieser reviewed Feb 6, 2026

View reviewed changes

Comment thread Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean Outdated

update docstring

91543a1

eric-wieser reviewed Feb 6, 2026

View reviewed changes

powser

d05b5ce

jcommelin reviewed Feb 10, 2026

View reviewed changes

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Feb 10, 2026

mathlib-bors bot changed the title ~~feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq~~ [Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq Feb 10, 2026

mathlib-bors bot closed this Feb 10, 2026

vasnesterov mentioned this pull request Feb 10, 2026

[Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: FriendlyOperation API #35072

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for `Seq`#34311

[Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for `Seq`#34311
vasnesterov wants to merge 9 commits intoleanprover-community:masterfrom
vasnesterov:compute_asymptotics_corecursion

vasnesterov commented Jan 23, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Jan 23, 2026 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

ocfnash commented Jan 29, 2026 •

edited

Loading

Uh oh!

vasnesterov commented Feb 2, 2026 •

edited

Loading

Uh oh!

eric-wieser Feb 6, 2026

Uh oh!

vasnesterov Feb 6, 2026

Uh oh!

Uh oh!

eric-wieser Feb 6, 2026 •

edited

Loading

Uh oh!

vasnesterov Feb 6, 2026

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors bot commented Feb 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

	It is not enough, however, to define multiplication and powser operation for multiseries.
	It is not enough, however, to define multiplication and power operations for multiseries.

Conversation

vasnesterov commented Jan 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary b87448799e

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

ocfnash commented Jan 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

eric-wieser Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

vasnesterov Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

eric-wieser Feb 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

vasnesterov Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Feb 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

vasnesterov commented Jan 23, 2026 •

edited

Loading

github-actions bot commented Jan 23, 2026 •

edited

Loading

ocfnash commented Jan 29, 2026 •

edited

Loading

vasnesterov commented Feb 2, 2026 •

edited

Loading

eric-wieser Feb 6, 2026 •

edited

Loading