所以，我正在尝试使用“计算逻辑导论”脚本来学习 Coq，并且我得到了一个练习。它是为了证明以下内容：“forall ab, a + S b = S (a + b)”。我得到了“nat_ind”的定义：
(p : nat -> Prop)
(basis : p 0)
(step : forall n, p n -> p (S n)) :
forall n, p n := fix f n :=
match n return p n with
| 0 => basis
| S n => step n (f n)
end.
我对此进行了尝试，并使用此方法解决了该问题，并且有效：
intros a b. revert a.
apply (nat_ind(fun a => a + S b = S (a+b))); simpl.
-reflexivity.
-intros. f_equal. exact H.
现在问题来了，我必须解决同样的问题，但我需要立即应用归纳引理，并且在我这样做之前不能使用介绍或归纳策略。我该怎么做？
我试图从我的第一次尝试中删除第一行，但它会引发错误：“在当前环境中找不到引用 b。”
更新：我已经到了某个地方。这是我当前的代码：
Goal forall a b, a + S b = S (a + b).
Proof.
apply nat_ind.
- intros a b. revert a.
apply (nat_ind (fun a => a + S b = S (a + b)));simpl.
+ reflexivity.
+ intros. f_equal. exact H.
-intros. revert a. apply (nat_ind (fun a => a + S b = S (a + b))); simpl.
+ reflexivity.
+ intros. f_equal. exact H0.
最后一个子目标只是 nat，我根本不知道该怎么做。