【Coq】?Rel III 自反传递闭包

自反传递闭包 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
【学习】函数语言程序设计 文章被收录于专栏

函数语言程序设计 Coq章节 Ch1 Basics【COQ中的函数编程】 Ch2 Induction【归纳法证明】 Ch3 Lists【使用结构化数据】 Ch4 Poly【多态性与高阶函数】 Ch5 Tactics【更基本的战术】 Ch6 Logic【COQ中的逻辑】 Ch7 IndProp【归纳定义命题】 Ch8 Maps【全图和局部图】 Ch9 Rel【关系的性质】

全部评论

相关推荐

点赞 评论 收藏
分享
评论
点赞
收藏
分享

创作者周榜

更多
牛客网
牛客网在线编程
牛客网题解
牛客企业服务