regexp.abstract.automata.simulation: Simulation of an NFA on an input



Overview

Given a string Ws of worlds, the goal of the simulation is to figure out what is the possible set of the state the machine is in.
  • next tr st W: Computes the set of states the NFA would be in on a single input world W starting from any one of the states in st
  • nexts like next but on a string of worlds (thickened string).
  • consume Run the automata on the give thickend string and give the result.
  • success Check whether the current state is a success.
  • accept The language of thickend strings on which the simulation is successfull.
  • correctness The correctness of the simulation.

Section Simulation.
  Context {B St : finType}(tr : transition.t B St).
  Definition (S : {set St})(W : world B) : {set St} :=
    \bigcup_(b in W) relation.img (tr b) S.

  Definition nexts : {set St} → seq (world B) → {set St} :=
    foldl next.

  Lemma step_next (W : world B) (S : {set St}) (u v : St) b : b \in W → u \in S → transition.step tr u v b → v \in next S W.
  Proof.
    rewrite /next /transition.step //=; move ⇒ Hb Hu Hv; apply/bigcupP; ∃ b.
      - done.
      - by apply /bigcupP; ∃ u.
  Qed.
  Lemma next_step (W : world B)(S : {set St}) (v : St) : v \in next S W → ∃ b u, b \in W ∧ u \in S ∧ transition.step tr u v b.
  Proof.
    by rewrite /next /transition.step; case /bigcupP ⇒ b hb; case /bigcupP ⇒ u hu hvtr; ∃ b; ∃ u.
  Qed.

  Lemma wpath_nexts (Ws : seq (world B)) : ∀ (S : {set St}) (u v : St), u \in S → (wpath tr u v Ws) → (v \in nexts S Ws).
  Proof.
    rewrite /nexts.
    elim: Ws ⇒ [|W WS IH].
    - move ⇒ S u v H; rewrite /nexts wpath_nilE ⇒ h; by rewrite -h.
    - move ⇒ S u v Hu. case /wpath_uncons; rewrite //= ⇒ mid.
      case ⇒ b [hb [hstep hwpath]].
      suffices hmid : mid \in next S W by apply/(IH _ mid v).
      by apply (step_next W S u mid b).
  Qed.

  Lemma nexts_wpath (Ws : seq (world B)) : ∀ (S : {set St}) (v : St), (v \in nexts S Ws) → ∃ u, u \in S ∧ (wpath tr u v Ws).
  Proof.
    rewrite /nexts.
    elim: Ws ⇒ [|W WS IH].
    - rewrite //=; move ⇒ S v H; ∃ v; intuition; ∃ [::]; rewrite //=; intuition; constructor.
    - rewrite //=; move ⇒ S v; case/IH ⇒ mid [/next_step [b [u [hb [hu Hstep]]]]] Hwpath.
      by ∃ u; intuition; rewrite wpath_uncons; ∃ mid; ∃ b.
  Qed.

  Lemma reachability (Ws : seq (world B))(U V : {set St}): wreachable tr U V Ws ↔ ∃ v, v \in (nexts U Ws :&: V).
  Proof.
    rewrite /wreachable; constructor.
    - by case ⇒ u [v [hu [hv hpath]]]; ∃ v; apply/setIP; intuition; apply (wpath_nexts Ws U u) .
    - by case ⇒ v /setIP [/nexts_wpath [u [hu hpath]] hvV]; ∃ u; ∃ v.
  Qed.

End Simulation.

Processing a single world
Definition process {B St : finType}(mac : NFA B St) := next (trans mac).
Is the current stating accepting
Definition success {B St : finType}(mac : NFA B St) (S : {set St}) :=
  ∃ v, v \in S :&: (final mac).

The state after consuming a given string of worlds
Definition consume {B St : finType}(mac : NFA B St) : seq (world B) → {set St} := nexts (trans mac) (start mac).

Definition accept {B St : finType}(mac : NFA B St) : lang (world B) := success mac \o consume mac.

Correctness.

The thickend strings on which the simulation succeeds, given by accept mac should be the same as the thickening of the language accepted by the machine mac

Theorem correctness {B St : finType}(mac : NFA B St) : (accept mac ≡ thicken (automata.accept mac))%lan.
  rewrite -path_thickening.
  by move ⇒ Ws; rewrite /accept /success //= -reachability.
Qed.