Library LabeledTransitionSystems

Require Import SfLib.
Require Import LibTactics.

  Class labeled_transition_system : Type:=
  { lts_S:> Type;
    lts_L:> Type;
    lstep: lts_S→lts_L→lts_S→Prop;
    tstep: lts_S→lts_S→Prop;
    is_halted: lts_S→Prop;
    halted_correct1: ∀ p p', is_halted p → tstep p p' → False;
    halted_correct2: ∀ p a p', is_halted p → lstep p a p' → is_halted p'
  }.

  Definition deterministic_lts (lts: labeled_transition_system) :=
    (∀ p a1 a2 p1' p2', lstep p a1 p1' → lstep p a2 p2' → a2=a1 ∧ p2' = p1') ∧
    (∀ p p1' p2', tstep p p1' → tstep p p2' → p2' = p1') ∧
    (∀ p a p1' p2', tstep p p1' → lstep p a p2' → False).

Module Stepping.
Section Stepping.
  Variable lts: labeled_transition_system.

 Definition stable p:= ∀ p', tstep p p' → False.

  Inductive step_star {lts: labeled_transition_system} : lts_S→list lts_L→lts_S→Prop :=
  | step_nil: ∀ (p:lts_S),
      step_star p nil p
  | step_lcons: ∀ p a p' la p'',
      lstep p a p' →
      step_star p' la p'' →
      step_star p (a::la) p''
  | step_tcons: ∀ p p' la p'',
      tstep p p' →
      step_star p' la p'' →
      step_star p la p''.

  Inductive lstep_star {lts: labeled_transition_system} : lts_S→list lts_L→lts_S→Prop :=
  | lstep_nil: ∀ (p:lts_S),
      lstep_star p nil p
  | lstep_lcons: ∀ p a p' la p'',
      lstep p a p' →
      lstep_star p' la p'' →
      lstep_star p (a::la) p''.

  Lemma single_tstep: ∀ p p',
    tstep p p' →
    step_star p nil p'.
  Proof. intros; eapply step_tcons; eauto; apply step_nil. Qed.

  Lemma single_lstep: ∀ p a p',
    lstep p a p' →
    step_star p [a] p'.
  Proof. intros; eapply step_lcons; eauto; apply step_nil. Qed.

  Lemma step_tsnoc: ∀ p la p' p'',
    step_star p la p' →
    tstep p' p'' →
    step_star p la p''.
  Proof.
    introv ?. revert p''.
    induction H; intros; auto.
    - apply single_tstep; auto.
    - eapply step_lcons; eauto.
    - eapply step_tcons; eauto.
  Qed.

  Lemma step_lsnoc: ∀ p la p' a p'',
    step_star p la p' →
    lstep p' a p'' →
    step_star p (la++[a]) p''.
  Proof.
    introv ?. revert a p''.
    induction H; intros; auto.
    - apply single_lstep; auto.
    - eapply step_lcons; eauto.
    - eapply step_tcons; eauto.
  Qed.

  Lemma step_star_app: ∀ p la1 p' la2 p'',
    step_star p la1 p' →
    step_star p' la2 p'' →
    step_star p (la1++la2) p''.
  Proof.
    intros.
    revert la2 p'' H0.
    induction H; intros.
    - simpl; auto.
    - eapply step_lcons; eauto.
    - eapply step_tcons; eauto.
  Qed.

  Lemma lstep_star_halted_resolve: ∀ p la p',
    is_halted p →
    step_star p la p' →
    lstep_star p la p'.
  Proof.
    intros.
    revert H.
    induction H0; intros; auto.
    apply lstep_nil.
    eapply lstep_lcons; eauto.
    apply IHstep_star.
    eapply halted_correct2; eauto.
    false; eapply halted_correct1; eauto.
  Qed.

  Lemma tstep_star_halted_resolve: ∀ p p',
    is_halted p →
    step_star p nil p' →
    p'=p.
  Proof.
    intros.
    apply lstep_star_halted_resolve in H0; auto.
    inverts H0; auto.
  Qed.

  Lemma lstep_star_halted_correct2: ∀ p la p',
    is_halted p → lstep_star p la p' → is_halted p'.
  Proof.
    intros.
    revert H.
    induction H0; intros; auto.
    apply IHlstep_star.
    eapply halted_correct2; eauto.
  Qed.

  Lemma lstep_star_step_star: ∀ p la p',
    lstep_star p la p' →
    step_star p la p'.
  Proof.
    intros.
    induction H; auto.
    apply step_nil. eapply step_lcons; eauto.
  Qed.

End Stepping.
End Stepping.