regexp.abstract.automata.epsilon

Automata construction for ε.

Definition State : finType := unit.

Section Transition.
  Context {B : finType}(b : B).

  Definition tr : transition.t B State := [ffun y ⇒ empty].

  Lemma state_deadend : path.deadEnd tr tt.
    move ⇒ st x; by rewrite /transition.step ?ffunE in_set0.
  Qed.

  Lemma emptyPath {xs} : path.t tr tt tt xs → xs = [::].
    by case /(path.trivialpathP state_deadend).
  Qed.

End Transition.

Definition build {B : finType} : NFA B State :=
  {|
    trans := tr;
    start := [set tt];
    final := [set tt]
  |}.

Require Import regexp.lang.

Theorem correctness {B : finType}:
  accept (@build B) ≡ lang.epsilon.
Proof.
  move ⇒ xs; split; rewrite /accept /path.reachable.
  - case ⇒ i; rewrite in_set1; case ⇒ [/eqP hi] haccess.
    case: haccess ⇒ f; rewrite in_set1; case ⇒ [/eqP hf].
    by rewrite hi hf; move/emptyPath.

  - rewrite /lang.epsilon ⇒ h; rewrite h; ∃ tt; split.
    + by rewrite ?in_set1.
    + ∃ tt; split.
      × by rewrite ?in_set1.
      × by apply /path.nilP.
Qed.