feat: have/let linter

[adomani]

trafficstars

The main PR for the have vs let linter.

The have vs let linter emits a warning on haves introducing a hypothesis whose Type is not Prop. There are three settings:

• 0 -- inactive;
• 1 -- active only on noisy declarations;
• 2 or more -- always active. The default value is 1.

The linter lints mathlib, but, by default, it is silent on complete proofs.

#12157 is an experiment showing what changes the linter would suggest on mathlib.

---

[adomani]

As a test, I ran the linter with the "new" monad on a fresh copy of mathlib: I wanted to make sure that it picked up the same issues that the previous version of the linter noticed.

The result is an improvement: I think that they flag essentially the same issues and the new monad pretty-prints better. However, there is an overflow that I cannot debug. You can see its effects in this failed linting step.

The two places that I identified are a run_cmd in Mathlib/Data/UInt.lean and a local notation3 in Mathlib/Algebra/Lie/Weights/Basic.lean.

[adomani]

Looking at the places where I had to unset the linter, I am guessing that this is just a matter of a slowdown: notation3, theorem, run_command` all appear among the list of unlinted commands.

diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean
index 7742e87568..3ea8cbfefe 100644
--- a/Mathlib/Algebra/Lie/Weights/Basic.lean
+++ b/Mathlib/Algebra/Lie/Weights/Basic.lean
@@ -56,8 +56,10 @@ open scoped BigOperators TensorProduct
 
 section notation_weightSpaceOf
 
+set_option linter.haveLet false
 /-- Until we define `LieModule.weightSpaceOf`, it is useful to have some notation as follows: -/
 local notation3 "𝕎("M", " χ", " x")" => (toEndomorphism R L M x).maximalGeneralizedEigenspace χ
+set_option linter.haveLet true
 
 /-- See also `bourbaki1975b` Chapter VII §1.1, Proposition 2 (ii). -/
 protected theorem weight_vector_multiplication (M₁ M₂ M₃ : Type*)
diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean
index 11aecab1ec..a209fdc975 100644
--- a/Mathlib/AlgebraicGeometry/Restrict.lean
+++ b/Mathlib/AlgebraicGeometry/Restrict.lean
@@ -35,10 +35,12 @@ section
 
 variable (X : Scheme)
 
+set_option linter.haveLet false in
 /-- `f ⁻¹ᵁ U` is notation for `(Opens.map f.1.base).obj U`,
   the preimage of an open set `U` under `f`. -/
 notation3:90 f:91 "⁻¹ᵁ " U:90 => (Opens.map (f : LocallyRingedSpace.Hom _ _).val.base).obj U
 
+set_option linter.haveLet false in
 /-- `X ∣_ᵤ U` is notation for `X.restrict U.openEmbedding`, the restriction of `X` to an open set
   `U` of `X`. -/
 notation3:60 X:60 " ∣_ᵤ " U:61 => Scheme.restrict X (U : Opens X).openEmbedding
diff --git a/Mathlib/MeasureTheory/Covering/Vitali.lean b/Mathlib/MeasureTheory/Covering/Vitali.lean
index 536f1a2dbd..e976f9c92f 100644
--- a/Mathlib/MeasureTheory/Covering/Vitali.lean
+++ b/Mathlib/MeasureTheory/Covering/Vitali.lean
@@ -192,6 +192,7 @@ theorem exists_disjoint_subfamily_covering_enlargment_closedBall [MetricSpace α
     exact ⟨c, cu, by simp only [closedBall_eq_empty.2 h'a, empty_subset]⟩
 #align vitali.exists_disjoint_subfamily_covering_enlargment_closed_ball Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall
 
+set_option linter.haveLet false in
 /-- The measurable Vitali covering theorem. Assume one is given a family `t` of closed sets with
 nonempty interior, such that each `a ∈ t` is included in a ball `B (x, r)` and covers a definite
 proportion of the ball `B (x, 3 r)` for a given measure `μ` (think of the situation where `μ` is ... -/
diff --git a/Mathlib/RingTheory/Kaehler.lean b/Mathlib/RingTheory/Kaehler.lean
index 1796e93347..052ed3af6a 100644
--- a/Mathlib/RingTheory/Kaehler.lean
+++ b/Mathlib/RingTheory/Kaehler.lean
@@ -481,10 +481,12 @@ noncomputable def KaehlerDifferential.kerTotal : Submodule S (S →₀ S) :=
       Set.range fun x : R => single (algebraMap R S x) 1)
 #align kaehler_differential.ker_total KaehlerDifferential.kerTotal
 
+set_option linter.haveLet false
 unsuppress_compilation in
 -- Porting note: was `local notation x "𝖣" y => (KaehlerDifferential.kerTotal R S).mkQ (single y x)`
 -- but not having `DFunLike.coe` leads to `kerTotal_mkQ_single_smul` failing.
 local notation3 x "𝖣" y => DFunLike.coe (KaehlerDifferential.kerTotal R S).mkQ (single y x)
+set_option linter.haveLet true
 
 theorem KaehlerDifferential.kerTotal_mkQ_single_add (x y z) : (z𝖣x + y) = (z𝖣x) + z𝖣y := by
   rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean
index ec92a0d3dc..6f3259b0d9 100644
--- a/Mathlib/SetTheory/Game/Basic.lean
+++ b/Mathlib/SetTheory/Game/Basic.lean
@@ -519,6 +519,7 @@ theorem quot_mul_neg (x y : PGame) : ⟦x * -y⟧ = (-⟦x * y⟧ : Game) :=
   Quot.sound (mulNegRelabelling x y).equiv
 #align pgame.quot_mul_neg SetTheory.PGame.quot_mul_neg
 
+set_option linter.haveLet false in
 @[simp]
 theorem quot_left_distrib (x y z : PGame) : (⟦x * (y + z)⟧ : Game) = ⟦x * y⟧ + ⟦x * z⟧ :=
   match x, y, z with
@@ -689,6 +690,7 @@ theorem one_mul_equiv (x : PGame) : 1 * x ≈ x :=
   Quotient.exact <| quot_one_mul x
 #align pgame.one_mul_equiv SetTheory.PGame.one_mul_equiv
 
+set_option linter.haveLet false in
 theorem quot_mul_assoc (x y z : PGame) : (⟦x * y * z⟧ : Game) = ⟦x * (y * z)⟧ :=
   match x, y, z with
   | mk xl xr xL xR, mk yl yr yL yR, mk zl zr zL zR => by

[eric-wieser]

I think the issue is that InfoTree.foldInfoM is a hack, and the right way to do it is to modify InfoTree.foldInfo to be monadic.

[adomani]

Eric, fair enough! Do you still think that this version is better or should I revert it to the one with the handcrafted MetaM state?

[github-actions[bot]]

PR summary 94894a93a9

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter	12	14	+2 (+16.67%)
Mathlib.Tactic	2144	2146	+2 (+0.09%)

Import changes for all files

Files	Import difference
There are 4048 files with changed transitive imports: this is too many to display!

---

Declarations diff

+ InfoTree.foldInfoM + areProp_toFormat + ghi + haveLetLinter + isHave? + nonPropHaves

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[joneugster]

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[mattrobball]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style