Read and repair an error
Preserve the valid part of a multi-step proof and repair its first error.
In this course 11 / 14
The Goal panel shows what remains to prove. The target follows ⊢. When there are parameters or hypotheses, they appear above it. A line such as n : Nat introduces a number; it does not tell you which number it is.
An error does not always mean the statement is false. It can mean the tactic you tried does not establish it. An unknown name can be a spelling error. An unsolved goals error means every step worked but the proof has more work to do, and Lean prints exactly what is left.
Read the first error before changing the code. Problems links an error to its line in the editor. After editing, run another check: the previous result describes the previous code.
The starter below successfully unfolds increase, then calls a misspelled arithmetic tactic. omega is an automatic prover for linear arithmetic over Nat and Int: it combines hypotheses such as a ≤ b with addition, subtraction and constants, and either closes the goal or reports that it cannot. Preserve the useful first step and repair only the unknown name.
Worked example
def addTwo (n : Nat) : Nat := n + 2
-- The first line is useful; the second name is misspelled:
-- example (n : Nat) : addTwo n ≥ n := by
-- unfold addTwo
-- omego
example (n : Nat) : addTwo n ≥ n := by
unfold addTwo
omegaThe first tactic succeeds before the typo stops the proof. Your repair follows the same pattern on a theorem with variables and a hypothesis.
A multi-step proof can make progress before it fails. Preserve the accepted steps, repair the first reported error and check the whole proof again.
Repair the misspelled second tactic without removing the unfolding step, then verify the general inequality.
Suggested steps
- Keep the successful unfolding step (done)
- Replace
omegowith the arithmetic tactic
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