on coq:Почему доказательство завершено после доказательства только для одной индукции, когда у нас есть более одной переменной?

Question

Итак, я изучаю coq.И вдобавок я наткнулся на доказательство ассоциативности forall (a b c : nat)

Очевидно, когда мы делаем induction a. после intros a b c., это создает 2 подцели

и после этого нам просто нужно показать, что две стороны в обеих подцел эквивалентны, и доказательство завершено.

Поэтому мне просто интересно, почему нам не нужно делать induction b. и induction c. чтобы завершить доказательство?Почему выполняется только индукция на a способен ли завершить доказательство?

Или, другими словами, как получается, что в функции, которая возвращает доказательство, мы просто получаем b и c за "бесплатно"?Конструктивно, разве нам не нужно что-то вроде двойной индукции, применяемой дважды?

Answer 1

Вы этого не делаете иметь чтобы доказать что-то с помощью индукции.Например, вы можете доказать $\для всех n :\mathbb{N} \,.\, n = n$ без индукция путем применения рефлексивности.В вашем доказательстве мы используем индукцию на $a$, но тогда нам не нужно использовать индукцию на $b$ и $c$ потому что мы можем закончить доказательство, просто используя другие методы.Мы мог бы иметь используемая индукция на $b$ и $c$, и вы должны попытаться сделать это, чтобы увидеть, как ненужные применения индукции просто делают ваше доказательство длиннее и менее понятным.

P.S.Это не имеет абсолютно никакого отношения к конструктивности.