verifying-crypto-with-lean/chapters/ch04-tactics.tex

\chapter{Tactics: Proving as a Dialogue}
\label{ch:tactics}

\section{From programs to conversations}

Here is the problem with everything you learned in the last chapter: a real
correctness proof for field multiplication --- the theorem this book is
climbing toward --- would, written as a raw proof program, be a program the
size of a small compiler. Nobody writes those by hand. (Chapter~\ref{ch:pat}'s
handcrafted terms were honest work; honest work does not scale.)
Instead, Lean offers \emph{tactic mode}: an interactive dialogue where you
issue commands and Lean builds the proof program for you, step by step,
showing you the remaining work after each move.

You enter the dialogue with the keyword \lean{by}:

\begin{lstlisting}[language=Lean]
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
  intro h
  constructor
  · exact h.2
  · exact h.1
\end{lstlisting}

Place your cursor after \lean{by} in the editor and Lean shows the
\textbf{goal state} --- the exact logical situation at that point:

\begin{lstlisting}
P Q : Prop
⊢ P ∧ Q → Q ∧ P
\end{lstlisting}

Everything above the turnstile \(\vdash\) is what you \emph{have} (the
context); the line after it is what you \emph{owe} (the goal). Every tactic
transforms this picture. After \lean{intro h}, the hypothesis moves above the
line; after \lean{constructor}, the goal splits in two. Proving becomes a
game whose board you can always see.

\begin{bigidea}
A tactic proof is a \textbf{recorded conversation with the goal state}. The
skill of proving is not memorizing tactic names --- it is learning to
\emph{read the goal state} and recognize which of a handful of moves makes it
simpler. Below is the core vocabulary; it covers the vast majority of every
proof in the real Ed25519 development.
\end{bigidea}

\begin{center}
\begin{tabular}{@{}lll@{}}
\toprule
\textbf{Tactic} & \textbf{When the goal looks like...} & \textbf{Effect} \\
\midrule
\lean{intro h}   & \lean{P → Q}, \ \lean{∀ x, P x} & assume it; name the evidence \\
\lean{exact e}   & anything      & finish: \lean{e} is a proof of the goal \\
\lean{apply f}   & \lean{Q}, given \lean{f : P → Q} & reduce the goal to \lean{P} \\
\lean{constructor} & \lean{P ∧ Q}, \lean{P ↔ Q}, ... & split into pieces \\
\lean{cases h}   & have \lean{h : P ∨ Q} (or \(\wedge\), \lean{∃}) & case analysis on \lean{h} \\
\lean{rw [eq]}   & contains a rewritable subterm & replace using equation \lean{eq} \\
\lean{simp}      & simplifiable clutter & rewrite with a lemma database \\
\lean{induction n} & \lean{∀ n : Nat, ...} & base case + inductive step \\
\lean{rfl}       & \lean{a = a} after computation & close by computation \\
\bottomrule
\end{tabular}
\end{center}

\section{Rewriting: equality as a tool}

The workhorse tactic of equational reasoning is \lean{rw} (rewrite). Given a
proven equation, it replaces one side by the other inside your goal:

\begin{lstlisting}[language=Lean]
example (a b : Nat) (h : a = b) : a + a = b + b := by
  rw [h]      -- goal becomes: b + b = b + b, closed by rfl automatically
\end{lstlisting}

Chains of rewrites read like the two-column proofs of school geometry,
except a machine checks every line. Here is commutativity-and-associativity
shuffling, Mathlib lemmas by name:

\begin{lstlisting}[language=Lean]
example (a b c : Nat) : a + b + c = c + b + a := by
  rw [Nat.add_comm a b]        -- b + a + c = c + b + a
  rw [Nat.add_assoc]           -- b + (a + c) = c + b + a
  rw [Nat.add_comm a c]        -- b + (c + a) = c + b + a
  rw [← Nat.add_assoc]         -- b + c + a = c + b + a
  rw [Nat.add_comm b c]        -- done
\end{lstlisting}

The arrow \(\leftarrow\) rewrites right-to-left. Nobody enjoys writing five-line
shuffles like this, which is exactly why Chapter~\ref{ch:automation}
introduces \lean{ring} --- but you must \emph{once} feel the manual version to
understand what the automation is doing on your behalf.

