Styling: tactic combinators vs (few) bullet points

Stream: new members

[Luigi Massacci]

Admittedly not the most important question, but suppose I have the following:

rw [stuff]
·   -- actual main stuff

-- 2 bullet points of silly checks, solvable by something like:
·  tac₁ ;  tac₂
·  tac₁ ;  tac₂

is this actually preferable to

rw [stuff]
any_goals (tac₁ ;  tac₂)
-- actual main stuff

?
Also, what is the preference vs <;> and all_goals (and I guess <;> try ( ) vs any_goals)?

[Kyle Miller]

The style is to write in a way where if any assumptions about what goals stuff produces changes, then you can read the tactic script and figure out what the intended proof structure was and repair it.

[Kyle Miller]

any_goals isn't good because it's not saying "this should close the goal"

It's also questionable because it's not clear whether it should apply to goals that were already there before rw

[Kyle Miller]

rw [stuff] <;> try · tac₁ ; tac₂ (or rw [stuff] <;> try tac₁; tac₂; done) is fairly robust

[Kyle Miller]

Or there's trying to make sure the case names are good and doing

rw [stuff]
case name1 | name2 => tac₁; tac₂
... main stuff ...

[Luigi Massacci]

Kyle Miller said:

rw [stuff] <;> try · tac₁ ; tac₂ (or rw [stuff] <;> try tac₁; tac₂; done) is fairly robust

Ahh, the point about giving information that the goal should be closed is quite convincing, and I like the option with done. Thank you!

[Kyle Miller]

There's also using the version of case in std where you can specify the types:

rw [stuff]
case _ : y = 0 | _ : y = 1 => tac₁; tac₂
... main stuff ...

[Joachim Breitner]

I wish rw would put the side goals first, so that you can return to the main stuff later. Or even better, explicit syntax for it as discussed in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20against.20.22multi-goal.20proofs.22/near/434777231 with more https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60on_sides.60.20tactic/near/434803235