Zulip Chat Archive

Stream: new members

Topic: Curious tactic syntax

Pedro Minicz (Aug 16 2020 at 16:48):

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 (Aug 16 2020 at 16:50):

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

Floris van Doorn (Aug 16 2020 at 16:51):

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 (Aug 16 2020 at 16:53):

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

Pedro Minicz (Aug 16 2020 at 16:54):

I see! Thanks!

Scott Morrison (Aug 17 2020 at 01:06):

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 (Aug 17 2020 at 02:12):

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 (Aug 17 2020 at 07:50):

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

Reid Barton (Aug 24 2020 at 14:39):

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

Last updated: Dec 20 2023 at 11:08 UTC