coq - COQ 中的依赖模式匹配问题

Question

(小更新，使其更接近我的实际任务)

如何写f2使用依赖模式匹配？ (下面的代码编译，但 f2 的定义除外)

Inductive parse_ret : Set :=
  No : parse_ret | Yes : parse_ret.

Inductive exp : parse_ret -> Set :=
| No_parse : exp No
| Yes_parse : exp Yes.

Definition f1 (p : parse_ret) : option (exp p) :=
  match p with
  | No => Some No_parse
  | Yes => Some Yes_parse
  end.
          
Definition f2' : option nat :=
  match f1 No with
  | Some No_parse => Some 1
  | Some Yes_parse => Some 1
  | None => None
  end.

所以，f2'几乎就是我所需要的，但是Some Yes_parse这里显然是多余的，因为我们提供了 No构造函数 f1和f1的返回类型变为option (exp No) .

如何编写 f2 的定义？避免Non exhaustive pattern-matching错误？

Definition f2 : option nat :=
  match f1 No with
  | Some No_parse => Some 1
  | None => None                            
  end.

Answer 1

我认为这是 Coq 模式匹配编译算法的一个缺陷。这部分负责将您作为用户编写的奇特模式匹配细化为内核可理解的模式。

在这里，它必须做两件事:一是将深度模式匹配(同时匹配 option 和 exp)脱糖为两个嵌套模式匹配;另一个是检测由于类型限制而不必考虑某些构造函数，这将允许您避免给出 Some Yes_parse 子句。然而，该算法在当前状态下无法做到这一点。

因此，你必须手动帮助它。一种可能性是为其完成第一部分，然后编写

Definition f2' : option nat :=
  match f1 No with
    | None => None
    | Some p =>
      match p in exp r with
        | No_parse => Some 1
      end
  end.

Coq 对此很满意，如果你打印出详细的术语，你会得到

match f1 No with
| Some p =>
    match p in (exp r) return match r with
                              | No => option nat
                              | Yes => IDProp
                              end with
    | No_parse => Some 1
    | Yes_parse => idProp
    end
| None => None
end

您可以看到阐述者对内部匹配进行了处理，并引入了一个智能返回子句来处理非详尽性问题。