Weekly linting log

Stream: mathlib4

[github mathlib4 bot]

Mathlib's nightly-testing branch (a778305ec3a679802f7dcfa64e2b903d4679ee21) regression run completed.
Warnings: 6

Warning counts

	Warning description
2	'have ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0 :=
1	'simp only [cons_append, isChain_cons_cons] at IH ⊢; grind' can be replaced with 'grind'
1	'simp only [Set.mem_toFinset]; grind' can be replaced with 'grind'
1	'rw [← card_pos]; grind' can be replaced with 'grind'
1	'rw [hn]; grind' can be replaced with 'grind'

[Kevin Buzzard]

What's the first warning?

[Edward van de Meent]

the warnings are:

'have ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0 :=
  by
  rw [StarOrderedRing.isStrictlyPositive_iff_spectrum_pos (R := ℝ) a] at ha
  grind; grind' can be replaced with 'grind'

and

'have ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0 :=
  by
  rw [StarOrderedRing.isStrictlyPositive_iff_spectrum_pos (R := ℝ) a] at ha
  grind; grind' can be replaced with 'grind'

[Edward van de Meent]

(dug through the logs)

[Alex Meiburg]

At https://github.com/leanprover-community/mathlib4-nightly-testing/blob/e7c30293bf22c84e003230699e8da7bd46c010ef/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean#L158, lines 142 and 158, the have := ... grind can be replaces with just a grind [log_smul] and grind [log_pow], it seems

[Chris Henson]

How is this linter intended to interact with <;>? Currently if you have a proof that does ... <;> have := ...; grind, each branch will lint individually. Is this intended? (I think it is fine to do this, just curious.)

[Kim Morrison]

Chris Henson said:

How is this linter intended to interact with <;>? Currently if you have a proof that does ... <;> have := ...; grind, each branch will lint individually. Is this intended? (I think it is fine to do this, just curious.)

This is relevant for the

'simp only [Set.mem_toFinset]; grind' can be replaced with 'grind'

table row above.

[Kim Morrison]

Besides this one, the others are cleaned up in #30528.

[github mathlib4 bot]

Mathlib's nightly-testing branch (9e574589c15b3b233d3223f1b35871a798cc2748) regression run completed.
Warnings: 2

Warning counts

	Warning description
1	'simp only [Set.mem_toFinset]; grind' can be replaced with 'grind'
1	'apply mul_left_injective₀ (hζ.sub_one_ne_zero (by omega)); grind' can be replaced with 'grind'

[github mathlib4 bot]

Mathlib's nightly-testing branch (88d330e19d35d91b0e5b0f6415a6939d00648f20) regression run completed.
Warnings: 4

Warning counts

	Warning description
1	'simp only [Set.mem_toFinset]; grind' can be replaced with 'grind'
1	'rw [← self_sub_monomial_natDegree_leadingCoeff]; grind' can be replaced with 'grind'
1	'have : Inhabited α := ⟨a⟩; grind' can be replaced with 'grind'
1	'apply mul_left_injective₀ (hζ.sub_one_ne_zero (by omega)); grind' can be replaced with 'grind'

[Kim Morrison]

2nd and 4th done in #30992. The 3rd one is incorrect. The 1st was discussed above: it only applies in one branch of a <;>.

[Anne Baanen]

I wanted to extend #29964 (don't warn if a tactic under a try combinator fails) to fix the 1st one, but it is more subtle than that. We'd have to correlate the TacticInfo across <;> branches, which I don't immediately see how to do...

[Anne Baanen]

My suspicion is that the 3rd one has to do with an instance cache not being reset somewhere, but I don't have time to investigate this in detail.

[Damiano Testa]

I think that the unreachable tactic stores the ranges of the tactics and then removes the ranges whenever something is used. This means that if a tactic is "shared", it counts as used if it is used at least once.

Maybe this machinery could do something similar? I have not actually inspected carefully how it works, though, so maybe this is already happening/unhelpful.

[Kim Morrison]

It's one spurious report in a not-that-important linter, let's not sink time into this.

A much cheaper solution would be to remove the <;> and write out both branches!

[Chris Henson]

Kim Morrison said:

A much cheaper solution would be to remove the <;> and write out both branches!

