[Merged by Bors] - feat(tactic/lint): add linter that type-checks statements

[fpvandoorn]

• Add linter that type-checks the statements of all declarations with the default reducibility settings. A statement might not type-check if locally a declaration was made not @[irreducible] while globally it is.
• Fix an issue where with_one.monoid.to_mul_one_class did not unify with with_one.mul_one_class.
• Fix some proofs in category_theory.opposites so that they work while keeping quiver.opposite irreducible.

---

Zulip

[sgouezel]

I thought that making things irreducible after the fact was now forbidden because it is not supported by Lean 4. Are the issues in this PR only due to examples in mathlib that do not conform yet to this rule? If this is the case, a better fix would be to make them irreducible from the start and adjust the proofs, no ?

[fpvandoorn]

Yes, all these examples are problems caused by locally making definitions not @[irreducible] (or not yet having them made @[irreducible]). The library is making some types @[irreducible] at the end of the file where it is defined, while keeping it @[semireducible] to develop some basic definitions/results about them.

Making all definitions immediately irreducible is a little painful, because that means that e.g. the option API is not available for with_zero/with_one.

Here is a gist of all automatically generated declarations that are ill-typed. That should catch all definitions (but not all lemmas) that only work because some other declaration is locally not irreducible.

[gebner]

Suggested change

	auto_decls := ff,
	auto_decls := tt,

Constructors are also auto decls and should be checked as well.

[fpvandoorn]

If we do that, we cannot define structure on a new irreducible type by using the corresponding structure on the old type.
In particular: all of the following instances have equational lemmas that are ill-typed once with_one is irreducible.

@[to_additive] instance : monad with_one := option.monad
@[to_additive] instance : has_one (with_one α) := ⟨none⟩
@[to_additive] instance [has_mul α] : has_mul (with_one α) := ⟨option.lift_or_get (*)⟩
@[to_additive] instance : inhabited (with_one α) := ⟨1⟩
@[to_additive] instance [nonempty α] : nontrivial (with_one α) := option.nontrivial
@[to_additive] instance : has_coe_t α (with_one α) := ⟨some⟩

More failures are in this Gist: https://gist.github.com/fpvandoorn/015ce16dbd42f3ec33f26f44ef031c3a

[gebner]

All of the errors here are equation lemmas and abstracted proofs terms. (And linarith.config.mk.inj* which is weird, but also a meta definition.)

It's unfortunate that auto_decls covers so much. My preference would be to set auto_decls := tt for the linter and exclude abstracted proofs and equation lemmas manually. But I'm also happy if you merge the linter as it is now before it sits another week.

bors d+

[fpvandoorn]

That is a good idea. I might do that in a follow-up PR.

bors merge

[bors]

✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests