| ← Ch. 3: Propositions & Proofs | Table of contents | Ch. 5: Rigor Check → |
Writing proof terms directly (as in Chapter 3) quickly becomes hard to manage. Instead,
Lean provides tactic mode, entered with by, in which a “goal” is
worked step by step, much as one would write a proof on paper. This chapter’s
real subject is not the list of tactics below, but how to work a goal
whose proof is not yet known, since that is the skill the rest of
the book practices. The tactic reference is secondary: read it once, then
return to it as needed. (For links to the official docs for
every tactic named in this chapter, see the
tactic and library reference.)
Learning objectives. By the end of this chapter, read a Lean goal
state, use intro/exact/apply/rw to work a goal one step at a time,
diagnose a failed tactic from its error message, use induction/cases/
constructor/unfold on inductively-defined data, and carry out a full
inductive proof (Nat.add’s commutativity) from scratch.
Sections
- The goal state, and a worked strategy session
- Core tactics
- Reading a tactic failure, and
sorry - More tactics:
simp,constructor,cases,induction,unfold - Worked example: proving
Nat.addis commutative from scratch - Exercises
| ← Ch. 3: Propositions & Proofs | Table of contents | Ch. 5: Rigor Check → |