FWIW I enabled the mergeWithGrind linter for CSlib, taking this approach for <;> false positives. Same as here, I think it was one proof to change, but I actually appreciated it identifying a proof where only one branch needed extra theorems passed to grind. Arguably writing out the branches in extreme cases of this is better for readability (and potentially performance I'd guess).

[Kim Morrison]

Yeah, <;> where quite different things happen, that happen to be compressible into a single tactic call, has always seemed to me like the obfuscatory side of golfing.

[github mathlib4 bot]

Mathlib's nightly-testing branch (d6b7d986955032cac54ae3d348326c295d51adfd) regression run completed.
Warnings: 24

Warning counts

	Warning description
4	'simp [d]; grind' can be replaced with 'grind'
2	'simp only [Xor']; grind' can be replaced with 'grind'
2	'simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'; grind' can be replaced with 'grind'
2	'rw [nextCoeff_of_natDegree_pos (h₇ ▸ P.natDegree.succ_pos), h₇] at h₉; grind' can be replaced with 'grind'
1	'use (a :: l); grind' can be replaced with 'grind'
1	'specialize ih (v := insert x v); grind' can be replaced with 'grind'
1	'simp only [mem_setOf_eq]; grind' can be replaced with 'grind'
1	'simp only [mem_image, exists_exists_and_eq_and, mem_setOf_eq]; grind' can be replaced with 'grind'
1	'simp only [Set.mem_toFinset]; grind' can be replaced with 'grind'
1	'simp only [Functor.map_comp]; grind' can be replaced with 'grind'
1	'rw [← Ioc_diff_right]; grind' can be replaced with 'grind'
1	'rw [update_eq_iff]; grind' can be replaced with 'grind'
1	'rw [Finset.prod_insert hjs, Finset.prod_insert hjs]; grind' can be replaced with 'grind'
1	'intro h; grind' can be replaced with 'grind'
1	'have h_prod :
1	'have h3 := le_trans c a b; grind' can be replaced with 'grind'
1	'have : Inhabited α := ⟨a⟩; grind' can be replaced with 'grind'
1	'dsimp [f]; grind' can be replaced with 'grind'

[Kim Morrison]

Mostly dealt with in #31578.

[github mathlib4 bot]

Mathlib's nightly-testing branch (6a739275610fda3b4c420565ec194b100d14b81b) regression run completed.
Warnings: 7

Warning counts

	Warning description
1	'simp only [mem_setOf_eq]; grind' can be replaced with 'grind'
1	'simp only [Set.mem_toFinset]; grind' can be replaced with 'grind'
1	'simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'; grind' can be replaced with 'grind'
1	'rw [← Ioc_diff_right]; grind' can be replaced with 'grind'
1	'rw [@w' _ _ mX mY f']; grind' can be replaced with 'grind'
1	'have : Inhabited α := ⟨a⟩; grind' can be replaced with 'grind'
1	'convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i); grind' can be replaced with 'grind'

[github mathlib4 bot]

Mathlib's nightly-testing branch (5e87abc94ce4317581dbb90a82be193457516dbe) regression run completed.
Warnings: 10

Warning counts

	Warning description
1	'simp only [mem_setOf_eq]; grind' can be replaced with 'grind'
1	'simp only [Set.mem_toFinset]; grind' can be replaced with 'grind'
1	'simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'; grind' can be replaced with 'grind'
1	'rw [← Ioc_diff_right]; grind' can be replaced with 'grind'
1	'rw [nextCoeff_of_natDegree_pos (h₇ ▸ P.natDegree.succ_pos), h₇] at h₉; grind' can be replaced with 'grind'
1	'rw [@w' _ _ mX mY f']; grind' can be replaced with 'grind'
1	'have : Inhabited α := ⟨a⟩; grind' can be replaced with 'grind'
1	'convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i); grind' can be replaced with 'grind'
1	'cases hinj h.1; grind' can be replaced with 'grind'
1	'apply Nat.pow_le_pow_right (by decide); grind' can be replaced with 'grind'

[github mathlib4 bot]

Mathlib's nightly-testing branch (dc19f2a67ff55a2078ba23a4c1740a5eb0d50e41) regression run completed.
Warnings: 21

Warning counts

	Warning description
