我可以强制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.

令我惊讶的是，如果我在finset中看到setDDr的原始编码。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

您可以使用以下命令关闭所有符号:

Unset Printing Notations.

Printing Notations为标志，Unset关闭。你可以从这里找到更多关于符号的信息:https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#syntax-extensions-and-interpretation-scopes.

例如,

(n + m) * 0 = n * 0 + m * 0

将被打印为

eq (Nat.mul (Nat.add n m) O) (Nat.add (Nat.mul n O) (Nat.mul m O))

我知道，这不是一个很好的解决方案。

Answer 2

在Coq的最新版本中，Set Printing Parentheses应该可以工作。

Answer 3

我不知道有什么机制可以做到你所建议的(但它很可能存在，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.

但是我建议你只是暂时使用这个，试着习惯当前的优先规则，因为你必须阅读其他人的证明，他们也必须阅读你的证明，所以偏离标准实践的代价是不小的。