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

Question

我在理解依赖类型的模式匹配方面遇到了困难。假设我们有以下代码：

Variant Op := op1 | op2.

Variant Res : Op -> Set :=
| r1 : Res op1
| r2 : Res op2
| rb : forall op, Res op
.

Variant Node := n1 | n2.

Definition nops (n: Node) : Op :=
  match n with
  | n1 => op1
  | n2 => op2
  end.

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

正如所写，它诅咒了

nedg

中的非详尽模式匹配，因为我们不考虑

n1, r2

和

n2, r1

分支。鉴于

nedg

声明，我们删除它们的道德权利是非常明显的，所以，问题是，最惯用的方法是什么来说服类型检查器省略分支实际上是不可能的？

Answer 1

欢迎来到依赖模式匹配的奇妙世界。您不能总是说服类型检查器排除某些情况，具体取决于（类型检查器的）当前版本中包含了多少调整。

但是你可以手工完成。通过为排除的情况产生荒谬。这是一个可能的解决方案：

Variant Op := op1 | op2.

Variant Res : Op -> Set :=
| r1 : Res op1
| r2 : Res op2
| rb : forall op, Res op
.

Variant Node := n1 | n2.

Definition nops (n: Node) : Op :=
  match n with
  | n1 => op1
  | n2 => op2
  end.

Definition not_op1 o :=
 match o with 
 | op1 => False
 | _ => True
 end.

Definition not_op2 o :=
 match o with 
 | op2 => False
 | _ => True
 end.

Definition nedg (n: Node) : Res (nops n) -> bool :=
  match n with
  | n1 => fun rv => match rv in Res o return not_op2 o -> bool with
    | r1   => fun _ => true
    | rb _ => fun _ => false
    | r2   => fun C => match C with end
    end I
  | n2 => fun rv => match rv in Res o return not_op1 o -> bool with
    | r2   => fun _ => true
    | rb _ => fun _ => false
    | r1   => fun C => match C with end
    end I
  end.

Goal nedg n1 r1 = true.         Proof. reflexivity. Qed.
Goal nedg n1 (rb op1) = false.  Proof. reflexivity. Qed.
Goal nedg n2 r2 = true.         Proof. reflexivity. Qed.
Goal nedg n2 (rb op2) = false.  Proof. reflexivity. Qed.

请注意，

第一个

C中的

match C with end

是类型

not_op2 op2

，可简化为

False

。此外，第一个

I

的类型为

not_op2 (nops n1)

，可简化为

True

。