[Merged by Bors] - feat(Convert): less aggressive congruence by JovanGerb · Pull Request #38071 · leanprover-community/mathlib4

JovanGerb · 2026-04-15T13:43:31Z

This PR tries to make convert behave more predictably, disabling some of the aggressive congruence steps that congr! does. In particular, when the two sides have a different head constants, then we should not use congruence on these applications.

github-actions · 2026-04-15T13:44:37Z

PR summary c631f6e5f1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

- Convert.CheapConfig.unfoldSameFun
- Convert.ExpensiveConfig.unfoldSameFun

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit c631f6e).

+1 new declarations
−3 removed declarations

-Convert.CheapConfig.unfoldSameFun
-Convert.ExpensiveConfig.toCheapConfig
+Convert.ExpensiveConfig.toConfig
-Convert.ExpensiveConfig.unfoldSameFun

No changes to strong technical debt.

No changes to weak technical debt.

Current commit c631f6e5f1
Reference commit 833b1ec7ee

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

mathlib-merge-conflicts · 2026-04-21T22:32:33Z

This pull request has conflicts, please merge master and resolve them.

Vierkantor · 2026-05-13T09:00:43Z

This change makes sense to me! If it were possible, I'd like to get it in before the very drastic changes of #39039. Could you fix the merge conflict and the build? Or do you want to have the convert! machinery up and working first? (Feel free to copy parts of my PR into this one in that case!)

This reverts commit 42dc41b.

joneugster

Thanks!

maintainer merge

github-actions · 2026-05-29T12:28:08Z

🚀 Pull request has been placed on the maintainer queue by joneugster.

joneugster · 2026-05-29T12:28:47Z

oh I missed that CI is failing

This PR implements the main behaviour change from #39039: `convert` now discharges side goals at reducible transparency. `convert!`, which we previously switched all calls inside Mathlib to, keeps the old behaviour of working at default transparency. (Everything discussed in this PR holds analogously for the other tactics in the family: `convert_to` and `ac_change`). The main trick in this PR is in allowing `convert!` to have different configuration options than `convert`, but still allow the user to override those options too. So `convert! (postTransparency := .instances)` will have transparency set to `.instances`, not `.default`. We achieve this by having two new structures that copy `Congr!.Config` but set different default values, and choosing between the corresponding elaborators for those configs based on the presence of an `!`. I got this trick from Jovan's #38071 which also changes settings in `Convert.Config`. This PR should be mostly compatible with #38071 and I'd like to get both this one and #38071 in before wrapping up #39039 by replacing unnecessary calls to `convert!` with `convert`.

This PR implements the main behaviour change from #39039: `convert` now discharges side goals at reducible transparency. `convert!`, which we previously switched all calls inside Mathlib to, keeps the old behaviour of working at default transparency. (Everything discussed in this PR holds analogously for the other tactics in the family: `convert_to` and `ac_change`). The main trick in this PR is in allowing `convert!` to have different configuration options than `convert`, but still allow the user to override those options too. So `convert! (postTransparency := .instances)` will have transparency set to `.instances`, not `.default`. We achieve this by having two new structures that copy `Congr!.Config` but set different default values, and choosing between the corresponding elaborators for those configs based on the presence of an `!`. I got this trick from Jovan's #38071 which also changes settings in `Convert.Config`. This PR should be mostly compatible with #38071 and I'd like to get both this one and #38071 in before wrapping up #39039 by replacing unnecessary calls to `convert!` with `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

JovanGerb · 2026-06-05T16:12:52Z

The trouble with the new convert congruence setting is that the doc-string examples of convert using now don't need the using clause anymore. So either we'll need to come up with new examples to explain what using does, or we can decide that convert using will probably we less common in the future, so we don't need to explain it so prominently anymore, and the variant explanation at the bottom will suffice.

JovanGerb · 2026-06-05T16:14:38Z

@kmill, as the original author, do you have some opinions on this PR?

Vierkantor · 2026-06-17T15:29:55Z

 Examples:

 ```lean
-- `convert using` controls the depth of congruence.


I'm okay with removing the emphasis on using, since it seems that there are indeed many cases where we no longer need to use using.

Vierkantor · 2026-06-17T15:35:22Z

Thanks!

bors r+

This PR tries to make `convert` behave more predictably, disabling some of the aggressive congruence steps that `congr!` does. In particular, when the two sides have a different head constants, then we should not use congruence on these applications. Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

mathlib-bors · 2026-06-17T16:38:34Z

Pull request successfully merged into master.

Build succeeded:

This PR tries to make `convert` behave more predictably, disabling some of the aggressive congruence steps that `congr!` does. In particular, when the two sides have a different head constants, then we should not use congruence on these applications. Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

…ommunity#39928) This PR implements the main behaviour change from leanprover-community#39039: `convert` now discharges side goals at reducible transparency. `convert!`, which we previously switched all calls inside Mathlib to, keeps the old behaviour of working at default transparency. (Everything discussed in this PR holds analogously for the other tactics in the family: `convert_to` and `ac_change`). The main trick in this PR is in allowing `convert!` to have different configuration options than `convert`, but still allow the user to override those options too. So `convert! (postTransparency := .instances)` will have transparency set to `.instances`, not `.default`. We achieve this by having two new structures that copy `Congr!.Config` but set different default values, and choosing between the corresponding elaborators for those configs based on the presence of an `!`. I got this trick from Jovan's leanprover-community#38071 which also changes settings in `Convert.Config`. This PR should be mostly compatible with leanprover-community#38071 and I'd like to get both this one and leanprover-community#38071 in before wrapping up leanprover-community#39039 by replacing unnecessary calls to `convert!` with `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

