Skip to content

fix: use pi_congr instead of forall_congr, deprecate the latter - #14516

Open
sgraf812 wants to merge 1 commit into
nightly-with-mathlibfrom
sg/7507-reapply
Open

fix: use pi_congr instead of forall_congr, deprecate the latter#14516
sgraf812 wants to merge 1 commit into
nightly-with-mathlibfrom
sg/7507-reapply

Conversation

@sgraf812

@sgraf812 sgraf812 commented Jul 23, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR generalizes the conv and simp tactics to apply pi_congr instead of forall_congr. The test case for #7507 has examples that work now, but only worked at universe v=0 before.

Since there are no more remaining uses of forall_congr, it is now deprecated.

Closes #7507.

This was referenced Jul 23, 2026
Merged
Merged
@sgraf812

sgraf812 commented Jul 23, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jul 23, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for f603f6b against 782c1b3 are in. There are significant results. @sgraf812

  • 🟥 build exited with code -1
  • 🟥 other exited with code -1

No significant changes detected.

@sgraf812 Sebastian Graf
fix: use pi_congr instead of forall_congr; deprecate the latter (#7577)
ac0e1b2 
This PR generalizes the `conv` and `simp` tactics to apply `pi_congr`
instead of `forall_congr`. The test case for #7507 has examples that
work now, but only worked at universe `v=0` before.

Since there are no more remaining uses of `forall_congr`, it is now
deprecated.

Closes #7507.

Co-authored-by: Sebastian Graf <sg@lean-fro.org>
@sgraf812
sgraf812 changed the base branch from sg/revert-7577 to nightly-with-mathlib July 23, 2026 11:43
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 23, 2026
@leanprover-bot

leanprover-bot commented Jul 23, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-07-23 12:11:07)

@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jul 23, 2026
@sgraf812

sgraf812 commented Jul 23, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jul 23, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for ac0e1b2 against 3259610 are in. No significant results found. @sgraf812

  • 🟥 build//instructions: +456.1M (+0.00%)

Small changes (2✅)

  • ✅ misc/leanchecker --fresh Init//task-clock: -1s (-3.73%)
  • ✅ misc/leanchecker --fresh Init//wall-clock: -1s (-3.70%)

@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jul 23, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 23, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

pull Bot pushed a commit to DaviRain-Su/lean4 that referenced this pull request Jul 23, 2026
@sgraf812
chore: revert "fix: use pi_congr instead of forall_congr; deprecate t…
7f03b50 
…he latter (leanprover#7577)" (leanprover#14515)

Reverts leanprover#7577, which reached `master` through a stale auto-merge (armed
on the PR back in March 2025) rather than a deliberate merge, before
review had concluded.

The change itself is sound and is re-proposed for normal review in
leanprover#14516 (stacked on this revert).
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jul 23, 2026
@sgraf812

sgraf812 commented Jul 23, 2026

Copy link
Copy Markdown
Contributor Author

!bench mathlib

@sgraf812
sgraf812 marked this pull request as ready for review July 23, 2026 14:57
@leanprover-radar

leanprover-radar commented Jul 23, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for leanprover-community/mathlib4-nightly-testing@c4659da against leanprover-community/mathlib4-nightly-testing@eaeb601 are in. There are significant results. @sgraf812

  • 🟥 build//instructions: +102.4G (+0.07%)

Large changes (1🟥)

  • 🟥 build/module/Mathlib.Algebra.Central.End//instructions: +17.5G (+116.71%)

Small changes (1🟥)

  • 🟥 build/module/Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries//instructions: +1.8G (+8.86%)

@sgraf812 sgraf812 added the awaiting-review Waiting for someone to review the PR label Jul 23, 2026
@sgraf812 sgraf812 changed the title fix: use pi_congr instead of forall_congr; deprecate the latter fix: use pi_congr instead of forall_congr, deprecate the latter Jul 24, 2026
@sgraf812

sgraf812 commented Jul 24, 2026

Copy link
Copy Markdown
Contributor Author

!bench mathlib

@leanprover-radar

leanprover-radar commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for leanprover-community/mathlib4-nightly-testing@16adcca against leanprover-community/mathlib4-nightly-testing@eaeb601 are in. No significant results found. @sgraf812

  • 🟥 build//instructions: +83.1G (+0.06%)

Medium changes (2✅)

  • ✅ build/module/Mathlib.Algebra.Central.End//instructions: -6.5G (-43.42%)
  • ✅ build/module/Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries//instructions: -6.6G (-32.55%)

Small changes (1🟥)

  • 🟥 build/module/Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv//instructions: +1.6G (+2.16%)

@sgraf812 sgraf812 added changelog-library Library changelog-tactics User facing tactics labels Jul 24, 2026
@sgraf812

sgraf812 commented Jul 24, 2026

Copy link
Copy Markdown
Contributor Author

!bench mathlib

@leanprover-radar

leanprover-radar commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for leanprover-community/mathlib4-nightly-testing@5f0457a against leanprover-community/mathlib4-nightly-testing@eaeb601 are in. No significant results found. @sgraf812

  • 🟥 build//instructions: +146.2G (+0.10%)

Medium changes (3✅)

  • ✅ build/module/Mathlib.Algebra.Central.End//instructions: -6.6G (-43.81%)
  • ✅ build/module/Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries//instructions: -6.6G (-32.78%)
  • ✅ build/module/Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs//instructions: -7.3G (-31.27%)

Small changes (3✅, 1🟥)

  • ✅ build/module/Mathlib.Algebra.MvPolynomial.NoZeroDivisors//instructions: -1.1G (-8.17%)
  • ✅ build/module/Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv//instructions: -3.2G (-4.36%)
  • ✅ build/module/Mathlib.Combinatorics.Enumerative.Partition.GenFun//instructions: -2.3G (-12.22%)
  • and 1 hidden

@sgraf812 sgraf812 removed the changelog-tactics User facing tactics label Jul 24, 2026
@sgraf812 sgraf812 mentioned this pull request Jul 24, 2026
Closed
@sgraf812

sgraf812 commented Jul 24, 2026

Copy link
Copy Markdown
Contributor Author

Note for review: this patch makes it possible for simp to rewrite in more situations, so it traverses more terms in mathlib for rewriting opportunities and regresses slightly. I think it's the right call nonetheless; on the adaptation branch I discovered a simp antipattern that way (blanket eq_zero [...] (lhs : α) : lhs = 0 as a simp lemma) that we or mathlib might want to incorporate into a simp linter at some point: leanprover-community/mathlib4#42053.

@sgraf812 sgraf812 added changelog-library Library and removed changelog-library Library labels Jul 24, 2026
robsimmons pushed a commit that referenced this pull request Jul 29, 2026
@sgraf812 @robsimmons
chore: revert "fix: use pi_congr instead of forall_congr; deprecate t…
86cd572 
…he latter (#7577)" (#14515)

Reverts #7577, which reached `master` through a stale auto-merge (armed
on the PR back in March 2025) rather than a deliberate merge, before
review had concluded.

The change itself is sound and is re-proposed for normal review in
#14516 (stacked on this revert).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner
@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@sgraf812 @leanprover-radar @leanprover-bot