Rewrite through a chain
Record each step of an equality argument in a readable calc proof.
In this course 10 / 13
A single rw hides the route it takes. When an argument has several equalities in a row, a calc block writes each intermediate expression down, and every line supplies its own justification.
The first line of a calc states the first step in full, for example calc a + 1 = b + 1 := by rw [hab]. Each later line starts with an underscore, which stands for the right-hand side of the line before, and states only where the next step goes.
This is more informative than asking automation to normalize everything. A reader sees that the argument first moves from a to b, then from b to c, and when a step is wrong, Lean reports that line and not the whole chain.
The justification of each step is an ordinary proof, so any tactic can appear there: a rewrite, omega for arithmetic, or rfl. The additions by one are deliberately carried through the chain, because rewriting works inside a larger expression.
Worked example
example (x y z : Nat) (hxy : x = y + 1) (hyz : y = z) : x = z + 1 := by
calc x = y + 1 := by rw [hxy]
_ = z + 1 := by rw [hyz]Two steps, each with its own reason. Your exercise has the same shape with the additions on both sides of the goal.
Equality is a substitution rule. calc turns several substitutions into a proof whose intermediate steps remain visible.
Use hab and hbc in a two-step calc proof from a + 1 to c + 1.
Suggested steps
- Open a
calcchain ata + 1 - Justify the first step
- Continue from
_and justify the second step
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct