pattern-matching - 在 Coq 模式匹配中使用上下文信息

Question

我想定义一个函数 app_1 ，它将 n-ary 函数 f : X ^^ n --> Y 转换为新函数 f' : (Z -> X) ^^ n --> Y，前提是有一个 z : Z 可以对其所有参数应用一次。例如，

Example ex1 : app_1 plus 2 S pred = 4.
trivial. Qed.

app_1 plus 2 能够将一元函数 S 和 pred 作为参数，因为它将它们都应用于 2 首先，然后将结果应用到 plus。

这是我尝试定义的 app_1:

Fixpoint app_1 {X Y Z : Type} {n : nat} 
(f : X ^^ n --> Y) (z : Z) :
(Z -> X) ^^ n --> Y :=
match n return ((Z -> X) ^^ n --> Y) with
| O    => f
| S n' => fun g => app_1 (f (g z)) z
end.

这不起作用，因为 Coq 不喜欢子句 | O => f，并表示:

The term "f" has type "X ^^ n --> Y" while it is expected to have type "(Z -> X) ^^ 0 --> Y".

但如果n = O，X ^^ n --> Y = X ^^ 0 --> Y = Y = (Z -> X) ^^ 0 --> Y，所以这不是类型不匹配。问题是 Coq 无法使用上下文信息 n = O 来找出等价关系。

一些初步搜索表明这是一个众所周知的问题，但如何将这些讨论应用于此案例有点令人困惑。例如，an almost identical question on SO使用return解决了，这也是我上面尝试过的，但没有成功。

有没有办法让这个模式匹配起作用？

Answer 1

像往常一样，您必须应用convoy 模式(参见 Adam Chlipala 的 CPDT 书)并使模式匹配返回一个函数:

Require Import Coq.Numbers.NaryFunctions.

Fixpoint app_1 {X Y Z : Type} {n : nat}
(f : X ^^ n --> Y) (z : Z) :
(Z -> X) ^^ n --> Y :=
match n return (X ^^ n --> Y) -> ((Z -> X) ^^ n --> Y) with
| O    => fun f => f
| S n' => fun f g => app_1 (f (g z)) z
end f.

为了使用有关 f 类型的信息，需要重新抽象它:在每个分支中，它将具有正确的类型。