How does one know what statements in Coq require Induction?

I was trying to learn Coq using the famous book Software Foundations. In it I found the following:

Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
  induction n as [| n IHn].
  - simpl. reflexivity.
  - simpl. rewrite -> IHn. reflexivity.
Qed.

which I understand perfectly but find rather unintuitive. I understand perfectly how each step works but it would have never occurred to me to use induction to prove such a trivial fact. In fact in the mathematical proof I had in mind that would have been a fact/property (or I guess an axiom) of 0. i.e. $\forall n \in N, n \cdot 0 = 0$ is true by definition. I guess in Coq (or the way we set up numbers? thats not true).

My biggest complaint or worry is that if such a trivial thing requires induction I feel now I am unable to recognize what needs induction (at least in Coq). I know it needs it here because I am in the induction chapter. But in normal maths its usually quite obvious because the problem is obviously recursive. But I wouldn't have really thought of that proposition as recursive. For example it goes on to prove more things as exercises:

Theorem plus_n_Sm : ∀n m : nat,
  S (n + m) = n + (S m).
Proof.
  (* FILL IN HERE *) Admitted.
Theorem plus_comm : ∀n m : nat,
  n + m = m + n.
Proof.
  (* FILL IN HERE *) Admitted.
Theorem plus_assoc : ∀n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  (* FILL IN HERE *) Admitted.

which I am sure are not too difficult, but my worry is that in isolation I would have never thought such trivial statements required something as sophisticated as induction. I didn't even learn induction until last 2 years of highschool and didn't really do it seriously until college. So now I see trivial statements requiring what seems to me, sophisticated mathematics.

I just feel my intuition got really lost. When I do Coq proofs (in isolation), how do I know when to use induction and on what? I doubt there is a general procedure (of course) but proofs do exist. So there m

Coq allows one to prove mathematical theorems in a completely formal way. At first, this copes with our experience of doing maths, which is far more informal.

Most of the time, people doing maths are not exposed to mathematical logic. They do not know, for instance, how to define the set of real numbers. Or even the set of natural numbers. Numeric sets are simply taken for granted, together with their operations and related properties. On top of these "basic facts" people build more complex theorems. Essentially, the "basic facts" are used as if they were axioms.

Note that one could work at a similar level in Coq, if one wishes. One can import the Arith Coq library, which provides the basic facts of arithmetics, and exploit those.

However, the underlying logic of Coq does not take those properties for granted. The type of natural numbers, for instance, is not a primitive concept in the logic, but rather something which is defined using induction. Since that makes nat an inductive type, virtually every proof about naturals will require induction. (This also holds in set theory, e.g. Zermelo-Fraenkel, where naturals are also defined in a sort-of inductive way.)

Arithmetical operators are also defined using induction. Using a simplified syntax, one could define multiplication as

x * 0     = 0
x * (S y) = x + (x * y)

or, alternatively,

0 * x     = 0
(S y) * x = x + (y * x)

Both definitions are equivalent. However, using the first one will result in us being able to prove x * 0 = 0 "without induction" -- it follows by definition. In Coq, we can simply write reflexivity and let the system expand the definition for us.

By comparison, 0 * x = 0 is not a trivial equation which follows from the definition: to expand the definition we need to know what is the second argument of the multiplication, but here it's merely an unknown x. Hence, for this we do need induction over x. There's no way around that.

Note that, if we used the second definition instead, we would prove 0 x = 0 immediately, and instead require induction for x 0 = 0. So, no definition is strictly better than the other one.

StackExchange Computer Science Q#103112, answer score: 6