\section{Induction: the tactic that conquers infinity}

Remember the embarrassment of Chapter~\ref{ch:pat}: \lean{0 + n = n} does not
hold by computation. Now we can prove it --- by induction, the proof
technique that inductive types were born for:

\begin{lstlisting}[language=Lean]
theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero      => rfl                -- 0 + 0 = 0: computes
  | succ k ih => rw [Nat.add_succ, ih]
\end{lstlisting}

The \lean{induction} tactic converts a statement about \emph{all} naturals
into two finite obligations: the statement for \lean{zero}, and the statement
for \lean{succ k} \emph{assuming it for} \lean{k} (the induction hypothesis
\lean{ih}). Because every natural number is built from those two
constructors, the two cases cover infinity.

\begin{worked}{the full board of \lean{zero\_add} --- every goal state, by hand}
Reading a finished tactic proof is like reading a chess score without a
board. Here is the same proof \emph{with} the board: every goal state
written out, exactly as the editor would show it. Reproduce this trace on
paper until the transitions feel inevitable --- it is the core skill of
this chapter. We prove \lean{0 + n = n}, where \lean{+} recurses on its
second argument (Chapter~\ref{ch:lean}).

\smallskip
\noindent After \lean{induction n with}, two boards appear.
\emph{Case} \lean{zero}:
\begin{lstlisting}
⊢ 0 + 0 = 0
\end{lstlisting}
The second argument is the literal \lean{0}, so the first defining
equation fires: \lean{0 + 0} \emph{computes} to \lean{0}. Both sides are
now the same term; \lean{rfl} closes the board. (Compare the worked
example in Chapter~\ref{ch:pat}: this is the ``computation sees it'' half.)

\smallskip
\noindent\emph{Case} \lean{succ}: the board now carries an assumption ---
the induction hypothesis:
\begin{lstlisting}
k : Nat
ih : 0 + k = k
⊢ 0 + (k + 1) = k + 1
\end{lstlisting}
The left side is \lean{add 0 (succ k)}; the \emph{second} defining
equation fires and rewrites it to \lean{succ (0 + k)}. That step is the
tactic \lean{rw [Nat.add_succ]} (or one layer of
\lean{simp only [Nat.add]}), and the board becomes:
\begin{lstlisting}
k : Nat
ih : 0 + k = k
⊢ (0 + k) + 1 = k + 1
\end{lstlisting}
Now the subterm \lean{0 + k} is \emph{exactly} the left side of \lean{ih}.
Rewriting with \lean{rw [ih]} replaces it:
\begin{lstlisting}
k : Nat
ih : 0 + k = k
⊢ k + 1 = k + 1
\end{lstlisting}
Identical sides --- \lean{rw} auto-closes with \lean{rfl}. Done.

\smallskip
Two habits to take from this trace. First, at every step ask ``which
defining equation \emph{can} fire, and on which subterm?'' --- that
question, not tactic names, is what drives the proof. Second, notice
where the induction hypothesis earned its keep: computation alone got
stuck at \lean{0 + k} (opaque variable --- Chapter~\ref{ch:pat}'s blocked
reduction), and \lean{ih} is precisely the permission to cross that gap.
An induction proof is computation, plus permission slips at the stuck
points.
\end{worked}

\begin{aha}
Induction is not a new axiom to swallow --- it falls out of the inductive
definition of \lean{Nat} itself. ``Every \lean{Nat} is \lean{zero} or a
\lean{succ}'' \emph{is} the license to do case analysis; recursion on the
structure \emph{is} the induction. Data and proof principle are two views of
the same declaration. This is Curry--Howard paying rent again.
\end{aha}

\section{When you get stuck --- and you will}

No chapter on tactics is honest without this section. The steady march of
examples above is what proving looks like \emph{afterwards}, cleaned up for
print. What it looks like \emph{during} is the next box --- and the
discipline it teaches is worth more than any tactic in the table.

