Induction chapter in Software Foundations
Theorem succ_is_plus_1: forall n: nat, S n = n + 1.
Proof.
induction n as [| n' ind_hyp].
- simpl. reflexivity.
- simpl. rewrite <- ind_hyp. reflexivity.
Qed.
Theorem plus_n_Sm : forall n m : nat,
S (n + m) = n + (S m).
Proof.
induction n as [| n' ind_hyp ].
- induction m as [| m' ind_m ].
+ simpl. reflexivity.
+ simpl. reflexivity.
- induction m as [| m' ind_m2 ].
+ rewrite -> succ_is_plus_1 . rewrite <- plus_n_O. reflexivity.
+ rewrite -> succ_is_plus_1. rewrite <- ind_m2.
此时的输出是
1 subgoal
n' : nat
ind_hyp : forall m : nat, S (n' + m) = n' + S m
m' : nat
ind_m2 : S (S n' + m') = S n' + S m'
______________________________________(1/1)
S (S n' + m') + 1 = S n' + S (S m')
我被困在这里了。我做错什么了?找到两个变量的归纳证明,正确的思维方式是什么?
