pattern-matching - 在 Coq 的单个子句中模式匹配多个构造函数

Question

假设我有一个归纳类型的算术表达式exp

Inductive exp : Type :=
| num : nat -> exp
| plus : exp -> exp -> exp
| minus : exp -> exp -> exp
| mult : exp -> exp -> exp
| div : exp -> exp -> exp.

我想定义一个函数 expsum，它返回 exp 中出现的所有数字的总和。明显的实现是

Fixpoint expsum (e : exp) : nat :=
match e with
| num n => n 
| plus e1 e2 => expsum e1 + expsum e2
| minus e1 e2 => expsum e1 + expsum e2
| mult e1 e2 => expsum e1 + expsum e2
| div e1 e2 => expsum e1 + expsum e2
end.

但对于构造函数 plus、minus、mult 和 div、expsum 在模式匹配之后做完全相同的事情。我想把它简化成类似的东西

Fixpoint expsum (e : exp) : nat :=
match e with
| num n => n 
| [ plus e1 e2 | minus e1 e2 | mult e1 e2 | div e1 e2 ]
   => expsum e1 + expsum e2
end.

这样单个子句就可以处理多个构造函数。我想我已经在其他函数式语言中看到过这样做。这在 Coq 中可能吗？

Answer 1

这在术语语言中是做不到的。由于依赖类型，Coq 的语言本身非常强大，但它不是自己的元语言；没有办法编写一个 Coq 术语来操纵 Coq 构造函数(仅作为术语，这不足以构建模式匹配)。

可能有一种方法可以用白话来做到这一点(顶级语言，你可以用它来编写术语的定义、策略语言的证明等)，但我认为没有。如果它存在于任何地方，我希望它在 Program 中。但是，将相同的模式应用于碰巧具有相同类型的构造函数是一个相当特殊的需求。

可以用证明语言来完成。 Coq 中的证明只是术语；有助于重复证明的策略可以以同样的方式帮助重复的术语。

Inductive exp : Type :=
| num : nat -> exp
| plus : exp -> exp -> exp
| minus : exp -> exp -> exp
| mult : exp -> exp -> exp
| div : exp -> exp -> exp.

(* The boring old code *)    
Fixpoint expsum (e : exp) : nat :=
match e with
| num n => n 
| plus e1 e2 => expsum e1 + expsum e2
| minus e1 e2 => expsum e1 + expsum e2
| mult e1 e2 => expsum e1 + expsum e2
| div e1 e2 => expsum e1 + expsum e2
end.

Definition expsum_tactic : exp -> nat.
  induction 1;
    (* Figure out the computation automatically based on what arguments are present *)
    exact n || exact (IHexp1 + IHexp2).
Defined. (* "Defined" rather than "Qed" to get a transparent definition *)

(* Show the two definitions in a nice way to visually compare them *)
Print expsum.
Eval compute [expsum expsum_tactic exp_rec] in (expsum, expsum_tactic).

这可以通过使用匹配目标战术构造来分析每个构造函数的参数并相应地构建结果项，从而将其推广到可变元数。

虽然这可行，但很棘手。策略适用于编写证明，其中计算内容无关紧要。当您使用它们来编写实际定义很重要(而不是类型)的术语时，您需要非常小心以确保您定义的是您期望的术语，而不是碰巧具有相同的其他术语类型。您可能已经思考了几分钟，该代码没有赢得可读性奖。

我一般不推荐这种方法，因为它容易出错。但当您有许多相似的类型和功能并且类型在开发过程中发生变化时，它会很有用。您最终会得到相当难以理解的策略，但是一旦您调试了它们，即使您调整表达式类型它们也可以工作。