在 Coq 中用两个递归变量定义递归表示法

【问题标题】：Define recursive notation with two recursive variables in Coq在 Coq 中用两个递归变量定义递归表示法
【发布时间】：2018-06-29 00:05:59
【问题描述】：

我想为类型上下文定义一个如下所示的符号：

{ x1 : T1, x2 : T2, x3 : T3 }

但是，我想不出一种方法来递归地定义这种符号。我的猜测如下：

Notation "{ x1 : T1 , .. , xn : Tn }" := (cons (x1, T1) .. (cons (xn, Tn)) ..).

我收到以下错误：“找不到递归模式的开始位置。”

这样的递归符号是否可行，如果可以，如何实现？

【问题讨论】：

我在 GitHub 上打开了issue #7959。让我们看看会发生什么。
它以某种方式被解析为{ x1 : (T1 , .. , xn) : Tn }...

标签： coq

【解决方案1】：

Coq 似乎不将 x1 : T1 和 xn : Tn 识别为表达式，而是将符号解析为 { x1 : (T1 , .. , xn) : Tn }。这建议在以下两个步骤中定义符号。

Section T. (* To see the effect of the notation after closing this section. *)

(* recursive list notation *)
Notation "{ x1 , .. , xn }" :=
  (cons x1 .. (cons xn nil) ..).

(* pair notation *)
Notation "x : T" := ((x, T))
(at level 100).

Definition z := { 3 : 4, 5 : 6, 7 : 8 }.

Print z.
(* z = {3 : 4, 5 : 6, 7 : 8} *)

End T.

Print z.
(* z = ((3, 4) :: (5, 6) :: (7, 8) :: nil)%list *)

【讨论】：

（欢迎修复以消除通常的类型注释语法的歧义！我对关卡系统不够熟悉。）
这看起来应该可以。稍后我将研究的其他内容是，是否有办法设置范围，以便第二个表示法仅在大括号内有效。谢谢！