\begin{worked}{a debugging session, reconstructed honestly}
Here is a stuck proof, exactly as it happens to everyone, worked
through with the discipline this chapter preaches. Goal: every number
is at most its double --- \lean{∀ n : Nat, n ≤ 2 * n}. Attempt one:
\begin{lstlisting}[language=Lean]
theorem le_double (n : Nat) : n ≤ 2 * n := by
  induction n with
  | zero => rfl                -- fine: 0 ≤ 0 checks
  | succ k ih => rw [ih]       -- ERROR
\end{lstlisting}
The error says \lean{rw} failed: \lean{ih} is
\lean{k ≤ 2 * k} --- an \emph{inequality}, and \lean{rw} rewrites with
\emph{equations} only. First lesson banked: the tactic wasn't wrong,
the \emph{move category} was --- inequalities compose by transitivity
and monotonicity, not substitution. Attempt two, reading the goal
state first this time:
\begin{lstlisting}
k : Nat
ih : k ≤ 2 * k
⊢ k + 1 ≤ 2 * (k + 1)
\end{lstlisting}
Plan on paper before touching the keyboard: $2(k+1) = 2k + 2$, and from
\lean{ih}, $k + 1 \le 2k + 1 \le 2k + 2$ ✓ --- a two-step transitivity
chain. That \emph{plan} is provable many ways
(\lean{calc}, \lean{Nat.succ_le_succ} plus lemmas)\dots{} at which
point the honest practitioner pauses: hypotheses and goal are all
\emph{linear arithmetic}. The entire induction was unnecessary:
\begin{lstlisting}[language=Lean]
theorem le_double (n : Nat) : n ≤ 2 * n := by omega
\end{lstlisting}
Third lesson, the big one: getting stuck is often the discovery that
you are proving something in the wrong \emph{fragment} --- and the next
chapter is precisely the field guide to fragments. Keep the session's
order of operations, though, because it generalizes: (1) read what the
error says about the move category; (2) write the goal state and plan
on paper; (3) only then ask whether a decision procedure owns the whole
goal. Ten seconds of (3) before an hour of (2) is the professional's
cheat --- but (2) is what makes you able to survive when (3) says no.
\end{worked}

