mathlib-preferred calc style

Stream: mathlib4

[Jireh Loreaux]

I'm currently rewriting / updating the style guide for the website. The calc syntax has changed slightly, and I'm wondering about what we consider the mathlib-preferred style for calc proofs. Of course, we probably want to allow some flexibility as with Lean 3, and calc mandates some style in order to parse properly, but the questions remains, "what is(are) the preferred style(s)?"

Some questions to consider:

1. Does calc itself go on (a) it's own line, (b) the end of the previous line (as with by), or (c) with the first LHS?
2. do we try to line up the relations (e.g., =)? what about the justifications :=?
3. how are _ justified? (left, right)
4. does the first LHS/RHS pair go on one line, or separate lines?

If I were going to suggest a style myself it would be (1. (b), 2. yes, no, 3. left, 4. separate), with the option to override any of these in situations where the expressions involved and/or justifications are short. This would lead to calc style that looks like:

have := calc
  some_big_long_term_here
    = the_second_term := first_eq_second
  _ ≤ the_third_term := by
    some
    sequence
    of
    tactics
  _ ≤ the_fourth_term := by h

and since these are small, this might be rewritten as:

have :=
  calc
    some_big_long_term_here = the_second_term := first_eq_second
    _                       ≤ the_third_term  := by some; sequence; of; tactics
    _                       ≤ the_fourth_term := by h

[Anatole Dedecker]

Is this second block supposed to be

have := calc
  some_big_long_term_here = the_second_term := first_eq_second
  _                       ≤ the_third_term  := by some; sequence; of; tactics
  _                       ≤ the_fourth_term := by h

[Jireh Loreaux]

well, I was just showing that it has the option to be different when everything is short and sweet (under my suggestion), so no, the calc placement was intentional.

[Anatole Dedecker]

Ah okay, I thought you only wanted flexibility on 2 3 4

[Anatole Dedecker]

Otherwise I think I agree with you.

[Anatole Dedecker]

I would say that making 1(b) a harder rule than the other ones would seem logical because of the parallel with by, but I don't have a strong opinion about it

[Jireh Loreaux]

You mean 1(b)?

[Anatole Dedecker]

Yes

[Eric Wieser]

I'll throw in another possible style:

have := calc
  some_big_long_term_here = _ := first_eq_second
  the_second_term         ≤ _ := by some; sequence; of; tactics
  the_third_term          ≤ the_fourth_term := by h

(mainly as a joke!)

[Jon Eugster]

have := calc
      some_big_long_term_here -- 1)
    = the_second_term := first_eq_second
  _ ≤ the_third_term := by
      some -- 2)
      sequence
      of
      tactics
  _ ≤ the_fourth_term := by h

two more (independent) options of alignment. Not even sure its legal to indent the first line though, so maybe not:thinking:

[Richard Copley]

It's allowed. Also allowed:

have := calc some_big_long_term_here
  _ = the_second_term := first_eq_second
  _ ≤ the_third_term  := by some; sequence; of; tactics
  _ ≤ the_fourth_term := by h

[Eric Wieser]

Jon Eugster said:

two more (independent) options of alignment. Not even sure its legal to indent the first line though, so maybe not:thinking:

I like 1) (as it makes the first line consistent with remaining lines) but not 2) (as it makes it harder visually separate the statement and proof

[Mario Carneiro]

(1) is not recommended, because it has a confusing behavior if you have a sequence of tactics in the proof (I'm not sure if it was deliberate but using first_eq_second instead of by some sequence of tactics on the first line is hiding some issues here)

[Mario Carneiro]

if you want to get all the terms lined up, you want

have := calc
      some_big_long_term_here
  _ = the_second_term := by
    tactic
    sequence
  _ ≤ the_third_term := by
    some
    sequence
    of
    tactics
  _ ≤ the_fourth_term := by h