在Coq依赖模式匹配中消除不可能分支的方法

针对你遇到的问题，有两种地道的方式让Coq类型检查器认可那些不可能出现的分支可以被省略：

方法一：使用带return子句的依赖模式匹配 #

通过return子句明确关联Node分支与对应的Res类型，让类型检查器跟踪nops n的具体值，从而自动排除不可能的构造子：

Definition nedg (n: Node) (rv: Res (nops n)) : bool :=
  match n as n0 return Res (nops n0) -> bool with
  | n1 => fun rv => match rv with
                   | r1 => true
                   | rb _ => false
                   end
  | n2 => fun rv => match rv with
                   | r2 => true
                   | rb _ => false
                   end
  end rv.

这里的return Res (nops n0) -> bool告诉Coq：对于每个n0分支，我们要返回一个接受Res (nops n0)类型参数的函数。这样在n1分支里，rv的类型被细化为Res op1，只能匹配r1和rb op1；n2分支同理，rv类型是Res op2，只能匹配r2和rb op2，自然不需要处理n1, r2或n2, r1的情况。

方法二：明确指定rb构造子的参数 #

直接在模式匹配中写出rb的参数，让Coq验证参数必须与nops n一致，从而排除不合法的分支：

Definition nedg (n: Node) (rv: Res (nops n)) : bool :=
  match n, rv with
  | n1, r1 => true
  | n1, rb op1 => false
  | n2, r2 => true
  | n2, rb op2 => false
  end.

这种写法利用了Coq的依赖类型约束：当n是n1时，rv的类型是Res op1，因此rb的参数只能是op1；同理n2时参数只能是op2。类型检查器会自动验证这一点，不再要求覆盖那些不可能的分支。

为什么原写法不生效？ #

原代码的模式匹配没有在n的分支和rv的类型之间建立明确的关联。虽然人类能推断出n1对应op1，但Coq需要显式的类型证据来确认r2不可能属于Res op1，通过上述两种方法就能提供这个证据。

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