Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(************************************************************************)

Some properties of the operators on relations

(************************************************************************)

Initial version by Bruno Barras

(************************************************************************)

Require Import Relation_Definitions.
Require Import Relation_Operators.

Section Properties.

  Arguments clos_refl [A] R x _.
  Arguments clos_refl_trans [A] R x _.
  Arguments clos_refl_trans_1n [A] R x _.
  Arguments clos_refl_trans_n1 [A] R x _.
  Arguments clos_refl_sym_trans [A] R _ _.
  Arguments clos_refl_sym_trans_1n [A] R x _.
  Arguments clos_refl_sym_trans_n1 [A] R x _.
  Arguments clos_trans [A] R x _.
  Arguments clos_trans_1n [A] R x _.
  Arguments clos_trans_n1 [A] R x _.
  Arguments inclusion [A] R1 R2.
  Arguments preorder [A] R.

  Variable A : Type.
  Variable R : relation A.

  Section Clos_Refl_Trans.

    Local Notation "R *" := (clos_refl_trans R)
      (at level 8, no associativity, format "R *").

Correctness of the reflexive-transitive closure operator

    Lemma clos_rt_is_preorder : preorder R*.A:Type
R:relation A
preorder R*
    Proof.A:Type
R:relation A
preorder R*
      apply Build_preorder.A:Type
R:relation A
reflexive A R*
A:Type
R:relation A
transitive A R*
      -A:Type
R:relation A
reflexive A R* exact (rt_refl A R).
      -A:Type
R:relation A
transitive A R* exact (rt_trans A R).
    Qed.

Idempotency of the reflexive-transitive closure operator

    Lemma clos_rt_idempotent : inclusion (R*)* R*.A:Type
R:relation A
inclusion (R*)* R*
    Proof.A:Type
R:relation A
inclusion (R*)* R*
      red.A:Type
R:relation A
forall x y : A, (R*)* x y -> R* x y
      induction 1; auto with sets.A:Type
R:relation A
x, y, z:A
H:(R*)* x y
H0:(R*)* y z
IHclos_refl_trans1:R* x y
IHclos_refl_trans2:R* y z
R* x z
      intros.A:Type
R:relation A
x, y, z:A
H:(R*)* x y
H0:(R*)* y z
IHclos_refl_trans1:R* x y
IHclos_refl_trans2:R* y z
R* x z
      apply rt_trans with y; auto with sets.
    Qed.

  End Clos_Refl_Trans.

  Section Clos_Refl_Sym_Trans.

Reflexive-transitive closure is included in the reflexive-symmetric-transitive closure

    Lemma clos_rt_clos_rst :
      inclusion (clos_refl_trans R) (clos_refl_sym_trans R).A:Type
R:relation A
inclusion (clos_refl_trans R) (clos_refl_sym_trans R)
    Proof.A:Type
R:relation A
inclusion (clos_refl_trans R) (clos_refl_sym_trans R)
      red.A:Type
R:relation A
forall x y : A,
clos_refl_trans R x y -> clos_refl_sym_trans R x y
      induction 1; auto with sets.A:Type
R:relation A
x, y, z:A
H:clos_refl_trans R x y
H0:clos_refl_trans R y z
IHclos_refl_trans1:clos_refl_sym_trans R x y
IHclos_refl_trans2:clos_refl_sym_trans R y z
clos_refl_sym_trans R x z
      apply rst_trans with y; auto with sets.
    Qed.

Reflexive closure is included in the reflexive-transitive closure

    Lemma clos_r_clos_rt :
      inclusion (clos_refl R) (clos_refl_trans R).A:Type
R:relation A
inclusion (clos_refl R) (clos_refl_trans R)
    Proof.A:Type
R:relation A
inclusion (clos_refl R) (clos_refl_trans R)
      induction 1 as [? ?| ].A:Type
R:relation A
x, y:A
H:R x y
clos_refl_trans R x y
A:Type
R:relation A
x:A
clos_refl_trans R x x
      -A:Type
R:relation A
x, y:A
H:R x y
clos_refl_trans R x y constructor; auto.
      -A:Type
R:relation A
x:A
clos_refl_trans R x x constructor 2.
    Qed.

    Lemma clos_rt_t : forall x y z,
      clos_refl_trans R x y -> clos_trans R y z ->
      clos_trans R x z.A:Type
R:relation A
forall x y z : A,
clos_refl_trans R x y ->
clos_trans R y z -> clos_trans R x z
    Proof.A:Type
R:relation A
forall x y z : A,
clos_refl_trans R x y ->
clos_trans R y z -> clos_trans R x z
      induction 1 as [b d H1|b|a b d H1 H2 IH1 IH2]; auto.A:Type
R:relation A
z, b, d:A
H1:R b d
clos_trans R d z -> clos_trans R b z
      intro H.A:Type
R:relation A
z, b, d:A
H1:R b d
H:clos_trans R d z
clos_trans R b z apply t_trans with (y:=d); auto.A:Type
R:relation A
z, b, d:A
H1:R b d
H:clos_trans R d z
clos_trans R b d
      constructor.A:Type
R:relation A
z, b, d:A
H1:R b d
H:clos_trans R d z
R b d auto.
    Qed.

Correctness of the reflexive-symmetric-transitive closure

    Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans R).A:Type
R:relation A
equivalence A (clos_refl_sym_trans R)
    Proof.A:Type
R:relation A
equivalence A (clos_refl_sym_trans R)
      apply Build_equivalence.A:Type
R:relation A
reflexive A (clos_refl_sym_trans R)
A:Type
R:relation A
transitive A (clos_refl_sym_trans R)
A:Type
R:relation A
symmetric A (clos_refl_sym_trans R)
      -A:Type
R:relation A
reflexive A (clos_refl_sym_trans R) exact (rst_refl A R).
      -A:Type
R:relation A
transitive A (clos_refl_sym_trans R) exact (rst_trans A R).
      -A:Type
R:relation A
symmetric A (clos_refl_sym_trans R) exact (rst_sym A R).
    Qed.

Idempotency of the reflexive-symmetric-transitive closure operator

    Lemma clos_rst_idempotent :
      inclusion (clos_refl_sym_trans (clos_refl_sym_trans R))
      (clos_refl_sym_trans R).A:Type
R:relation A
inclusion
  (clos_refl_sym_trans (clos_refl_sym_trans R))
  (clos_refl_sym_trans R)
    Proof.A:Type
R:relation A
inclusion
  (clos_refl_sym_trans (clos_refl_sym_trans R))
  (clos_refl_sym_trans R)
      red.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans (clos_refl_sym_trans R) x y ->
clos_refl_sym_trans R x y
      induction 1; auto with sets.A:Type
R:relation A
x, y, z:A
H:clos_refl_sym_trans (clos_refl_sym_trans R) x y
H0:clos_refl_sym_trans (clos_refl_sym_trans R) y z
IHclos_refl_sym_trans1:clos_refl_sym_trans R x y
IHclos_refl_sym_trans2:clos_refl_sym_trans R y z
clos_refl_sym_trans R x z
      apply rst_trans with y; auto with sets.
    Qed.

  End Clos_Refl_Sym_Trans.

  Section Equivalences.

