regexp.concrete.automata.concat

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

  Context (mac0 : NFA B St0) (mac1 : NFA B St1).

  Definition State : sort := (St0 ∐ St1).

  Definition start0 : subset.t St0 := start mac0.
  Definition start1 : subset.t St1 := start mac1.

  Definition final0 : subset.t St0 := final mac0.
  Definition final1 : subset.t St1 := final mac1.

  Definition hasfinal0 (U : subset.t St0) := subset.inhabited (intersection U final0).

  Lemma hasfinal0_denote (U : subset.t St0) : hasfinal0 U = abstract.automata.concat.hasfinal0 (automata.denote mac0) (subset.denote U).
    rewrite /hasfinal0 /concat.hasfinal0.
    apply/subset.inhabitedP/existsP; by case ⇒ x; rewrite subset.intersection_spec; ∃ x.
  Qed.

  Definition crossing (U : subset.t St0) : subset.t St1 := if hasfinal0 U then start1 else subset.empty.
  Definition crossRel : relation.binary.t St0 → relation.t St0 St1 := function.map crossing.

  Definition rel01 : B ~> relation.t St0 St1 := function.map crossRel (trans mac0).

  Definition mkTrans : transition.t B State :=
    function.zipWith4 relation.matrix (trans mac0) rel01 (function.constant relation.empty) (trans mac1).

  Definition initial : subset.t State := if hasfinal0 start0 then start0 ⊎ start1 else start0 ⊎ ∅.
  Definition terminal : subset.t State := ∅ ⊎ final1.

  Definition build := {|
                       trans := mkTrans;
                       start := initial;
                       final := terminal
                     |}.

  Lemma equality : automata.denote build = (abstract.automata.concat.build (automata.denote mac0) (automata.denote mac1)).
  Proof using Type.
    apply abstract.automata.eq_equiv.
    rewrite /build /initial /terminal /mkTrans /automata.equiv //= /concat.initial /concat.terminal /concat.mkTrans.
    intuition; apply /eqP.
    - rewrite hasfinal0_denote.
      set u := concat.hasfinal0 _ _.
      by case: u; rewrite ?injDU ?union_spec ?injl_spec ?injr_spec ?empty_spec ?imset0 ?setU0 //=; intuition.
    - by rewrite ?injDU ?union_spec ?injl_spec ?injr_spec ?empty_spec ?imset0 ?set0U //=; intuition.
    - rewrite -ffunP /utmatrix ⇒ x.
      rewrite ffunE function.to_map zip_pointwise4 ffunE matrix_spec; apply abstract.relation.matrix_eq.
      rewrite /concat.tr0 /concat.tr1 constantE /transition.denote ?ffunE ?function.to_map ?relation.empty_spec -?ffunP; intuition.

      rewrite ?ffunE /crossRel ?function.to_map /crossing /concat.prefinal0 hasfinal0_denote /abstract.automata.trans //=.
      do 2 rewrite /transition.denote function.denoteE function.to_map /relation.denote.
      set cond := concat.hasfinal0 _ _; by case: cond; rewrite ?subset.empty_spec.
  Qed.

  Theorem correctness : (accept build ≡ accept mac0 ++ accept mac1)%lan.
  Proof using Type.
    by rewrite /accept equality abstract.automata.concat.correctness.
  Qed.
End Cxt.