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.
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.