如何证明Coq引理even_plus_split？仅限指定库与定义使用

嘿，作为Coq新手遇到这类分情况的证明很正常！我来一步步帮你搞定这个引理，完全用你给定的库和定义来实现。

首先，先把完整的证明代码贴出来，之后再拆解每一步的思路：

Require Import Arith.
Require Import Coq.omega.Omega.

Definition even (n: nat) := exists k, n = 2 * k.
Definition odd (n: nat) := exists k, n = 2 * k + 1.

Lemma even_plus_split n m : even (n + m) -> even n /\ even m \/ odd n /\ odd m.
Proof.
  (* 先展开even和odd的定义，方便直接处理存在量词与等式 *)
  unfold even, odd.
  (* 假设n+m是偶数，拆解为存在k满足n+m=2k *)
  intros [k Hkm].
  (* 对n的奇偶性做穷尽分情况讨论：自然数要么偶要么奇 *)
  destruct (Nat.even_odd_dec n) as [Hn_even | Hn_odd].
  - (* 情况1：n是偶数，拆解为存在a满足n=2a *)
    destruct Hn_even as [a Hna].
    (* 将n=2a代入n+m=2k的等式 *)
    rewrite Hna in Hkm.
    (* 推导m是偶数：整理等式得到m=2(k-a) *)
    assert (Hm_even: exists b, m = 2 * b).
    { exists (k - a). omega. }
    (* 构造目标的第一个析取支：n偶且m偶 *)
    left. split; assumption.
  - (* 情况2：n是奇数，拆解为存在a满足n=2a+1 *)
    destruct Hn_odd as [a Hna].
    (* 将n=2a+1代入n+m=2k的等式 *)
    rewrite Hna in Hkm.
    (* 推导m是奇数：整理等式得到m=2(k-a-1)+1 *)
    assert (Hm_odd: exists b, m = 2 * b + 1).
    { exists (k - a - 1). omega. }
    (* 构造目标的第二个析取支：n奇且m奇 *)
    right. split; assumption.
Qed.

关键步骤拆解 #

• 展开定义：unfold even, odd把自定义的奇偶性转化为存在量词形式，让我们能直接操作底层等式。
• 引入假设：intros [k Hkm]把“n+m是偶数”的假设拆解为具体的自然数k和对应的等式关系。
• 分情况讨论：Nat.even_odd_dec n是Arith库提供的判定工具，帮我们覆盖自然数的所有可能（偶/奇），确保证明没有遗漏。
• omega工具：omega是Coq的线性算术自动证明器，能快速解决2a + m = 2k这类整数等式的推导，不用手动做繁琐的自然数加减推理。
• 构造目标：根据n的奇偶性推导出m的对应性质后，用left/right选择析取式分支，再用split构造合取结论，最后用assumption复用已证的前提。

这个证明完全符合你要求的库和定义，逻辑清晰，适合新手理解分情况证明和存在量词的处理方式~

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