Zulip Chat Archive

Stream: lean4

Topic: indenting after "by"

Dan Velleman (Nov 13 2022 at 17:27):

These two examples work:

example (x : Nat) (h : x = 1) : 2 * x = 2 :=
  have h2 : 2 * x = 2 := by
    rw [h]
  h2

example (x : Nat) (h : x = 1) : 2 * x = 2 :=
  calc
    2 * x = 2 := by rw [h]

This one doesn't:

example (x : Nat) (h : x = 1) : 2 * x = 2 :=
  calc
    2 * x = 2 := by
      rw [h]

This one does:

example (x : Nat) (h : x = 1) : 2 * x = 2 :=
  calc
    2 * x = 2 := by
                  rw [h]

I'm trying to figure out what the rules are for indenting after by. It appears that the rules after have are different from the rules after calc. Can someone explain what the rules are?

Sebastian Ullrich (Nov 13 2022 at 17:49):

This is probably because of https://github.com/leanprover/lean4/pull/1811 (/cc @Adrien Champion). It looks like we should special-case by in the calcStep parser.

Adrien Champion (Nov 13 2022 at 21:40):

Yeah @Mario Carneiro pointed something similar to me earlier

Adrien Champion (Nov 13 2022 at 22:24):

So what's happening is that calc does a withPosition on the RHS of the :=:

Adrien Champion (Nov 13 2022 at 22:26):

I'm not completely sure why it does that, but then by's tactics need to be colGt that position because of my PR

Adrien Champion (Nov 13 2022 at 22:27):

@Mario Carneiro (correct me if I'm wrong) and I feel like this withPosition on the RHS should not be there, we're trying to understand whether it is important or not

Adrien Champion (Nov 13 2022 at 22:30):

Also, sorry if my PR caused some confusion :crying_cat:

Mario Carneiro (Nov 13 2022 at 22:30):

it looks like that withPosition has been there from the beginning, cc: @Sebastian Ullrich

Mario Carneiro (Nov 13 2022 at 22:32):

If you really want to use line indentation @Adrien Champion, one way to accomplish that would be a combinator withPositionAtLineStart(p) which sets the position to the first non-whitespace character in the line

Adrien Champion (Nov 13 2022 at 23:44):

@Mario Carneiro and myself's current plan is to just remove the withPosition in calcStep, which solves the issue but makes custom-aligned calc lines like

theorem foo : t1 = t4 :=
  calc
    t1 = t2 := pf12
     _ = t3 := pf23
     _ = t4 := pf34

illegal, it would need to be rewritten as

theorem foo : t1 = t4 :=
  calc
    t1 = t2 := pf12
    _ = t3 := pf23
    _ = t4 := pf34

or

theorem foo : t1 = t4 :=
  calc
    t1 = t2 := pf12
    _  = t3 := pf23
    _  = t4 := pf34

if you're feeling fancy, which I feel is a fair tradeoff

Sebastian Ullrich (Nov 14 2022 at 08:42):

Sure, the last example looks like our conventional formatting for patterns

Adrien Champion (Nov 14 2022 at 09:16):

I tend to see the first one a lot more, where the LHS is right-aligned, but maybe that's a coincidence

Sebastian Ullrich (Nov 14 2022 at 09:26):

I can't say I see calc at all in the code I'm usually looking at, so I don't know what's more common

Dan Velleman (Nov 14 2022 at 14:37):

If the left side of the first equation (t1 in examples above) is long, then the third possibility will look a little funny, with a large gap between _ and =. But I can get used to it.
I suspect the first and second are more common than the third, but I don't really know. Here are two examples from Chapter 7 of "Theorem Proving in Lean 4":

    calc m + succ n = succ (m + n) := rfl
                  _ = succ (n + m) := by rw [ih]
                  _ = succ n +  m  := sorry)

     calc succ n + succ m = succ (succ n + m) := rfl
           _  = succ (succ (n + m))           := by rw [ih]
           _  = succ (n + succ m)             := rfl)

Sebastian Ullrich (Nov 14 2022 at 14:40):

How would you format the first example if the tactic step took multiple lines?

Dan Velleman (Nov 14 2022 at 14:49):

Do you mean would I indent further than the _, or even the =? Yes, my instinct would be to make the tactic proof not interfere, visually, with the sequence of equations, so I would probably want to indent past the =. Which means I would probably use the style of the second example, with the lines after the first not indented so far.
Is something like the following allowed?

    calc m + succ n
        = succ (m + n) := rfl
      _ = succ (n + m) := by rw [ih]
      _ = succ n +  m  := sorry

Sometimes, when writing calculational proofs in LaTeX, I have used that style if the formulas were long.

Adrien Champion (Nov 17 2022 at 10:07):

The fix where we remove the withPosition in calcStep accounts for both styles above

Adrien Champion (Nov 17 2022 at 10:07):

I prepared a PR and added a few tests inspired by these examples:

Adrien Champion (Nov 17 2022 at 10:08):

In particular these two:

Adrien Champion (Nov 17 2022 at 14:34):

FYI: https://github.com/leanprover/lean4/pull/1844

Sebastian Ullrich (Nov 17 2022 at 14:38):

It would be good to have more opinions on whether the new style is acceptable (see PR tests). Just to reiterate, special-casing by in calc would allow us to keep the old style (as long as you indent your tactics more than the next calc line).

Dan Velleman (Nov 17 2022 at 16:05):

Will the example from my original message work with this fix? Perhaps something like this could be added to the test file:

theorem foo : t1 = t4 :=
  calc
    t1 = t2 := pf12
    _  = t3 := by
      exact pf23
    _  = t4 := pf34

Mario Carneiro (Nov 17 2022 at 18:36):

yes, that will work

Adrien Champion (Nov 18 2022 at 08:00):

Dan Velleman said:

Will the example from my original message work with this fix? Perhaps something like this could be added to the test file:

theorem foo : t1 = t4 :=
  calc
    t1 = t2 := pf12
    _  = t3 := by
      exact pf23
    _  = t4 := pf34

Added your example as a test thanks :smile:

Last updated: Dec 20 2023 at 11:08 UTC