\begin{pitfall}
When a proof gets stuck, resist the urge to try random tactics --- the
formal-methods equivalent of mashing buttons. The goal state is telling you
something. Three honest questions unstick most situations: (1)~Is the
statement actually true as written --- check a small example with
\lean{\#eval}! (2)~Am I missing a hypothesis --- is there an unstated bound or
nonzero condition? (3)~Is my induction on the right variable? In the real
projects behind this book, ``the proof is stuck'' was, more often than not,
the \emph{statement} being subtly wrong --- a truncated subtraction, a missing
bound. The proof assistant was the messenger.
\end{pitfall}

\section{Structuring real proofs: \texttt{have} and \texttt{calc}}

Big proofs are not flat lists of tactics; they are structured arguments with
named intermediate results. The \lean{have} tactic states and proves a
stepping stone; \lean{calc} lays out a chain of equalities or inequalities
the way you would on a whiteboard:

\begin{lstlisting}[language=Lean]
example (a b : Nat) (h : a = 2 * b) : a + a = 4 * b := by
  have h2 : a + a = 2 * a := by rw [Nat.two_mul]
  calc a + a = 2 * a       := h2
       _     = 2 * (2 * b) := by rw [h]
       _     = 4 * b       := by rw [← Nat.mul_assoc]
\end{lstlisting}

\begin{worked}{planning a \lean{calc} on paper --- backwards from the target}
Professionals do not type a \lean{calc} top-to-bottom and hope; they plan
it on paper, usually \emph{backwards}. Watch the method on the real
reduction identity from the Ed25519 code (Chapter~\ref{ch:modular} proves
the ingredients): given a 256-bit value split as
$x = x_{\mathrm{lo}} + 2^{255} x_{\mathrm{hi}}$, the code returns
$x_{\mathrm{lo}} + 19 x_{\mathrm{hi}}$, and we owe
\[
x_{\mathrm{lo}} + 19\, x_{\mathrm{hi}}
\;\equiv\;
x \pmod{p}.
\]
Plan backwards: the target's right side is $x$, which we only know through
its \emph{definition}, so the last line of the chain will be
``$\ldots = x_{\mathrm{lo}} + 2^{255} x_{\mathrm{hi}} = x$ by the split.''
What could precede it? Something that turns $19$ into $2^{255}$: the fact
$19 \equiv 2^{255}$, i.e.\ the constant identity $2^{255} - 19 = p
\equiv 0$. So the middle step is a congruence rewrite, and the paper plan
reads, bottom to top:
\[
\begin{array}{lll}
\text{(3)} & x_{\mathrm{lo}} + 2^{255} x_{\mathrm{hi}} = x & \text{definition of the split}\\
\text{(2)} & x_{\mathrm{lo}} + 19\, x_{\mathrm{hi}} \equiv x_{\mathrm{lo}} + 2^{255} x_{\mathrm{hi}} & \text{since } 19 \equiv 2^{255} \pmod p\\
\text{(1)} & \text{start: } x_{\mathrm{lo}} + 19\, x_{\mathrm{hi}} & \\
\end{array}
\]
Reverse it, and the \lean{calc} types itself --- each line's justification
was decided \emph{before} any Lean was written. The habit scales: the real
multiplication proof in \code{dalek-ed25519-verified} was planned exactly
this way, as a page of paper algebra whose lines became \lean{have}s. When
you cannot plan the chain on paper, you are not ready to type it; the
proof assistant checks reasoning, it does not supply it.
\end{worked}

This style is not cosmetic. In the verified field arithmetic you will read
later, a single multiplication correctness proof is a \lean{calc} chain
tracking limb products through carries --- dozens of steps, each trivial,
whose \emph{composition} is the theorem. \lean{have} and \lean{calc} are how
proofs stay readable at that scale; they are also how they stay
\emph{maintainable}, because a broken step localizes the damage to one line.

There is one more structuring fact worth knowing early, because it saved the
real project from a crash-course (literally --- see
Chapter~\ref{ch:honesty}): breaking a proof into small named \lean{have}
steps also controls the proof assistant's \emph{memory appetite}. A monolithic
``figure it all out at once'' tactic call over a huge context can consume
gigabytes; ten targeted steps, pennies each, prove the same thing. Structure
is not just style --- it is engineering.

\begin{tryit}
Open \code{exercises/Ch04.lean}. It sets up each theorem with the goal state
drawn in a comment, then asks you to: prove \lean{and_swap} in tactic mode;
prove \lean{zero_add} \emph{without} peeking above; and repair a broken
\lean{calc} chain in which exactly one step is wrong. The third
exercise is secretly the most realistic job training in this book.
\end{tryit}

\section*{Exercises}

\exercise{Prove by induction: \lean{∀ n : Nat, n + 0 = n} and
\lean{∀ n m : Nat, n + succ m = succ (n + m)}. (These are the mirror images
of the definitional equations --- the ones computation gives you for free ---
and together they yield commutativity.)}

\exercise{Using the previous exercise, prove
\lean{∀ n m : Nat, n + m = m + n} by induction on \lean{m}. Write out, in
one prose sentence per case, what each branch of your proof says.}

\exercise{Prove \lean{∀ n : Nat, 2 * n = n + n} twice: once with
\lean{induction}, once with a single \lean{rw} using a Mathlib lemma you find
yourself (search hint: \lean{exact?} asks Lean to search for you).}

\exercise{(Reading) In the goal state
\lean{h : a < 2\textasciicircum{}51 ⊢ a * 19 < 2\textasciicircum{}56}, no induction is needed --- this is pure
arithmetic. Which tactic from the table would you \emph{guess} handles it?
(Answer next chapter; your guess is the point.)}

\section*{Solutions and pathways}
\solutionsintro

\solhead{4.1}
\pathway Before proving anything, predict which facts are \emph{free}:
addition recurses on its second argument, so any statement whose second
argument exhibits a constructor should compute. Both requested statements
--- \lean{n + 0 = n} and \lean{n + succ m = succ (n + m)} --- have
constructor-shaped second arguments (\lean{0} and \lean{succ m}). The
honest content of this exercise is noticing that.
\answer \lean{theorem a : ∀ n : Nat, n + 0 = n := fun n => rfl} --- the
first defining equation. \lean{theorem b : ∀ n m, n + succ m = succ (n+m)
:= fun n m => rfl} --- the second. Neither needs induction; both are the
definitional mirror images of the two facts that \emph{do}
(\lean{0 + n = n}, \lean{succ n + m = succ (n + m)}), which is exactly the
asymmetry the worked example traced. If you reached for \lean{induction}
here, nothing is wrong --- it succeeds --- but recognizing a free fact
saves you thirty seconds a hundred times a day.

\solhead{4.2}
\pathway Induct on \lean{m} (the variable the recursion consumes on the
\emph{right} of \lean{n + m}), so the definitional equations fire on one
side and 4.1's lemmas patch the other. In each case, before touching
tactics, write the goal and ask: which side steps by definition, which
needs a lemma?
\answer
\begin{lstlisting}[language=Lean]
theorem add_comm' (n m : Nat) : n + m = m + n := by
  induction m with
  | zero      => rw [Nat.add_zero, Nat.zero_add]
  | succ k ih => rw [Nat.add_succ, Nat.succ_add, ih]
\end{lstlisting}
Prose, one sentence per case, as requested. \emph{Zero case:} ``$n + 0$ is
$n$ by definition, and $0 + n$ is $n$ by the mirror lemma, so both sides
are $n$.'' \emph{Successor case:} ``both sides compute to a successor ---
the left by the defining equation, the right by the mirror lemma --- and
under the \lean{succ} the two sides are the induction hypothesis.'' Note
the architecture: two definitional equations, two mirror lemmas, one
induction --- commutativity is not one fact but a small \emph{ecosystem},
and you have now built all of it from bare constructors.

\solhead{4.3}
\pathway For the induction route, the \lean{succ} case needs
$2(k+1) = (k+1) + (k+1)$ reorganized into the induction hypothesis's shape
plus successors --- expect two rewrites. For the library route, the skill
is \emph{search}: place the cursor on the goal and run \lean{exact?}.
\answer Induction:
\begin{lstlisting}[language=Lean]
theorem two_mul' (n : Nat) : 2 * n = n + n := by
  induction n with
  | zero      => rfl
  | succ k ih => rw [Nat.mul_succ, ih, Nat.succ_add, Nat.add_succ]
\end{lstlisting}
Library: \lean{exact?} finds \lean{Nat.two_mul}, giving
\lean{theorem two_mul\textquotesingle\textquotesingle\ (n : Nat) : 2 * n = n + n}
proved by \lean{Nat.two_mul n}. Both
are legitimate craft: the first when you are building the ecosystem, the
second when you are using it. Mathlib has over 200{,}000 lemmas ---
searching \emph{is} a proof technique, and \lean{exact?} is its tactic.

\solhead{4.4}
\pathway The goal mixes a hypothesis bound, multiplication by a
\emph{constant}, and powers of two --- inspect the table: nothing fits
perfectly, which is the setup's point. What you want is a decision
procedure for linear arithmetic.
\answer The intended guess is \lean{simp} or \lean{rw}-with-lemmas ---
and the intended discovery is that neither is pleasant. The actual answer,
one chapter ahead: \lean{omega}, which decides such goals instantly
because $a \cdot 19$ is \emph{linear} in $a$ (19 is a constant). If you
guessed \lean{omega} from the table's absence, better still: you have
started classifying goals by \emph{logical fragment}, which is precisely
the professional habit Chapter~\ref{ch:automation} installs.

\begin{checkpoint}
You should now be able to: read a goal state (context, turnstile, goal);
drive the core tactics \lean{intro}, \lean{exact}, \lean{apply},
\lean{cases}, \lean{rw}, \lean{induction}; structure a multi-step argument
with \lean{have} and \lean{calc}; and --- most importantly --- when stuck,
interrogate the \emph{statement} before blaming the proof. One goal from the
exercises is deliberately still open: the bound
$a \cdot 19 < 2^{56}$, which no tactic in this chapter's table owns. Carry it
with you --- the next chapter opens by handing you the tactic that eats it in
one line.
\end{checkpoint}