Library Diagrams

Results about commutation 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.