Curious tactic syntax

Stream: new members

[Pedro Minicz]

Exploring mathlib I found the following proof:

lemma mul_self_pos {a : α} (ha : a ≠ 0) : 0 < a * a :=
by rcases lt_trichotomy a 0 with h|h|h;
   [exact mul_pos_of_neg_of_neg h h, exact (ha h).elim, exact mul_pos h h]

What is that syntax in the last line? I've never seen a tactic block surrounded by square brackets before.

[Kevin Buzzard]

There are three goals and I guess each tactic in the list solves one goal

[Floris van Doorn]

tac0; [tac1, tac2, ... ] indeed applies tac0 and then applies tac1 to the first subgoal generated by tac0, tac2 to the second subgoal, and so on. I think it fails if you give an incorrect number of tactics.

[Floris van Doorn]

Coq has similar syntax, but theirs has more bells and whistles than Lean's.

[Pedro Minicz]

I see! Thanks!

[Scott Morrison]

Can I suggest not using it much? It seems like an over-strenuous effort to reduce LOC, compared to just a begin ... end block and some braces. :-)

[Floris van Doorn]

I agree with Scott.
I myself only use it in the form t0; [t1, t2, t3]; t4. This is not the best proof style, but in some boring proofs it seems fine.

[Chris Wong]

If it's so discouraged, would it be worth removing it from the language altogether?

[Reid Barton]

Since this was mentioned here I've been noticing that it's pretty useful actually.