This PR tries to make `convert` behave more predictably, disabling some of the aggressive congruence steps that `congr!` does. In particular, when the two sides have a different head constants, then we should not use congruence on these applications. Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

This PR fixes a regression introduced in #38071, which had caused the congruence algorithm of `convert` to not support over-applications. I added a test to show this now works again.

…unity#40740) This PR fixes a regression introduced in leanprover-community#38071, which had caused the congruence algorithm of `convert` to not support over-applications. I added a test to show this now works again.

feat(Convert): less aggressive congruence

aceb46e

grunweg added the t-meta Tactics, attributes or user commands label Apr 15, 2026

JovanGerb added 2 commits April 15, 2026 22:39

fix syntax

d9d4331

fixes

42dc41b

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 21, 2026

JovanGerb mentioned this pull request May 9, 2026

feat(Tactic): convert now discharges side goals at reducible transparency #39039

Open

3 tasks

Vierkantor self-assigned this May 13, 2026

JovanGerb added 2 commits May 26, 2026 13:24

Revert "fixes"

ad07c6a

This reverts commit 42dc41b.

Merge branch 'master' into Jovan-convert-config

dac46fe

mathlib-merge-conflicts Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 26, 2026

Vierkantor mentioned this pull request May 27, 2026

[Merged by Bors] - feat(Tactic): convert discharges side goals reducibly #39928

Closed

joneugster approved these changes May 29, 2026

View reviewed changes

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 29, 2026

Merge remote-tracking branch 'origin/master' into Jovan-convert-config

3cdc8d2

joneugster self-assigned this May 29, 2026

joneugster added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 29, 2026

JovanGerb added 2 commits June 5, 2026 16:41

Merge branch 'master' into Jovan-convert-config

13e19d2

re-implement after merge

9a3e5a8

JovanGerb temporarily deployed to cache-upload-forks June 5, 2026 16:19 — with GitHub Actions Inactive

fix

c631f6e

JovanGerb temporarily deployed to cache-upload-forks June 6, 2026 11:54 — with GitHub Actions Inactive

JovanGerb removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 6, 2026

Vierkantor mentioned this pull request Jun 16, 2026

feat: solve equalities of instances in convert #40663

Open

Vierkantor reviewed Jun 17, 2026

View reviewed changes

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Jun 17, 2026

mathlib-bors Bot changed the title ~~feat(Convert): less aggressive congruence~~ [Merged by Bors] - feat(Convert): less aggressive congruence Jun 17, 2026

mathlib-bors Bot closed this Jun 17, 2026

JovanGerb mentioned this pull request Jun 17, 2026

[Merged by Bors] - fix(Tactic/Convert): support over-applications again #40740

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[Merged by Bors] - feat(Convert): less aggressive congruence#38071

[Merged by Bors] - feat(Convert): less aggressive congruence#38071
JovanGerb wants to merge 9 commits into
leanprover-community:masterfrom
JovanGerb:Jovan-convert-config

JovanGerb commented Apr 15, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Apr 15, 2026 •

edited

Loading

Declarations diff (regex)

Uh oh!

mathlib-merge-conflicts Bot commented Apr 21, 2026

Uh oh!

Vierkantor commented May 13, 2026

Uh oh!

joneugster left a comment

Uh oh!

github-actions Bot commented May 29, 2026

Uh oh!

joneugster commented May 29, 2026

Uh oh!

JovanGerb commented Jun 5, 2026

Uh oh!

JovanGerb commented Jun 5, 2026

Uh oh!

Vierkantor Jun 17, 2026

Uh oh!

Vierkantor commented Jun 17, 2026

Uh oh!

mathlib-bors Bot commented Jun 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

JovanGerb commented Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c631f6e5f1

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-merge-conflicts Bot commented Apr 21, 2026

Uh oh!

Vierkantor commented May 13, 2026

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented May 29, 2026

Uh oh!

joneugster commented May 29, 2026

Uh oh!

JovanGerb commented Jun 5, 2026

Uh oh!

JovanGerb commented Jun 5, 2026

Uh oh!

Vierkantor Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

Vierkantor commented Jun 17, 2026

Uh oh!

mathlib-bors Bot commented Jun 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

JovanGerb commented Apr 15, 2026 •

edited

Loading

github-actions Bot commented Apr 15, 2026 •

edited

Loading