7	'ext; grind' can be replaced with 'grind'
3	'simp only [Set.mem_toFinset]; grind' can be replaced with 'grind'
1	'simp_rw [find?_eq_some_iff, Fin.find_spec h, lt_find_iff]; grind' can be replaced with 'grind'
1	'simp only [mem_setOf_eq]; grind' can be replaced with 'grind'
1	'simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'; grind' can be replaced with 'grind'
1	'simp only [CharP.cast_eq_zero, neg_zero, Icc_self, zero_add, Int.reduceNeg, union_insert, union_singleton, mem_insert,
1	'rw [← Ioc_diff_right]; grind' can be replaced with 'grind'
1	'rw [nextCoeff_of_natDegree_pos (h₇ ▸ P.natDegree.succ_pos), h₇] at h₉; grind' can be replaced with 'grind'
1	'rw [@w' _ _ mX mY f']; grind' can be replaced with 'grind'
1	'have : Inhabited α := ⟨a⟩; grind' can be replaced with 'grind'
1	'convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i); grind' can be replaced with 'grind'
1	'cases hinj h.1; grind' can be replaced with 'grind'
1	'apply Nat.pow_le_pow_right (by decide); grind' can be replaced with 'grind'

[github mathlib4 bot]

Mathlib's nightly-testing branch (b7d2fa97710d4c43ddee0c0dfb1b4595bbc767e5) regression run completed.
Warnings: 20

Warning counts

	Warning description
7	'ext; grind' can be replaced with 'grind'
3	'simp only [Set.mem_toFinset]; grind' can be replaced with 'grind'
1	'simp_rw [find?_eq_some_iff, Fin.find_spec h, lt_find_iff]; grind' can be replaced with 'grind'
1	'simp only [mem_setOf_eq]; grind' can be replaced with 'grind'
1	'simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'; grind' can be replaced with 'grind'
1	'simp only [CharP.cast_eq_zero, neg_zero, Icc_self, zero_add, Int.reduceNeg, union_insert, union_singleton, mem_insert,
1	'rw [← Ioc_diff_right]; grind' can be replaced with 'grind'
1	'rw [nextCoeff_of_natDegree_pos (h₇ ▸ P.natDegree.succ_pos), h₇] at h₉; grind' can be replaced with 'grind'
1	'rw [@w' _ _ mX mY f']; grind' can be replaced with 'grind'
1	'convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i); grind' can be replaced with 'grind'
1	'cases hinj h.1; grind' can be replaced with 'grind'
1	'apply Nat.pow_le_pow_right (by decide); grind' can be replaced with 'grind'

[Kim Morrison]

Mostly dealt with in #32713

[github mathlib4 bot]

Mathlib's nightly-testing branch (3ea6690c3470d61c7d4fd71e7efd6336a6d05ffd) regression run completed.
Warnings: 13

Warning counts

	Warning description
2	'field_simp; grind' can be replaced with 'grind'
1	'subst hi₁; grind' can be replaced with 'grind'
1	'subst h'; grind' can be replaced with 'grind'
1	'simp only [setOf_subset_setOf, forall_exists_index, and_imp]; grind' can be replaced with 'grind'
1	'simp only [extract_append]; grind' can be replaced with 'grind'
1	'simp only [Subtype.exists, exists_and_right] at hu; grind' can be replaced with 'grind'
1	'simp only [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, true_and] at mf'; grind' can be replaced with 'grind'
1	'rw [nextCoeff_of_natDegree_pos (h₇ ▸ P.natDegree.succ_pos), h₇] at h₉; grind' can be replaced with 'grind'
1	'refine ⟨fun h ↦ by constructor <;> congr, fun h_eq => ?_⟩; grind' can be replaced with 'grind'
1	'ext; grind' can be replaced with 'grind'
1	'convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i); grind' can be replaced with 'grind'
1	'apply mem_image_of_mem; grind' can be replaced with 'grind'

[Kim Morrison]

Mostly dealt with in #32893.

[Chris Henson]

Probably too messy to be worth detecting automatically, but do you know if any of these are the same proof requiring changes over time? When we were running this linter for every day in CSLib's nightly testing I recall seeing a bit of this.

[Kim Morrison]

I'm sorry, I don't understand what you mean by "the same proof requiring changes over time".

[Chris Henson]

I've had the experience that between different nightlies/releases this linter will suggest removing a line that later needs to be added back.

[Kim Morrison]

Interesting. I haven't seen that; if you see it again please let me know!

[Violeta Hernández]

How do you run this linter on another repository?

[Chris Henson]

The linter set is linter.weeklyLintSet, which currently just has linter.tacticAnalysis.mergeWithGrind. As I learned by experience, you don't want to set this by default for performance reasons, as it does make grind run in duplicate. For CSLib we set up something similar to Mathlib's .github/workflows/weekly-lints.yml which once a week adds the option to the lakefile and then builds.