Library Diagrams
Require Export Relations.
Definitions
Section Def1.
Variables X X' Y Y': Type.
Variable RX: relation2 X X'.
Variable R: relation2 X Y.
Variable RY: relation2 Y Y'.
Variable R': relation2 X' Y'.
Definition diagram := forall x x' y, RX x x' -> R x y -> exists2 y', RY y y' & R' x' y'.
End Def1.
Section Def2.
Variable X: Type.
Variables R S: relation X.
Definition strong_commute := diagram R S R S.
Definition local_commute := diagram R S (star R) (star S).
Definition semi_commute := diagram R S (star R) S.
Definition commute := diagram (star R) (star S) (star R) (star S).
Definition confluent := diagram (star R) (star R) (star R) (star R).
End Def2.
Variance w.r.t inclusion
Section Incl.
Variables X X' Y Y': Type.
Variable RX: relation2 X X'.
Variable R R': relation2 X Y.
Variable RY: relation2 Y Y'.
Variables S S': relation2 X' Y'.
Hypothesis H: diagram RX R RY S.
Hypothesis HR: forall x y, R' x y -> R x y.
Hypothesis HS: forall x y, S x y -> S' x y.
Theorem diagram_incl: diagram RX R' RY S'.
End Incl.
Reversing diagrams
Section Reverse.
Variables X X' Y Y': Type.
Variable RX: relation2 X X'.
Variable R: relation2 X Y.
Variable RY: relation2 Y Y'.
Variable R': relation2 X' Y'.
Hypothesis H: diagram RX R RY R'.
Theorem diagram_reverse: diagram R RX R' RY.
End Reverse.
Composing diagrams
Section Compose.
Variables X Y Z X' Y' Z': Type.
Variable RY: relation2 Y Y'.
Variable RX: relation2 X X'.
Variable R1: relation2 X Y.
Variable R2: relation2 Y Z.
Variable RZ: relation2 Z Z'.
Variable S1: relation2 X' Y'.
Variable S2: relation2 Y' Z'.
Hypothesis H1: diagram RX R1 RY S1.
Hypothesis H2: diagram RY R2 RZ S2.
Theorem diagram_comp: diagram RX (comp R1 R2) RZ (comp S1 S2).
End Compose.
Merging diagrams
Section Union.
Variables X Y X' Y' I: Type.
Variable RX: relation2 X X'.
Variables R: I -> relation2 X Y.
Variable RY: relation2 Y Y'.
Variable S: relation2 X' Y'.
Hypothesis H: forall i, diagram RX (R i) RY S.
Theorem diagram_union: diagram RX (union R) RY S.
End Union.
Iterating one side of a diagram
Section Star.
Variables X X': Type.
Variable RX: relation2 X X'.
Variable R: relation X.
Variable S: relation X'.
Hypothesis H: diagram RX R RX (star S).
Theorem diagram_star: diagram RX (star R) RX (star S).
End Star.
Iterating strictly one side of a diagram
Section Plus.
Variables X X': Type.
Variable RX: relation2 X X'.
Variable R: relation X.
Variable S: relation X'.
Hypothesis HR: diagram RX R RX (plus S).
Theorem diagram_plus: diagram RX (plus R) RX (plus S).
End Plus.
A First Termination Argument : Subsection 4.1
Section PlusWf.
Variable X: Set.
Variable S: relation X.
Variable TX: relation X.
Hypothesis HS: diagram TX S (star TX) (plus S).
Hypothesis Hwf: well_founded (trans S).
Let Hpwf: well_founded (trans (plus S)) := plus_wf Hwf.
Lemma 4.1
Lemma diagram_plus_wf: diagram (star TX) (plus S) (star TX) (plus S).
Variable TX': relation X.
Hypothesis HS': diagram TX' S (comp (star TX) TX') (plus S).
Lemma 4.3
Lemma diagram_plus_wf_1: strong_commute (comp (star TX) TX') (plus S).
Variable Y: Type.
Variables R R': relation2 X Y.
Variable TY TY': relation Y.
Hypothesis HR: diagram TX R (star TY) (comp (star S) R).
Hypothesis HR': diagram TX' R (comp (star TY) TY') (comp (star S) R').
Proposition 4.4
Theorem diagram_plus_wf_2: diagram (comp (star TX) TX') (comp (star S) R) (comp (star TY) TY') (comp (star S) R').
End PlusWf.
A Generalisation of Newmann's Lemma : Subsection 4.2
Section StarWf.
Variable X: Set.
Variable S: relation X.
Variable TX: relation X.
Hypothesis HS: local_commute TX S.
Hypothesis Hwf: well_founded (trans (comp (plus S) (plus TX))).
Section Gen.
Variable Y: Type.
Variable R: relation2 X Y.
Variable TY: relation Y.
Let SR := comp (star S) R.
Hypothesis HR: diagram TX R (star TY) SR.
Lemma 4.5
Lemma diagram_star_wf_1: diagram (star TX) SR (star TY) SR.
Variables X' Y': Type.
Variable TaX: relation2 X X'.
Variable TaY: relation2 Y Y'.
Variable S' : relation2 X' X'.
Variable R' : relation2 X' Y'.
Let SR' := comp (star S') R'.
Let TAX := comp (star TX) TaX.
Let TAY := comp (star TY) TaY.
Hypothesis HT: diagram TaX S TAX (star S').
Hypothesis HRT: diagram TaX R TAY SR'.
Proposition 4.8
Theorem diagram_star_wf_2: diagram TAX SR TAY SR'.
End Gen.
Corollary 4.6
Lemma diagram_star_wf: commute TX S.
End StarWf.