9

我是 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.vsetDDr的原始编码，它的括号如下

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

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

4

3 回答 3

3

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

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))

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

于 2019-09-26T15:03:20.403 回答
2

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

于 2021-01-04T14:49:00.917 回答
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.

但我建议你只是暂时使用它，试着习惯当前的优先规则，因为你必须阅读其他人的证明，他们也必须阅读你的证明，所以偏离标准做法并非易事成本。

于 2016-10-04T08:59:03.463 回答