coq에:하나 이상의 변수가 있을 때 하나의 귀납법에 대해서만 증명한 후에 증명이 완료되는 이유는 무엇입니까?

Question

그래서 coq를 배우고 있어요.그리고 연관성에 대한 증거도 발견했습니다. forall (a b c : nat)

분명히 우리가 할 때 induction a. ~ 후에 intros a b c., 2개의 하위 목표를 생성합니다.

그런 다음 두 하위 목표의 양측이 동일하다는 것을 보여주면 증명이 완료됩니다.

그래서 우리가 왜 그렇게 할 필요가 없는지 궁금합니다. induction b. 그리고 induction c. 증명을 완료하려면?인덕션만 하는 이유 a 증명을 완료할 수 있나요?

또는 다른 말로 하면, 증명을 반환하는 함수가 어떻게 들어왔는지, 우리는 다음과 같은 결과를 얻습니다. b 그리고 c 무료로"?건설적으로 우리는 이중 유도를 두 번 적용하는 것과 같은 것이 필요하지 않습니까?

Answer 1

당신은하지 않습니다 가지다 귀납법으로 사물을 증명합니다.예를 들어, 다음을 증명할 수 있습니다. $\forall n :\mathbb{N} \,.\, n = n$ 없이 반사성을 적용하여 유도합니다.귀하의 증거에서는 유도를 사용합니다. $a$, 하지만 우리는 필요하지 않다 인덕션을 사용하다 $b$ 그리고 $c$ 왜냐하면 다른 방법을 통해서도 증명을 끝낼 수 있기 때문입니다.우리 가질 수 있었어 인덕션을 사용했어요 $b$ 그리고 $c$, 그리고 당신은 그렇게 하려고 노력해야 하며, 불필요한 귀납법 적용이 어떻게 증명을 더 길고 덜 명확하게 만드는지 확인해야 합니다.

추신이것은 건설성과 전혀 관련이 없습니다.