Library Relations
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.