em coq:Por que a prova fica completa depois de provar apenas uma indução quando temos mais de uma variável?

Question

Então estou aprendendo coq.E me deparei com a prova da associatividade além forall (a b c : nat)

Aparentemente, quando fazemos induction a. depois intros a b c., ele cria 2 submetas

e depois precisamos simplesmente mostrar que os dois lados em ambos os subobjetivos são equivalentes, e a prova está concluída.

Então, só estou me perguntando por que não precisamos fazer induction b. e induction c. para completar a prova?Por que realizar apenas indução em a é capaz de completar a prova?

Ou em outras palavras, como é que na função que retorna a prova, obtemos apenas b e c de graça"?Construtivamente, não precisamos de algo como uma indução dupla aplicada duas vezes?

Answer 1

Você não ter provar coisas por indução.Por exemplo, você pode provar $\forall n :\mathbb{N} \,.\, n = n$ sem indução aplicando reflexividade.Na sua prova, usamos indução em $a$, mas então nós não precisamos usar indução em $b$ e $c$ porque podemos terminar a prova simplesmente utilizando outros métodos.Nós poderia ter indução usada em $b$ e $c$, e você deveria tentar fazer isso, para ver como aplicações desnecessárias de indução apenas tornam sua prova mais longa e menos clara.

P.S.Isso não tem absolutamente nada a ver com construtividade.