Skip to content
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

fix: FunInd to clear match discriminants if possible #7110

Merged
merged 3 commits into from
Feb 17, 2025
Merged

fix: FunInd to clear match discriminants if possible #7110

merged 3 commits into from
Feb 17, 2025

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Feb 17, 2025

This PR tries to remove from functional induction principles hypotheses that have been matched, as we expect the corresponding pattern to be more useful. This avoids duplicate hypotheses due to the way match refines hypotheses. Fixes #6281.

@nomeata nomeata added the changelog-language Language features, tactics, and metaprograms label Feb 17, 2025
@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 Feb 17, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 17, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7110
34509d9
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 17, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7110
b26f851
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Feb 17, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 17, 2025 •
edited
Loading

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-7110 build failed against this PR. (2025-02-17 11:25:59) View Log
  • 🟡 Mathlib branch lean-pr-testing-7110 build against this PR was cancelled. (2025-02-17 12:05:50) View Log
  • ✅ Mathlib branch lean-pr-testing-7110 has successfully built against this PR. (2025-02-17 12:50:48) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3825c48405bb86a9e34a27bc945e3a9b9c3c499e --onto 88664e4a995883877a5d85211a5cfab0a672b5ed. (2025-02-17 17:05:24)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 17, 2025 11:56 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 17, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7110
75d941b
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 17, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7110
fba7885
@leanprover-community-bot leanprover-community-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 Feb 17, 2025
@nomeata nomeata marked this pull request as ready for review February 17, 2025 14:18
@nomeata nomeata requested a review from leodemoura as a code owner February 17, 2025 14:18
@nomeata nomeata enabled auto-merge February 17, 2025 14:18
@nomeata nomeata added this pull request to the merge queue Feb 17, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Feb 17, 2025
@nomeata
Copy link
Collaborator Author

nomeata commented Feb 17, 2025

Hmm, this runs into stage0 update issues. I should make sure that the features I add to lean are so bad or unreliable that we don’t use them internally.

(I’ll do the dance with the rebase-merge later.)

@nomeata
fix: FunInd to clear match discriminants if possible
7d65e24 
This PR tries to remove from functional induction principles hypotheses
that have been matched, as we expect the corresponding pattern to be
more useful. This avoids duplicate hypotheses due to the way `match`
refines hypotheses. Fixes #6281.
@nomeata
chore: update stage0
4f4c961
@nomeata nomeata added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Feb 17, 2025
@nomeata nomeata requested a review from TwoFX as a code owner February 17, 2025 16:19
@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Feb 17, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 17, 2025 16:40 Inactive
@Kha Kha merged commit 2cdf4b1 into master Feb 17, 2025
16 checks passed
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

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms changes-stage0 Contains stage0 changes, merge manually using rebase merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. 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.

FunInd: Redundant assumptions due to match-elaboration
3 participants
@nomeata @leanprover-community-bot @Kha