Equivalences between the different definition of the reflexive,

symmetric, transitive closures

Contributed by P. Castéran

Direct transitive closure vs left-step extension

    Lemma clos_t1n_trans : forall x y, clos_trans_1n R x y -> clos_trans R x y.A:Type
R:relation A
forall x y : A,
clos_trans_1n R x y -> clos_trans R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_trans_1n R x y -> clos_trans R x y
     induction 1.A:Type
R:relation A
x, y:A
H:R x y
clos_trans R x y
A:Type
R:relation A
x, y, z:A
H:R x y
H0:clos_trans_1n R y z
IHclos_trans_1n:clos_trans R y z
clos_trans R x z
     -A:Type
R:relation A
x, y:A
H:R x y
clos_trans R x y left; assumption.
     -A:Type
R:relation A
x, y, z:A
H:R x y
H0:clos_trans_1n R y z
IHclos_trans_1n:clos_trans R y z
clos_trans R x z right with y; auto.A:Type
R:relation A
x, y, z:A
H:R x y
H0:clos_trans_1n R y z
IHclos_trans_1n:clos_trans R y z
clos_trans R x y
       left; auto.
    Qed.

    Lemma clos_trans_t1n : forall x y, clos_trans R x y -> clos_trans_1n R x y.A:Type
R:relation A
forall x y : A,
clos_trans R x y -> clos_trans_1n R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_trans R x y -> clos_trans_1n R x y
      induction 1.A:Type
R:relation A
x, y:A
H:R x y
clos_trans_1n R x y
A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_1n R x y
IHclos_trans2:clos_trans_1n R y z
clos_trans_1n R x z
      -A:Type
R:relation A
x, y:A
H:R x y
clos_trans_1n R x y left; assumption.
      -A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_1n R x y
IHclos_trans2:clos_trans_1n R y z
clos_trans_1n R x z generalize IHclos_trans2; clear IHclos_trans2; induction IHclos_trans1.A:Type
R:relation A
z, x, y:A
H:clos_trans R x y
H0:clos_trans R y z
H1:R x y
clos_trans_1n R y z -> clos_trans_1n R x z
A:Type
R:relation A
z, x, z0:A
H:clos_trans R x z0
H0:clos_trans R z0 z
y:A
H1:R x y
IHclos_trans1:clos_trans_1n R y z0
IHIHclos_trans1:clos_trans R y z0 ->
clos_trans R z0 z ->
clos_trans_1n R z0 z ->
clos_trans_1n R y z
clos_trans_1n R z0 z -> clos_trans_1n R x z
        +A:Type
R:relation A
z, x, y:A
H:clos_trans R x y
H0:clos_trans R y z
H1:R x y
clos_trans_1n R y z -> clos_trans_1n R x z right with y; auto.
        +A:Type
R:relation A
z, x, z0:A
H:clos_trans R x z0
H0:clos_trans R z0 z
y:A
H1:R x y
IHclos_trans1:clos_trans_1n R y z0
IHIHclos_trans1:clos_trans R y z0 ->
clos_trans R z0 z ->
clos_trans_1n R z0 z ->
clos_trans_1n R y z
clos_trans_1n R z0 z -> clos_trans_1n R x z right with y; auto.A:Type
R:relation A
z, x, z0:A
H:clos_trans R x z0
H0:clos_trans R z0 z
y:A
H1:R x y
IHclos_trans1:clos_trans_1n R y z0
IHIHclos_trans1:clos_trans R y z0 ->
clos_trans R z0 z ->
clos_trans_1n R z0 z ->
clos_trans_1n R y z
IHclos_trans2:clos_trans_1n R z0 z
clos_trans_1n R y z
      eapply IHIHclos_trans1; auto.A:Type
R:relation A
z, x, z0:A
H:clos_trans R x z0
H0:clos_trans R z0 z
y:A
H1:R x y
IHclos_trans1:clos_trans_1n R y z0
IHIHclos_trans1:clos_trans R y z0 ->
clos_trans R z0 z ->
clos_trans_1n R z0 z ->
clos_trans_1n R y z
IHclos_trans2:clos_trans_1n R z0 z
clos_trans R y z0
      apply clos_t1n_trans; auto.
    Qed.

    Lemma clos_trans_t1n_iff : forall x y,
        clos_trans R x y <-> clos_trans_1n R x y.A:Type
R:relation A
forall x y : A,
clos_trans R x y <-> clos_trans_1n R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_trans R x y <-> clos_trans_1n R x y
      split.A:Type
R:relation A
x, y:A
clos_trans R x y -> clos_trans_1n R x y
A:Type
R:relation A
x, y:A
clos_trans_1n R x y -> clos_trans R x y
      -A:Type
R:relation A
x, y:A
clos_trans R x y -> clos_trans_1n R x y apply clos_trans_t1n.
      -A:Type
R:relation A
x, y:A
clos_trans_1n R x y -> clos_trans R x y apply clos_t1n_trans.
    Qed.

Direct transitive closure vs right-step extension

    Lemma clos_tn1_trans : forall x y, clos_trans_n1 R x y -> clos_trans R x y.A:Type
R:relation A
forall x y : A,
clos_trans_n1 R x y -> clos_trans R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_trans_n1 R x y -> clos_trans R x y
      induction 1.A:Type
R:relation A
x, y:A
H:R x y
clos_trans R x y
A:Type
R:relation A
x, y, z:A
H:R y z
H0:clos_trans_n1 R x y
IHclos_trans_n1:clos_trans R x y
clos_trans R x z
      -A:Type
R:relation A
x, y:A
H:R x y
clos_trans R x y left; assumption.
      -A:Type
R:relation A
x, y, z:A
H:R y z
H0:clos_trans_n1 R x y
IHclos_trans_n1:clos_trans R x y
clos_trans R x z right with y; auto.A:Type
R:relation A
x, y, z:A
H:R y z
H0:clos_trans_n1 R x y
IHclos_trans_n1:clos_trans R x y
clos_trans R y z
        left; assumption.
    Qed.

    Lemma clos_trans_tn1 :  forall x y, clos_trans R x y -> clos_trans_n1 R x y.A:Type
R:relation A
forall x y : A,
clos_trans R x y -> clos_trans_n1 R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_trans R x y -> clos_trans_n1 R x y
      induction 1.A:Type
R:relation A
x, y:A
H:R x y
clos_trans_n1 R x y
A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
clos_trans_n1 R x z
      -A:Type
R:relation A
x, y:A
H:R x y
clos_trans_n1 R x y left; assumption.
      -A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
clos_trans_n1 R x z elim IHclos_trans2.A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
forall y0 : A, R y y0 -> clos_trans_n1 R x y0
A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
forall y0 z0 : A,
R y0 z0 ->
clos_trans_n1 R y y0 ->
clos_trans_n1 R x y0 -> clos_trans_n1 R x z0
        +A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
