## Proof by Induction

The `destruct`

tactic could push the proof one step further, but it won’t work in some cases.

Proof by *induction* is useful when we want to prove that some property holds for all the members of an infinite set, such natural numbers, as well as lists, trees, and other data-types.

In Coq, we use induction beginning with a goal of proving the proposition $P(n)$ for all $n$ and break it down into separate subgoals, each having its own inductive hypothesis.

## Proofs Within Proofs

Sometimes a proof requires trivial facts that are too small to separate as lemmas. We could use `assert`

tactic to list and prove these facts. This tactic also helps in complex rewriting, for example, when `plus_comm`

applies to contents in both parentheses, we could specify which part to rewrite:

```
Theorem plus_rearrange : ∀ n m p q : ℕ,
(n + m) + (p + q) = (m + n) + (p + q).
Proof.
intros n m p q.
assert (H: n + m = m + n).
{ rewrite → plus_comm. reflexivity. }
rewrite → H. reflexivity. Qed.
```

A proof of a mathematical proposition $P$ is a written or spoken text that convinces someone that $P$ is true.

Coq is like a “reader” of such text (proof), and the proof guides the program to check if $P$ could be derived from certain rules. Such proofs are *formal* proofs.

Formal proofs are explicit in some way, such as what tactics are used, but less explicit in other ways, such as the “proof state” at given point in proof.