自反传递闭包 Reflexive, Transitive Closure

关系R的自反传递闭包是包含R的最小关系，它既是自反的又是传递的。形式上，在Coq标准库的关系模块中定义如下：

Inductive clos_refl_trans {A: Type} (R: relation A)

Inductive clos_refl_trans {A: Type} (R: relation A) : relation A :=
  | rt_step x y (H : R x y) : clos_refl_trans R x y
  | rt_refl x : clos_refl_trans R x x
  | rt_trans x y z
        (Hxy : clos_refl_trans R x y)
        (Hyz : clos_refl_trans R y z) :
        clos_refl_trans R x z.

例如，next_nat关系的自反和传递闭包与le关系一致。

Theorem next_nat_closure_is_le

Theorem next_nat_closure_is_le : forall n m,
  (n <= m) <-> ((clos_refl_trans next_nat) n m).

Proof

Proof.
  intros n m. split.
  - (* -> *)
    intro H. induction H.
    + (* le_n *) apply rt_refl.
    + (* le_S *)
      apply rt_trans with m. apply IHle. apply rt_step.
      apply nn.
  - (* <- *)
    intro H. induction H.
    + (* rt_step *) inversion H. apply le_S. apply le_n.
    + (* rt_refl *) apply le_n.
    + (* rt_trans *)
      apply le_trans with y.
      apply IHclos_refl_trans1.
      apply IHclos_refl_trans2. Qed.

上面对自反传递闭包的定义是自然的：它明确地说，R的自反传递闭包是包含R的最小关系，并且在自反性和传递性规则下是封闭的。但事实证明，这个定义对于进行证明并不十分方便，因为rt_trans规则的“不确定性”有时会导致复杂的归纳。以下是一个更有用的定义：

Inductive clos_refl_trans_1n {A : Type}(R : relation A) (x : A)

Inductive clos_refl_trans_1n {A : Type}
                             (R : relation A) (x : A)
                             : A -> Prop :=
  | rt1n_refl : clos_refl_trans_1n R x x
  | rt1n_trans (y z : A)
      (Hxy : R x y) (Hrest : clos_refl_trans_1n R y z) :
      clos_refl_trans_1n R x z.

我们对自反传递闭包的新定义将rt_步骤和rt_trans规则“捆绑”到单个规则步骤中。这一步的左侧前提是R的一次使用，导致了更简单的归纳原理。

在继续之前，我们应该检查这两个定义是否确实定义了相同的关系。。。

首先，我们证明了两个引理，表明clos_refl_trans_1n模仿了两个“缺失”clos_refl_trans构造函数的行为。

Lemma rsc_R

Lemma rsc_R : forall (X:Type) (R:relation X) (x y : X),
  R x y -> clos_refl_trans_1n R x y.

Proof

Proof.
  intros X R x y H.
  apply rt1n_trans with y. apply H. apply rt1n_refl.   Qed.

Exercise: 2 stars, standard, optional (rsc_trans)

Lemma rsc_trans

Lemma rsc_trans :
  forall (X:Type) (R: relation X) (x y z : X),
      clos_refl_trans_1n R x y  ->
      clos_refl_trans_1n R y z ->
      clos_refl_trans_1n R x z.
Proof.
  (* FILL IN HERE *) Admitted.

Solution

然后我们用这些事实来证明，自反、传递闭包的两个定义确实定义了相同的关系。

Exercise: 3 stars, standard, optional (rtc_rsc_coincide)

Theorem rtc_rsc_coincide

Theorem rtc_rsc_coincide :
  forall (X:Type) (R: relation X) (x y : X),
    clos_refl_trans R x y <-> clos_refl_trans_1n R x y.
Proof.
  (* FILL IN HERE *) Admitted.

Solution