unused tactic linter for `show`

Stream: mathlib4

[Robin Arnez]

I'm changing show to its documented behavior in lean4#7395; however, as a consequence "trivial" shows (i.e. shows that don't change the goal) get flagged by the unused tactic linter. Should show be added as an exception for this linter then to allow for shows as "checkpoints"? Example:

import Mathlib.Tactic.Linter.UnusedTactic

example (a b c : Nat) : a + b + c = a + (c + b) := by
  rw [Nat.add_assoc]
  show a + (b + c) = a + (c + b) -- warns: ... tactic does nothing
  rw [Nat.add_comm b]

[Damiano Testa]

In the online editor, there is no warning.

[Robin Arnez]

Yes, again, the warning occurs with this PR; the warning behavior can be compared to change today

[Damiano Testa]

Still, I think that it is a good idea to know when show is literally not doing anything, or when it is doing something.

[Damiano Testa]

The unusedTactic linter has a very strict notion of not doing anything. For instance, refine ?_ is doing something, according to the linter.

[Robin Arnez]

Yeah, the change with this PR for the unused tactic linter is that it no longer works like a refine but rather a change

[Kyle Miller]

Damiano Testa said:

Still, I think that it is a good idea to know when show is literally not doing anything, or when it is doing something.

Why should a show need to change the goal? It could be a reminder of what's being shown.

[Robin Arnez]

Maybe a better example that I found on mathlib (no attempt on making it an mwe, just for illustration):

theorem preimage_asSubtype (f : α →. β) (s : Set β) :
    f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s := by
  ext x
  simp only [Set.mem_preimage, Set.mem_setOf_eq, PFun.asSubtype, PFun.mem_preimage]
  show f.fn x.val _ ∈ s ↔ ∃ y ∈ s, y ∈ f x.val
  exact
    Iff.intro (fun h => ⟨_, h, Part.get_mem _⟩) fun ⟨y, ys, fxy⟩ =>
      have : f.fn x.val x.property ∈ f x.val := Part.get_mem _
      Part.mem_unique fxy this ▸ ys

The unused tactic linter warning implies that you should remove the show here.

[Robin Arnez]

But that's maybe not fair, since the show here helps for proof readability and to "show" intermediate states.

[Kyle Miller]

This show tactic is friendlier than guard_target, and it has a more sophisticated elaboration strategy that's more likely to succeed. The latter tactic is allowed by the linter, right?

[Damiano Testa]

My personal opinion is that when show is actually not doing anything, it should be flagged.

[Damiano Testa]

guard_target should (and I think is) allowed.

[Damiano Testa]

But that tactic is expected to not change the goal in any way, so calling it means "I know that this is not changing anything, but I still want to do it".

[Kyle Miller]

Can you substantiate that opinion? There's a clear benefit to discretionary shows.

[Kyle Miller]

(Oops, didn't see your substantiation.)

[Damiano Testa]

I would say that if you want to guarantee that the goal is something, you should use guard_target, not show.

[Damiano Testa]

I view show as a means to change the goal to something defeq to what is already there, but not identical.

[Robin Arnez]

That's what change is for though, isn't it?

[Damiano Testa]

Here is an example:

import Mathlib.Tactic.Linter.UnusedTactic

example (a b c : Nat) : 0 = 0 := by
  change _ -- useless, flagged
  change _ + 0 = _ -- not useless, not flagged
  sorry

[Kyle Miller]

I think I remember the argument about change being linted is that change sounds like it should change the goal.

[Damiano Testa]

I personally would not treat change and show differently and I think that the purpose of the unusedTactic linter is to let you know when some tactic can be omitted, unless the tactic is there to serve a goal that is not making progress towards a proof.

[Robin Arnez]

The thing about guard_target though is that it's more for tests (it's not even used in mathlib outside of MathlibTest) and is generally more awkward to write.

[Robin Arnez]

Besides, if you really wanted to make sure it has an effect, you can always use change

[Robin Arnez]

Okay, well, how should I then go about fixing the warnings in mathlib? Making show an exception was the original but should I instead use guard_target? Remove these tactic calls altogether?

[Damiano Testa]

As I think more about this, I think that my personal view is shifting to thinking that show and change should be merged into a single tactic. I personally do not see too much value in adding show midproof to help legibility: unless the proof is really trivial, reading lean code without looking at the infoview is not really what you should do to understand a proof.

[Damiano Testa]

My preference would be to remove the calls. But others may have a different view.

[Damiano Testa]

In some cases, set_option ... false in may ne a better solution.

[Robin Arnez]

Hmm let's maybe wait and see what other people think

[Kyle Miller]

@Damiano Testa I think one of the values of show is that it's a checkpoint after a heavy simp only [...] for example. It's less awkward than trying to phrase things using suffices.

I agree with Robin that guard_target is a testing-oriented tactic. I thought that it was in the unused tactic exception list because it's used heavily in test files and it would be inconvenient to have to add set_options there.

There are some differences between show and guard_target for elaboration too. Both show and change work harder to interleave elaboration and the defeq check to get some tricker instance problems to succeed, but guard_target, being a testing-oriented tactic, I think shouldn't try to absorb instances from the target while elaborating. Example:

example (p : Prop) [Decidable p] (hp : p) : (if p then 1 else 2) = 1 := by
  change (if _ then _ else _) = _
  -- ^ works
  guard_target = (if _ then _ else _) = _
  -- ^ doesn't work
  -- typeclass instance problem is stuck, it is often due to metavariables
  --   Decidable ?m.4386

Another perspective on this is: why should show not be allowed if we allow the show t from ... term when the expected type is known and exactly t?

[Kyle Miller]

One last thought: maybe mathlib can lint show to make sure that it doesn't change the goal?

The feature Robin has been working on is to make show select a goal. This will be disallowed by the stream-of-consciousness linter anyway. It seems reasonable to have a "this show should be a change linter".

[Damiano Testa]

I like the idea of show being linted to not change the goal and only use change for that. I'd be happy with that choice.

[Robin Arnez]

Yeah, I guess that would be a reasonable compromise. I'm probably not going to do this directly in the mathlib adaptation though but rather in a different PR. For now I'm just going to disable the unused tactic linter for show.

[Robin Arnez]

Oh, hmm since the change to use forks instead of write permission on mathlib, I can't actually push to the adaptation branch

[Robin Arnez]

Should I make a PR then?

[Johan Commelin]

Yes please!

[Robin Arnez]

Okay here: #25749. I actually decided to add the linter though

[Robin Arnez]

Just a quick confirmation: Is everybody fine with this change? The new behavior is that show doesn't get caught by the unused tactic linter (basically like before) but there is a mathlib style linter to warn if the show did actually change the goal.

[Eric Wieser]

Damiano Testa said:

I like the idea of show being linted to not change the goal and only use change for that. I'd be happy with that choice.

Isn't this inconsistent with term-mode show, which explicitly changes the goal?

[Robin Arnez]

I guess but for tactic mode there is an alternative, change, an for term mode there isn't

[Kyle Miller]

The term-mode show can explicitly change the expected type, but it's also not specifically for changing the expected type. I'm not sure there's an inconsistency.

Expected types are also somewhat different from goals. With a goal, you must produce a term of that type, and in contrast expected types are mere suggestions — it's up to elaborators to decide if the term they receive from elabTerm is ok.