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 must be something guiding us to use induction in Coq.