regexp.concrete.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.

Definition next {b s}(tr : transition.t b s)(st : subset.t s)(W : subset.t b) : subset.t s :=
   big.union (function.map (relation.img ^~ st) tr) W.

Lemma next_spec {b s} (tr : transition.t b s) st W
  : subset.denote (next tr st W) = abstract.automata.simulation.next (transition.denote tr)(subset.denote st)(subset.denote W).
Proof.
  have h :
    (∀ x, subset.denote (map (relation.img ^~ st) tr x) = subset.denote (big.union (tr x) st)) by move ⇒ x; rewrite to_map.
  rewrite big.union_spec; apply/eq_big.
  - done.
  - move ⇒ i Hi; rewrite h big.union_spec; apply/eq_big.
    + done.
    + move ⇒ x Hyp; by rewrite ?ffunE ?to_map /relation.denote function.denoteE ?funE to_map.
Qed.

Definition process {b s}(mac : NFA b s) := next (trans mac).

Lemma process_spec {b s} (mac : NFA b s) st W :
  subset.denote (process mac st W) = abstract.automata.simulation.process (denote mac) (subset.denote st) (subset.denote W).
Proof.
  by rewrite /process /simulation.process next_spec.
Qed.

Definition consume {b s} (mac : NFA b s) : seq (subset.t b) → subset.t s := foldl (process mac) (start mac).

Lemma consume_spec{b s}(mac : NFA b s)
  : ∀ xs, subset.denote (consume mac xs) =
            abstract.automata.simulation.consume (denote mac) (seq.map subset.denote xs).
  move ⇒ xs.
  rewrite /consume /abstract.automata.simulation.consume /nexts //=.
  move: (start mac).
  elim: xs ⇒ [|x xs IH].
  - rewrite //=.
  - by move ⇒ st; rewrite //= IH next_spec .
Qed.

Definition success {b s} (nfa : NFA b s) (st : subset.t s) : bool := inhabited (intersection st (final nfa)).

Lemma success_spec {b s} (nfa : NFA b s) (st : subset.t s) :
  success nfa st ↔ abstract.automata.simulation.success (denote nfa) (subset.denote st).
  destruct nfa.
  rewrite /success /abstract.automata.simulation.success inhabited_spec intersection_spec //=. split.
  - case /utils.inhabitedIP ⇒ x [h1 h2]; ∃ x; by apply/setIP.
  - case ⇒ x /setIP [h1 h2]; apply /utils.inhabitedIP; by ∃ x.
Qed.

Definition accept {b s}(mac : NFA b s) : lang (subset.t b) := success mac \o consume mac.

Proof of correctness.

The language accepted by the concrete automata is the same as the language accepted by the underlying abstract automata. Thickening it gives the corresponding language in the abstract domain. Since subset.denote maps concrete sets to abstract sets, the contravariant comap needs to be applied to get it as a language on concrete subsets.

Theorem correctness {b s}(mac : NFA b s) : (accept mac ≡ lang.comap subset.denote (lang.world.thicken (automata.accept mac)))%lan.
  move ⇒ xs.
  rewrite /accept /comap /comp success_spec consume_spec.
  set dmac := denote mac.
  set Ws := [seq subset.denote i | i <- xs].
  rewrite
    -/(comp (abstract.automata.simulation.success dmac) (abstract.automata.simulation.consume dmac) Ws)
      -/(abstract.automata.simulation.accept dmac).
  rewrite (simulation.correctness dmac Ws).

  suffices Hyp: (world.thicken (abstract.automata.accept dmac) ≡ world.thicken (automata.accept mac))%lan by rewrite (Hyp Ws).
  by rewrite /dmac /accept.
Qed.