8000 refactor: remove `InductiveVal.isReflexive` by cppio · Pull Request #9016 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

refactor: remove InductiveVal.isReflexive #9016

New issue 8000

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 3 commits into
base: master
Choose a base branch
from
Open

refactor: remove InductiveVal.isReflexive #9016

wants to merge 3 commits into from
+8 −52

Conversation

cppio
Copy link
Contributor
@cppio cppio commented Jun 26, 2025 •
edited
Loading

As observed on Zulip, the isReflexive field of InductiveVal is not correct in the prescence of nested inductives:

import Lean

inductive T
  | mk (x : List ((fun α => α) (Unit → T)))

#eval return (← Lean.getConstInfoInduct ``T).isReflexive -- false

Since the field is no longer used anywhere in Lean, this PR removes the field.

@nomeata
Copy link
Collaborator
nomeata commented Jun 26, 2025

Is just the field not used, or did the whole concept disappear? (If the former, then we should rescue the documentation somewhere.)

@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 Jun 26, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#9016
10b322c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#9016
ce2c1f0
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Jun 26, 2025 •
edited
Loading

Mathlib CI status (docs):

@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 Jun 26, 2025
@cppio
Copy link
Contributor Author
cppio commented Jun 26, 2025

Looks like it is used in mathlib. I'll replace it with a Lean implementation that looks at the type of the recursor, as that is a reliable method that works in the prescence of nested inductives.

@cppio cppio changed the title refactor: remove InductiveVal.isReflexive refactor: replace InductiveVal.isReflexive with Lean implementation Jun 26, 2025
@cppio
Copy link
Contributor Author
cppio commented Jun 26, 2025

@nomeata I moved the documentation to the new Lean implementation.

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9016
41e1cce
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9016
a45ed1f
@nomeata
Copy link
Collaborator
nomeata commented Jun 26, 2025

Thanks, it’s good to check for downstream breakage! But if this is used by mathlib, maybe it should live there? Where and how is it used there?

@cppio
Copy link
Contributor Author
cppio commented Jun 26, 2025

It's used in a couple of deriving handlers (Countable and Encodable) to filter out unsupported inductives. Neither handler supports nested inductives anyways, so the fixed implementation doesn't make a difference. I can move isReflexive to mathlib if that makes the most sense, or maybe there's some other way for the tactics to reject the unsupported inductives without using isReflexive.

@nomeata
Copy link
Collaborator
nomeata commented Jun 26, 2025

It seems reasonable for such deriving code to ”own” the logic for which data types they support.

@cppio cppio changed the title refactor: replace InductiveVal.isReflexive with Lean implementation refactor: remove InductiveVal.isReflexive Jun 26, 2025
@cppio
Copy link
Contributor Author
cppio commented Jun 26, 2025

I removed the Lean implementation. I'm not sure what the new method is for adaptations, but the mathlib build can be fixed by removing || indVal.isReflexivefrom DeriveCountable and DeriveEncodable.

@cppio cppio marked this pull request as ready for review June 26, 2025 20:13
@cppio cppio requested a review from leodemoura as a code owner June 26, 2025 20:13
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9016
ee98c41
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#9016
ada5822
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

Assignees
No one assigned
Labels
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
@cppio @nomeata @leanprover-community-bot
0