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.

[github mathlib4 bot]

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

Warning counts

	Warning description
3	'ext; grind' can be replaced with 'grind'
2	'simp [h] at hs; grind' can be replaced with 'grind'
1	'simp only [Finset.mem_Ioc, Finset.mem_range_succ_iff] at hi ⊢; 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	'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'

[github mathlib4 bot]

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

Warning counts

	Warning description
3	'ext; grind' can be replaced with 'grind'
2	'simp [h] at hs; grind' can be replaced with 'grind'
1	'simp only [Finset.mem_Ioc, Finset.mem_range_succ_iff] at hi ⊢; 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	'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'

[github mathlib4 bot]

Mathlib's nightly-testing branch (d55eaa8cc83e0ecbcbd6a552d5994acd3c4c688f) regression run completed.
Warnings: 11

Warning counts

	Warning description
3	'ext; grind' can be replaced with 'grind'
2	'simp [h] at hs; grind' can be replaced with 'grind'
1	'simp only [Finset.mem_Ioc, Finset.mem_range_succ_iff] at hi ⊢; 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	'haveI := b.neZero; grind' can be replaced with 'grind'
1	'haveI := a.neZero; 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'

[github mathlib4 bot]

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

Warning counts

	Warning description
4	'ext; grind' can be replaced with 'grind'
2	'simp [h] at hs; grind' can be replaced with 'grind'
1	'simp; grind' can be replaced with 'grind'
1	'simp only [mem_union, mem_setOf_eq, kl, kr]; grind' can be replaced with 'grind'
1	'simp only [Finset.mem_Ioc, Finset.mem_range_succ_iff] at hi ⊢; grind' can be replaced with 'grind'
1	'rw [← hsum'] at hsum; 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 [hq.2.1] at h₂; grind' can be replaced with 'grind'
1	'rw [h]; grind' can be replaced with 'grind'
1	'rw [getElem?_append_right (by simp [Nat.le_sub_one_of_lt j_lt_j']), getElem?_drop]; grind' can be replaced with 'grind'
1	'ring_nf; grind' can be replaced with 'grind'
1	'intro; grind' can be replaced with 'grind'
1	'haveI := b.neZero; grind' can be replaced with 'grind'
1	'haveI := a.neZero; grind' can be replaced with 'grind'
1	'have : √2 ^ 2 = 2 := by norm_num; grind' can be replaced with 'grind'
1	'grw [hr hx]; 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	'change #(insert _ <
1	'by_contra! h; grind' can be replaced with 'grind'
1	'apply mem_image_of_mem; grind' can be replaced with 'grind'

[Chris Henson]

I have opened #34121 addressing most of these.

[Chris Henson]

Thanks for reviewing quickly! I have two questions regarding the cases I left out:

• What is the preferred way to mark something to be ignored by the mergeWithGrind linter? It would be nice to mark places where we currently ignore the linter for performance reasons. You could do this with an #adaptation_note attached to the grind call, does that seem appropriate?
• docs#Associated.prod gives an odd false positive, which I think is maybe incompatibility between how convert/convert_to and the linter work with mvars? (Just a guess, I didn't go compare their implementations)

[Anne Baanen]

1: Wouldn't set_option linter.tacticAnalysis.mergeWithGrind false in ... (plus a comment explaining that this is not merged for performance reasons) work too? Probably choose a standard format for the comment, so that the grind developers can easily find test cases.

[Anne Baanen]

2: This should be considered a bug in the linter. My schedule is busy this week but hopefully I can check it out next week if that is important for you.

[Chris Henson]

1. This works too, and is probably better because searching for the linter option is straightforward.
2. I'd call this very low priority as it happens on one theorem and is just a tiny bit of CI noise. I'm happy to take a stab at it myself if you'd like.

[Anne Baanen]

2: Sounds good! Distributing more knowledge of the tactic analysis linters is a good plan, I'd be happy to help out if you get stuck anywhere :)

