regexp.abstract.automata.transition

regexp.abstract.automata.transition : Transitions of an NFA

Overview

t B St the type of transition of an automata on letters B and state set St
step tr u v b: Reachability from u to v on the letter b (single step).
neighbours tr U b Neighbours of the set U on the letter b

Definition t (B St : finType) := {ffun B → relation.binary.t St}.

Predicate that asserts whether the transition system can go from state u to v on the letter b. This is nothing but the relational form of the transition system.

Definition step {B St : finType}(tr : t B St)(u v : St)(b : B) : bool := v \in tr b u.

Definition neighbours {B St : finType}(tr : t B St)(U : {set St})(b : B) := \bigcup_(u in U) tr b u.

Disjoint union automata

Section Matrix.
  Context {B St0 St1 : finType}.
  Definition utmatrix (tr0 : t B St0)
    (r01 : {ffun B → relation.t St0 St1})
    (tr1 : t B St1) : t B (St0 + St1)%type := [ffun y ⇒ matrix (tr0 y) (r01 y) relation.empty (tr1 y)].

  Definition diagonal (tr0 : t B St0)(tr1 : t B St1) : t B (St0 + St1)%type :=
    utmatrix tr0 [ffun _ ⇒ relation.empty] tr1.

  Context {tr0 : t B St0}
    {r01 : {ffun B → relation.t St0 St1}}
    {tr1 : t B St1}.

  Lemma noStepLRE {u v b} : step (diagonal tr0 tr1) (inl u) (inr v) b = false.
  Proof using Type.
    by rewrite /transition.step ?ffunE imset0 setU0 imset_inr_inl.
  Qed.

  Definition tr := utmatrix tr0 r01 tr1.
  Lemma noStepRLE {u v b} : step tr (inr u) (inl v) b = false.
  Proof using Type.
    by rewrite /transition.step ?ffunE imset0 set0U imset_inl_inr.
  Qed.

  Lemma stepLP {x} u v : reflect (transition.step tr0 u v x) (transition.step tr (inl u)(inl v) x).
  Proof using Type.
    rewrite /transition.step ?ffunE; apply/(iffP setUP).
    × case; by rewrite ?imset_inl ?imset_inl_inr.
    × by left; rewrite ?imset_inl.
  Qed.

  Lemma stepRP {x} u v : reflect (transition.step tr1 u v x) (transition.step tr (inr u)(inr v) x).
  Proof using Type.
    by rewrite /transition.step /tr ?ffunE imset0 set0U imset_inr; exact: idP.
  Qed.

End Matrix.