Это одно и то же утверждение, но с разными числами: одно около n', другое около n, что соответствует S n' в цели. Индукция точно показывает, что что-то действительно для S n', просто зная, что это верно для n' Тот факт, что они являются разными числами, делает это нетривиальным. Например, не можно показать, что S n' нечетно, при условии, что n' нечетно, даже если оба оператора "одинаковы".
Вы спрашивали о механике переписывания. После упрощения ваша цель выглядит так:
n' : nat
IHn' : n' = n' + O
---------------------------------------
S n' = S (n' + O)
Когда вы звоните rewrite, вы говорите Coq заменить n' + O на n' в цели. Это приводит к утверждению S n' = S n', которое является простым равенством, которое может быть выполнено по аксиоме рефлексивности.
Редактировать
Вот еще один способ думать об индукции. Давайте на секунду забудем о тактике induction. Можно доказать, что 0 = 0 + 0:
Lemma plus_0_0 : 0 = 0 + 0.
Proof. reflexivity. Qed.
Мы можем доказать аналогичные утверждения о любом конкретном натуральном числе:
Lemma plus_1_0 : 1 = 1 + 0.
Proof. reflexivity. Qed.
Lemma plus_2_0 : 2 = 2 + 0.
Proof. reflexivity. Qed.
Однако мы можем получить эти доказательства по-разному, сделав меньше предположений о форме числа, о котором мы говорим. Сначала докажем следующее условное утверждение.
Lemma plus_Sn_0 : forall n', n' = n' + 0 -> S n' = S n' + 0.
Proof. intros n' Hn'. simpl. rewrite <- Hn'. reflexivity. Qed.
Эта лемма устанавливает индуктивный шаг доказательства по индукции. Обратите внимание, что в нем не говорится, что n = n + 0 верно для всех натуральных чисел n, но что оно справедливо только для чисел вида n = S n' при условии, что n' = n' + 0. Мы знаем, что это работает для n' = 0, потому что мы доказали это выше. В сочетании с plus_Sn_0 у нас есть еще одно доказательство 1 = 1 + 0.
Lemma plus_1_0' : 1 = 1 + 0.
Proof. apply plus_Sn_0. apply plus_0_0. Qed.
Теперь мы знаем, что утверждение верно для n' = 1, мы можем сыграть тот же трюк для n = 2:
Lemma plus_2_0' : 2 = 2 + 0.
Proof. apply plus_Sn_0. apply plus_1_0'. Qed.
Это доказательство не использует непосредственно тот факт, что 0 = 0 + 0. Вот почему тот факт, что мы доказали базовый случай, не имеет значения для доказательства индуктивного шага : все, что нам нужно знать, - это предшественник числа, которое нас интересует - в данном случае этот предшественник является 1.
Естественно, мы могли бы расширить доказательство plus_1_0' внутри доказательства plus_2_0':
Lemma plus_2_0'' : 2 = 2 + 0.
Proof. apply plus_Sn_0. apply plus_Sn_0. apply plus_0_0. Qed.
В более общем смысле, учитывая любую натуральную числовую константу n, мы можем доказать, что n = n + 0 без индукции , применив plus_Sn_0 n раз, а затем plus_0_0. Принцип математической индукции экстраполирует это интуитивное наблюдение на любое выражение n, обозначающее натуральное число, а не только константы.