I am learning to use the Lean 4 proof assistant. I have a simple question about what the underscore symbol _ does in the following context:
The following example (src) works fine.
example {p q : ℚ} (h1 : p - 2 * q = 1) (h2 : q = -1) : p = -1 :=
calc
p = (p - 2 * q) + (2 * q) := by ring
_ = (1) + (2 * -1) := by rw [h1,h2]
_ = -1 := by ring
However, as a beginner, I'm tempted to use actual variable name p at the start of each line as follows:
example {p q : ℚ} (h1 : p - 2 * q = 1) (h2 : q = -1) : p = -1 :=
calc
p = (p - 2 * q) + (2 * q) := by ring
p = (1) + (2 * -1) := by rw [h1,h2]
p = -1 := by ring
gives the following error:
invalid 'calc' step, left-hand-side is
p : ℚ
previous right-hand-side is
p - 2 * q + 2 * q : ℚ
Q: why is this?
I would have expected p = to be valid and justified as the start of each proof line, and that _ = merely to be a shorthand for "previous" much like we write pen and paper proof where we omit the LHS for all but the first line.
Clearly _ is doing something I don't understand or expect.
My Analysis
I haven't found an answer - most of the online tutorials and guides are too advanced and assume we know simple stuff like this.
My attempt to understand is as follows:
so there shouldn't be an error.
As the error message implies, the expected thing you are supposed to put there is p - 2 * q + 2 * q. That is, lean wants you to write something of the form
calc
a = b := <proof of a = b>
b = c := <proof of b = c>
c = d := <proof of c = d>
which is itself a proof of a = d. The reason is because we want the proofs on the other side of the := to be proofs of the expressions on the left of the :=. Since the LHS of each line is the RHS of the previous line, you can leave off all the LHS's except the first and they will be inferred, and this is the standard style. (Actually you can even leave off the first LHS and the last RHS, if they can be inferred from the goal.)