Correctness Proof

The core concat-intersect algorithm comes with a mechanically verified proof of correctness in Coq 8.1. The proof transcript is shown below (without comments); the documented transcript can be downloaded here.

Require Import Bool.
Require Import EqNat.
Require Import List.
Require Import Omega.
Require Import Peano_dec.

Inductive Char : Set := Char_Index : nat -> Char.

Fixpoint char_eq (a b : Char) { struct b } : bool :=
 match a, b with
  | Char_Index m, Char_Index n => EqNat.beq_nat m n
 end.

Lemma char_eq_dec : forall a b : Char, {a = b} + {a <> b}.
  intros.
  decide equality.
  apply eq_nat_dec.
Qed.

Inductive String : Set :=
 | EmptyString : String
 | Str : Char -> String -> String.

Fixpoint concat (s s': String) {struct s} : String :=
  match s with
  | EmptyString => s'
  | Str c w => Str c (concat w s')
 end.

Lemma concat_empty : forall (s : String), concat s EmptyString = s.
  intros.
  induction s.
  auto.
  simpl.
  rewrite IHs.
  reflexivity.
Qed.

Inductive Symbol : Set :=
 | Character : Char -> Symbol
 | Epsilon : Symbol.

Fixpoint sym_eq (a b : Symbol) { struct b } : bool :=
  match a, b with
   | Character m, Character n => char_eq m n
   | Epsilon, Epsilon => true
   | _ , _ => false
  end.

Lemma sym_eq_dec : forall a b : Symbol, {a = b} + {a <> b}.
  intros.
  decide equality.
  apply char_eq_dec.
Qed.

Lemma nat_neq_bneq : forall n n', n<>n' -> false = beq_nat n n'.
  double induction n n'; intuition.
  simpl.
  auto.
Qed.


Module Type NFADEF.
  Parameter Qtype : Set.
  Parameter Q_dec : forall a b : Qtype,
                         {a = b} + {a <> b}.
  Parameter Q : list Qtype.
  Parameter s : Qtype.
  Parameter f : Qtype.
  Parameter D : Qtype -> Symbol -> list Qtype.
  Parameter D_dec : forall (q q' : Qtype) (s : Symbol),
                     {In q' (D q s)} + {~(In q' (D q s))}.

  Parameter beq_q : Qtype -> Qtype -> bool.
  Parameter beq_q_eq : forall q q' : Qtype,
                        q = q' <-> true = beq_q q q'.
  Parameter beq_q_refl : forall q : Qtype,
                          true = beq_q q q.

End NFADEF.

Module NFA (n : NFADEF).
  Definition Qtype := n.Qtype.
  Definition Q := n.Q.
  Definition s := n.s.
  Definition f := n.f.
  Definition D := n.D.
  Definition Q_dec := n.Q_dec.
  Definition D_dec := n.D_dec.
  Definition beq_q := n.beq_q.
  Definition beq_q_eq := n.beq_q_eq.
  Definition beq_q_refl := n.beq_q_refl.


  Inductive reachable : Qtype -> String -> Qtype -> Prop :=
   | Done : forall (q : Qtype), In q Q -> reachable q EmptyString q
   | Step : forall (q : Qtype) (c : Char) (s : String) (q' q'' : Qtype),
              In q Q -> In q' Q -> In q'' Q ->
              In q' (D q (Character c)) ->
                reachable q' s q'' ->
                 reachable q (Str c s) q''
   | StepEpsilon : forall (q : Qtype) (s : String) (q' q'' : Qtype),
              In q Q -> In q' Q -> In q'' Q ->
                In q' (D q Epsilon) ->
                 reachable q' s q'' ->
                  reachable q s q''.

  Definition language := fun x => reachable s x f.

  Lemma concat_reachability : forall (q q' q'' : Qtype) (s s' : String),
        reachable q s q' ->
          reachable q' s' q'' ->
           reachable q (concat s s') q''.
    intros.
    induction H.
    simpl.
    assumption.
    apply IHreachable in H0.
    simpl.
    apply Step with (q:=q) (q':=q') (q'':=q'') (s:=concat s0 s') (c:=c); (assumption || idtac).
    destruct H0; assumption.
    simpl.
    apply IHreachable in H0.
    apply StepEpsilon with (q:=q) (q':=q') (q'':=q'') (s:=concat s0 s');
      (assumption || idtac).
      destruct H0; assumption.
  Qed.

End NFA.


Module M1' <: NFADEF.
  Inductive Qtype' : Set := Index : nat -> Qtype'.

  Definition Qtype := Qtype'.

  Lemma Q_dec : forall (q q' : Qtype),
                  {q = q'} + {q <> q'}.
   decide equality.
   apply eq_nat_dec.
  Qed.

  Variable s : Qtype.
  Variable f : Qtype.
  Variable Q' : list Qtype.
  Definition Q := s :: f :: Q' : list Qtype.

  Variable D : Qtype -> Symbol -> list Qtype.

  Lemma D_dec : forall (q q' : Qtype) (s : Symbol),
                  {In q' (D q s)} + {~(In q' (D q s))}.
   intros.
   apply In_dec.
   apply Q_dec.
  Qed.

  Fixpoint beq_q (q q' : Qtype) { struct q' } : bool :=
   match q, q' with
   | Index m, Index n => EqNat.beq_nat m n
  end.

  Lemma beq_q_eq : forall q q' : Qtype, q = q' <-> true = beq_q q q'.
   intros.
   split.
    intro.
      rewrite H in |- *.
      destruct q'.
      unfold beq_q in |- *.
      assert (true = beq_nat n n).
     apply beq_nat_refl.
    auto.
   intro.
     destruct q; destruct q'.
     unfold beq_q in H.
     assert (true = beq_nat n n0).
    auto.
    apply beq_nat_eq in H0.
     auto.
  Qed.

  Lemma beq_q_refl : forall q : Qtype, true = beq_q q q.
   intro.
   destruct q.
   unfold beq_q in |- *.
   apply beq_nat_refl.
  Qed.

End M1'.

Module M2' <: NFADEF.
  Inductive Qtype' : Set := Index : nat -> Qtype'.

  Definition Qtype := Qtype'.

  Lemma Q_dec : forall (q q' : Qtype),
                  {q = q'} + {q <> q'}.
   decide equality.
   apply eq_nat_dec.
  Qed.

  Variable s : Qtype.
  Variable f : Qtype.
  Variable Q' : list Qtype.
  Definition Q := s :: f :: Q' : list Qtype.
  Variable D : Qtype -> Symbol -> list Qtype.

  Lemma D_dec : forall (q q' : Qtype) (s : Symbol),
                  {In q' (D q s)} + {~(In q' (D q s))}.
   intros.
   apply In_dec.
   apply Q_dec.
  Qed.

  Fixpoint beq_q (q q' : Qtype) { struct q' } : bool :=
   match q, q' with
   | Index m, Index n => EqNat.beq_nat m n
  end.

  Lemma beq_q_eq : forall q q' : Qtype, q = q' <-> true = beq_q q q'.
   intros.
   split.
    intro.
      rewrite H in |- *.
      destruct q'.
      unfold beq_q in |- *.
      assert (true = beq_nat n n).
     apply beq_nat_refl.
    auto.
   intro.
     destruct q; destruct q'.
     unfold beq_q in H.
     assert (true = beq_nat n n0).
    auto.
    apply beq_nat_eq in H0.
     auto.
  Qed.

  Lemma beq_q_refl : forall q : Qtype, true = beq_q q q.
   intro.
   destruct q.
   unfold beq_q in |- *.
   apply beq_nat_refl.
  Qed.

End M2'.

Module M3' <: NFADEF.
  Inductive Qtype' : Set := Index : nat -> Qtype'.

  Definition Qtype := Qtype'.

  Lemma Q_dec : forall (q q' : Qtype),
                  {q = q'} + {q <> q'}.
   decide equality.
   apply eq_nat_dec.
  Qed.

  Variable s : Qtype.
  Variable f : Qtype.
  Variable Q' : list Qtype.
  Definition Q := s :: f :: Q' : list Qtype.
  Variable D : Qtype -> Symbol -> list Qtype.

  Lemma D_dec : forall (q q' : Qtype) (s : Symbol),
                  {In q' (D q s)} + {~(In q' (D q s))}.
   intros.
   apply In_dec.
   apply Q_dec.
  Qed.

  Fixpoint beq_q (q q' : Qtype) { struct q' } : bool :=
   match q, q' with
   | Index m, Index n => EqNat.beq_nat m n
  end.

  Lemma beq_q_eq : forall q q' : Qtype, q = q' <-> true = beq_q q q'.
   intros.
   split.
    intro.
      rewrite H in |- *.
      destruct q'.
      unfold beq_q in |- *.
      assert (true = beq_nat n n).
     apply beq_nat_refl.
    auto.
   intro.
     destruct q; destruct q'.
     unfold beq_q in H.
     assert (true = beq_nat n n0).
    auto.
    apply beq_nat_eq in H0.
     auto.
  Qed.

  Lemma beq_q_refl : forall q : Qtype, true = beq_q q q.
   intro.
   destruct q.
   unfold beq_q in |- *.
   apply beq_nat_refl.
  Qed.

End M3'.


Module M1 := NFA M1'. Module M2 := NFA M2'. Module M3 := NFA M3'.


Inductive Q4 : Set :=
  | InQ1 : M1.Qtype -> Q4
  | InQ2 : M2.Qtype -> Q4.

Module M4' <: NFADEF.
  Definition Qtype := Q4.

  Lemma Q_dec : forall a b : Qtype,
                  {a = b} + {a <> b }.
  Proof.
   intros.
    decide equality.
    apply M1.Q_dec.
   apply M2.Q_dec.
  Qed.

  Definition Q := (List.map (fun x => InQ1 x) M1.Q) ++
                  (List.map (fun x => InQ2 x) M2.Q).

  Definition s := InQ1 M1.s.
  Definition f := InQ2 M2.f.

  Definition D := fun (q : Q4) (s : Symbol) =>
                     match q with
                    | InQ1 q' => if andb (M1.beq_q M1.f q') (sym_eq s Epsilon) then
                                    (InQ2 M2.s :: (List.map (fun x => InQ1 x) (M1.D q' s)))
                                 else
                                                           (List.map (fun x => InQ1 x) (M1.D q' s))
                    | InQ2 q' => (List.map (fun x => InQ2 x) (M2.D q' s))
                    end.

  Lemma D_dec : forall (q q' : Qtype) (s : Symbol),
                    {In q' (D q s)} + {~(In q' (D q s))}.
  Proof.
   intros.
   apply In_dec.
   apply Q_dec.
  Qed.

  Fixpoint beq_q (q q' : Qtype) { struct q' } : bool :=
   match q, q' with
    | InQ1 _, InQ2 _ => false
    | InQ2 _, InQ1 _ => false
    | InQ1 q, InQ1 q' => M1.beq_q q q'
    | InQ2 q, InQ2 q' => M2.beq_q q q'
   end.

  Lemma beq_q_eq : forall q q' : Qtype, q = q' <-> true = beq_q q q'.
  Proof.
    intros.
    split; intro.
     rewrite H in |- *.
       destruct q'; unfold beq_q in |- *.
      apply M1.beq_q_refl.
     apply M2.beq_q_refl.
    destruct q.
     destruct q'.
      unfold beq_q in H.
        assert (q = q0 <-> true = M1.beq_q q q0).
       apply M1.beq_q_eq.
      destruct H0.
         apply H1 in H.
        rewrite H in |- *.
        trivial.
     unfold beq_q in H.
        apply eq_true_false_abs in H.
       intuition.
     trivial.
    destruct q'.
     unfold beq_q in H.
        apply eq_true_false_abs in H.
       intuition.
     trivial.
    unfold beq_q in H.
      assert (q = q0 <-> true = M2.beq_q q q0).
     apply M2.beq_q_eq.
    destruct H0.
       apply H1 in H.
      rewrite H in |- *.
      trivial.
  Qed.

  Lemma beq_q_refl : forall q : Qtype, true = beq_q q q.
  Proof.
    intro.
    destruct q; unfold beq_q in |- *.
     apply M1.beq_q_refl.
    apply M2.beq_q_refl.
  Qed.
End M4'.

Module M4 := NFA M4'.



Lemma m4_q_union_left : forall (q : M1.Qtype), (In q M1.Q) -> (In (InQ1 q) M4.Q).
  intros.
  unfold M4.Q in |- *.
  unfold M4'.Q in |- *.
   apply in_map with (l := M1.Q) (x := q) (f := fun x : M1.Qtype => InQ1 x) in
   H.
  apply
   in_or_app
    with
      (m := map (fun x : M2.Qtype => InQ2 x) M2.Q)
      (l := map (fun x : M1.Qtype => InQ1 x) M1.Q)
      (a := InQ1 q).
  left.
  assumption.
Qed.

Lemma m4_d_left : forall (q q' : M1.Qtype) (c : Symbol), In q' (M1.D q c) -> In (InQ1 q') (M4.D (InQ1 q) c).
  intros.
  unfold M4.D. unfold M4'.D.
  assert ({q = M1.f} + {q <> M1.f}).
  apply M1.Q_dec.
  destruct H0.
  assert ( M1.f = q <-> true = M1.beq_q M1.f q).
  apply M1.beq_q_eq.
  destruct H0.
  assert (M1.f = q); auto.
  apply H0 in H2.
  rewrite <- H2.
  simpl.
  destruct c.
  apply in_map with (l := M1.D q (Character c)) (x := q') (f := fun x => InQ1 x).
  assumption.
  assert (In (InQ1 q') (map (fun x : M1.Qtype => InQ1 x) (M1.D q Epsilon))).
  apply in_map with (l := M1.D q Epsilon) (x := q') (f := fun x : M1.Qtype => InQ1 x).
  assumption.
  apply in_cons.
  assumption.
  assert (false = M1.beq_q M1.f q).
  destruct q; destruct M1.f.
  simpl.
  assert (n1 <> n0).
  intuition.
  apply nat_neq_bneq in H0.
  assumption.
  rewrite <- H0.
  simpl.
  apply in_map with (l := M1.D q c) (x := q') (f := fun x => InQ1 x).
  assumption.
Qed.

Lemma m4_d_left2 : forall (q q' : M1.Qtype) (c : Symbol), In (InQ1 q') (M4.D (InQ1 q) c) -> In q' (M1.D q c).
  intros.
  unfold M4.D in H. unfold M4'.D in H.
  assert ({q = M1.f} + {q <> M1.f}).
  apply M1.Q_dec.
  destruct H0.
  assert ( M1.f = q <-> true = M1.beq_q M1.f q).
  apply M1.beq_q_eq.
  destruct H0.
  assert (M1.f = q); auto.
  apply H0 in H2.
  rewrite <- H2 in H.
  assert ({c = Epsilon} + {c <> Epsilon}).
  apply sym_eq_dec.
  destruct H3.
  rewrite e0 in H.
  simpl in H.
  destruct H.
  discriminate.
  assert (In (InQ1 q') (map (fun x : M1.Qtype => InQ1 x) (M1.D q Epsilon)) <-> exists x, (fun x => InQ1 x) x = InQ1 q' /\ In x (M1.D q Epsilon)).
  apply in_map_iff with (y := (InQ1 q')) (f := fun x : M1.Qtype => InQ1 x) (l:=M1.D q Epsilon).
  destruct H3.
  clear H4.
  apply H3 in H.
  destruct H.
  assert (x = q').
  destruct H.
  inversion H.
  trivial.
  rewrite H4 in H.
  destruct H.
  rewrite e0.
  assumption.
  assert (sym_eq c Epsilon = false).
  destruct c.
  unfold sym_eq.
  reflexivity.
  intuition.
  rewrite H3 in H.
  simpl in H.
  assert (In (InQ1 q') (map (fun x : M1.Qtype => InQ1 x) (M1.D q c)) <-> exists x, (fun x => InQ1 x) x = InQ1 q' /\ In x (M1.D q c)).
  apply in_map_iff with (y := (InQ1 q')) (f := fun x : M1.Qtype => InQ1 x) (l:=M1.D q c).
  destruct H4.
  clear H5.
  apply H4 in H.
  destruct H.
  assert (x = q').
  destruct H.
  inversion H.
  reflexivity.
  rewrite H5 in H.
  destruct H.
  assumption.
  assert (false = M1.beq_q M1.f q).
  destruct q; destruct M1.f.
  simpl.
  assert (n1 <> n0).
  intuition.
  apply nat_neq_bneq in H0.
  intuition.
  rewrite <- H0 in H.
  simpl in H.
  assert (In (InQ1 q') (map (fun x : M1.Qtype => InQ1 x) (M1.D q c)) <-> exists x, (fun x => InQ1 x) x = InQ1 q' /\ In x (M1.D q c)).
  apply in_map_iff with (y := (InQ1 q')) (f := fun x : M1.Qtype => InQ1 x) (l:=M1.D q c).
  destruct H1.
  clear H2.
  apply H1 in H.
  destruct H.
  assert (x = q').
  destruct H.
  inversion H.
  reflexivity.
  rewrite H2 in H.
  destruct H.
  assumption.
Qed.


Lemma m4_q_union_right : forall (q : M2.Qtype), (In q M2.Q) -> (In (InQ2 q) M4.Q).
  intros.
  unfold M4.Q in |- *.
  unfold M4'.Q in |- *.
   apply in_map with (l := M2.Q) (x := q) (f := fun x : M2.Qtype => InQ2 x) in
   H.
  apply
   in_or_app
    with
      (m := map (fun x : M2.Qtype => InQ2 x) M2.Q)
      (l := map (fun x : M1.Qtype => InQ1 x) M1.Q)
      (a := InQ2 q).
  right.
  assumption.
Qed.

Lemma m4_d_right : forall (q q' : M2.Qtype) (c : Symbol), In q' (M2.D q c) -> In (InQ2 q') (M4.D (InQ2 q) c).
  intros.
  unfold M4.D. unfold M4'.D.
  apply in_map with (l := M2.D q c) (x := q') (f := fun x => InQ2 x).
  assumption.
Qed.

Lemma m4_d_right2 : forall (q q' : M2.Qtype) (c : Symbol), In (InQ2 q') (M4.D (InQ2 q) c) -> In q' (M2.D q c).
  intros.
  unfold M4.D in H. unfold M4'.D in H.
  assert (In (InQ2 q') (map (fun x : M2.Qtype => InQ2 x) (M2.D q c)) <-> exists x, (fun x => InQ2 x) x = InQ2 q' /\ In x (M2.D q c)).
  apply in_map_iff with (y := (InQ2 q')) (f := fun x : M2.Qtype => InQ2 x) (l:=M2.D q c).
  destruct H0.
  clear H1.
  destruct H0.
  assumption.
  destruct H0.
  assert (x = q').
  inversion H0.
  trivial.
  rewrite <- H2.
  assumption.
Qed.


Lemma m4_q_union : forall (q: M4.Qtype), (In q M4.Q) ->
         match q with
           | InQ1 q1 => In q1 M1.Q
           | InQ2 q2 => In q2 M2.Q
          end.
  intros.
  destruct q.
  unfold M4.Q in H.
  unfold M4'.Q in H.
  apply in_app_or with (m := map (InQ2) M2.Q)
        (l := map (InQ1) M1.Q)
        (a := InQ1 q) in H.
  destruct H.
  assert (In (InQ1 q) (map (InQ1) M1.Q) <-> exists x, InQ1 x = InQ1 q /\ In x M1.Q).
  apply in_map_iff.
  destruct H0.
  clear H1.
  destruct H0.
  assumption.
  destruct H0.
  inversion H0.
  rewrite H3 in H1.
  assumption.
  induction M2.Q.
  simpl in H.
  intuition.
  simpl in H.
  destruct H.
  assert (InQ2 a <> InQ1 q).
  discriminate.
  intuition.
  apply IHl in H.
  assumption.
  unfold M4.Q in H.
  unfold M4'.Q in H.
  apply in_app_or with (m := map (InQ2) M2.Q)
        (l := map (InQ1) M1.Q)
        (a := InQ2 q) in H.
  destruct H.
  induction M1.Q.
  simpl in H.
  intuition.
  simpl in H.
  destruct H.
  assert (InQ1 a <> InQ2 q).
  discriminate.
  intuition.
  apply IHl in H.
  assumption.
  assert (In (InQ2 q) (map (InQ2) M2.Q) <-> exists x, InQ2 x = InQ2 q /\ In x M2.Q).
  apply in_map_iff.
  destruct H0.
  clear H1.
  destruct H0.
  assumption.
  destruct H0.
  inversion H0.
  rewrite H3 in H1.
  assumption.
Qed.

Lemma m4_no_going_back : forall (q : M2.Qtype) (q' : M1.Qtype) (c : Symbol), In (InQ1 q') (M4.D (InQ2 q) c) -> False.
  intros.
  unfold M4.D in H.
  unfold M4'.D in H.
  induction (M2.D q c).
  simpl in H.
  contradiction.
  destruct H.
  discriminate H.
  apply IHl in H.
  contradiction.
Qed.


Lemma m4_left : forall (q q' : M1.Qtype) (s : String), M1.reachable q s q' -> M4.reachable (InQ1 q) s (InQ1 q') .
  intros.
  induction H.
  apply M4.Done.
  apply m4_q_union_left.
  assumption.
  apply m4_d_left in H2.
  apply m4_q_union_left in H.
  apply m4_q_union_left in H0.
  apply m4_q_union_left in H1.
  apply M4.Step with (q:=InQ1 q) (q':=InQ1 q') (q'':=InQ1 q'') (c := c) (s:=s); (assumption || idtac).
  apply m4_d_left in H2.
  apply m4_q_union_left in H.
  apply m4_q_union_left in H0.
  apply m4_q_union_left in H1.
  apply M4.StepEpsilon with (q:=InQ1 q) (q':=InQ1 q') (q'':=InQ1 q'') (s:=s); (assumption || idtac).
Qed.

Lemma m4_left_right : forall (q q' : M4.Qtype) (s : String), M4.reachable q s q' ->
                                                                     match q, q' with
                                                                         | InQ1 q1, InQ1 q1' => M1.reachable q1 s q1'
                                                                         | InQ2 q2, InQ2 q2' => M2.reachable q2 s q2'
                                                                         | InQ2 _, InQ1 _ => False
                                                                         | InQ1 _, InQ2 _ => True
                                                                      end.
  intros.
  induction H.
  destruct q.
  apply M1.Done.
  apply m4_q_union in H.
  assumption.
  apply M2.Done.
  apply m4_q_union in H.
  intuition.
  destruct q; destruct q''.
  destruct q'.
  apply m4_d_left2 in H2.
  apply m4_q_union in H.
  apply m4_q_union in H0.
  apply m4_q_union in H1.
  apply M1.Step with (q:=q) (q':=q1) (q'':=q0) (c:=c) (s :=s); try assumption.
  contradiction.
  trivial.
  destruct q'.
  unfold M4.D in H2.
  unfold M4'.D in H2.
  induction (M2.D q (Character c)).
  simpl in H2.
  contradiction.
  destruct H2.
  discriminate H2.
  apply IHl in H2.
  contradiction.
  contradiction.
  destruct q'.
  apply m4_no_going_back in H2.
  contradiction.
  apply m4_d_right2 in H2.
  apply m4_q_union in H.
  apply m4_q_union in H0.
  apply m4_q_union in H1.
  apply M2.Step with (q:=q) (q':=q1) (q'':=q0) (s := s) (c:=c); try assumption.
  destruct q''.
  destruct q'.
  destruct q.
  apply m4_d_left2 in H2.
  apply m4_q_union in H.
  apply m4_q_union in H0.
  apply m4_q_union in H1.
  apply M1.StepEpsilon with (q:=q) (q':=q1) (q'':=q0) (s:=s); try assumption.
  apply m4_no_going_back in H2.
  contradiction.
  destruct q.
  contradiction.
  contradiction.
  destruct q.
  trivial.
  destruct q'.
  apply m4_no_going_back in H2.
  contradiction.
  apply m4_d_right2 in H2.
  apply m4_q_union in H.
  apply m4_q_union in H0.
  apply m4_q_union in H1.
  apply M2.StepEpsilon with (q:=q) (q':=q1) (q'':=q0) (s:=s); try assumption.
Qed.

Lemma m4_right : forall (q q' : M2.Qtype) (s : String), M2.reachable q s q' -> M4.reachable (InQ2 q) s (InQ2 q') .
  intros.
  induction H.
  apply M4.Done.
  apply m4_q_union_right.
  assumption.
  apply m4_d_right in H2.
  apply m4_q_union_right in H.
  apply m4_q_union_right in H0.
  apply m4_q_union_right in H1.
  apply M4.Step with (q:=InQ2 q) (q':=InQ2 q') (q'':=InQ2 q'') (c := c) (s:=s); (assumption || idtac).
  apply m4_d_right in H2.
  apply m4_q_union_right in H.
  apply m4_q_union_right in H0.
  apply m4_q_union_right in H1.
  apply M4.StepEpsilon with (q:=InQ2 q) (q':=InQ2 q') (q'':=InQ2 q'') (s:=s); (assumption || idtac).
Qed.


Definition Q5 := prod M4.Qtype M3.Qtype.

Module M5' <: NFADEF.
  Definition Qtype := Q5.
  Lemma Q_dec : forall a b : Qtype,
                         {a = b} + {a <> b}.
   intros.
    decide equality.
     apply M3.Q_dec.
    apply M4.Q_dec.
  Qed.

  Definition Q := List.list_prod (M4.Q) (M3.Q).

  Definition s := (M4.s, M3.s).
  Definition f := (M4.f, M3.f).

  Definition D := fun (q : Q5) (s : Symbol) =>
           if (sym_eq s Epsilon) then
               map (fun x => (x, snd q)) (M4.D (fst q) Epsilon) ++
               map (fun y => (fst q, y)) (M3.D (snd q) Epsilon) ++
               list_prod (M4.D (fst q) Epsilon) (M3.D (snd q) Epsilon)
           else
               list_prod (M4.D (fst q) s) (M3.D (snd q) s).

  Lemma D_dec : forall (q q' : Qtype) (s : Symbol),
                  {In q' (D q s)} + {~(In q' (D q s))}.
   intros.
   apply In_dec.
   apply Q_dec.
  Qed.

  Fixpoint beq_q (q q' : Qtype) { struct q' } : bool :=
   match q, q' with
    | (q4, q3), (q4', q3') => andb (M4.beq_q q4 q4') (M3.beq_q q3 q3')
   end.

  Lemma beq_q_eq : forall q q' : Qtype, q = q' <-> true = beq_q q q'.
    intros.
    split; intro.
     rewrite H in |- *.
       destruct q'.
       unfold beq_q in |- *.
       assert (true = M4.beq_q q0 q0).
      apply M4.beq_q_refl.
     assert (true = M3.beq_q q1 q1).
      apply M3.beq_q_refl.
     rewrite <- H0 in |- *.
       rewrite <- H1 in |- *.
       auto.
    destruct q.
      destruct q'.
      unfold beq_q in H.
      assert (M4.beq_q q q1 && M3.beq_q q0 q2 = true).
     auto.
    clear H.
       apply andb_prop in H0.
      destruct H0.
      assert (true = M4.beq_q q q1).
     auto.
    clear H.
      assert (true = M3.beq_q q0 q2).
     auto.
    assert (q = q1 <-> true = M4.beq_q q q1).
     apply M4.beq_q_eq.
    assert (q0 = q2 <-> true = M3.beq_q q0 q2).
     apply M3.beq_q_eq.
    destruct H2; destruct H3.
       apply H5 in H.
       apply H4 in H1.
      rewrite H1 in |- *.
      rewrite H in |- *.
      trivial.
  Qed.

  Lemma beq_q_refl : forall q : Qtype, true = beq_q q q.
    intro.
    destruct q.
    unfold beq_q in |- *.
    assert (true = M4.beq_q q q /\ true = M3.beq_q q0 q0).
     split.
      apply M4.beq_q_refl.
     apply M3.beq_q_refl.
    destruct H.
      rewrite <- H in |- *.
      rewrite <- H0 in |- *.
      trivial.
  Qed.
End M5'.

Module M5 := NFA M5'.


Lemma m5_q_cross : forall (q4 : M4.Qtype) (q3 : M3.Qtype),
                    In q4 M4.Q -> In q3 M3.Q -> In (q4, q3) M5.Q.
  intros.
  unfold M5.Q in |- *.
  unfold M5'.Q in |- *.
  apply in_prod with (l := M4.Q) (l' := M3.Q) (x := q4) (y := q3).
   assumption.
  assumption.
Qed.

Lemma m5_q_cross2 : forall (q4 : M4.Qtype) (q3 : M3.Qtype),
                                                   In (q4,q3) M5.Q -> In q4 M4.Q /\ In q3 M3.Q.
  intros.
  unfold M5.Q in H.
  unfold M5'.Q in H.
  assert (In (q4, q3) (list_prod M4.Q M3.Q) <-> In q4 M4.Q /\ In q3 M3.Q).
  apply in_prod_iff with (l := M4.Q) (l' := M3.Q) (x:=q4) (y:=q3).
  destruct H0.
  apply H0 in H; assumption.
Qed.

Lemma m5_eq_m4_eq : forall (a b : M4.Qtype * M3.Qtype),
                                               a = b -> fst a = fst b.
  intros.
  destruct a.
  destruct H.
  auto.
Qed.

Lemma m5_eq_m3_eq : forall (a b : M4.Qtype * M3.Qtype),
                                               a = b -> snd a = snd b.
  intros.
  destruct a.
  destruct H.
  auto.
Qed.


Lemma m5_d_cross2 : forall (q4 q4' : M4.Qtype) (q3 q3' : M3.Qtype) (c : Char),
                                            In (q4', q3') (M5.D (q4, q3) (Character c)) -> In q4' (M4.D q4 (Character c)) /\ In q3' (M3.D q3 (Character c)).
  intros.
  unfold M5.D in H.
  unfold M5'.D in H.
  simpl in H.
  assert (In (q4', q3') (list_prod (M4.D q4 (Character c)) (M3.D q3 (Character c))) <-> In q4' (M4.D q4 (Character c)) /\ In q3' (M3.D q3 (Character c))).
  apply in_prod_iff with (l := M4.D q4 (Character c)) (l' := M3.D q3 (Character c)) (x := q4') (y := q3').
  destruct H0.
  apply H0 in H.
  assumption.
Qed.

Lemma m5_d_cross2_epsilon :
                  forall (q4 q4' : M4.Qtype) (q3 q3' : M3.Qtype),
                                  In (q4', q3') (M5.D (q4, q3) Epsilon) -> (In q4' (M4.D q4 Epsilon) /\ In q3' (M3.D q3 Epsilon))
                                           \/ (In q4' (M4.D q4 Epsilon) /\ q3 = q3') \/ (In q3' (M3.D q3 Epsilon) /\ q4=q4').
  intros.
  unfold M5.D in H.
  unfold M5'.D in H.
  simpl in H.
  apply in_app_or in H.
  destruct H.
  right; left.
  assert (In (q4',q3') (map (fun x => (x, q3)) (M4.D q4 Epsilon)) <-> exists x, (fun x => (x, q3)) x = (q4', q3') /\ In x (M4.D q4 Epsilon)).
  apply in_map_iff.
  destruct H0.
  apply H0 in H.
  clear H0 H1.
  destruct H.
  destruct H.
  split.
  apply m5_eq_m4_eq in H; simpl in H.
  rewrite H in H0; assumption.
  apply m5_eq_m3_eq in H; simpl in H.
  assumption.

  apply in_app_or in H.
  destruct H.
  right; right.
  assert (In (q4', q3') (map (fun y : M3.Qtype => (q4, y)) (M3.D q3 Epsilon)) <-> exists x, (fun y : M3.Qtype => (q4, y)) x = (q4', q3') /\ In x (M3.D q3 Epsilon)).
  apply in_map_iff with (l := (M3.D q3 Epsilon)) (f := fun y : M3.Qtype => (q4, y)) (y := (q4', q3')).
  destruct H0.
  apply H0 in H.
  clear H0 H1.
  destruct H.
  destruct H.
  split.
  apply m5_eq_m3_eq in H; simpl in H.
  rewrite H in H0; assumption.
  apply m5_eq_m4_eq in H; simpl in H.
  assumption.

  left.
  assert (In (q4', q3') (list_prod (M4.D q4 Epsilon) (M3.D q3 Epsilon)) <-> In q4' (M4.D q4 Epsilon) /\ In q3' (M3.D q3 Epsilon)).
  apply in_prod_iff with (l := M4.D q4 Epsilon) (l' := M3.D q3 Epsilon) (x := q4') (y := q3').
  destruct H0.
  apply H0 in H.
  clear H0 H1.
  assumption.
Qed.

Lemma m5_d_cross_epsilon_m4 : forall (q4 q4' : M4.Qtype) (q3 q3' : M3.Qtype),
                                                             In q4' (M4.D q4 Epsilon) -> q3 = q3' -> In (q4',q3') (M5.D (q4,q3) Epsilon).
  intros.
  unfold M5.D.
  unfold M5'.D.
  simpl.
  apply in_or_app.
  left.
  assert (In (q4', q3') (map (fun x => (x, q3)) (M4.D q4 Epsilon)) <-> exists x, (fun x => (x, q3)) x = (q4', q3') /\ In x (M4.D q4 Epsilon)).
  apply in_map_iff.
  destruct H1.
  apply H2.
  exists q4'.
  split.
  rewrite H0; trivial.
  assumption.
Qed.

Lemma m5_d_cross_epsilon_m3 : forall (q4 q4' : M4.Qtype) (q3 q3' : M3.Qtype),
                                                             In q3' (M3.D q3 Epsilon) -> q4 = q4' -> In (q4',q3') (M5.D (q4,q3) Epsilon).
  intros.
  unfold M5.D.
  unfold M5'.D.
  simpl.
  apply in_or_app.
  right.
  apply in_or_app.
  left.
  assert (In (q4', q3') (map (fun x : M3.Qtype => (q4, x)) (M3.D q3 Epsilon)) <-> exists x, (fun x : M3.Qtype=> (q4, x)) x = (q4', q3') /\ In x (M3.D q3 Epsilon)).
  apply in_map_iff with (f := fun x : M3.Qtype => (q4, x)) (y:= (q4', q3')) (l := M3.D q3 Epsilon).
  destruct H1.
  apply H2.
  exists q3'.
  split.
  rewrite H0; trivial.
  assumption.
Qed.

Lemma m5_d_cross: forall (q4 q4' : M4.Qtype) (q3 q3' : M3.Qtype) (c : Symbol),
                                            In q4' (M4.D q4 c) -> In q3' (M3.D q3 c) -> In (q4',q3') (M5.D (q4,q3) c).
  intros.
  unfold M5.D.
  unfold M5'.D.
  destruct c; simpl.
  apply in_prod; assumption.
  repeat (apply in_or_app; right).
  assert (In (q4', q3') (list_prod (M4.D q4 Epsilon) (M3.D q3 Epsilon)) <-> In q4' (M4.D q4 Epsilon) /\ In q3' (M3.D q3 Epsilon)).
  apply in_prod_iff with (l := M4.D q4 Epsilon) (l' := M3.D q3 Epsilon) (x := q4') (y := q3').
  destruct H1.
  apply H2.
  split; assumption.
Qed.


Lemma m5_equiv2 : forall (q5 q5' : M5.Qtype) (s : String),
                                           M5.reachable q5 s q5' ->
                                                    M4.reachable (fst q5) s (fst q5') /\ M3.reachable (snd q5) s (snd q5').
  intros.
  split.
  induction H.
  apply M4.Done.
  destruct q.
  apply m5_q_cross2 in H.
  destruct H; auto.
  destruct q; destruct q'; destruct q''.
  apply m5_q_cross2 in H; destruct H.
  apply m5_q_cross2 in H0; destruct H0.
  apply m5_q_cross2 in H1; destruct H1.
  apply m5_d_cross2 in H2; destruct H2.
  simpl in IHreachable |- *.
  apply M4.Step with (q:= q) (q':=q1) (q'' := q3) (c := c) (s := s); try assumption.
  destruct q; destruct q'; destruct q''.
  apply m5_q_cross2 in H; destruct H.
  apply m5_q_cross2 in H0; destruct H0.
  apply m5_q_cross2 in H1; destruct H1.
  apply m5_d_cross2_epsilon in H2. repeat destruct H2.
  simpl in IHreachable |- *.
  apply M4.StepEpsilon with (q:= q) (q':=q1) (q'' := q3) (s:=s); try assumption.
  simpl in IHreachable |- *.
  apply M4.StepEpsilon with (q:= q) (q':=q1) (q'' := q3) (s:=s); try assumption.
  simpl in IHreachable |- *.
  rewrite H7; assumption.

  induction H.
  apply M3.Done.
  destruct q.
  apply m5_q_cross2 in H.
  destruct H; auto.
  destruct q; destruct q'; destruct q''.
  apply m5_q_cross2 in H; destruct H.
  apply m5_q_cross2 in H0; destruct H0.
  apply m5_q_cross2 in H1; destruct H1.
  apply m5_d_cross2 in H2; destruct H2.
  simpl in IHreachable |- *.
  apply M3.Step with (q:= q0) (q':=q2) (q'' := q4) (c := c) (s := s); try assumption.
  destruct q; destruct q'; destruct q''.
  apply m5_q_cross2 in H; destruct H.
  apply m5_q_cross2 in H0; destruct H0.
  apply m5_q_cross2 in H1; destruct H1.
  apply m5_d_cross2_epsilon in H2; repeat destruct H2; simpl in IHreachable |- *.
  apply M3.StepEpsilon with (q:= q0) (q':=q2) (q'' := q4) (s:=s); try assumption.
  rewrite H7; assumption.
  apply M3.StepEpsilon with (q:= q0) (q':=q2) (q'' := q4) (s:=s); try assumption.
Qed.

Axiom m5_equiv : forall (q5 q5' : M5.Qtype) (s : String),
                                                        M3.reachable (snd q5) s (snd q5') ->
                                                          M4.reachable (fst q5) s (fst q5') ->
                                                           M5.reachable (fst q5, snd q5) s (fst q5', snd q5').

Theorem m4_concat_works : forall (s s' : String), M1.language s -> M2.language s' -> M4.language (concat s s').
Proof.
  intros.
  unfold M1.language in H.
  unfold M2.language in H0.
  unfold M4.language.
  apply m4_left in H.
  apply m4_right in H0.
  unfold M4.s; unfold M4'.s.
  unfold M4.f; unfold M4'.f.
  assert (In M1.s M1.Q).
  unfold M1.Q. unfold M1'.Q.
  unfold M1.s.
  compute. left. trivial.
  assert (In M1.f M1.Q).
  unfold M1.Q. unfold M1'.Q.
  unfold M1.f.
  compute. right. left. trivial.
  assert (In M2.s M2.Q).
  unfold M2.Q. unfold M2'.Q.
  unfold M2.s.
  compute. left. trivial.
  apply m4_q_union_left in H1.
  apply m4_q_union_left in H2.
  apply m4_q_union_right in H3.
  assert (In (InQ2 M2.s) (M4.D (InQ1 M1.f) Epsilon)).
  simpl.
  assert (true = M1.beq_q M1.f M1.f).
  apply M1.beq_q_refl.
  rewrite <- H4.
  simpl.
  left.
  reflexivity.
  assert (M4.reachable (InQ1 M1.f) EmptyString (InQ2 M2.s)).
  apply M4.StepEpsilon with (q:= InQ1 M1.f) (q' := InQ2 M2.s) (q'' := InQ2 M2.s) (s := EmptyString) in H4; try assumption.
  apply M4.Done; assumption.
  assert (M4.reachable (InQ1 M1.s) (concat s EmptyString) (InQ2 M2.s)).
  apply M4.concat_reachability with (q:= InQ1 M1.s) (q' := InQ1 M1.f) (q'':=InQ2 M2.s) (s:=s) (s':=EmptyString); assumption.
  assert (concat s EmptyString = s).
  apply concat_empty.
  rewrite H7 in H6.
  apply M4.concat_reachability with (q:= InQ1 M1.s) (q' := InQ2 M2.s) (q'':=InQ2 M2.f) (s:=s) (s':=s'); assumption.
Qed.

Lemma m5_intersectworks : forall s : String, M3.language s -> M4.language s -> M5.language s.
Proof.
  intros.
  unfold M3.language in H.
  unfold M4.language in H0.
  unfold M5.language in |- *.
  assert (M5.s = (M4.s, M3.s)).
   unfold M5.s in |- *.
     unfold M5'.s in |- *.
     trivial.
  rewrite H1 in |- *.
    assert (M5.f = (M4.f, M3.f)).
   unfold M5.f in |- *.
     unfold M5'.f in |- *.
     trivial.
  rewrite H2 in |- *.
    apply m5_equiv with (q5 := (M4.s, M3.s)) (q5' := (M4.f, M3.f)).
   assumption.
  assumption.
Qed.



Definition Qlhs (q : M5.Qtype) : Prop := match q with (q4, _) => q4 = InQ1 M1.f end.
Definition Qrhs (q : M5.Qtype) : Prop := match q with (q4, _) => q4 = InQ2 M2.s end.


Definition SolutionPair (q q' : M5.Qtype) : Prop :=
          In q M5.Q /\ In q' M5.Q /\ Qlhs q /\ Qrhs q' /\ In q' (M5.D q Epsilon).

Lemma satisfying_left : forall (q : M4.Qtype) (q' : M3.Qtype) (s : String),
                              Qlhs (q, q') ->
                               match q with
                                | InQ1 q1 => M5.reachable M5.s s (q, q') -> M1.reachable M1.s s q1
                                | InQ2 q2 => False
                              end.
Proof.
  intros.
  unfold Qlhs in H.
  rewrite H in |- *.
  intro.
  unfold M5.s in H0.
  unfold M5'.s in H0.
   apply m5_equiv2 in H0.
  destruct H0.
  unfold M4.s in H0.
  unfold M4'.s in H0.
   apply m4_left_right in H0.
  auto.
Qed.

Lemma satisfying_right : forall (q : M4.Qtype) (q' : M3.Qtype) (s : String),
                              Qrhs (q, q') ->
                               match q with
                                | InQ1 q1 => False
                                | InQ2 q2 => M5.reachable (q, q') s M5.f -> M2.reachable q2 s M2.f
                              end.
Proof.
  intros.
  unfold Qrhs in H.
  rewrite H in |- *.
  intro.
  unfold M5.f in H0.
  unfold M5'.f in H0.
   apply m5_equiv2 in H0.
  destruct H0.
  unfold M4.f in H0.
  unfold M4'.f in H0.
   apply m4_left_right in H0.
  auto.
Qed.

Theorem allsolutions : forall (q q' : Q5) (s s': String),
                    SolutionPair q q' ->
                     M5.reachable M5.s s q ->
                      M5.reachable q' s' M5.f -> M5.reachable M5.s (concat s s') M5.f.
Proof.
  intros.
  unfold SolutionPair in H.
  decompose [ and ] H.
  assert (M5.reachable q EmptyString q').
   apply M5.StepEpsilon with (q := q) (q' := q') (q'' := q') (s := EmptyString); try assumption.
   apply M5.Done; assumption.
  assert (M5.reachable M5.s (concat s EmptyString) q').
   apply
    M5.concat_reachability
     with (q := M5.s) (q' := q) (q'' := q') (s := s) (s' := EmptyString).
    assumption.
   assumption.
  assert (concat s EmptyString = s).
   apply concat_empty.
  rewrite H9 in H8.
    assert (M5.reachable M5.s (concat s s') M5.f).
   apply
    M5.concat_reachability with (q := M5.s) (q' := q') (q'' := M5.f) (s := s) (s' := s'); assumption.
    assumption.
Qed.