regexp.abstract.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 : finType := (unit + unit)%type.
Definition initial : State := inl tt.
Definition terminal : State := inr tt.

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

  Definition mkTrans : transition.t B State :=
    [ffun y ⇒ if y == b then matrix empty full empty empty else empty].

This lemma states that there are no transitions out of the terminal state. Equivalently we can construct elements of an arbitrary type A from such a step.

  Lemma terminal_deadend : path.deadEnd mkTrans terminal.
    move ⇒ st x; rewrite /transition.step /mkTrans ?ffunE; case (x==b); by rewrite ?ffunE /empty /full //= ?ffunE ?imset0 ?setU0 in_set0.
  Qed.

  Lemma stepP : ∀ st x, reflect (st = terminal ∧ x = b) (transition.step mkTrans initial st x).
    have hunit : [set: unit] = [set tt] by rewrite -setP; case; rewrite ?in_set1 ?in_setT //=.
    move ⇒ st x; rewrite /mkTrans /transition.step ?ffunE; apply /(iffP idP).
    - split; apply /eqP; move: H; case (x == b);
        rewrite ?ffunE //= /empty /full //= ?ffunE ?imset0 ?imset1 ?set0U ?in_set0 ?hunit ?imset_set1 ?in_set1 //=; by move/eqP.
    - case ⇒ hst hb; by rewrite hst hb eq_refl //= /empty /full ?ffunE //= ?ffunE ?hunit imset0 ?set0U imset_set1 in_set1.
  Qed.

  Lemma pathP {xs} : reflect (xs = [:: b]) (path.t mkTrans initial terminal xs).
    case xs ⇒ [|z zs].
    - rewrite /path.t /mkTrans; apply /(iffP idP).
      + move/eqP ⇒ h; inversion h.
      + move ⇒ h; inversion h.
    - apply/(iffP path.consP).
      + case ⇒ mid; rewrite -(rwP (stepP mid z)).
        case ⇒ [[hmid hz]]; rewrite hmid; by case /(path.trivialpathP terminal_deadend) ⇒ h; rewrite h hz.
      + move ⇒ h; inversion h.
        ∃ terminal; by rewrite -(rwP (path.trivialpathP terminal_deadend [::])) -(rwP (stepP terminal b)).
  Qed.

End Transition.

Definition build {B : finType}(x : B) : NFA B State :=
  {|
    trans := mkTrans x;
    start := [set initial];
    final := [set terminal]
  |}.

Require Import regexp.lang.

Theorem correctness {B : finType}(x : B) :
  accept (build x) ≡ lang.singleton x.
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].
    rewrite hi hf ⇒ /pathP hp.
    by rewrite hp.

  - rewrite /lang.singleton ⇒ h; rewrite h.
    ∃ initial; rewrite in_set1 eqxx; intuition.
    ∃ terminal; rewrite in_set1 eqxx; intuition.
    by apply/pathP.
Qed.