Coq 中的符号答案

【问题标题】：Notations in CoqCoq 中的符号
【发布时间】：2018-02-02 12:17:12
【问题描述】：

我想用符号来表示谓词test如下：

Variable A B : Type.

Inductive test : A -> B -> A -> B -> Prop :=
| test1 : forall a1 a2 b1 b2,
    a1 \ b1 || a2 \ b2
where "c1 '\' st '||' c2 '\' st'" := (test c1 st c2 st')
.

但是，Coq 有一个错误：

为什么 Coq 不能接受这种表示法？

【问题讨论】：

标签： coq

【解决方案1】：

符号被接受，实际上是 Coq 错误地解析了您在 test1 的定义中使用的符号。要正确解析此符号，您需要调整其术语的解析级别。您可以使用保留符号来做到这一点，因为这些用于归纳内符号的 where 子句不支持配置符号的语法：

Variable A B : Type.

Reserved Notation "c1 '\' st '||' c2 '\' st'" (at level 40, st at next level, c2 at next level, no associativity).

Inductive test : A -> B -> A -> B -> Prop :=
| test1 : forall a1 a2 b1 b2,
    a1 \ b1 || a2 \ b2
where "c1 '\' st '||' c2 '\' st'" := (test c1 st c2 st')
.

我对哪些解析级别运行良好没有很好的直觉（40 以上有点随意），所以我能给出的最好建议是进行实验，如果在某处解析不正确，请尝试调整级别。

【讨论】：

它必须在50 或以下级别，因为orb 的|| 级别为50。不过，我承认，我不完全确定冲突的形式。