regexp.abstract.automata.alt

Section Cxt.

Given the state space and transition functions of the individual automata the alt operation for automata essentially involves taking the diagonal relation. The proof is organised as follows.

  Context {B : finType}{St0 St1 : finType}.
  Definition State : finType := (St0 + St1)%type.
  Context (mac0 : NFA B St0)(mac1 : NFA B St1).
  Definition build : NFA B (St0 + St1)%type :=
    {| trans := transition.diagonal (trans mac0) (trans mac1);
      start := (inl @: start mac0) :|: (inr @: start mac1);
      final := (inl @: final mac0) :|: (inr @: final mac1)
    |}.

  Theorem correctness : accept (build) ≡ (accept mac0 || accept mac1)%lan.
  Proof using Type.
    rewrite /lang.alt /accept /build //= ⇒ xs.
    rewrite ?path.reachableULE ?path.reachableURE.
    set tr0 := trans mac0.
    set tr1 := trans mac1.
    rewrite -path.reachableLL -path.reachableRR; split.
    - case ⇒ h; case: h ⇒ h.
      + by left.
      + by contradict h; apply/path.unReachableLR.
      + by contradict h; apply/path.unReachableRL.
      + by right.
    - by intuition.
  Qed.
End Cxt.