Coq证明中如何将项替换为其对应属性？以list_even_split引理为例

卡住部分的补全代码 #

你当前的证明步骤只需要补充以下代码即可完成证明：

exists (Nat.even a).
split.
- (* 证明 a :: c = [a] ++ c，符合列表连接的定义 *)
  reflexivity.
- split.
  + (* 展开list_even定义化简map，直接成立 *)
    unfold list_even. simpl. reflexivity.
  + (* 展开list_even定义化简map对非空列表的操作，直接成立 *)
    unfold list_even. simpl. reflexivity.

你不需要对a的奇偶性做分支讨论，因为你要找的b本身就是Nat.even a的计算结果，不管结果是true还是false，后续的等式都天然成立，直接用这个值实例化b即可。

无需归纳法的完整证明 #

你判断的没错，这个引理确实不需要用到归纳法，因为我们只需要区分列表是否为空的两种情况即可：非空列表直接取第一个元素组成长度为1的c1，剩下的部分作为c2就满足所有条件，不需要用到归纳假设。完整证明代码如下：

Proof.
  intros c.
  destruct c as [| a c2].
  - left. reflexivity.
  - right.
    exists [a], c2, (Nat.even a).
    split; [reflexivity | split; unfold list_even; simpl; reflexivity].
Qed.

内容的提问来源于stack exchange，提问作者sdpoll