forall y0 : A, R y y0 -> clos_trans_n1 R x y0 intro y0; right with y.A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
y0:A
H1:R y y0
R y y0
A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
y0:A
H1:R y y0
clos_trans_n1 R x y
          *A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
y0:A
H1:R y y0
R y y0  auto.
          *A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
y0:A
H1:R y y0
clos_trans_n1 R x y auto.
        +A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
forall y0 z0 : A,
R y0 z0 ->
clos_trans_n1 R y y0 ->
clos_trans_n1 R x y0 -> clos_trans_n1 R x z0 intros.A:Type
R:relation A
x, y, z:A
H:clos_trans R x y
H0:clos_trans R y z
IHclos_trans1:clos_trans_n1 R x y
IHclos_trans2:clos_trans_n1 R y z
y0, z0:A
H1:R y0 z0
H2:clos_trans_n1 R y y0
H3:clos_trans_n1 R x y0
clos_trans_n1 R x z0
          right with y0; auto.
    Qed.

    Lemma clos_trans_tn1_iff : forall x y,
        clos_trans R x y <-> clos_trans_n1 R x y.A:Type
R:relation A
forall x y : A,
clos_trans R x y <-> clos_trans_n1 R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_trans R x y <-> clos_trans_n1 R x y
      split.A:Type
R:relation A
x, y:A
clos_trans R x y -> clos_trans_n1 R x y
A:Type
R:relation A
x, y:A
clos_trans_n1 R x y -> clos_trans R x y
      -A:Type
R:relation A
x, y:A
clos_trans R x y -> clos_trans_n1 R x y apply clos_trans_tn1.
      -A:Type
R:relation A
x, y:A
clos_trans_n1 R x y -> clos_trans R x y apply clos_tn1_trans.
    Qed.

Direct reflexive-transitive closure is equivalent to transitivity by left-step extension

    Lemma clos_rt1n_step : forall x y, R x y -> clos_refl_trans_1n R x y.A:Type
R:relation A
forall x y : A, R x y -> clos_refl_trans_1n R x y
    Proof.A:Type
R:relation A
forall x y : A, R x y -> clos_refl_trans_1n R x y
      intros x y H.A:Type
R:relation A
x, y:A
H:R x y
clos_refl_trans_1n R x y
      right with y;[assumption|left].
    Qed.

    Lemma clos_rtn1_step : forall x y, R x y -> clos_refl_trans_n1 R x y.A:Type
R:relation A
forall x y : A, R x y -> clos_refl_trans_n1 R x y
    Proof.A:Type
R:relation A
forall x y : A, R x y -> clos_refl_trans_n1 R x y
      intros x y H.A:Type
R:relation A
x, y:A
H:R x y
clos_refl_trans_n1 R x y
      right with x;[assumption|left].
    Qed.

    Lemma clos_rt1n_rt : forall x y,
        clos_refl_trans_1n R x y -> clos_refl_trans R x y.A:Type
R:relation A
forall x y : A,
clos_refl_trans_1n R x y -> clos_refl_trans R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_trans_1n R x y -> clos_refl_trans R x y
      induction 1.A:Type
R:relation A
x:A
clos_refl_trans R x x
A:Type
R:relation A
x, y, z:A
H:R x y
H0:clos_refl_trans_1n R y z
IHclos_refl_trans_1n:clos_refl_trans R y z
clos_refl_trans R x z
      -A:Type
R:relation A
x:A
clos_refl_trans R x x constructor 2.
      -A:Type
R:relation A
x, y, z:A
H:R x y
H0:clos_refl_trans_1n R y z
IHclos_refl_trans_1n:clos_refl_trans R y z
clos_refl_trans R x z constructor 3 with y; auto.A:Type
R:relation A
x, y, z:A
H:R x y
H0:clos_refl_trans_1n R y z
IHclos_refl_trans_1n:clos_refl_trans R y z
clos_refl_trans R x y
        constructor 1; auto.
    Qed.

    Lemma clos_rt_rt1n : forall x y,
        clos_refl_trans R x y -> clos_refl_trans_1n R x y.A:Type
R:relation A
forall x y : A,
clos_refl_trans R x y -> clos_refl_trans_1n R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_trans R x y -> clos_refl_trans_1n R x y
      induction 1.A:Type
R:relation A
x, y:A
H:R x y
clos_refl_trans_1n R x y
A:Type
R:relation A
x:A
clos_refl_trans_1n R x x
A:Type
R:relation A
x, y, z:A
H:clos_refl_trans R x y
H0:clos_refl_trans R y z
IHclos_refl_trans1:clos_refl_trans_1n R x y
IHclos_refl_trans2:clos_refl_trans_1n R y z
clos_refl_trans_1n R x z
      -A:Type
R:relation A
x, y:A
H:R x y
clos_refl_trans_1n R x y apply clos_rt1n_step; assumption.
      -A:Type
R:relation A
x:A
clos_refl_trans_1n R x x left.
      -A:Type
R:relation A
x, y, z:A
H:clos_refl_trans R x y
H0:clos_refl_trans R y z
IHclos_refl_trans1:clos_refl_trans_1n R x y
IHclos_refl_trans2:clos_refl_trans_1n R y z
clos_refl_trans_1n R x z generalize IHclos_refl_trans2; clear IHclos_refl_trans2;
          induction IHclos_refl_trans1; auto.A:Type
R:relation A
z, x, z0:A
H:clos_refl_trans R x z0
H0:clos_refl_trans R z0 z
y:A
H1:R x y
IHclos_refl_trans1:clos_refl_trans_1n R y z0
IHIHclos_refl_trans1:clos_refl_trans R y z0 ->
clos_refl_trans R z0 z ->
clos_refl_trans_1n R z0 z ->
clos_refl_trans_1n R y z
clos_refl_trans_1n R z0 z -> clos_refl_trans_1n R x z

        right with y; auto.A:Type
R:relation A
z, x, z0:A
H:clos_refl_trans R x z0
H0:clos_refl_trans R z0 z
y:A
H1:R x y
IHclos_refl_trans1:clos_refl_trans_1n R y z0
IHIHclos_refl_trans1:clos_refl_trans R y z0 ->
clos_refl_trans R z0 z ->
clos_refl_trans_1n R z0 z ->
clos_refl_trans_1n R y z
IHclos_refl_trans2:clos_refl_trans_1n R z0 z
clos_refl_trans_1n R y z
        eapply IHIHclos_refl_trans1; auto.A:Type
R:relation A
z, x, z0:A
H:clos_refl_trans R x z0
H0:clos_refl_trans R z0 z
y:A
H1:R x y
IHclos_refl_trans1:clos_refl_trans_1n R y z0
IHIHclos_refl_trans1:clos_refl_trans R y z0 ->
clos_refl_trans R z0 z ->
clos_refl_trans_1n R z0 z ->
clos_refl_trans_1n R y z
IHclos_refl_trans2:clos_refl_trans_1n R z0 z
clos_refl_trans R y z0
        apply clos_rt1n_rt; auto.
    Qed.

    Lemma clos_rt_rt1n_iff : forall x y,
      clos_refl_trans R x y <-> clos_refl_trans_1n R x y.A:Type
