Skip to content

feat: add Decidable, Fintype, Encodable linters#10235

Closed
urkud wants to merge 323 commits intomasterfrom
YK-dec-lint
Closed

feat: add Decidable, Fintype, Encodable linters#10235
urkud wants to merge 323 commits intomasterfrom
YK-dec-lint

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Feb 4, 2024 •
edited
Loading

This PR ports the decidableClassical, fintypeFinite and encodableCountable linters from mathlib3: all three are environment linters which flag declarations that have a hypothesis [Decidable p] etc., but do not use the underlying assumption in this type. Restructuring the code can make the statement more general.
The implementation is in fact quite general, and can easily adapt to include further types. PRs #17518 and #17519 are two examples of further such linters.

Please don't fix the failures related to HasFDerivWithinAt.pi. Finiteness assumptions in these lemmas will be completely removed during porting to TVS.

Open in Gitpod

@urkud urkud added the t-meta Tactics, attributes or user commands label Feb 4, 2024
urkud added a commit that referenced this pull request Feb 4, 2024
@urkud
chore(LinearAlgebra,BigOperators): drop some decidability assumptions
0809e96 
Found by a linter from #10235.
@urkud urkud mentioned this pull request Feb 4, 2024
Closed
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 4, 2024
mathlib-bors bot pushed a commit that referenced this pull request Feb 4, 2024
@urkud
chore(LinearAlgebra,BigOperators): drop some decidability assumptions (…
3646044 
…#10237)

Found by a linter from #10235.
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Feb 5, 2024
Vierkantor pushed a commit that referenced this pull request Feb 5, 2024
@urkud @Vierkantor
chore(LinearAlgebra,BigOperators): drop some decidability assumptions (…
f311478 
…#10237)

Found by a linter from #10235.
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 6, 2024
atarnoam pushed a commit that referenced this pull request Feb 9, 2024
@urkud @atarnoam
chore(LinearAlgebra,BigOperators): drop some decidability assumptions (…
d2108ac 
…#10237)

Found by a linter from #10235.
urkud added 9 commits February 11, 2024 14:53
@urkud
Merge branch 'master' into YK-dec-lint
483e274
@urkud
chore(PowerSeries/Basic): drop a DecidableEq assumption
4909412
@urkud
chore(LinearAlgebra/Multilinear): drop a DecidableEq assumption
8449fe5
@urkud
chore(CategoryTheory/Sites): Fintype → Finite
abf39d8 
Also rename `Presieve.extensive` to `Presieve.Extensive`
to follow the naming convention.
@urkud
chore(SimpleGraph/Finite): drop some DecidableEq assumptions
c498cd2 
- don't assume `DecidableEq` in `card_edgeFinset_le_card_choose_two`;
- make `edgeFinset_deleteEdges` work with any `Fintype G.edgeSet`
  and `Fintype (G.deleteEdges s).edgeSet` instances;
- don't assume `DecidbaleEq` in theorems about `DeleteFar`.
@urkud
chore(SetFamily/FourFunctions): drop some unneeded DecidableEq assu…
25bcade 
…mptions
@urkud
chore(SimpleGraph/DegreeSum): drop some DecidableEq assumptions
f425dad
@urkud
chore(SimpleGraph/IncMatrix): drop 2 DecidableEq assumptions
cba0511
@urkud
Update
58b1f05
This was referenced Feb 15, 2025
Closed
Closed
Closed
Closed
Closed
Closed
@urkud
Copy link
Copy Markdown
Member Author

urkud commented Feb 16, 2025

Note: I'm working on HasFDerivAt.pi etc. I want to do it the right way (drop the Normed* assumptions at the same time), should be ready for review soon.

This was referenced Apr 26, 2025
Closed
Closed
Closed
Closed
@urkud urkud mentioned this pull request Sep 18, 2025
Closed
@Vierkantor
Copy link
Copy Markdown
Contributor

Vierkantor commented Oct 23, 2025

This PR is flagged as awaiting-author, what are you planning to do before this is ready for review? I would like to see this PR in Mathlib somewhat soon so I am willing to help out fix some of the build errors.

@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 9, 2025

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

@thorimur thorimur mentioned this pull request Nov 16, 2025
Closed
@thorimur
Copy link
Copy Markdown
Contributor

thorimur commented Nov 16, 2025

I started (and finished) porting the decidableClassical linter at #31142 without knowledge of this PR; I hope that's alright! :)

One major difference is that I wrote a syntax linter instead of an environment linter, so that it runs while editing. I also tried to take some care with performance, and avoided telescopes entirely until constructing the suggestion itself (which is allowed to be expensive, since it's impermanent). I also only lint user-written declarations due to searching the infotrees instead of the environment (which goes a bit beyond isAutoDecl, if I recall), and stick to linting theorems (and lemmas, and instances of Prop-valued classes).

Let me know what you think! I'm happy to pick up the torch if that's alright.

This was referenced Nov 18, 2025
Closed
Closed
@thorimur thorimur mentioned this pull request Dec 8, 2025
Closed
1 task
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Feb 15, 2026

Can this PR be closed now, or is there anything else that's missing? If so, we could track that in #35340.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kmill kmill kmill approved these changes

@grunweg grunweg grunweg left review comments

+1 more reviewer

@Command-Master Command-Master Command-Master left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

awaiting-author A reviewer has asked the author a question or requested changes. awaiting-bench This PR needs to be benchmarked before merging large-import Automatically added label for PRs with a significant increase in transitive imports merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-linter Linter t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.