regexp.concrete.automata.singleton

Automata construction for a singleton letter. The state space is captured by the finite type of two elements initial and terminal.

Definition State : sort := (𝟙 ∐ 𝟙)%con.
Definition initial : State := inl tt.
Definition terminal : State := inr tt.

Definition emptyRel : relation.t State State := const ∅ ++ const ∅.

Definition mkTrans {B : sort} (x : B) : B ~> (relation.t State State ) :=
  ifeq (matrix empty full empty empty) empty x.

Definition build {B : sort }(x : B) : NFA B (𝟙 ∐ 𝟙) :=
  {|
    trans := mkTrans x;
    start := subset.singleton initial;
    final := subset.singleton terminal
  |}.

Lemma transition_equality {B : sort}(x : B) :
  transition.denote (mkTrans x) = abstract.automata.singleton.mkTrans x.
Proof.
  apply/ffunP ⇒ y.
  rewrite /mkTrans /transition.denote function.denoteE to_map ifeq_spec /automata.singleton.mkTrans ?ffunE.
  set u := y==x; case: u; by rewrite ?ffunE ?relation.matrix_spec ?relation.empty_spec ?relation.full_spec.
Qed.

Lemma equality {B : sort}(x : B) : automata.denote (build x) = (abstract.automata.singleton.build x ).
Proof.
  apply /eqP.
  by rewrite /automata.denote /build
       injl_spec injr_spec
       ?subset.full_spec ?subset.setUnit
       ?imset_set1 transition_equality.
Qed.

Theorem correctness {B : sort}(x : B) : (accept (build x) ≡ singleton x)%lan.
Proof using Type.
  by rewrite /accept equality abstract.automata.singleton.correctness.
Qed.