Skip to content

feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: more FriendlyOperation API#37342

Open
vasnesterov wants to merge 16 commits intoleanprover-community:masterfrom
vasnesterov:compute_asymptotics_corecursion_3
Open

feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: more FriendlyOperation API#37342
vasnesterov wants to merge 16 commits intoleanprover-community:masterfrom
vasnesterov:compute_asymptotics_corecursion_3

Conversation

@vasnesterov
Copy link
Copy Markdown
Collaborator

@vasnesterov vasnesterov commented Mar 29, 2026

This is a continuation of #35072.

This PR adds more API about friendly operations:

  • FriendlyOperation.coind: a coinductive principle for proving that operation is friendly
  • FriendlyOperationClass.eq_of_bisim: a generalisation of Seq.eq_of_bisim' for proving two sequences are equal.

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

Open in Gitpod

@vasnesterov vasnesterov added t-meta Tactics, attributes or user commands t-data Data (lists, quotients, numbers, etc) labels Mar 29, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 29, 2026 •
edited
Loading

PR summary c7cd377ce0

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ FriendlyOperation.coind
+ FriendlyOperation.coind_comp_friend_left
+ FriendlyOperation.coind_comp_friend_right
+ FriendlyOperationClass.eq_of_bisim

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

Increase in tech debt: (relative, absolute) = (2.00, 0.00)
Current number Change Type
6903 2 backward.isDefEq.respectTransparency

Current commit 3d23594230
Reference commit c7cd377ce0

You can run this locally as

./scripts/reporting/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).

@vasnesterov vasnesterov mentioned this pull request Mar 29, 2026
Closed
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 29, 2026
@vasnesterov vasnesterov mentioned this pull request Mar 29, 2026
Open
12 tasks
@vasnesterov vasnesterov changed the title feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: FriendlyOperation API feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: more FriendlyOperation API Mar 31, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 2, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Apr 2, 2026

This PR/issue depends on:

@Vierkantor Vierkantor self-requested a review April 2, 2026 13:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Vierkantor Vierkantor Awaiting requested review from Vierkantor

Assignees

No one assigned

Labels

t-data Data (lists, quotients, numbers, etc) t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@vasnesterov