R:relation A
forall x y : A,
clos_refl_trans R x y <-> clos_refl_trans_1n R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_trans R x y <-> clos_refl_trans_1n R x y
      split.A:Type
R:relation A
x, y:A
clos_refl_trans R x y -> clos_refl_trans_1n R x y
A:Type
R:relation A
x, y:A
clos_refl_trans_1n R x y -> clos_refl_trans R x y
      -A:Type
R:relation A
x, y:A
clos_refl_trans R x y -> clos_refl_trans_1n R x y apply clos_rt_rt1n.
      -A:Type
R:relation A
x, y:A
clos_refl_trans_1n R x y -> clos_refl_trans R x y apply clos_rt1n_rt.
    Qed.

Direct reflexive-transitive closure is equivalent to transitivity by right-step extension

    Lemma clos_rtn1_rt : forall x y,
        clos_refl_trans_n1 R x y -> clos_refl_trans R x y.A:Type
R:relation A
forall x y : A,
clos_refl_trans_n1 R x y -> clos_refl_trans R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_trans_n1 R x y -> clos_refl_trans R x y
      induction 1.A:Type
R:relation A
x:A
clos_refl_trans R x x
A:Type
R:relation A
x, y, z:A
H:R y z
H0:clos_refl_trans_n1 R x y
IHclos_refl_trans_n1:clos_refl_trans R x y
clos_refl_trans R x z
      -A:Type
R:relation A
x:A
clos_refl_trans R x x constructor 2.
      -A:Type
R:relation A
x, y, z:A
H:R y z
H0:clos_refl_trans_n1 R x y
IHclos_refl_trans_n1:clos_refl_trans R x y
clos_refl_trans R x z constructor 3 with y; auto.A:Type
R:relation A
x, y, z:A
H:R y z
H0:clos_refl_trans_n1 R x y
IHclos_refl_trans_n1:clos_refl_trans R x y
clos_refl_trans R y z
        constructor 1; assumption.
    Qed.

    Lemma clos_rt_rtn1 :  forall x y,
        clos_refl_trans R x y -> clos_refl_trans_n1 R x y.A:Type
R:relation A
forall x y : A,
clos_refl_trans R x y -> clos_refl_trans_n1 R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_trans R x y -> clos_refl_trans_n1 R x y
      induction 1.A:Type
R:relation A
x, y:A
H:R x y
clos_refl_trans_n1 R x y
A:Type
R:relation A
x:A
clos_refl_trans_n1 R x x
A:Type
R:relation A
x, y, z:A
H:clos_refl_trans R x y
H0:clos_refl_trans R y z
IHclos_refl_trans1:clos_refl_trans_n1 R x y
IHclos_refl_trans2:clos_refl_trans_n1 R y z
clos_refl_trans_n1 R x z
      -A:Type
R:relation A
x, y:A
H:R x y
clos_refl_trans_n1 R x y apply clos_rtn1_step; auto.
      -A:Type
R:relation A
x:A
clos_refl_trans_n1 R x x left.
      -A:Type
R:relation A
x, y, z:A
H:clos_refl_trans R x y
H0:clos_refl_trans R y z
IHclos_refl_trans1:clos_refl_trans_n1 R x y
IHclos_refl_trans2:clos_refl_trans_n1 R y z
clos_refl_trans_n1 R x z elim IHclos_refl_trans2; auto.A:Type
R:relation A
x, y, z:A
H:clos_refl_trans R x y
H0:clos_refl_trans R y z
IHclos_refl_trans1:clos_refl_trans_n1 R x y
IHclos_refl_trans2:clos_refl_trans_n1 R y z
forall y0 z0 : A,
R y0 z0 ->
clos_refl_trans_n1 R y y0 ->
clos_refl_trans_n1 R x y0 -> clos_refl_trans_n1 R x z0
        intros.A:Type
R:relation A
x, y, z:A
H:clos_refl_trans R x y
H0:clos_refl_trans R y z
IHclos_refl_trans1:clos_refl_trans_n1 R x y
IHclos_refl_trans2:clos_refl_trans_n1 R y z
y0, z0:A
H1:R y0 z0
H2:clos_refl_trans_n1 R y y0
H3:clos_refl_trans_n1 R x y0
clos_refl_trans_n1 R x z0
        right with y0; auto.
    Qed.

    Lemma clos_rt_rtn1_iff : forall x y,
        clos_refl_trans R x y <-> clos_refl_trans_n1 R x y.A:Type
R:relation A
forall x y : A,
clos_refl_trans R x y <-> clos_refl_trans_n1 R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_trans R x y <-> clos_refl_trans_n1 R x y
      split.A:Type
R:relation A
x, y:A
clos_refl_trans R x y -> clos_refl_trans_n1 R x y
A:Type
R:relation A
x, y:A
clos_refl_trans_n1 R x y -> clos_refl_trans R x y
      -A:Type
R:relation A
x, y:A
clos_refl_trans R x y -> clos_refl_trans_n1 R x y apply clos_rt_rtn1.
      -A:Type
R:relation A
x, y:A
clos_refl_trans_n1 R x y -> clos_refl_trans R x y apply clos_rtn1_rt.
    Qed.

Induction on the left transitive step

    Lemma clos_refl_trans_ind_left :
      forall (x:A) (P:A -> Prop), P x ->
	(forall y z:A, clos_refl_trans R x y -> P y -> R y z -> P z) ->
	forall z:A, clos_refl_trans R x z -> P z.A:Type
R:relation A
forall (x : A) (P : A -> Prop),
P x ->
(forall y z : A,
 clos_refl_trans R x y -> P y -> R y z -> P z) ->
forall z : A, clos_refl_trans R x z -> P z
    Proof.A:Type
R:relation A
forall (x : A) (P : A -> Prop),
P x ->
(forall y z : A,
 clos_refl_trans R x y -> P y -> R y z -> P z) ->
forall z : A, clos_refl_trans R x z -> P z
      intros.A:Type
R:relation A
x:A
P:A -> Prop
H:P x
H0:forall y z0 : A,
clos_refl_trans R x y -> P y -> R y z0 -> P z0
z:A
H1:clos_refl_trans R x z
P z
      revert H H0.A:Type
R:relation A
x:A
P:A -> Prop
z:A
H1:clos_refl_trans R x z
P x ->
(forall y z0 : A,
 clos_refl_trans R x y -> P y -> R y z0 -> P z0) ->
P z
      induction H1; intros; auto with sets.A:Type
