Coq证明求助：证明num_occ x (n_copies n x) = n时遇瓶颈

相关定义与待证定理 #

Fixpoint n_copies (n x : nat) : list nat :=
  match n with
  | 0 => []
  | S n' => x :: n_copies n' x
  end.

Theorem exercise3
  : forall x n, num_occ x (n_copies n x) = n.
Proof.

我的尝试 #

我尝试的证明步骤：

intros x n. induction n. simpl.
  - congruence.
  - destruct (eq_dec x n).
    + induction e.
    +

当前卡住的证明目标：

1 goal
x : nat
IHn : num_occ x (n_copies x x) = x
______________________________________(1/1)
num_occ x (n_copies (S x) x) = S x

我认为需要消去两边的S构造子，但不知道具体方法，请求帮助解决该证明问题。

正确证明步骤 #

你之前的错误在于多余引入了destruct (eq_dec x n)——实际上n_copies (S n) x的构造就是x :: n_copies n x，而num_occ在遇到头元素等于目标x时，会直接返回S (num_occ x 剩余列表)，完全不需要区分x和n的关系。

完整证明步骤如下：

intros x n. induction n.
- (* n = 0 *) simpl. reflexivity.
- (* n = S n' *) simpl. rewrite IHn. reflexivity.
Qed.

步骤解释 #

1. 基例（n=0）：n_copies 0 x是[]，num_occ x []等于0，直接用reflexivity（或你之前的congruence）即可证明。
2. 归纳步骤（n=S n'）：
   • simpl后，目标变为num_occ x (x :: n_copies n' x) = S n'。
   • 根据num_occ的定义，num_occ x (x :: l)会展开为S (num_occ x l)，左边因此简化为S (num_occ x (n_copies n' x))。
   • 应用归纳假设IHn : num_occ x (n_copies n' x) = n'，用rewrite IHn替换后，左边变为S n'，与右边完全一致，reflexivity完成证明。

内容的提问来源于stack exchange，提问作者Alessandro D'angelo