Skip to content

fix: use pi_congr instead of forall_congr; deprecate the latter #7577

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

fix: use pi_congr instead of forall_congr; deprecate the latter #7577

wants to merge 1 commit into from

Conversation

sgraf812
Copy link
Contributor

@sgraf812 sgraf812 commented Mar 19, 2025 •
edited
Loading

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.

@sgraf812 sgraf812 added the changelog-language Language features, tactics, and metaprograms label Mar 19, 2025
@sgraf812 sgraf812 force-pushed the sg/7507 branch 2 times, most recently from 5563647 to 157ddfe Compare March 19, 2025 16:53
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 19, 2025 17:08 Inactive
@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 Mar 19, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 720f6fca94e24f21ba84805917edacef1bac9349 --onto a97813e11f962bc422a03c30b7e29dd2eefb92c8. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-19 17:19:44)

nomeata
nomeata reviewed Mar 19, 2025
View reviewed changes
fix: use pi_congr instead of forall_congr; deprecate the latter
5ec0ded 
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.

Fixes #7507.
@sgraf812 sgraf812 changed the title fix: use pi_congr instead of forall_congr; remove the latter fix: use pi_congr instead of forall_congr; deprecate the latter Mar 20, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 20, 2025 10:04 Inactive
@sgraf812 sgraf812 enabled auto-merge March 26, 2025 08:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@nomeata nomeata nomeata left review comments

@TwoFX TwoFX TwoFX left review comments

@b-mehta b-mehta b-mehta left review comments

@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
changelog-language Language features, tactics, and metaprograms 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.

forall_congr should be generalized from Prop to Sort
5 participants
@sgraf812 @leanprover-community-bot @nomeata @TwoFX @b-mehta