Library Reductions

Labelled Transition Systems (LTS)


Require Export Diagrams.

Ltac cgen H := generalize H; clear H.

Section Reductions.

  Section R.
    Variables A X: Type.
    Definition reduction := A -> relation X.
    Definition incl_r: relation reduction := fun R1 R2 => forall a, incl (R1 a) (R2 a).
    Definition eeq_r: relation reduction := fun R1 R2 => forall a, eeq (R1 a) (R2 a).
  End R.

  Variable A: Type.

  Section Diagram.
    Variables X Y: Type.
    Definition diagram_r(RX: reduction A X) R (RY: reduction A Y) S := forall a, diagram (RX a) R (RY a) S.
  End Diagram.

  Section Weak.

A `label' is either the silent action, or a visible one
    Inductive Lbl: Type := T | L(a: A).
    Definition reduction_t := reduction Lbl.

    Variable X: Type.
    Variable Red: reduction_t X.

Weak transition relation
    Definition Weak: reduction_t X := fun l =>
      match l with
        | T => star (Red T)
        | L a => comp (star (Red T)) (comp (Red (L a)) (star (Red T)))
      end.

Transition relation for expansion
    Definition EWeak: reduction_t X := fun l =>
      match l with
        | T => union2 (eq (A:=X)) (Red T)
        | L a => Red (L a)
      end.

Transition relation for relaxed expansion
    Definition REWeak: reduction_t X := fun l =>
      match l with
        | T => union2 (eq (A:=X)) (Red T)
        | L a => comp (Red (L a)) (star (Red T))
      end.

    Lemma weak_refl: forall x, Weak T x x.
    Hint Immediate weak_refl.

    Lemma tau_weak: forall y l x z, Red T x y -> Weak l y z -> Weak l x z.

    Lemma weak_tau: forall y l x z, Red l x y -> Weak T y z -> Weak l x z.

    Lemma red_weak: forall l x y, Red l x y -> Weak l x y.

    Lemma taus_weak: forall y l x z, Weak T x y -> Weak l y z -> Weak l x z.

    Lemma weak_taus: forall y l x z, Weak l x y -> Weak T y z -> Weak l x z.

A useful induction principle: just look at the first action
    Theorem Weak_ind:
       forall P: Lbl -> X -> X -> Prop,
       (forall x, P T x x) ->
       (forall y l x z ,
        Red T x y -> Weak l y z -> P l y z -> P l x z) ->
       (forall y a x z,
        Red (L a) x y -> Weak T y z -> P T y z -> P (L a) x z) ->
       forall l x x', Weak l x x' -> P l x x'.

  End Weak.

End Reductions.

Hint Immediate weak_refl.
Hint Resolve red_weak.