COQ中子序列传递性subseq_trans证明归纳假设选择问题求助

你当前陷入死局的核心原因是归纳策略的泛化程度不足：你在固定了l3和第二个子序列假设后才对第一个子序列假设做归纳，此时得到的归纳假设仅对当前固定的l3生效，无法覆盖后续case拆分中l3结构变化的场景。

正确归纳方案 #

优先选择对第二个子序列关系subseq l2 l3进行归纳，同时泛化l1变量，确保归纳假设可以适配任意的subseq l1 l2前提，完全避免反向推导子序列的需求。

可直接运行的证明参考 #

Inductive subseq : list nat -> list nat -> Prop :=
  | sseq_e (l2 : list nat) : subseq ([]) (l2)
  | sseq_m (l1 l2 : list nat) (n : nat) (H: subseq l1 l2) : subseq (n::l1) (n::l2)
  | sseq_nm (l1 l2 : list nat) (n : nat) (H: subseq l1 l2) : subseq (l1) (n::l2) 
  .

Theorem subseq_trans : forall (l1  l2 l3 : list nat),
  subseq l1 l2 ->
  subseq l2 l3 ->
  subseq l1 l3.
Proof.
  intros l1 l2 l3 H1 H2.
  (* 关键操作：将l1和对应的子序列假设泛化到归纳假设中 *)
  generalize dependent l1.
  induction H2.
  - (* 分支1：l2是空列表，l1必然也是空列表 *)
    intros l1 H1. inversion H1. apply sseq_e.
  - (* 分支2：l2和l3的首元素匹配，由sseq_m构造 *)
    intros l1 H1.
    inversion H1; subst.
    + apply sseq_e.
    + apply sseq_m. apply IHH2. assumption.
    + apply sseq_nm. apply IHH2. assumption.
  - (* 分支3：l3首元素是额外插入的元素，由sseq_nm构造 *)
    intros l1 H1.
    apply sseq_nm. apply IHH2. assumption.
Qed.

关键逻辑说明 #

• 沿l2 -> l3的子序列构造方向做归纳，永远正向推导，不会出现需要从subseq l2 (x::l3)反推subseq l2 l3的死局
• 泛化l1的目的是让归纳假设可以适配所有可能的l1结构，覆盖子序列三个构造子对应的所有分支场景

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