regexp.concrete.automata.epsilon

Automata construction for ε.

Require regexp.abstract.automata.epsilon.
Require Import regexp.lang.

Section Epsilon.
  Definition State : sort := Unit.
  Context {B : sort}.

  Definition build : NFA B State :=
  {|
    trans := constant relation.empty;
    start := subset.singleton (tt : typeOf State);
    final := subset.singleton (tt : typeOf State)
  |}.

  Lemma transition_equality :
    transition.denote (concrete.automata.trans build) = abstract.automata.trans abstract.automata.epsilon.build.
  Proof.
    apply/ffunP ⇒ y.
    by rewrite /transition.denote function.denoteE to_map ?ffunE constantE relation.empty_spec.
  Qed.

  Lemma equality : automata.denote build = abstract.automata.epsilon.build.
  Proof using Type.
    apply /eqP.
    by rewrite /automata.denote transition_equality subset.full_spec set_unit.
  Qed.

  Theorem correctness : (accept build ≡ ε)%lan.
  Proof using Type.
    by rewrite /accept equality abstract.automata.epsilon.correctness.
  Qed.
End Epsilon.