R:relation A
P:A -> Prop
x, y:A
H:R x y
H0:P x
H1:forall y0 z : A,
clos_refl_trans R x y0 -> P y0 -> R y0 z -> P z
P y
A:Type
R:relation A
P:A -> Prop
x, y, z:A
H1_:clos_refl_trans R x y
H1_0:clos_refl_trans R y z
IHclos_refl_trans1:P x ->
(forall y0 z0 : A,
 clos_refl_trans R x y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P y
IHclos_refl_trans2:P y ->
(forall y0 z0 : A,
 clos_refl_trans R y y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P z
H:P x
H0:forall y0 z0 : A,
clos_refl_trans R x y0 -> P y0 -> R y0 z0 -> P z0
P z
      -A:Type
R:relation A
P:A -> Prop
x, y:A
H:R x y
H0:P x
H1:forall y0 z : A,
clos_refl_trans R x y0 -> P y0 -> R y0 z -> P z
P y apply H1 with x; auto with sets.

      -A:Type
R:relation A
P:A -> Prop
x, y, z:A
H1_:clos_refl_trans R x y
H1_0:clos_refl_trans R y z
IHclos_refl_trans1:P x ->
(forall y0 z0 : A,
 clos_refl_trans R x y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P y
IHclos_refl_trans2:P y ->
(forall y0 z0 : A,
 clos_refl_trans R y y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P z
H:P x
H0:forall y0 z0 : A,
clos_refl_trans R x y0 -> P y0 -> R y0 z0 -> P z0
P z apply IHclos_refl_trans2.A:Type
R:relation A
P:A -> Prop
x, y, z:A
H1_:clos_refl_trans R x y
H1_0:clos_refl_trans R y z
IHclos_refl_trans1:P x ->
(forall y0 z0 : A,
 clos_refl_trans R x y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P y
IHclos_refl_trans2:P y ->
(forall y0 z0 : A,
 clos_refl_trans R y y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P z
H:P x
H0:forall y0 z0 : A,
clos_refl_trans R x y0 -> P y0 -> R y0 z0 -> P z0
P y
A:Type
R:relation A
P:A -> Prop
x, y, z:A
H1_:clos_refl_trans R x y
H1_0:clos_refl_trans R y z
IHclos_refl_trans1:P x ->
(forall y0 z0 : A,
 clos_refl_trans R x y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P y
IHclos_refl_trans2:P y ->
(forall y0 z0 : A,
 clos_refl_trans R y y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P z
H:P x
H0:forall y0 z0 : A,
clos_refl_trans R x y0 -> P y0 -> R y0 z0 -> P z0
forall y0 z0 : A,
clos_refl_trans R y y0 -> P y0 -> R y0 z0 -> P z0
        +A:Type
R:relation A
P:A -> Prop
x, y, z:A
H1_:clos_refl_trans R x y
H1_0:clos_refl_trans R y z
IHclos_refl_trans1:P x ->
(forall y0 z0 : A,
 clos_refl_trans R x y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P y
IHclos_refl_trans2:P y ->
(forall y0 z0 : A,
 clos_refl_trans R y y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P z
H:P x
H0:forall y0 z0 : A,
clos_refl_trans R x y0 -> P y0 -> R y0 z0 -> P z0
P y apply IHclos_refl_trans1; auto with sets.

        +A:Type
R:relation A
P:A -> Prop
x, y, z:A
H1_:clos_refl_trans R x y
H1_0:clos_refl_trans R y z
IHclos_refl_trans1:P x ->
(forall y0 z0 : A,
 clos_refl_trans R x y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P y
IHclos_refl_trans2:P y ->
(forall y0 z0 : A,
 clos_refl_trans R y y0 ->
 P y0 -> R y0 z0 -> P z0) -> 
P z
H:P x
H0:forall y0 z0 : A,
clos_refl_trans R x y0 -> P y0 -> R y0 z0 -> P z0
forall y0 z0 : A,
clos_refl_trans R y y0 -> P y0 -> R y0 z0 -> P z0 intros.A:Type
R:relation A
P:A -> Prop
x, y, z:A
H1_:clos_refl_trans R x y
H1_0:clos_refl_trans R y z
IHclos_refl_trans1:P x ->
(forall y1 z1 : A,
 clos_refl_trans R x y1 ->
 P y1 -> R y1 z1 -> P z1) -> 
P y
IHclos_refl_trans2:P y ->
(forall y1 z1 : A,
 clos_refl_trans R y y1 ->
 P y1 -> R y1 z1 -> P z1) -> 
P z
H:P x
H0:forall y1 z1 : A,
clos_refl_trans R x y1 -> P y1 -> R y1 z1 -> P z1
y0, z0:A
H1:clos_refl_trans R y y0
H2:P y0
H3:R y0 z0
P z0
          apply H0 with y0; auto with sets.A:Type
R:relation A
P:A -> Prop
x, y, z:A
H1_:clos_refl_trans R x y
H1_0:clos_refl_trans R y z
IHclos_refl_trans1:P x ->
(forall y1 z1 : A,
 clos_refl_trans R x y1 ->
 P y1 -> R y1 z1 -> P z1) -> 
P y
IHclos_refl_trans2:P y ->
(forall y1 z1 : A,
 clos_refl_trans R y y1 ->
 P y1 -> R y1 z1 -> P z1) -> 
P z
H:P x
H0:forall y1 z1 : A,
clos_refl_trans R x y1 -> P y1 -> R y1 z1 -> P z1
y0, z0:A
H1:clos_refl_trans R y y0
H2:P y0
H3:R y0 z0
clos_refl_trans R x y0
          apply rt_trans with y; auto with sets.
    Qed.

Induction on the right transitive step

    Lemma rt1n_ind_right : forall (P : A -> Prop) (z:A),
      P z ->
      (forall x y, R x y -> clos_refl_trans_1n R y z -> P y -> P x) ->
      forall x, clos_refl_trans_1n R x z -> P x.A:Type
R:relation A
forall (P : A -> Prop) (z : A),
P z ->
(forall x y : A,
 R x y -> clos_refl_trans_1n R y z -> P y -> P x) ->
forall x : A, clos_refl_trans_1n R x z -> P x
      induction 3; auto.A:Type
R:relation A
P:A -> Prop
z:A
H:P z
H0:forall x0 y0 : A,
R x0 y0 ->
clos_refl_trans_1n R y0 z -> P y0 -> P x0
x, y:A
H1:R x y
H2:clos_refl_trans_1n R y z
IHclos_refl_trans_1n:P z ->
(forall x0 y0 : A,
 R x0 y0 ->
 clos_refl_trans_1n R y0 z ->
 P y0 -> P x0) -> 
P y
P x
      apply H0 with y; auto.
    Qed.

    Lemma clos_refl_trans_ind_right : forall (P : A -> Prop) (z:A),
      P z ->
      (forall x y, R x y -> P y -> clos_refl_trans R y z -> P x) ->
      forall x, clos_refl_trans R x z -> P x.A:Type
R:relation A
forall (P : A -> Prop) (z : A),
P z ->
(forall x y : A,
 R x y -> P y -> clos_refl_trans R y z -> P x) ->
forall x : A, clos_refl_trans R x z -> P x
      intros P z Hz IH x Hxz.A:Type
R:relation A
P:A -> Prop
z:A
Hz:P z
IH:forall x0 y : A,
R x0 y -> P y -> clos_refl_trans R y z -> P x0
x:A
Hxz:clos_refl_trans R x z
P x
      apply clos_rt_rt1n_iff in Hxz.A:Type
R:relation A
P:A -> Prop
z:A
Hz:P z
IH:forall x0 y : A,
R x0 y -> P y -> clos_refl_trans R y z -> P x0
x:A
Hxz:clos_refl_trans_1n R x z
P x
      elim Hxz using rt1n_ind_right; auto.A:Type
R:relation A
P:A -> Prop
z:A
Hz:P z
IH:forall x0 y : A,
R x0 y -> P y -> clos_refl_trans R y z -> P x0
x:A
Hxz:clos_refl_trans_1n R x z
forall x0 y : A,
R x0 y -> clos_refl_trans_1n R y z -> P y -> P x0
      clear x Hxz.A:Type
R:relation A
P:A -> Prop
z:A
Hz:P z
IH:forall x y : A,
R x y -> P y -> clos_refl_trans R y z -> P x
forall x y : A,
R x y -> clos_refl_trans_1n R y z -> P y -> P x
      intros x y Hxy Hyz Hy.A:Type
R:relation A
P:A -> Prop
z:A
Hz:P z
IH:forall x0 y0 : A,
R x0 y0 -> P y0 -> clos_refl_trans R y0 z -> P x0
x, y:A
Hxy:R x y
Hyz:clos_refl_trans_1n R y z
Hy:P y
P x
      apply clos_rt_rt1n_iff in Hyz.A:Type
R:relation A
P:A -> Prop
z:A
Hz:P z
IH:forall x0 y0 : A,
R x0 y0 -> P y0 -> clos_refl_trans R y0 z -> P x0
x, y:A
Hxy:R x y
Hyz:clos_refl_trans R y z
Hy:P y
P x
      eauto.
    Qed.

Direct reflexive-symmetric-transitive closure is equivalent to transitivity by symmetric left-step extension

    Lemma clos_rst1n_rst  : forall x y,
      clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans R x y.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans_1n R x y ->
clos_refl_sym_trans R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans_1n R x y ->
clos_refl_sym_trans R x y
      induction 1.A:Type
R:relation A
x:A
clos_refl_sym_trans R x x
A:Type
R:relation A
x, y, z:A
H:R x y \/ R y x
H0:clos_refl_sym_trans_1n R y z
IHclos_refl_sym_trans_1n:clos_refl_sym_trans R y z
clos_refl_sym_trans R x z
      -A:Type
R:relation A
x:A
clos_refl_sym_trans R x x constructor 2.
      -A:Type
R:relation A
x, y, z:A
H:R x y \/ R y x
H0:clos_refl_sym_trans_1n R y z
IHclos_refl_sym_trans_1n:clos_refl_sym_trans R y z
clos_refl_sym_trans R x z constructor 4 with y; auto.A:Type
R:relation A
x, y, z:A
H:R x y \/ R y x
H0:clos_refl_sym_trans_1n R y z
IHclos_refl_sym_trans_1n:clos_refl_sym_trans R y z
clos_refl_sym_trans R x y
        case H;[constructor 1|constructor 3; constructor 1]; auto.
    Qed.

    Lemma clos_rst1n_trans : forall x y z, clos_refl_sym_trans_1n R x y ->
        clos_refl_sym_trans_1n R y z -> clos_refl_sym_trans_1n R x z.A:Type
R:relation A
forall x y z : A,
clos_refl_sym_trans_1n R x y ->
clos_refl_sym_trans_1n R y z ->
clos_refl_sym_trans_1n R x z
      induction 1.A:Type
R:relation A
z, x:A
clos_refl_sym_trans_1n R x z ->
clos_refl_sym_trans_1n R x z
A:Type
R:relation A
z, x, y, z0:A
H:R x y \/ R y x
H0:clos_refl_sym_trans_1n R y z0
IHclos_refl_sym_trans_1n:clos_refl_sym_trans_1n R z0
  z ->
clos_refl_sym_trans_1n R y
  z
clos_refl_sym_trans_1n R z0 z ->
clos_refl_sym_trans_1n R x z
      -A:Type
R:relation A
z, x:A
clos_refl_sym_trans_1n R x z ->
clos_refl_sym_trans_1n R x z auto.
      -A:Type
R:relation A
z, x, y, z0:A
H:R x y \/ R y x
H0:clos_refl_sym_trans_1n R y z0
IHclos_refl_sym_trans_1n:clos_refl_sym_trans_1n R z0
  z ->
clos_refl_sym_trans_1n R y
  z
clos_refl_sym_trans_1n R z0 z ->
clos_refl_sym_trans_1n R x z intros; right with y; eauto.
    Qed.

    Lemma clos_rst1n_sym : forall x y, clos_refl_sym_trans_1n R x y ->
      clos_refl_sym_trans_1n R y x.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans_1n R x y ->
clos_refl_sym_trans_1n R y x
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans_1n R x y ->
clos_refl_sym_trans_1n R y x
      intros x y H; elim H.A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_1n R x y
forall x0 : A, clos_refl_sym_trans_1n R x0 x0
A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_1n R x y
forall x0 y0 z : A,
R x0 y0 \/ R y0 x0 ->
clos_refl_sym_trans_1n R y0 z ->
clos_refl_sym_trans_1n R z y0 ->
clos_refl_sym_trans_1n R z x0
      -A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_1n R x y
forall x0 : A, clos_refl_sym_trans_1n R x0 x0 constructor 1.
      -A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_1n R x y
forall x0 y0 z : A,
R x0 y0 \/ R y0 x0 ->
clos_refl_sym_trans_1n R y0 z ->
clos_refl_sym_trans_1n R z y0 ->
clos_refl_sym_trans_1n R z x0 intros x0 y0 z D H0 H1; apply clos_rst1n_trans with y0; auto.A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_1n R x y
x0, y0, z:A
D:R x0 y0 \/ R y0 x0
H0:clos_refl_sym_trans_1n R y0 z
H1:clos_refl_sym_trans_1n R z y0
clos_refl_sym_trans_1n R y0 x0
        right with x0.A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_1n R x y
x0, y0, z:A
D:R x0 y0 \/ R y0 x0
H0:clos_refl_sym_trans_1n R y0 z
H1:clos_refl_sym_trans_1n R z y0
R y0 x0 \/ R x0 y0
A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_1n R x y
x0, y0, z:A
D:R x0 y0 \/ R y0 x0
H0:clos_refl_sym_trans_1n R y0 z
H1:clos_refl_sym_trans_1n R z y0
clos_refl_sym_trans_1n R x0 x0
        +A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_1n R x y
x0, y0, z:A
D:R x0 y0 \/ R y0 x0
H0:clos_refl_sym_trans_1n R y0 z
H1:clos_refl_sym_trans_1n R z y0
R y0 x0 \/ R x0 y0 tauto.
        +A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_1n R x y
x0, y0, z:A
D:R x0 y0 \/ R y0 x0
H0:clos_refl_sym_trans_1n R y0 z
H1:clos_refl_sym_trans_1n R z y0
clos_refl_sym_trans_1n R x0 x0 left.
    Qed.

    Lemma clos_rst_rst1n  : forall x y,
      clos_refl_sym_trans R x y -> clos_refl_sym_trans_1n R x y.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans R x y ->
clos_refl_sym_trans_1n R x y
      induction 1.A:Type
R:relation A
x, y:A
H:R x y
clos_refl_sym_trans_1n R x y
A:Type
R:relation A
x:A
clos_refl_sym_trans_1n R x x
A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans R x y
IHclos_refl_sym_trans:clos_refl_sym_trans_1n R x y
clos_refl_sym_trans_1n R y x
A:Type
R:relation A
x, y, z:A
H:clos_refl_sym_trans R x y
H0:clos_refl_sym_trans R y z
IHclos_refl_sym_trans1:clos_refl_sym_trans_1n R x y
IHclos_refl_sym_trans2:clos_refl_sym_trans_1n R y z
clos_refl_sym_trans_1n R x z
      -A:Type
R:relation A
x, y:A
H:R x y
clos_refl_sym_trans_1n R x y constructor 2 with y; auto.A:Type
R:relation A
x, y:A
H:R x y
clos_refl_sym_trans_1n R y y
        constructor 1.
      -A:Type
R:relation A
x:A
clos_refl_sym_trans_1n R x x constructor 1.
      -A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans R x y
IHclos_refl_sym_trans:clos_refl_sym_trans_1n R x y
clos_refl_sym_trans_1n R y x apply clos_rst1n_sym; auto.
      -A:Type
R:relation A
x, y, z:A
H:clos_refl_sym_trans R x y
H0:clos_refl_sym_trans R y z
IHclos_refl_sym_trans1:clos_refl_sym_trans_1n R x y
IHclos_refl_sym_trans2:clos_refl_sym_trans_1n R y z
clos_refl_sym_trans_1n R x z eapply clos_rst1n_trans; eauto.
    Qed.

    Lemma clos_rst_rst1n_iff : forall x y,
      clos_refl_sym_trans R x y <-> clos_refl_sym_trans_1n R x y.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans R x y <->
clos_refl_sym_trans_1n R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans R x y <->
clos_refl_sym_trans_1n R x y
      split.A:Type
R:relation A
x, y:A
clos_refl_sym_trans R x y ->
clos_refl_sym_trans_1n R x y
A:Type
R:relation A
x, y:A
clos_refl_sym_trans_1n R x y ->
clos_refl_sym_trans R x y
      -A:Type
R:relation A
x, y:A
clos_refl_sym_trans R x y ->
clos_refl_sym_trans_1n R x y apply clos_rst_rst1n.
      -A:Type
R:relation A
x, y:A
clos_refl_sym_trans_1n R x y ->
clos_refl_sym_trans R x y apply clos_rst1n_rst.
    Qed.

Direct reflexive-symmetric-transitive closure is equivalent to transitivity by symmetric right-step extension

    Lemma clos_rstn1_rst : forall x y,
      clos_refl_sym_trans_n1 R x y -> clos_refl_sym_trans R x y.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans_n1 R x y ->
clos_refl_sym_trans R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans_n1 R x y ->
clos_refl_sym_trans R x y
      induction 1.A:Type
R:relation A
x:A
clos_refl_sym_trans R x x
A:Type
R:relation A
x, y, z:A
H:R y z \/ R z y
H0:clos_refl_sym_trans_n1 R x y
IHclos_refl_sym_trans_n1:clos_refl_sym_trans R x y
clos_refl_sym_trans R x z
      -A:Type
R:relation A
x:A
clos_refl_sym_trans R x x constructor 2.
      -A:Type
R:relation A
x, y, z:A
H:R y z \/ R z y
H0:clos_refl_sym_trans_n1 R x y
IHclos_refl_sym_trans_n1:clos_refl_sym_trans R x y
clos_refl_sym_trans R x z constructor 4 with y; auto.A:Type
R:relation A
x, y, z:A
H:R y z \/ R z y
H0:clos_refl_sym_trans_n1 R x y
IHclos_refl_sym_trans_n1:clos_refl_sym_trans R x y
clos_refl_sym_trans R y z
        case H;[constructor 1|constructor 3; constructor 1]; auto.
    Qed.

    Lemma clos_rstn1_trans : forall x y z, clos_refl_sym_trans_n1 R x y ->
      clos_refl_sym_trans_n1 R y z -> clos_refl_sym_trans_n1 R x z.A:Type
R:relation A
forall x y z : A,
clos_refl_sym_trans_n1 R x y ->
clos_refl_sym_trans_n1 R y z ->
clos_refl_sym_trans_n1 R x z
    Proof.A:Type
R:relation A
forall x y z : A,
clos_refl_sym_trans_n1 R x y ->
clos_refl_sym_trans_n1 R y z ->
clos_refl_sym_trans_n1 R x z
      intros x y z H1 H2.A:Type
R:relation A
x, y, z:A
H1:clos_refl_sym_trans_n1 R x y
H2:clos_refl_sym_trans_n1 R y z
clos_refl_sym_trans_n1 R x z
      induction H2.A:Type
R:relation A
x, y:A
H1:clos_refl_sym_trans_n1 R x y
clos_refl_sym_trans_n1 R x y
A:Type
R:relation A
x, y:A
H1:clos_refl_sym_trans_n1 R x y
y0, z:A
H:R y0 z \/ R z y0
H2:clos_refl_sym_trans_n1 R y y0
IHclos_refl_sym_trans_n1:clos_refl_sym_trans_n1 R x
  y0
clos_refl_sym_trans_n1 R x z
      -A:Type
R:relation A
x, y:A
H1:clos_refl_sym_trans_n1 R x y
clos_refl_sym_trans_n1 R x y auto.
      -A:Type
R:relation A
x, y:A
H1:clos_refl_sym_trans_n1 R x y
y0, z:A
H:R y0 z \/ R z y0
H2:clos_refl_sym_trans_n1 R y y0
IHclos_refl_sym_trans_n1:clos_refl_sym_trans_n1 R x
  y0
clos_refl_sym_trans_n1 R x z intros.A:Type
R:relation A
x, y:A
H1:clos_refl_sym_trans_n1 R x y
y0, z:A
H:R y0 z \/ R z y0
H2:clos_refl_sym_trans_n1 R y y0
IHclos_refl_sym_trans_n1:clos_refl_sym_trans_n1 R x
  y0
clos_refl_sym_trans_n1 R x z
        right with y0; eauto.
    Qed.

    Lemma clos_rstn1_sym : forall x y, clos_refl_sym_trans_n1 R x y ->
      clos_refl_sym_trans_n1 R y x.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans_n1 R x y ->
clos_refl_sym_trans_n1 R y x
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans_n1 R x y ->
clos_refl_sym_trans_n1 R y x
      intros x y H; elim H.A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
clos_refl_sym_trans_n1 R x x
A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
forall y0 z : A,
R y0 z \/ R z y0 ->
clos_refl_sym_trans_n1 R x y0 ->
clos_refl_sym_trans_n1 R y0 x ->
clos_refl_sym_trans_n1 R z x
      -A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
clos_refl_sym_trans_n1 R x x constructor 1.
      -A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
forall y0 z : A,
R y0 z \/ R z y0 ->
clos_refl_sym_trans_n1 R x y0 ->
clos_refl_sym_trans_n1 R y0 x ->
clos_refl_sym_trans_n1 R z x intros y0 z D H0 H1.A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
y0, z:A
D:R y0 z \/ R z y0
H0:clos_refl_sym_trans_n1 R x y0
H1:clos_refl_sym_trans_n1 R y0 x
clos_refl_sym_trans_n1 R z x apply clos_rstn1_trans with y0; auto.A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
y0, z:A
D:R y0 z \/ R z y0
H0:clos_refl_sym_trans_n1 R x y0
H1:clos_refl_sym_trans_n1 R y0 x
clos_refl_sym_trans_n1 R z y0
        right with z.A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
y0, z:A
D:R y0 z \/ R z y0
H0:clos_refl_sym_trans_n1 R x y0
H1:clos_refl_sym_trans_n1 R y0 x
R z y0 \/ R y0 z
A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
y0, z:A
D:R y0 z \/ R z y0
H0:clos_refl_sym_trans_n1 R x y0
H1:clos_refl_sym_trans_n1 R y0 x
clos_refl_sym_trans_n1 R z z
        +A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
y0, z:A
D:R y0 z \/ R z y0
H0:clos_refl_sym_trans_n1 R x y0
H1:clos_refl_sym_trans_n1 R y0 x
R z y0 \/ R y0 z tauto.
        +A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans_n1 R x y
y0, z:A
D:R y0 z \/ R z y0
H0:clos_refl_sym_trans_n1 R x y0
H1:clos_refl_sym_trans_n1 R y0 x
clos_refl_sym_trans_n1 R z z left.
    Qed.

    Lemma clos_rst_rstn1 : forall x y,
      clos_refl_sym_trans R x y -> clos_refl_sym_trans_n1 R x y.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans R x y ->
clos_refl_sym_trans_n1 R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans R x y ->
clos_refl_sym_trans_n1 R x y
      induction 1.A:Type
R:relation A
x, y:A
H:R x y
clos_refl_sym_trans_n1 R x y
A:Type
R:relation A
x:A
clos_refl_sym_trans_n1 R x x
A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans R x y
IHclos_refl_sym_trans:clos_refl_sym_trans_n1 R x y
clos_refl_sym_trans_n1 R y x
A:Type
R:relation A
x, y, z:A
H:clos_refl_sym_trans R x y
H0:clos_refl_sym_trans R y z
IHclos_refl_sym_trans1:clos_refl_sym_trans_n1 R x y
IHclos_refl_sym_trans2:clos_refl_sym_trans_n1 R y z
clos_refl_sym_trans_n1 R x z
      -A:Type
R:relation A
x, y:A
H:R x y
clos_refl_sym_trans_n1 R x y constructor 2 with x; auto.A:Type
R:relation A
x, y:A
H:R x y
clos_refl_sym_trans_n1 R x x
        constructor 1.
      -A:Type
R:relation A
x:A
clos_refl_sym_trans_n1 R x x constructor 1.
      -A:Type
R:relation A
x, y:A
H:clos_refl_sym_trans R x y
IHclos_refl_sym_trans:clos_refl_sym_trans_n1 R x y
clos_refl_sym_trans_n1 R y x apply clos_rstn1_sym; auto.
      -A:Type
R:relation A
x, y, z:A
H:clos_refl_sym_trans R x y
H0:clos_refl_sym_trans R y z
IHclos_refl_sym_trans1:clos_refl_sym_trans_n1 R x y
IHclos_refl_sym_trans2:clos_refl_sym_trans_n1 R y z
clos_refl_sym_trans_n1 R x z eapply clos_rstn1_trans; eauto.
    Qed.

    Lemma clos_rst_rstn1_iff : forall x y,
      clos_refl_sym_trans R x y <-> clos_refl_sym_trans_n1 R x y.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans R x y <->
clos_refl_sym_trans_n1 R x y
    Proof.A:Type
R:relation A
forall x y : A,
clos_refl_sym_trans R x y <->
clos_refl_sym_trans_n1 R x y
      split.A:Type
R:relation A
x, y:A
clos_refl_sym_trans R x y ->
clos_refl_sym_trans_n1 R x y
A:Type
R:relation A
x, y:A
clos_refl_sym_trans_n1 R x y ->
clos_refl_sym_trans R x y
      -A:Type
R:relation A
x, y:A
clos_refl_sym_trans R x y ->
clos_refl_sym_trans_n1 R x y apply clos_rst_rstn1.
      -A:Type
R:relation A
x, y:A
clos_refl_sym_trans_n1 R x y ->
clos_refl_sym_trans R x y apply clos_rstn1_rst.
    Qed.

  End Equivalences.

  Lemma clos_trans_transp_permute : forall x y,
    transp _ (clos_trans R) x y <-> clos_trans (transp _ R) x y.A:Type
R:relation A
forall x y : A,
transp A (clos_trans R) x y <->
clos_trans (transp A R) x y
  Proof.A:Type
R:relation A
forall x y : A,
transp A (clos_trans R) x y <->
clos_trans (transp A R) x y
    split; induction 1;
    (apply t_step; assumption) || eapply t_trans; eassumption.
  Qed.

End Properties.

(* begin hide *)
(* Compatibility *)
Notation trans_tn1 := clos_trans_tn1 (only parsing).
Notation tn1_trans := clos_tn1_trans (only parsing).
Notation tn1_trans_equiv := clos_trans_tn1_iff (only parsing).

Notation trans_t1n := clos_trans_t1n (only parsing).
Notation t1n_trans := clos_t1n_trans (only parsing).
Notation t1n_trans_equiv := clos_trans_t1n_iff (only parsing).

Notation R_rtn1 := clos_rtn1_step (only parsing).
Notation trans_rt1n := clos_rt_rt1n (only parsing).
Notation rt1n_trans := clos_rt1n_rt (only parsing).
Notation rt1n_trans_equiv := clos_rt_rt1n_iff (only parsing).

Notation R_rt1n := clos_rt1n_step (only parsing).
Notation trans_rtn1 := clos_rt_rtn1 (only parsing).
Notation rtn1_trans := clos_rtn1_rt (only parsing).
Notation rtn1_trans_equiv := clos_rt_rtn1_iff (only parsing).

Notation rts1n_rts := clos_rst1n_rst (only parsing).
Notation rts_1n_trans := clos_rst1n_trans (only parsing).
Notation rts1n_sym := clos_rst1n_sym (only parsing).
Notation rts_rts1n := clos_rst_rst1n (only parsing).
Notation rts_rts1n_equiv := clos_rst_rst1n_iff (only parsing).

Notation rtsn1_rts := clos_rstn1_rst (only parsing).
Notation rtsn1_trans := clos_rstn1_trans (only parsing).
Notation rtsn1_sym := clos_rstn1_sym (only parsing).
Notation rts_rtsn1 := clos_rst_rstn1 (only parsing).
Notation rts_rtsn1_equiv := clos_rst_rstn1_iff (only parsing).
(* end hide *)