Multiple goals and linter.unnecessarySimpa

Stream: new members

[Nico]

I noticed that if a goal can be closed by simp and another by simpa then closing both using a single simpa statements triggers linter.unnecessarySimpa as in:

example {P : Prop} (h : P) : true ∧ P := by
  apply And.intro <;> simpa

In this case simp does not work (because the second goal requires assumption) and the warning message try 'simp' instead of 'simpa' is confusing. But I wonder if the warning could be disabled altogether when closing multiple goals.

Of course this particular example can take a simpler form:

example {P : Prop} (h : P) : true ∧ P := ⟨by simp, by simpa⟩

But I have encountered this pattern with several tactics which create multiple goals (by_cases, rewrite, split...)

Any advice? In particular:

• is there a better way to solve some goals by simp and others by simpa in a single statement?
• would disabling the warning as I suggest even be feasible? (I tried to follow the code in src/Lean/Elab/Tactic/Simpa.lean but I am not sure)
• would there be cases where disabling the warning as I suggest would be undesirable?

[Damiano Testa]

If you are using Batteries, an alternative is to use the <;> [...;...] combinator as follows:

import Batteries

example {P : Prop} (h : P) : true ∧ P := by
  apply And.intro <;> [simp; simpa]

[Damiano Testa]

The tactic is docs#Batteries.Tactic.seq_focus.

[Damiano Testa]

As a matter of personal preference, I am not a huge fan of the <;> combinator and its friends. They certainly avoid code duplication, which is great. However, using them for complicated proofs (which is certainly not the case in what you mention above), produces code that is hard to maintain.

[Damiano Testa]

From this perspective, the seq_focus above is better: it tells you explicitly what you are doing in each branch at the (small) cost of writing a few extra characters.

[Nico]

thanks! this tactic is a neat trick :thumbs_up:
I like a short proof and <;> is great for that, but I am starting to see what you mean :sweat_smile:
modifying a proof with <;> often requires me to unfold all the cases, rewite some of them and find a way to fold them back...

[Damiano Testa]

Right: if you are doing this once, it is ok. If you later start refactoring and some branch breaks, it becomes a mess to maintain.