(* Copyright (c) 2008-2009, University of Virginia All rights reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: * Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. * Neither the name of the University of Virginia nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. Author: Pieter Hooimeijer *) (* PRELIMINARIES *) Require Import Bool. (* for andb and related *) Require Import EqNat. (* for beq_nat and beq_nat_refl *) Require Import List. (* to model transition functions *) Require Import Omega. (* for misc. integer lemmas *) Require Import Peano_dec. (* for eq_nat_dec *) (* Char - characters are just an indexed type String - character sequence concat - recursively append s' to s Symbol - union type: character or epsilon *) 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. (* Nondeterministic Finite Automata NFADEF - This interface defines what is a 'proper' NFA. NFA - Given a module that satisfies the NFADEF interface, this provides an NFA with reachability and language inclusion defined. *) Module Type NFADEF. Parameter Qtype : Set. (* state space *) Parameter Q_dec : forall a b : Qtype, {a = b} + {a <> b}. (* decidable equality *) Parameter Q : list Qtype. (* states *) Parameter s : Qtype. (* start state *) Parameter f : Qtype. (* final state *) Parameter D : Qtype -> Symbol -> list Qtype. (* transition function *) 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'. (* eq <=> beq *) 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. (* We define reachability by cases: Done - q reaches itself on EmptyString Step - if q has a transition to q' on c and q' reaches q'' on s then q reaches q'' on (c::s) StepEpsilon - if q has a transition to q' on epsilon and q' reaches q'' on s then q reaches q'' on s language - behaves as expected concat_reachability - relates string concatenation to 'reachability concatenation' *) 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. (* Input NFAs M1, M2, and M3 *) 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'. (* Construct the actual NFAs. This gives us access to e.g. M1.language *) Module M1 := NFA M1'. Module M2 := NFA M2'. Module M3 := NFA M3'. (* Concat machine M4 (line 3 of Figure 3). Q4 is the union type over Q1 and Q2 D4 is the union of D1 and D2, and adds a single epsilon transition from f1 to s2 s3 := s1 f3 := f2 *) 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'. (* Properies of M4 *) (* The 'left'-hand isde of M4 is just like M1 *) 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. (* The 'right'-hand side of M4 is just like M2 *) 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. (* General statements about M4 *) 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. (* We show the equivalence of M4 to M1 and M2 in both direction. *) 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. (* Intersect machine M5 Q5 is a product type Q4 * Q3 D5((q4, q3), s) = { (q4', q3') | q4' in D4(q4, c) and q3' in D3(q3, c) } (treating epsilon transitions specially) s5 = (s4, s3) f5 = (f4, 3f) *) 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'. (* Facts about M5 - state space *) 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. (* Facts about M5 - transition function *) 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. (* Equivalence of M5 *) 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. (* We now prove the All Solutions and Satisfying properties given in the paper *) (* Q_lhs and Q_rhs, as in the text *) 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. (* A solution pair is a pair of states q, q' with q in Qlhs, q' in Qrhs, and an epsilon transition between them in M5. *) 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.