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, rfl when the two sides compute to the same thing, or a hypothesis by itself. 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]
At the start of the proof on line 1. Everything above ⊢ may be used; the line below it is what must be proved.
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