时间戳

首页 > 解决方案 > 在 Coq 中正确地进行双重归纳

coq - 在 Coq 中正确地进行双重归纳

问题描述

我正在尝试从软件基础的归纳章节证明 plus_n_Sm 定理

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')

我被困在这里。我究竟做错了什么？找到两个变量的归纳证明的正确思维方式是什么？

标签： coqproofinduction

解决方案

正如第一条评论所说，关键是对 n 的归纳就足够了， m 可以是一个常数。那么证明就很简单了。

推荐阅读