这一短小的（可选的）章节发展了一些关于Coq中二元关系的基本定义和几个定理。关键定义在实际使用的地方重复（在编程语言基础的Smallstep一章中），因此已经熟悉这些概念的读者可以安全地浏览或跳过本章。然而，关系也是使用Coq的基本推理工具开发工具的一个很好的练习来源，因此在IndProp一章之后查看此材料可能会很有用。

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export IndProp.

关系 Relations

集合X上的二元关系是由X的两个元素参数化的命题族，即关于X元素对的命题。

Definition relation (X: Type) := X -> X -> Prop.

相当令人困惑的是，Coq标准库劫持了这个想法的特定实例的通用术语“关系”。为了保持与库的一致性，我们也将这样做。因此，从今往后，Coq标识符关系将始终指某个集合（集合与自身之间）上的二元关系，而在普通数学英语中，“关系”一词可以指这个特定概念，也可以指任何数量的可能不同集合之间关系的更一般概念。讨论的背景应始终明确其含义。

nat上的一个示例关系是le，小于或等于关系，我们通常写n1≤ n2。

Print le.
(* ====> Inductive le (n : nat) : nat -> Prop :=
             le_n : n <= n
           | le_S : forall m : nat, n <= m -> n <= S m *)
Check le : nat -> nat -> Prop.
Check le : relation nat.

Inductive le (n : nat) : nat -> Prop :=  le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m

Arguments le (_ _)%nat_scope
Arguments le_n _%nat_scope
Arguments le_S (_ _)%nat_scope _

（为什么我们这样写，而不是从

Inductive le : relation nat...

？因为我们想把第一个nat放在:,的左边,这使得Coq产生了一个更好的归纳原理来推理≤。）