Coq：通过对其参数的数量进行模式匹配来定义函数

【问题标题】：Coq: Defining a function by pattern matching on the arity of its argumentCoq：通过对其参数的数量进行模式匹配来定义函数
【发布时间】：2017-04-22 19:03:09
【问题描述】：

我想定义一个函数，其行为取决于它的参数是否（至少）是一个 n 位函数。一个基本的（失败的）尝试是

Definition rT {y:Type}(x:y) := ltac: (match y with
 | _ -> _ -> _ => exact True
 | _ => exact False end).

Check prod: Type -> Type -> Type.
Compute rT prod. (*= False: Prop*)
Print rT. (*rT = fun (y : Type) (_ : y) => False: forall y : Type, y -> Prop*)

如您所见，rT 将所有内容映射到 False。为什么？如果我将匹配子句中的y 替换为type of x，结果保持不变

【问题讨论】：

标签： function match definition coq

【解决方案1】：

你想要的函数不能以你期望的类型存在于 Gallina 中。

你的函数被接受了，但是如果你打印它，你可以看到它的主体是：

rT = fun (y : Type) (_ : y) => False

Gallina 无法在Type 上使用match-ing。有一些方法可以处理 n 元函数，这样您就可以检查它们的元数，但它涉及依赖类型来静态捕获元数。例如，对于统一的 n 元函数：

https://coq.inria.fr/library/Coq.Numbers.NaryFunctions.html

【讨论】：

这背后的原因是 Coq 的模式匹配被设计为仅适用于归纳类型的构造函数吗？
模式匹配有两个级别。 “Gallina”模式匹配确实只适用于归纳和共归纳类型。您的代码使用的“Ltac”模式匹配更具语法性，因此它的作用不能表示为 Gallina 术语（通常）。