基本性质 Basic Properties

任何人都知道，上过离散数学本科课程的人，一般来说，关于关系有很多话要说，包括对关系进行分类的方法（如自反、传递等），关于某些类型的关系可以一般证明的定理，从一个关系到另一个关系的构造，等等。例如。。。

偏函数 Partial Functions

集合X上的关系R是一个偏函数，如果对于每个X，至多有一个y，使得 R x y ——即R x y1和 R x y2 一起表示y1=y2。

Definition partial_function {X: Type} (R: relation X)

Definition partial_function {X: Type} (R: relation X) :=
  forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.

例如，前面定义的next_nat关系是一个分部函数。

Print next_nat.
(* ====> Inductive next_nat (n : nat) : nat -> Prop :=
           nn : next_nat n (S n) *)
Check next_nat : relation nat.

Inductive next_nat : nat -> nat -> Prop

Inductive next_nat : nat -> nat -> Prop :=  nn : forall n : nat, next_nat n (S n)

Arguments next_nat (_ _)%nat_scope
Arguments nn _%nat_scope

Theorem next_nat_partial_function

Theorem next_nat_partial_function :
  partial_function next_nat.

Proof

Proof.
  unfold partial_function.
  intros x y1 y2 H1 H2.
  inversion H1. inversion H2.
  reflexivity.  Qed.

但是，数字上的≤关系不是部分函数。（假设，对于一个矛盾，≤是一个部分函数。但是，由于0≤0和0≤ 1，由此得出0=1。这是胡说八道，所以我们的假设是矛盾的。）

Theorem le_not_a_partial_function

Theorem le_not_a_partial_function :
  ~ (partial_function le).

Proof

Proof.
  unfold not. unfold partial_function. intros Hc.
  assert (0 = 1) as Nonsense. {
    apply Hc with (x := 0).
    - apply le_n.
    - apply le_S. apply le_n. }
  discriminate Nonsense.   Qed.

Exercise: 2 stars, standard, optional (total_relation_not_partial)

表明IndProp（中的练习）中定义的total_relation不是部分函数。

(* FILL IN HERE *)

Exercise: 2 stars, standard, optional (empty_relation_partial)

显示在IndProp(中的练习)中定义的empty_relation是一个部分函数。

(* FILL IN HERE *)

自反关系 Reflexive Relations

集合X上的自反关系是X的每个元素都与其自身相关的关系。

Definition reflexive {X: Type} (R: relation X)

Definition reflexive {X: Type} (R: relation X) :=
  forall a : X, R a a.

Theorem le_reflexive

Theorem le_reflexive :
  reflexive le.

Proof

Proof.
  unfold reflexive. 
  intros n. 
  apply le_n.  
  Qed.

传递关系 Transitive Relations

当R a b和R b c成立时，如果R a c成立，则关系R是可传递的。

Definition transitive {X: Type} (R: relation X)

Definition transitive {X: Type} (R: relation X) :=
  forall a b c : X, (R a b) -> (R b c) -> (R a c).

Theorem le_trans

Theorem le_trans :
  transitive le.

Proof

Proof.
  intros n m o Hnm Hmo.
  induction Hmo.
  - (* le_n *) apply Hnm.
  - (* le_S *) apply le_S. 
               apply IHHmo.  
               Qed.

Theorem lt_trans:

Theorem lt_trans:
  transitive lt.

Proof

Proof.
  unfold lt. 
  unfold transitive.
  intros n m o Hnm Hmo.
  apply le_S in Hnm.
  apply le_trans with (a := (S n)) (b := (S m)) (c := o).
  apply Hnm.
  apply Hmo. 
  Qed.

Exercise: 2 stars, standard, optional (le_trans_hard_way)

我们也可以通过归纳法更费力地证明 lt_tran，而不使用le_trans。这样做。

Theorem lt_trans'

Theorem lt_trans' :
  transitive lt.
Proof.
  (* Prove this by induction on evidence that [m] is less than [o]. *)
  unfold lt. unfold transitive.
  intros n m o Hnm Hmo.
  induction Hmo as [| m' Hm'o].
    (* FILL IN HERE *) Admitted.

Solution

Theorem lt_trans' :
  transitive lt.
Proof.
  (* Prove this by induction on evidence that [m] is less than [o]. *)
  unfold lt. unfold transitive.
  intros n m o Hnm Hmo.
  induction Hmo as [| m' Hm'o].
-  apply le_S in Hnm. 
   rewrite Hnm. 
   apply le_n.
- apply le_S in IHHm'o. 
  rewrite IHHm'o. 
  apply le_n.
