我可以强制Coq打印括号吗？

Question

我是Coq的新手，从事集合论证明写作。

我意识到省略了括号，这使我很难阅读公式。例如，

1 subgoal
A, B : {set T}
H : B \subset A
______________________________________(1/1)
A :\: A :|: A :&: B = B

但我希望Coq打印(A :\: A) :|: (A :&: B) = B。上面的输出是通过以下代码获得的。

Require Import ssreflect ssrbool ssrnat fintype finset.
Theorem a_a_b__b' (A B : {set T}) : B \subset A -> (A :\: (A :\: B)) = B.
Proof.
  move=> H.
  rewrite setDDr.

令我惊讶的是，如果我setDDr在finset.v中看到的原始编码，则其括号如下所示

Lemma setDDr A B C : A :\: (B :\: C) = (A :\: B) :|: (A :&: C).
Proof. by rewrite !setDE setCI setIUr setCK. Qed.

所以我想知道为什么括号会消失，以及如何强制Coq在CoqIde中显式打印括号。

Answer 1

我不知道有一种机制可以实现您的建议（但它很可能存在，Coq 表示法支持丰富且复杂）。

Coq 应该根据运算符的优先级插入括号，这意味着您必须重新定义 的优先级:|:才能实现您想要的效果。这并不容易做到，而且大多数人不会喜欢它。当前的优先级:|:是数学家所期望的。

一种可能的解决方法是定义一个不同的本地符号供您自己使用：

From mathcomp
Require Import ssreflect ssrbool eqtype ssrnat seq choice fintype finset.

Section U.

Variable (T: finType).

Local Notation "A :||: B" := (@setU T A B) (at level 48, left associativity).

Theorem a_a_b__b' (A B : {set T}) : B \subset A -> (A :\: (A :\: B)) = B.
Proof.
move=> H; rewrite setDDr.

但我建议你暂时使用这个，尝试习惯当前的优先规则，因为你必须阅读其他人的证明，他们也必须阅读你的证明，所以偏离标准实践有一个不小的意义成本。