regexp.concrete.automata.alt

Section Cxt.
  Context {B : sort}{St0 St1 : sort}.

  Context (tr0 : transition.t B St0)(tr1 : transition.t B St1).
  Definition State : sort := St0 ∐ St1.

  Definition mkTrans : transition.t B State :=
    function.zipWith concrete.relation.diagonal tr0 tr1.

End Cxt.

Section Build.
 Context {B St0 St1 : sort}(mac0 : NFA B St0)(mac1 : NFA B St1).

 Definition build : NFA B (St0 ∐ St1) :=
   {|
     trans := mkTrans (automata.trans mac0) (trans mac1);
     start := start mac0 ⊎ start mac1;
     final := final mac0 ⊎ final mac1
   |}.

 Lemma equality : automata.denote build = (abstract.automata.alt.build (automata.denote mac0) (automata.denote mac1)).
 Proof using Type.
   apply abstract.automata.eq_equiv.
   rewrite /build /automata.denote /automata.equiv ?injDU ?union_spec ?injl_spec ?injr_spec //=. intuition.
   apply /eqP; rewrite -ffunP /mkTrans /transition.denote ⇒ x.
   rewrite function.denoteE /alt.mkTrans function.to_map function.zip_pointwise concrete.relation.diagonal_spec ?ffunE ?function.to_map.
   by rewrite abstract.relation.diagonal_matrix.
 Qed.

 Theorem correctness : (accept build ≡ accept mac0 || accept mac1)%lan.
 Proof using Type.
   by rewrite /accept equality abstract.automata.alt.correctness.
 Qed.

End Build.