why exactly are 1-line calc sections bad?

Stream: new members

[rzeta0]

I've been advised a few times that 1-line calc sections are not good.

Is it possible to explain why?

I vaguely recall something about "it messes up the parsing" but that doesn't seem plausible, given my albeit limited understanding of how languages work.

[Edward van de Meent]

i don't exactly understand why either... but empirically, it is true.

[Edward van de Meent]

take for example one of the codesnippets you sent

[Aaron Liu]

rzeta0 said:

example {x : ℝ} (hx : x ^ 2 + 2 * x - 3 = 0) : x = -3 ∨ x = 1 := by
  have h1 := by
    calc
      (x + 3) * (x - 1) = x ^ 2 + 2 * x - 3 := by ring
      _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  obtain ha | hb := h2
  left
  calc
    x = - 3 := by addarith [ha]
  right  -- <- error here "unexpected token 'calc'; expected ':='Lean 4"
  calc -- <-- error here "unexpected token 'calc'; expected ':='Lean 4"
    x = 1 := by addarith [ha]

[Etienne Marion]

These errors illustrate the fact that calc was not designed for one-line computations I think. The purpose of calc is to be able to decompose a computation between different steps in a paper-like way. It allows you to state each step clearly, while doing it without stating the steps might be harder (it is always easier to prove something in Lean when you told it what you want to prove beforehand, because it might be impossible to infer some data and this forces you to specify some arguments which might have been unnecessary otherwise). In the case of a one line though, the goal is already stated, so there is nothing to be gained with a one-line calc IMO.

[Edward van de Meent]

if you search public zulip channels for calc error, you will find that the parsing aspect is something that has been run into on multiple occasions.

[Aaron Liu]

I don't think this syntax should be valid.

example : 1 = 1 :=
  calc
      1 = 1 := rfl
    1 = 1 := rfl
    1 = 1 := rfl

[Aaron Liu]

Since you can do

example : 1 = 1 :=
  calc
    1 = 1 := rfl
  1 = 1 := rfl
  1 = 1 := rfl

when you have

example : 1 = 1
  calc
    1 = 1 := rfl
  someTactic

the someTactic gets parsed as a calc line, and then fails when there is no accompanying :=.
This is the source of all the errors coming from one-line calc blocks.

[Kevin Buzzard]

A 1-line calc is completely pointless, isn't it? calc x = y := by tactic is just the same as writing tactic, right?

[Aaron Liu]

yes

[Aaron Liu]

The problem is that calc supports indenting the first line freely, and then all the other lines must be lined up.

[Kyle Miller]

The underlying issue is that calc supports not having a := for the first line:

example : 1 = 1 := by
  calc
        1
    _ = 1 := by rfl

This might be something you're looking for @rzeta0, a way to do one-line calcs. You do it over two lines like so.

[Kyle Miller]

Or you could use exact show.

example : 1 = 1 := by
  exact show 1 = 1 by rfl

[Kyle Miller]

It might be possible to add a withPosition and some colGts to the syntax definition for calc help with the one-line calc problem.

[Yaël Dillies]

Kevin Buzzard said:

A 1-line calc is completely pointless, isn't it? calc x = y := by tactic is just the same as writing tactic, right?

Only if y is defeq to the RHS (and actually if x = y is synteq to the goal). Otherwise it's more like

transitivity y
. show x = _
  tactic

[rzeta0]

Thanks for the continuing replies - very insightful.

To be clear, I don't want to do 1-line calcs, I wanted to understand better what they actually are (they're different from the other structures like have and induction ) .. and when I asked the original question weeks ago I hadn't learned to just apply a tactic.

[rzeta0]

Just a naive suggestion - perhaps calc could have a more rigorous syntax to avoid the syntax errors? something like begincalc and endcalc or [ .. ] .. that sort of thing?

[Kyle Miller]

calc a = b := by tac is (pretty much) the same as

change a = b
tac

or exact show a = b by tac as a one-liner.

It ensures the goal is a = b, and then it runs the tactic.

If you know the goal is a = b, then there is no need for it, you just do tac.

[Aaron Liu]

I think the syntax should be "an optional first line without a :=, followed by one or more indentation-aligned lines with :=", instead of what it is now, which is "a first line that optionally has a :=, followed by zero or more indentation aligned lines with :=". In addition to solving the problems with 1-line calc, this also makes the zero-line calc invalid:

example : 1 = 1 := calc 1 -- this elaborates as `rfl`