Qed.

Exercise: 2 stars, standard, optional (lt_trans'')

通过对o的归纳再次证明同样的事情。

Theorem lt_trans''

Theorem lt_trans'' :
  transitive lt.
Proof.
  unfold lt. unfold transitive.
  intros n m o Hnm Hmo.
  induction o as [| o'].
  (* FILL IN HERE *) Admitted.

Solution

Theorem lt_trans'' :
  transitive lt.
Proof.
  unfold lt. unfold transitive.
  intros n m o Hnm Hmo.
  induction o as [| o'].
-  apply le_S in Hnm. 
    apply le_trans with (a := (S n)) (b := (S m)) (c := 0).
-- apply Hnm.
-- apply Hmo.
- apply le_S in Hnm.
apply le_trans with (a := (S n)) (b := (S m)) (c := S o').
-- apply Hnm.
-- apply Hmo.
Qed.

le的及物性反过来可以用来证明一些事实，这些事实在以后将是有用的（例如，用于证明下面的反对称性）。。。

Theorem le_Sn_le

Theorem le_Sn_le : forall n m, S n <= m -> n <= m.

Proof

Proof.
  intros n m H. apply le_trans with (S n).
  - apply le_S. apply le_n.
  - apply H.
Qed.

Exercise: 1 star, standard, optional (le_S_n)

Theorem le_S_n

Theorem le_S_n : forall n m,
  (S n <= S m) -> (n <= m).
Proof.
  (* FILL IN HERE *) Admitted.

Solution

Exercise: 2 stars, standard, optional (le_Sn_n_inf)

提供以下定理的非正式证明：

Theorem: For every n, ¬ (S n ≤ n)

下面是一个可选的正式证明，但是试着写一个非正式证明，而不先做正式证明。

Exercise: 1 star, standard, optional (le_Sn_n)

Theorem le_Sn_n

Theorem le_Sn_n : forall n,
  ~ (S n <= n).
Proof.
  (* FILL IN HERE *) Admitted.

Solution

自反性和及物性是我们在后面章节中需要用到的主要概念，但是，对于在Coq中处理关系的一些额外实践，让我们看看其他一些常见的概念。。。

对称与反对称关系 Symmetric and Antisymmetric Relations

如果 R a b 意味着 R b a ，则关系R是对称的。

Definition symmetric

Definition symmetric {X: Type} (R: relation X) :=
  forall a b : X, (R a b) -> (R b a).

Exercise: 2 stars, standard, optional (le_not_symmetric)

Theorem le_not_symmetric

Theorem le_not_symmetric :
  ~ (symmetric le).
Proof.
  (* FILL IN HERE *) Admitted.

Solution

关系R是反对称的，如果 R a b 和 R b a 一起意味着 a = b ——也就是说，如果R中唯一的“循环”是平凡的循环。

Definition antisymmetric {X: Type} (R: relation X)

Definition antisymmetric {X: Type} (R: relation X) :=
  forall a b : X, (R a b) -> (R b a) -> a = b.

Exercise: 2 stars, standard, optional (le_antisymmetric)

Theorem le_antisymmetric

Theorem le_antisymmetric :
  antisymmetric le.
Proof.
  (* FILL IN HERE *) Admitted.

Solution

Exercise: 2 stars, standard, optional (le_step)

Theorem le_step

Theorem le_step : forall n m p,
  n < m ->
  m <= S p ->
  n <= p.
Proof.
  (* FILL IN HERE *) Admitted.

Solution

等价关系 Equivalence Relations

如果关系是自反的、对称的和传递的，那么它就是等价的。

Definition equivalence {X:Type} (R: relation X)

Definition equivalence {X:Type} (R: relation X) :=
  (reflexive R) /\ (symmetric R) /\ (transitive R).

偏序与预序 Partial Orders and Preorders

关系是自反的、反对称的和传递的偏序。在Coq标准库中，简称为“订单”。

Definition order {X:Type} (R: relation X)

Definition order {X:Type} (R: relation X) :=
  (reflexive R) /\ (antisymmetric R) /\ (transitive R).

前序几乎类似于偏序，但不一定是反对称的。

Definition preorder {X:Type} (R: relation X)

Definition preorder {X:Type} (R: relation X) :=
  (reflexive R) /\ (transitive R).

Theorem le_order

Theorem le_order :
  order le.

Proof

Proof.
  unfold order. split.
    - (* refl *) apply le_reflexive.
    - split.
      + (* antisym *) apply le_antisymmetric.
      + (* transitive. *) apply le_trans.  
Qed.