[github mathlib4 bot]

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

Warning counts

	Warning description
1	'simp [Opens.forall]; 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'

[github mathlib4 bot]

Mathlib's nightly-testing branch (20310f506a423528948d509cfa22adc6d4e98936) regression run completed.
Warnings: 14

Warning counts

	Warning description
3	'simp; grind' can be replaced with 'grind'
1	'simp only [Nat.succ_eq_add_one] at this; grind' can be replaced with 'grind'
1	'simp [t']; grind' can be replaced with 'grind'
1	'simp [Opens.forall]; grind' can be replaced with 'grind'
1	'simp [K, sUnion_eq_biUnion] at hJs ⊢; grind' can be replaced with 'grind'
1	'norm_cast at this; grind' can be replaced with 'grind'
1	'have key :=
1	'have := ne_zero_of_dvd_ne_zero hn hd; grind' can be replaced with 'grind'
1	'have : c ≠ d :=
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 :bot:]

#34714

[github mathlib4 bot]

Mathlib's nightly-testing branch (efc0e39ef9a2a927977844acbabd01dc95fe5987) regression run completed.
Errors: 2

Warnings: 11

Error counts

	Error description
1	error: Lean exited with code 1
1	Application type mismatch: The argument

Warning counts

	Warning description
3	'simp; grind' can be replaced with 'grind'
2	'ext; grind' can be replaced with 'grind'
1	'norm_cast at this; grind' can be replaced with 'grind'
1	'have key :=
1	'convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i); grind' can be replaced with 'grind'
1	'convert vol_sum with z; grind' can be replaced with 'grind'
1	'by_contra!; grind' can be replaced with 'grind'
1	'apply mem_image_of_mem; grind' can be replaced with 'grind'

[github mathlib4 bot]

Mathlib's nightly-testing branch (3bbc5c706c3a2ef00ded08af13c3f36be6e58a65) regression run completed.
Errors: 2

Warnings: 13

Error counts

	Error description
1	error: Lean exited with code 1
1	Application type mismatch: The argument

Warning counts

	Warning description
3	'simp; grind' can be replaced with 'grind'
2	'ext; grind' can be replaced with 'grind'
1	'simp only [map_mul, e', map_zero]; grind' can be replaced with 'grind'
1	'norm_cast at this; grind' can be replaced with 'grind'
1	'have key :=
1	'convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i); grind' can be replaced with 'grind'
1	'convert vol_sum with z; grind' can be replaced with 'grind'
1	'convert this; grind' can be replaced with 'grind'
1	'by_contra!; grind' can be replaced with 'grind'
1	'apply mem_image_of_mem; grind' can be replaced with 'grind'

[Chris Henson]

In addressing these in #35490, I found the failure in docs#IndexedPartition.coarserPartition interesting, because the reason it fails is that removing a by_contra! changes the this used in the call to grind.

I ended up rewriting the proof in a way I think is better, but the fact that these lines of the log have both an error and warning from the linter seem like a bug in the try/catch logic, right?

[Chris Henson]

(I never got around to looking into the last bug I mentioned above, but I'd still like to look into these since they're low priority and a chance for me to learn more about the tactic analysis framework.)

[Kim Morrison]

Yes, that sounds like a bug! I'll leave it for you to investigate unless you tell me otherwise. :-)

[github mathlib4 bot]

Mathlib's nightly-testing branch (6466c770d151531dc8ce2903db0a959fd582439e) regression run completed.
Warnings: 11

Warning counts

	Warning description
4	'use F; grind' can be replaced with 'grind'
2	'simp; grind' can be replaced with 'grind'
2	'have := mx.2 (hs _ mx.1); grind' can be replaced with 'grind'
2	'convert this (j : Fin (k + 1)) (by grind) using 3; grind' can be replaced with 'grind'
1	'obtain ⟨rfl⟩ : q = -1 :=