Coq中列表In谓词的可判定性函数编写问题求助

首先得明确：{In s l} + {~ In s l} 是Coq的sumbool类型，它不是直接包含In s l或~In s l这两个Prop，而是需要用left和right构造子把对应的证明包装起来——left接收一个In s l的证明，返回sumbool类型的实例；right接收一个~In s l的证明，返回另一个实例。你直接返回Prop类型的In s l或~In s l，会触发类型不匹配的错误。

修正后的代码 #

方式1：不用Program，直接写Fixpoint #

Fixpoint InDec (s : K) (l : list K) : {In s l} + {~ In s l} :=
  match l with
  | nil => right (fun H => match H with end)
  | head :: tail => 
    match eq_dec s head with
    | left eq => left (or_introl eq)
    | right neq => 
      match InDec s tail with
      | left in_tail => left (or_intror in_tail)
      | right not_in_tail => right (fun H => 
          match H with
          | or_introl h_eq => neq h_eq
          | or_intror h_in => not_in_tail h_in
          end)
      end
    end
  end.

方式2：用Program Fixpoint（自动补全证明义务） #

如果你坚持用Program Fixpoint，需要先加上构造子占位，再补全对应的证明义务：

Program Fixpoint InDec (s : K) (l : list K) : {In s l} + {~ In s l} :=
  match l with
  | nil => right _
  | head :: tail => 
    if eq_dec s head
    then left _
    else InDec s tail
  end.
Next Obligation. (* 补全空列表下~In s nil的证明 *)
exact (fun H => match H with end).
Qed.
Next Obligation. (* 补全s=head时In s (head::tail)的证明 *)
exact (or_introl eq_refl).
Qed.
Next Obligation. (* 补全s≠head且不在tail时，~In s (head::tail)的证明 *)
intros H.
destruct H as [h_eq | h_in].
- apply (neq h_eq).
- apply (not_in_tail h_in).
Qed.

关键细节解释 #

1. sumbool类型的本质：{P} + {Q} 是带证明的可判定结果类型，它的构造子left/right必须接收对应Prop的证明作为参数，而不是直接传入Prop本身。你之前的误解在于把sumbool类型和它包含的证明内容混淆了——它不是Prop的集合，而是承载"可判定结果+对应证明"的容器。
2. 空列表的证明：In s nil没有合法的构造子，所以用fun H => match H with end构造矛盾证明，以此得到~In s nil。
3. 非空列表的分支处理：
   • 当s=head时，利用In的定义（In a (b::l) = a=b \/ In a l），用or_introl eq构造s在列表中的证明。
   • 当s≠head时，递归判断s是否在尾部：若在尾部，用or_intror把递归证明转换为s在整个列表中的证明；若不在尾部，则构造证明说明s既不等于头部也不在尾部，因此不在整个列表里。

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