Coq中使用通配符'_'匹配失败的问题求助

你的问题核心在于混淆了返回逻辑命题（Prop）的In函数和返回布尔值（bool）的成员判断函数，同时错误地尝试对Prop类型进行模式匹配。

为什么原代码报错？ #

1. In n t返回的是Prop类型（逻辑上“n在t中”这个命题），而非可计算的bool类型。Coq不允许直接对Prop做模式匹配来构造可计算函数，且你写的| False => ...是把逻辑命题False当成了布尔常量false，二者完全是不同概念。
2. 正因为In n t的类型是Prop，Coq认为你的通配符_冗余——前面的False分支根本匹配不到任何合法的Prop值，所有情况都会被通配符覆盖，因此抛出提示。
3. 移除通配符后写| => ...属于语法错误，Coq要求match分支必须明确写出模式，不能空着。

修正方案1：使用布尔值版本的成员判断（推荐） #

Coq标准库List模块提供了返回bool的mem函数，用它替换In即可正常定义函数：

Require Import List.

Fixpoint norepeat_subseq {X : Type} (l : list X) : list X :=
  match l with
  | [] => []
  | n :: t => match List.mem n t with
              | false => n :: norepeat_subseq t  (* n不在后续列表中，保留 *)
              | true => norepeat_subseq t         (* n已在后续列表中，跳过 *)
              end
  end.

修正方案2：基于可判定性处理Prop类型的In #

如果一定要用返回Prop的In，需要借助可判定性引理，将命题转换为可匹配的sumbool类型（{P} + {~P}，表示P成立或不成立）。这需要为类型X提供相等性判定函数：

Require Import List.
Require Import Decidable.

Fixpoint norepeat_subseq {X : Type} (eq_dec : forall x y : X, {x = y} + {x <> y}) (l : list X) : list X :=
  match l with
  | [] => []
  | n :: t => match In_dec eq_dec n t with
              | right _ => n :: norepeat_subseq eq_dec t  (* In n t 不成立，保留n *)
              | left _ => norepeat_subseq eq_dec t         (* In n t 成立，跳过n *)
              end
  end.

这个版本需要传入eq_dec参数来判定X中元素的相等性，适合需要保留Prop语义的场景。

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