on coq: Why is the proof complete after proving only for one induction when we have more than one variable?

Question

So I'm learning coq. And I came across the proof for associativity in addition forall (a b c : nat)

Appearntly when we do induction a. after intros a b c., it creates 2 subgoals

and afterwards we simply need to show that the two sides in both subgoals are equivalent, and the proof is completed.

So I'm just wondering why we don't need to do induction b. and induction c. to complete the proof? Why only performing induction on a is able to complete the proof?

Or in other words, how come in the function that returns the proof, we just get b and c for "free"? Constructively don't we need something like a double induction applied twice?

Answer 1

You do not have to prove things by induction. For example, you can prove $\forall n : \mathbb{N} \,.\, n = n$ without induction by applying reflexivity. In your proof, we use induction on $a$, but then we do not need to use induction on $b$ and $c$ because we can finish the proof simply using other methods. We could have used induction on $b$ and $c$, and you should try to do so, to see how unecessary applications of induction just make your proof longer and less clear.

P.S. This has absolutely nothing to do with constructivity.