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在这里显然是多余的，因为我们为f1和f1的[=提供了No构造函数29=] 类型变为 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

我不太熟悉花哨的 match 表达式，但是，在这种非常特殊的情况下，似乎在匹配中只使用 Some _ 会更容易。如果你需要这个，你可以证明一个引理表明 f1 No 总是 Some No_parse.

您也可以改为定义 f2 以采用 option (exp No) 类型的参数，并将问题委托给函数调用者。

当然，所有这些可能都在说明显而易见的...

Answer 2

我认为这是 Coq pattern-matching 编译算法的缺陷。这是负责将您作为用户编写的一个奇特的 pattern-matching 设计成内核可以理解的部分。

这里，它要做两件事：一是将一个深度pattern-matching（一次匹配option和exp）脱糖成两个嵌套的pattern-matching ;另一个是检测某些构造函数由于类型约束而不被考虑，这将允许您避免给出 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

你看到阐述者已经修改了内部匹配并引入了一个聪明的 return 子句来处理 non-exhaustiveness 问题。

COQ 中依赖模式匹配的问题

Problem with Dependent pattern matching in COQ

coq