1
$\begingroup$

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

enter image description here

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

enter image description here

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?

enter image description here

Improve this question
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Gilles 'SO- stop being evil'
    Commented Jun 5, 2020 at 11:23

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
3

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.