``` ```

# Definition of binary relations, auxiliary results

``` Ltac cgen H := generalize H; clear H. Ltac celim H := elim H; clear H. ```
A binary relation is a predicate over pairs of processes
``` Definition relation2(X Y: Type) := X -> Y -> Prop. Definition relation (X: Type) := relation2 X X. Definition set(X: Type) := X -> Prop. Section Definitions.   Variables X Y Z: Type. ```
Inclusion
```   Definition incl: relation (relation2 X Y) := fun R1 R2 => forall x y, R1 x y -> R2 x y. ```
Extensional equality
```   Definition eeq: relation (relation2 X Y) := fun R1 R2 => incl R1 R2 /\ incl R2 R1.   Variable R: relation X.   Definition reflexive := forall x, R x x.   Definition transitive := forall y x z, R x y -> R y z -> R x z.   Definition symmetric := forall x y, R x y -> R y x.   Definition antisymmetric := forall x y, R x y -> R y x -> x=y. End Definitions. Hint Unfold incl. Section Operators.   Section O.     Variables X Y Z: Type.     Variable Rxy: relation2 X Y.     Variable Rxy': relation2 X Y.     Variable Ryz: relation2 Y Z. ```
Transposition, composition, union, union `such that'
```     Definition trans: relation2 Y X := fun y x => Rxy x y.     Definition comp: relation2 X Z := fun x z => exists2 y, Rxy x y & Ryz y z.     Definition union2: relation2 X Y := fun x y => Rxy x y \/ Rxy' x y.     Definition union (I: Type) R: relation2 X Y := fun x y => exists i: I, R i x y.     Definition union_st (P: set (relation2 X Y)) := fun x y => exists2 R, P R & R x y.   End O.   Variable X: Type.   Variable R: relation X. ```
Reflexive, transitive closure
```   Inductive star: relation X :=     | star_refl: forall x, star x x     | S_star: forall y x z, R x y -> star y z -> star x z. ```
Transitive closure
```   Definition plus: relation X := comp R star. End Operators. Hint Unfold trans. Hint Immediate star_refl. Section Eeq1.   Variables I X Y Z: Type.   Variable R' R1': relation2 X Y.   Variable S': relation2 Y Z.   Variable R R1: relation2 X Y.   Variable S : relation2 Y Z.   Variables T' T: relation X.   Variables F' F: I -> relation2 X Y.   Lemma trans_incl: incl R R' -> incl (trans R) (trans R').   Lemma trans_eeq: eeq R R' -> eeq (trans R) (trans R').   Lemma comp_incl: incl R R' -> incl S S' -> incl (comp R S) (comp R' S').   Lemma comp_eeq: eeq R R' -> eeq S S' -> eeq (comp R S) (comp R' S').   Lemma union_incl: (forall i, incl (F i) (F' i)) -> incl (union F) (union F').   Lemma union_eeq: (forall i, eeq (F i) (F' i)) -> eeq (union F) (union F').   Lemma union2_incl: incl R R' -> incl R1 R1' -> incl (union2 R R1) (union2 R' R1').   Lemma union2_eeq: eeq R R' -> eeq R1 R1' -> eeq (union2 R R1) (union2 R' R1').   Lemma star_incl: incl T T' -> incl (star T) (star T').   Lemma star_eeq: eeq T T' -> eeq (star T) (star T').   Lemma plus_incl: incl T T' -> incl (plus T) (plus T').   Lemma plus_eeq: eeq T T' -> eeq (plus T) (plus T'). End Eeq1. Hint Resolve trans_incl. Hint Resolve comp_incl. Hint Resolve union_incl. Hint Resolve star_incl. Hint Resolve plus_incl. Hint Resolve trans_eeq. Hint Resolve comp_eeq. Hint Resolve union_eeq. Hint Resolve star_eeq. Hint Resolve plus_eeq. Section InclEeq.   Variables X Y: Type.   Variables S R T: relation2 X Y.   Lemma incl_refl: incl R R.   Lemma incl_trans: incl R S -> incl S T -> incl R T.   Lemma eeq_refl: eeq R R.   Lemma eeq_trans: eeq R S -> eeq S T -> eeq R T.   Lemma eeq_sym: eeq R S -> eeq S R. End InclEeq. Hint Immediate incl_refl. Hint Immediate eeq_refl. Hint Resolve eeq_sym. Section star.   Variable X: Type.   Variable R: relation X.   Lemma star1: forall x y, R x y -> star R x y.   Lemma star_S: forall x y z, star R x y -> R y z -> star R x z.   Lemma star_trans: forall x y z, star R x y -> star R y z -> star R x z.   Lemma plus_star: forall x y, plus R x y -> star R x y.   Lemma plus_star_plus: forall y x z, plus R x y -> star R y z -> plus R x z.   Lemma star_plus_plus: forall y x z, star R x y -> plus R y z -> plus R x z.   Lemma plus_trans: forall y x z, plus R x y -> plus R y z -> plus R x z.   Lemma plus1: forall x y, R x y -> plus R x y.   Lemma plus_S: forall y x z, star R x y -> R y z -> plus R x z.   Lemma S_plus: forall y x z, R x y -> star R y z -> plus R x z. End star. Hint Resolve star1. Hint Resolve plus1. Hint Resolve plus_star. Ltac destar H w :=   match type of H with     star _ ?x ?y => destruct H as [ x | w x y _H1 _H2 ];       [ idtac | generalize (S_plus _ _H1 _H2); clear _H1 _H2; intro H ]     | _ => fail "not a star hypothesis"   end. Section Plus_WF.   Variable X: Set.   Variable R: relation X.   Hypothesis Rwf: well_founded (trans R).   Lemma Acc_clos_trans : forall x, Acc (trans R) x -> Acc (trans (plus R)) x.   Hint Resolve Acc_clos_trans.   Theorem plus_wf: well_founded (trans (plus R)). End Plus_WF. Section Eeq2.   Variables I X Y Z: Type.   Variables R R': relation2 X Y.   Variable S: relation2 Y Z.   Variable T: relation X.   Variable F: I -> relation2 X Y.   Lemma inv_inv: eeq (trans (trans T)) T.   Lemma inv_comp: eeq (trans (comp R S)) (comp (trans S) (trans R)).   Lemma inv_union: eeq (trans (union F)) (union (fun i => trans (F i))).   Lemma inv_star: eeq (trans (star T)) (star (trans T)).   Lemma inv_plus: eeq (trans (plus T)) (plus (trans T)).   Lemma inv_union2: eeq (trans (union2 R R')) (union2 (trans R) (trans R')).   Lemma comp_assoc: forall W: Type, forall U: relation2 Z W,     eeq (comp (comp R S) U) (comp R (comp S U)).   Lemma comp_star_star: eeq (comp (star T) (star T)) (star T).   Lemma comp_plus_star: eeq (comp (plus T) (star T)) (plus T).   Lemma comp_star_plus: eeq (comp (star T) (plus T)) (plus T). End Eeq2. Hint Immediate inv_inv. Hint Immediate inv_comp. Hint Immediate inv_union. Hint Immediate inv_star. Hint Immediate inv_plus. Hint Immediate comp_assoc. Hint Immediate comp_star_star. Hint Immediate comp_plus_star. Hint Immediate comp_star_plus. ```