Library HistoricalExamples.Rstar

Properties of a binary relation R on type A

Section Rstar.

Variable A : Type.
Variable R : AAProp.

Definition of the reflexive-transitive closure R× of R Smallest reflexive P containing R o P

Definition Rstar (x y:A) :=
P:AAProp,
( u:A, P u u) → ( u v w:A, R u vP v wP u w) → P x y.

Theorem Rstar_reflexive : x:A, Rstar x x.
Proof
fun (x:A) (P:AAProp) (h1: u:A, P u u)
(h2: u v w:A, R u vP v wP u w) ⇒
h1 x.

Theorem Rstar_R : x y z:A, R x yRstar y zRstar x z.
Proof
fun (x y z:A) (t1:R x y) (t2:Rstar y z) (P:AAProp)
(h1: u:A, P u u) (h2: u v w:A, R u vP v wP u w) ⇒
h2 x y z t1 (t2 P h1 h2).

We conclude with transitivity of Rstar :

Theorem Rstar_transitive :
x y z:A, Rstar x yRstar y zRstar x z.
Proof
fun (x y z:A) (h:Rstar x y) ⇒
h (fun u v:ARstar v zRstar u z) (fun (u:A) (t:Rstar u z) ⇒ t)
(fun (u v w:A) (t1:R u v) (t2:Rstar w zRstar v z)
(t3:Rstar w z) ⇒ Rstar_R u v z t1 (t2 t3)).

Another characterization of R× Smallest reflexive P containing R o R×

Definition Rstar' (x y:A) :=
P:AAProp,
P x x → ( u:A, R x uRstar u yP x y) → P x y.

Theorem Rstar'_reflexive : x:A, Rstar' x x.
Proof
fun (x:A) (P:AAProp) (h:P x x)
(h': u:A, R x uRstar u xP x x) ⇒ h.

Theorem Rstar'_R : x y z:A, R x zRstar z yRstar' x y.
Proof
fun (x y z:A) (t1:R x z) (t2:Rstar z y) (P:AAProp)
(h1:P x x) (h2: u:A, R x uRstar u yP x y) ⇒
h2 z t1 t2.

Equivalence of the two definitions:

Theorem Rstar'_Rstar : x y:A, Rstar' x yRstar x y.
Proof
fun (x y:A) (h:Rstar' x y) ⇒
h Rstar (Rstar_reflexive x) (fun u:ARstar_R x u y).

Theorem Rstar_Rstar' : x y:A, Rstar x yRstar' x y.
Proof
fun (x y:A) (h:Rstar x y) ⇒
h Rstar' (fun u:ARstar'_reflexive u)
(fun (u v w:A) (h1:R u v) (h2:Rstar' v w) ⇒
Rstar'_R u w v h1 (Rstar'_Rstar v w h2)).

Property of Commutativity of two relations

Definition commut (A:Set) (R1 R2:AAProp) :=
x y:A,
R1 y x z:A, R2 z yexists2 y' : A, R2 y' x & R1 z y'.

End Rstar.