Coq中的Unicode“不等于”表示法（≠）

Question

以下文本出现在 SF 书中：

我们过去常常使用“不是”来说明 0 和 1 是自然数的不同元素：

Theorem zero_not_one : ~(0 = 1).
Proof.
  intros contra. inversion contra.
Qed.

Such inequality statements are frequent enough to warrant a special notation, x ≠ y:

Check (0 ≠ 1).
(* ===> Prop *)

但是当我在Coq中尝试这样做时：

Check (0 ≠ 1).

它给我返回了这个错误信息：

Syntax Error: Lexer: Undefined token

实际上，在查看标准库时，我无法找到任何与此相关的符号。那么，它的正确符号是什么？

- Sibi

---

不熟悉 Coq 类型语言，但看标准库，肯定“不等于”是 <> 或 <-> 吧？ - Jonathon Ogden

@JonathonOgden 是的，你说得对。是 <>。我看过它但忽略了，因为它在单子上操作。 :) 你能把它发表成一个答案吗？ - Sibi

完成。另外建议查看@Elazar的答案。很有道理。 - Jonathon Ogden

Answer 1

如@jonathon所说，操作符的写法是<>。

Check 1 <> 2.

但你也可以这样做：

Require Import Unicode.Utf8.
Check 1 ≠ 2.

- Elazar

Answer 2

虽然不熟悉Coq类型语言，但是从标准库来看，“不等于”应该写成<>。

- Jonathon Ogden

---

"<->" 是“当且仅当”的意思。 - Elazar