# Library Coq.Relations.Rstar

``` ```
Properties of a binary relation `R` on type `A`
``` Section Rstar.   Variable A : Type.   Variable R : A -> A -> Prop. ```
Definition of the reflexive-transitive closure `R*` of `R`
``` ```
Smallest reflexive `P` containing `R o P`
```   Definition Rstar (x y:A) :=     forall P:A -> A -> Prop,       (forall u:A, P u u) -> (forall u v w:A, R u v -> P v w -> P u w) -> P x y.   Theorem Rstar_reflexive : forall x:A, Rstar x x.   Proof.     unfold Rstar. intros x P P_refl RoP. apply P_refl.   Qed.   Theorem Rstar_R : forall x y z:A, R x y -> Rstar y z -> Rstar x z.   Proof.     intros x y z R_xy Rstar_yz.     unfold Rstar.     intros P P_refl RoP. apply RoP with (v:=y).       assumption.       apply Rstar_yz; assumption.   Qed. ```
We conclude with transitivity of `Rstar` :
```   Theorem Rstar_transitive :     forall x y z:A, Rstar x y -> Rstar y z -> Rstar x z.   Proof.     intros x y z Rstar_xy; unfold Rstar in Rstar_xy.     apply Rstar_xy; trivial.     intros u v w R_uv fz Rstar_wz.     apply Rstar_R with (y:=v); auto.   Qed. ```
Another characterization of `R*`
``` ```
Smallest reflexive `P` containing `R o R*`
```   Definition Rstar' (x y:A) :=     forall P:A -> A -> Prop,       P x x -> (forall u:A, R x u -> Rstar u y -> P x y) -> P x y.   Theorem Rstar'_reflexive : forall x:A, Rstar' x x.   Proof.     unfold Rstar'; intros; assumption.   Qed.   Theorem Rstar'_R : forall x y z:A, R x z -> Rstar z y -> Rstar' x y.   Proof.     unfold Rstar'. intros x y z Rxz Rstar_zy P Pxx RoP.     apply RoP with (u:=z); trivial.   Qed. ```
Equivalence of the two definitions:
```   Theorem Rstar'_Rstar : forall x y:A, Rstar' x y -> Rstar x y.   Proof.     intros x z Rstar'_xz; unfold Rstar' in Rstar'_xz.     apply Rstar'_xz.       exact (Rstar_reflexive x).       intro y; generalize x y z; exact Rstar_R.   Qed.   Theorem Rstar_Rstar' : forall x y:A, Rstar x y -> Rstar' x y.   Proof.     intros.     apply H.       exact Rstar'_reflexive.       intros u v w R_uv Rs'_vw. apply Rstar'_R with (z:=v).         assumption.         apply Rstar'_Rstar; assumption.   Qed. ```
Property of Commutativity of two relations
```   Definition commut (A:Set) (R1 R2:A -> A -> Prop) :=     forall x y:A,       R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. End Rstar. ```