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

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?

• I think it's simpler to see on the proof of symmetry, where you also need induction only on one of the numbers, not both. Jun 5 '20 at 11:23

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.
• Reflexivity is the constructor for the identity types, see the standard library definition. The reflexivity tactic is lipstick on top of that definition. Jun 16 '20 at 11:06