Library Coq.Relations.Operators_Properties
Require Import Relation_Definitions.
Require Import Relation_Operators.
Require Import Setoid.
Section Properties.
Variable A : Type.
Variable R : relation A.
Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y.
Section Clos_Refl_Trans.
Correctness of the reflexive-transitive closure operator
Idempotency of the reflexive-transitive closure operator
Lemma clos_rt_idempotent :
incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R).
End Clos_Refl_Trans.
Section Clos_Refl_Sym_Trans.
Reflexive-transitive closure is included in the
reflexive-symmetric-transitive closure
Correctness of the reflexive-symmetric-transitive closure
Idempotency of the reflexive-symmetric-transitive closure operator
Lemma clos_rst_idempotent :
incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
(clos_refl_sym_trans A R).
End Clos_Refl_Sym_Trans.
Section Equivalences.
Direct transitive closure vs left-step extension
Lemma t1n_trans : forall x y, clos_trans_1n A R x y -> clos_trans A R x y.
Lemma trans_t1n : forall x y, clos_trans A R x y -> clos_trans_1n A R x y.
Lemma t1n_trans_equiv : forall x y,
clos_trans A R x y <-> clos_trans_1n A R x y.
Direct transitive closure vs right-step extension
Lemma tn1_trans : forall x y, clos_trans_n1 A R x y -> clos_trans A R x y.
Lemma trans_tn1 : forall x y, clos_trans A R x y -> clos_trans_n1 A R x y.
Lemma tn1_trans_equiv : forall x y,
clos_trans A R x y <-> clos_trans_n1 A R x y.
Direct reflexive-transitive closure is equivalent to
transitivity by left-step extension
Lemma R_rt1n : forall x y, R x y -> clos_refl_trans_1n A R x y.
Lemma R_rtn1 : forall x y, R x y -> clos_refl_trans_n1 A R x y.
Lemma rt1n_trans : forall x y,
clos_refl_trans_1n A R x y -> clos_refl_trans A R x y.
Lemma trans_rt1n : forall x y,
clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
Lemma rt1n_trans_equiv : forall x y,
clos_refl_trans A R x y <-> clos_refl_trans_1n A R x y.
Direct reflexive-transitive closure is equivalent to
transitivity by right-step extension
Lemma rtn1_trans : forall x y,
clos_refl_trans_n1 A R x y -> clos_refl_trans A R x y.
Lemma trans_rtn1 : forall x y,
clos_refl_trans A R x y -> clos_refl_trans_n1 A R x y.
Lemma rtn1_trans_equiv : forall x y,
clos_refl_trans A R x y <-> clos_refl_trans_n1 A 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 A R x y -> P y -> R y z -> P z) ->
forall z:A, clos_refl_trans A 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 A R y z -> P y -> P x) ->
forall x, clos_refl_trans_1n A 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 A R y z -> P x) ->
forall x, clos_refl_trans A R x z -> P x.
Direct reflexive-symmetric-transitive closure is equivalent to
transitivity by symmetric left-step extension
Lemma rts1n_rts : forall x y,
clos_refl_sym_trans_1n A R x y -> clos_refl_sym_trans A R x y.
Lemma rts_1n_trans : forall x y, clos_refl_sym_trans_1n A R x y ->
forall z, clos_refl_sym_trans_1n A R y z ->
clos_refl_sym_trans_1n A R x z.
Lemma rts1n_sym : forall x y, clos_refl_sym_trans_1n A R x y ->
clos_refl_sym_trans_1n A R y x.
Lemma rts_rts1n : forall x y,
clos_refl_sym_trans A R x y -> clos_refl_sym_trans_1n A R x y.
Lemma rts_rts1n_equiv : forall x y,
clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_1n A R x y.
Direct reflexive-symmetric-transitive closure is equivalent to
transitivity by symmetric right-step extension
Lemma rtsn1_rts : forall x y,
clos_refl_sym_trans_n1 A R x y -> clos_refl_sym_trans A R x y.
Lemma rtsn1_trans : forall y z, clos_refl_sym_trans_n1 A R y z->
forall x, clos_refl_sym_trans_n1 A R x y ->
clos_refl_sym_trans_n1 A R x z.
Lemma rtsn1_sym : forall x y, clos_refl_sym_trans_n1 A R x y ->
clos_refl_sym_trans_n1 A R y x.
Lemma rts_rtsn1 : forall x y,
clos_refl_sym_trans A R x y -> clos_refl_sym_trans_n1 A R x y.
Lemma rts_rtsn1_equiv : forall x y,
clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_n1 A R x y.
End Equivalences.
End Properties.