# Initial version by Bruno Barras

Require Import Relation_Definitions.
Require Import Relation_Operators.

Section Properties.

Variable A : Type.
Variable R : relation A.

Section Clos_Refl_Trans.

Correctness of the reflexive-transitive closure operator
Idempotency of the reflexive-transitive closure operator

Lemma clos_rt_idempotent : inclusion (R*)* R*.

End Clos_Refl_Trans.

Section Clos_Refl_Sym_Trans.

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

Lemma clos_r_clos_rt :
inclusion (clos_refl R) (clos_refl_trans R).

Lemma clos_rt_t : forall x y z,
clos_refl_trans R x y -> clos_trans R y z ->
clos_trans R x z.

Correctness of the reflexive-symmetric-transitive closure
Idempotency of the reflexive-symmetric-transitive closure operator

### 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.

Lemma clos_trans_t1n : forall x y, clos_trans R x y -> clos_trans_1n R x y.

Lemma clos_trans_t1n_iff : forall x y,
clos_trans R x y <-> clos_trans_1n R x y.

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.

Lemma clos_trans_tn1 : forall x y, clos_trans R x y -> clos_trans_n1 R x y.

Lemma clos_trans_tn1_iff : forall x y,
clos_trans R x y <-> clos_trans_n1 R x y.

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.

Lemma clos_rtn1_step : forall x y, R x y -> clos_refl_trans_n1 R x y.

Lemma clos_rt1n_rt : forall x y,
clos_refl_trans_1n R x y -> clos_refl_trans R x y.

Lemma clos_rt_rt1n : forall x y,
clos_refl_trans R x y -> clos_refl_trans_1n R x y.

Lemma clos_rt_rt1n_iff : forall x y,
clos_refl_trans R x y <-> clos_refl_trans_1n R x y.

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.

Lemma clos_rt_rtn1 : forall x y,
clos_refl_trans R x y -> clos_refl_trans_n1 R x y.

Lemma clos_rt_rtn1_iff : forall x y,
clos_refl_trans R x y <-> clos_refl_trans_n1 R x y.

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.

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.

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.

Direct reflexive-symmetric-transitive closure is equivalent to transitivity by symmetric left-step extension
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.

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.

Lemma clos_rstn1_sym : forall x y, clos_refl_sym_trans_n1 R x y ->
clos_refl_sym_trans_n1 R y x.

Lemma clos_rst_rstn1 : forall x y,
clos_refl_sym_trans R x y -> clos_refl_sym_trans_n1 R x y.

Lemma clos_rst_rstn1_iff : forall x y,
clos_refl_sym_trans R x y <-> clos_refl_sym_trans_n1 R x y.

End Equivalences.

Lemma clos_trans_transp_permute : forall x y,
transp _ (clos_trans R) x y <-> clos_trans (transp _ R) x y.

End Properties.