如何在Coq中用自然数分情况证明？附具体定理证明求助

完整可运行证明代码 #

Require Import List.
Require Import Nat.

Fixpoint Inb(x: nat) (A: list nat) :=
 match A with
 | nil => false
 | h :: t => if h =? x then true else (Inb x t)
 end.

Definition In (x: nat) (A: list nat) := 
  Inb x A = true.

Theorem inside_thm: forall x, In x (3::4::nil) -> x = 3 \/ x = 4.
Proof.
  unfold In.
  intros x H.
  case_eq (3 =? x); intro H_eq.
  - rewrite Nat.eqb_eq in H_eq.
    left.
    exact H_eq.
  - rewrite Nat.eqb_neq in H_eq.
    simpl in H.
    rewrite Nat.eqb_eq in H.
    right.
    exact H.
Qed.

证明思路与步骤拆解 #

1. 展开定义：用unfold In把自定义的In展开为底层的Inb等式，明确目标的逻辑结构。
2. 引入变量与假设：intros x H提取出全称量词的变量x和前提条件H（即Inb x (3::4::nil) = true）。
3. 分情况讨论：通过case_eq (3 =? x)拆分x是否等于3的两种场景：
   • 当3 =? x为true时，借助Nat.eqb_eq引理将布尔相等判断转化为自然数的相等关系，直接证明x=3。
   • 当3 =? x为false时，先用Nat.eqb_neq得到x≠3，此时简化假设H会自动推导出4 =? x = true，再用Nat.eqb_eq转化为x=4，完成右边析取项的证明。

注：Nat.eqb_eq和Nat.eqb_neq是Coq标准库中提供的引理，分别对应“布尔相等为真当且仅当自然数相等”和“布尔相等为假当且仅当自然数不相等”。

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