Set Implicit Arguments.
Require Import Utils.
Require Import Strings.
Require Import Sequences.
Require Import NFAs.
Require Import RegularLanguages.
Require Import Utils.
Require Import Strings.
Require Import Sequences.
Require Import NFAs.
Require Import RegularLanguages.
Büchi Automata
We define Büchi acceptance for NFAs, introduce quasi runs, use the notion of a match to show that emptiness of Büchi automata is decidable, and provide various operations implementing closure properties:- for image and preimage of functions translating alphabets
- union
- intersection
- ω-iteration of regular languages
- prepending regular languages
Büchi Acceptance
Büchi acceptance is defined by quantifying over an accepting run. Formally, we regard a run just as a sequence of states, that has to agree with the transition relation, start in an initial state, and (in order to be accepting) visit accepting states infinitely often.
Section BuechiAutomaton.
Context {Sigma:finType}.
Variable (aut: NFA Sigma).
Notation Run := (Seq (state aut)).
Implicit Types (r: Run ) (w: Seq Sigma).
Definition initial r := initial_state (r 0).
Definition accepting r := inf_often (accepting_state (aut:=aut)) r.
Definition accepting_for r w := (valid_run r w) /\ (initial r) /\ (accepting r).
Definition accepts : Language (Seq Sigma) := fun w => exists r, accepting_for r w.
Lemma accepting_extensional r r' w w' : r == r' -> w == w' -> accepting_for r w -> accepting_for r' w'.
Proof.
intros Er Ew [V [In Fin]]. repeat split.
- now rewrite <-Er, <- Ew.
- unfold initial. now rewrite <-Er.
- unfold accepting. now rewrite <-Er.
Qed.
Global Instance accepting_proper : Proper (@seq_equiv _ _ ==> iff) accepting.
Proof.
intros rho rho' E. unfold accepting. now rewrite E.
Qed.
Global Instance accepting_for_proper: Proper (@seq_equiv _ (state aut) ==> @seq_equiv _ Sigma ==> iff) accepting_for.
Proof.
intros rho rho' Er sigma sigma' Ew. split; apply accepting_extensional; auto; now symmetry.
Qed.
Global Instance accepts_proper : Proper (@seq_equiv _ Sigma ==> iff) accepts.
Proof.
intros sigma sigma' E; split; intros [rho Acc]; exists rho. now rewrite <-E. now rewrite E.
Qed.
End BuechiAutomaton.
Hint Unfold accepting.
Notation "'L_B'" := accepts.
Context {Sigma:finType}.
Variable (aut: NFA Sigma).
Notation Run := (Seq (state aut)).
Implicit Types (r: Run ) (w: Seq Sigma).
Definition initial r := initial_state (r 0).
Definition accepting r := inf_often (accepting_state (aut:=aut)) r.
Definition accepting_for r w := (valid_run r w) /\ (initial r) /\ (accepting r).
Definition accepts : Language (Seq Sigma) := fun w => exists r, accepting_for r w.
Lemma accepting_extensional r r' w w' : r == r' -> w == w' -> accepting_for r w -> accepting_for r' w'.
Proof.
intros Er Ew [V [In Fin]]. repeat split.
- now rewrite <-Er, <- Ew.
- unfold initial. now rewrite <-Er.
- unfold accepting. now rewrite <-Er.
Qed.
Global Instance accepting_proper : Proper (@seq_equiv _ _ ==> iff) accepting.
Proof.
intros rho rho' E. unfold accepting. now rewrite E.
Qed.
Global Instance accepting_for_proper: Proper (@seq_equiv _ (state aut) ==> @seq_equiv _ Sigma ==> iff) accepting_for.
Proof.
intros rho rho' Er sigma sigma' Ew. split; apply accepting_extensional; auto; now symmetry.
Qed.
Global Instance accepts_proper : Proper (@seq_equiv _ Sigma ==> iff) accepts.
Proof.
intros sigma sigma' E; split; intros [rho Acc]; exists rho. now rewrite <-E. now rewrite E.
Qed.
End BuechiAutomaton.
Hint Unfold accepting.
Notation "'L_B'" := accepts.
Empty and Universal Büchi Automaton
Section SimpleAutomata.
Context {Sigma:finType}.
Definition empty_aut := mknfa (fun (s : finType_False)(x:Sigma) (s':finType_False) => False) (fun _ => False) (fun _ => False).
Lemma empty_aut_correct: L_B empty_aut =$= {}.
Proof.
apply language_empty_iff. intros w [r [? [I ?]]].
unfold initial in I. now cbn in I.
Qed.
Lemma univ_aut_correct: L_B (@univ_aut Sigma) =$= universal_language.
Proof.
intros w. split; firstorder.
exists (const tt); repeat split.
intros n. exists n; oauto.
Qed.
End SimpleAutomata.
Context {Sigma:finType}.
Definition empty_aut := mknfa (fun (s : finType_False)(x:Sigma) (s':finType_False) => False) (fun _ => False) (fun _ => False).
Lemma empty_aut_correct: L_B empty_aut =$= {}.
Proof.
apply language_empty_iff. intros w [r [? [I ?]]].
unfold initial in I. now cbn in I.
Qed.
Lemma univ_aut_correct: L_B (@univ_aut Sigma) =$= universal_language.
Proof.
intros w. split; firstorder.
exists (const tt); repeat split.
intros n. exists n; oauto.
Qed.
End SimpleAutomata.
Quasi Runs
We introduce quasi runs for runs on sequences on nonempty strings. A quasi run is a sequence of strings, such that the automaton can do multiple transition on the next nonempty string to go to the next state. A quasi run is accepting if the automaton can visit accepting states infinitely often. Formally, quasi runs can easily be defined using the ===> and =!=> relations.
Section QuasiRun.
Context {Sigma: finType}.
Variable (aut : NFA Sigma).
Implicit Types (rho : Seq (state aut)) (tau : Seq (NStr Sigma)).
Definition accepting_quasi_run rho tau:=
(forall n, rho n ===> rho (S n) on (tau n)) /\
initial_state (hd rho) /\
(forall m, exists n, m <= n /\ rho n =!=> rho (S n) on (tau n)).
Context {Sigma: finType}.
Variable (aut : NFA Sigma).
Implicit Types (rho : Seq (state aut)) (tau : Seq (NStr Sigma)).
Definition accepting_quasi_run rho tau:=
(forall n, rho n ===> rho (S n) on (tau n)) /\
initial_state (hd rho) /\
(forall m, exists n, m <= n /\ rho n =!=> rho (S n) on (tau n)).
The direction form accepting runs to accepting quasi runs is easy.
Lemma accepting_implies_quasirun tau: L_B aut (flatten tau) -> exists rho, accepting_quasi_run rho tau.
Proof.
intros [rho [V [I F]]].
exists (map (fun (v: NStr (state aut)) => v 0) (cut rho (map delta tau))).
repeat split.
+ intros n. rewrite !map_nth. clear F I. revert tau rho V. induction n; intros tau rho V.
* rewrite cut_correct, nth_step, !nth_first, cut_correct, nth_first, !closed_prefix_nth, drop_nth', map_correct, hd_correct by auto.
cbn. enough (tau 0 = closed_substr (flatten tau) 0 (delta (hd tau))) as H.
-- rewrite H. apply valid_run_transforms_everywhere; auto.
-- now rewrite flatten_correct, closed_substr_begin, closed_prefix_eq.
* rewrite cut_correct, !nth_step, map_correct, tl_correct, (nth_step_tl tau), hd_correct.
apply IHn. rewrite flatten_correct in V.
apply valid_run_drop with (n0 := S (delta (hd tau))) in V.
now rewrite revert_nstr_prepend in V.
+ rewrite map_correct, hd_correct, cut_correct, hd_correct, closed_prefix_nth; auto.
+ rewrite <-flatten_cut_inv with (tau := map delta tau) in F.
apply inf_often_flatten in F.
intros m. destruct (F m) as [n [H1 H2]].
exists n. split; auto.
rewrite !map_nth. apply transforms_accepting_equiv. exists (((cut rho (map delta tau)) n)). repeat split. auto.
* now rewrite <-map_nth, cut_delta, map_nth.
* clear I F H1 H2 m. revert rho tau V. induction n; intros rho tau V k.
-- rewrite cut_correct, !nth_first, closed_prefix_delta, map_correct, hd_correct.
intros L. rewrite !closed_prefix_nth by auto.
specialize (V k). now rewrite flatten_correct, prepend_nstr_nth_first in V by auto.
-- rewrite cut_correct, !nth_step, map_correct, tl_correct, !hd_correct, (nth_step_tl tau). apply IHn.
rewrite flatten_correct in V.
apply valid_run_drop with (n0 := S (delta (hd tau))) in V.
now rewrite revert_nstr_prepend in V.
* clear H1 H2 I F m. revert rho tau V. induction n; intros rho tau V.
-- rewrite cut_correct, nth_step, cut_correct, !nth_first, closed_prefix_nth, drop_nth', map_correct, hd_correct by auto.
unfold nlst_step. rewrite closed_prefix_delta, closed_prefix_nth by auto. cbn.
specialize (V (delta (hd tau))). now rewrite flatten_correct, prepend_nstr_nth_first in V.
-- rewrite cut_correct, !nth_step, map_correct, tl_correct, !hd_correct, (nth_step_tl tau). apply IHn.
rewrite flatten_correct in V.
apply valid_run_drop with (n0 := S (delta (hd tau))) in V.
now rewrite revert_nstr_prepend in V.
* assumption.
Qed.
Build the accepting run from an accepting quasi run is more effort as ===> and =!=>
are only relations and hence we need to use constructive choice to obtain the finite runs.
Section QuasiRunImpliesAccepting.
Variable (tau: Seq (NStr Sigma)).
Variable (rho : Run aut).
Variable (Acc : accepting_quasi_run rho tau).
Lemma tau_transforms_zip k : (fun T : ((state aut) * (state aut)) * (NStr Sigma)=>
(fst (fst T)) ===> (snd (fst T)) on (snd T) ) ((zip (zip rho (tl rho)) tau) k).
Proof.
simpl. rewrite !zip_nth. apply Acc.
Qed.
Definition compute_run : {T : ((state aut) * (state aut)) * (NStr Sigma) |
(fst (fst T)) ===> (snd (fst T)) on (snd T) } -> NStr (state aut):=
fun T => match T with
| exist _ ((p,q),x) P =>
match (decision( p =!=> q on x)) with
| left D => proj1_sig (transforms_accepting_run_cc D)
| right _ => proj1_sig (transforms_run_cc P)
end
end.
Definition rho' := map compute_run (annotate tau_transforms_zip).
Lemma pair_eq3 (B C D: Type) (b b':B)(c c':C)(d d':D) : (b,c,d)=(b',c',d') -> b=b' /\ c=c' /\ d =d'.
Proof.
repeat split; congruence.
Qed.
Ltac destruct_annotate_spec n P1 :=
let Q := fresh in let Q1 := fresh in let Q2 := fresh in let Q3 := fresh in
let r := fresh in let r':= fresh in let x := fresh in
pose proof (annotate_correct tau_transforms_zip n) as Q;
destruct (annotate tau_transforms_zip n) as [[[r r'] x] P1];
simpl in Q; rewrite !zip_nth in Q; apply pair_eq3 in Q; destruct Q as[Q1 [Q2 Q3]]; subst r r' x.
Lemma rho'_firsts n : compute_run ((annotate tau_transforms_zip) n) 0 = rho n.
Proof.
unfold compute_run. destruct_annotate_spec n P.
destruct decision as [D|D].
- now destruct transforms_accepting_run_cc.
- now destruct transforms_run_cc.
Qed.
Lemma new_run_valid : valid_run (flatten rho') (flatten tau).
Proof.
apply flatten_valid. intros n.
unfold rho'. rewrite !map_nth. destruct_annotate_spec n P. unfold compute_run at 1 2.
destruct decision as [D|D]; [destruct transforms_accepting_run_cc as [s Q] | destruct transforms_run_cc as [s Q]]; simpl;
rewrite <-nth_step_tl in Q; split; try tauto; now rewrite rho'_firsts.
Qed.
Lemma new_run_initial : initial (flatten rho').
Proof.
unfold rho', initial. rewrite flatten_correct, prepend_nstr_first, map_correct, hd_correct.
rewrite <-nth_first_hd, rho'_firsts. apply Acc.
Qed.
Lemma new_run_accepting : accepting (flatten rho').
Proof.
unfold rho'.
apply inf_often_flatten.
intros n. destruct Acc as [_ [_ F]].
destruct (F n) as [m [G H]].
exists m. split; auto.
rewrite map_nth. destruct_annotate_spec m P. unfold compute_run.
destruct decision as [D|D].
- now destruct transforms_accepting_run_cc.
- now exfalso.
Qed.
Lemma rho'_accepts: accepting_for (aut:=aut) (flatten rho') (flatten tau).
Proof.
repeat split.
- apply new_run_valid.
- apply new_run_initial.
- apply new_run_accepting.
Qed.
Lemma quasi_run_implies_accepting: L_B aut (flatten tau).
Proof.
exists (flatten rho'). apply rho'_accepts.
Qed.
End QuasiRunImpliesAccepting.
Lemma accepting_quasi_run_iff_accepts tau: L_B aut (flatten tau) <-> exists rho, accepting_quasi_run rho tau.
Proof.
split.
- apply accepting_implies_quasirun.
- intros [rho Q]. eapply quasi_run_implies_accepting. apply Q.
Qed.
End QuasiRun.
Matches
We use matches for two different purposes: first, to decide emptiness of Büchi automata and second the express some properties for UP sequences.Section Match.
Context{Sigma: finType}.
Variable (aut: NFA Sigma).
Implicit Types (x y : NStr Sigma)(p q : state aut).
Definition is_match x y := exists p q, initial_state p /\ p ===> q on x /\ q =!=> q on y.
Lemma dec_is_match x y : dec (is_match x y).
Proof. auto. Qed.
Instance dec_exists_match : dec (exists x y, is_match x y).
Proof.
apply dec_trans with (P:=(exists p q, initial_state p /\ (exists x, p===> q on x ) /\ exists y, q =!=> q on y)); auto.
split.
- unfold is_match. intros [p [q [In [[x Tx] [y Ty]]]]].
now exists x,y,p,q.
- firstorder.
Qed.
Lemma match_accepted x y : is_match x y -> L_B aut (x +++ (omega_iter y)).
Proof.
intros [p [q [I [T1 T2]]]].
unfold omega_iter. rewrite flatten_prepend.
apply accepting_quasi_run_iff_accepts.
exists (p ::: const q). repeat split; auto.
- intros [|n]; cbn.
+ now rewrite nth_step, !nth_first, const_nth.
+ apply transforms_accepting_implies_transform. now rewrite !nth_step, !const_nth.
- intros m. exists (S m). split; auto. cbn.
now rewrite !nth_step, !const_nth.
Qed.
Lemma nonempty_iff_match: (exists sigma, L_B aut sigma) <-> (exists x y, is_match x y).
Proof.
split.
- intros [sigma [rho [I [V F]]]].
enough (forall k, exists (l : NStr (state aut * nat)),
delta l >= k /\
(forall n, n < |l| -> fst ( l n) = rho (S(snd ( l n)))/\ accepting_state (fst (l n))) /\
(forall n m, n < m <= delta l -> snd(l n) > snd (l m))) as H.
+ destruct (H (Cardinality (state aut))) as [l [H1 [H2 H9]]].
pose proof (nstr_to_str_length l) as Q1. pose proof (nstr_to_str_length (nstr_map fst l)) as Q2. pose proof (nstr_map_delta fst l) as Q3.
destruct (duplicates (x:= nstr_map (@fst _ _) l)) as [j [i [H3 H4]]]; auto.
exists (closed_substr sigma 0 (snd (l i))), (closed_substr sigma (S (snd (l i))) (snd(l j))), (rho 0), (rho (S (snd (l i)))). repeat split; auto.
* apply valid_run_transforms_everywhere; auto.
* apply trans_accepting_base.
-- destruct (H2 i) as [H5 H6]; auto. now rewrite <-H5.
-- rewrite !str_nth_nstr, !nstr_map_nth in H4; auto.
destruct (H2 i) as [H5 H6]; auto.
rewrite <-H5 at 2. rewrite <-H4.
destruct (H2 j) as [H7 H8]; auto. rewrite H7.
apply valid_run_transforms_everywhere; auto.
specialize (H9 j i). omega.
+ intros k. induction k.
* exists (sing (rho (cc_nat_first_geq_exists (F 1)), pred (cc_nat_first_geq_exists (F 1)))). repeat split; auto.
-- cbn in H. destruct n; auto. cbn.
f_equal. pose proof (cc_nat_first_geq_exists_increasing (F 1)). omega.
-- cbn. apply cc_nat_first_geq_exists_correct.
-- intros n m L. cbn in *. exfalso. omega.
* destruct IHk as [l [H1 [H2 H3]]].
exists (ncons (rho (cc_nat_first_geq_exists (F (S(S(snd (l 0)))))), (pred (cc_nat_first_geq_exists (F (S(S(snd ( l 0)))))))) l). repeat split.
-- cbn. omega.
-- destruct n; cbn.
++ f_equal. pose proof (cc_nat_first_geq_exists_increasing (F (S(S(snd (l 0)))))). omega.
++ apply H2. cbn in H. omega.
-- destruct n; cbn.
++ apply cc_nat_first_geq_exists_correct.
++ apply H2. cbn in H. omega.
-- cbn. intros [|n] [|m] L; cbn; try (now exfalso); pose proof (cc_nat_first_geq_exists_increasing (F (S(S(snd (l 0)))))).
++ destruct m; auto.
specialize (H3 0 (S m)). omega.
++ apply H3. omega.
- intros [x [y M]]. exists (x +++ (omega_iter y)). now apply match_accepted.
Qed.
Lemma obtain_match : (exists x y, is_match x y) -> { x : NStr Sigma & { y | is_match x y}}.
Proof.
intros E.
enough ({p : state aut & { q : state aut & prod (initial_state p) (prod { x| p ===> q on x} { y| q =!=> q on y})}}) as [p [q [I [[x Tx] [y Ty]]]]].
-- now exists x, y, p, q.
-- enough (exists p q, initial_state p /\ (exists x, p ===> q on x) /\ (exists y, q =!=> q on y)) as
[p [q [I [Tx %ex_transforms_cc Ty %ex_transforms_accepting_cc]]]%finType_cc] %finType_cc; auto.
++ exists p ,q. repeat split; auto.
++ firstorder.
Qed.
Lemma dec_buechi_empty_informative: {exists x y, is_match x y } + {L_B aut =$= {}}.
Proof.
decide (exists x y, is_match x y) as [D|D]; auto.
right. intros sigma. split;intros H; try now exfalso.
exfalso. apply D. apply nonempty_iff_match. now exists sigma.
Qed.
Definition is_buechi_empty := ~ exists x y, is_match x y.
Global Instance dec_is_buechi_empty: dec (is_buechi_empty).
Proof.
auto. Qed.
Global Instance dec_is_buechi_nonempty: dec (exists sigma, L_B aut sigma).
Proof.
destruct dec_buechi_empty_informative as [D|D].
- left. destruct D as [x [y H % match_accepted]].
firstorder.
- right. intros [sigma M]. now apply (D sigma).
Qed.
Corollary in_buechi_implies_up sigma : L_B aut sigma -> exists (x y: NStr Sigma), L_B aut (x +++ omega_iter y).
Proof.
intros L. destruct (dec_buechi_empty_informative) as [[x [y L']] | D ].
- exists x,y. now apply match_accepted.
- exfalso. now apply (D sigma).
Qed.
Corollary is_buechi_empty_correct : is_buechi_empty <-> L_B aut =$= {}.
Proof.
unfold is_buechi_empty. split.
- intros F sigma. split; intros H; try now exfalso.
apply F, nonempty_iff_match. now exists sigma.
- intros E [x [y M]].
now apply (E (x +++ omega_iter y)), match_accepted.
Qed.
End Match.
Operations Implementing Closure Properties
We provide operations implementing well-known closure properties of Büchi automata.Image and Preimage
Given two alphabets, a function between these alphabets and a Büchi automaton, we can construct a Büchi automaton accepting the preimage resp. preimage of the given automaton.
The preimage is very easy.
Context {Sigma_1 Sigma_2:finType}.
Variable (f: Sigma_1 -> Sigma_2).
Variable (aut: NFA Sigma_2).
Implicit Types (p q : state aut).
Definition preimage_aut := mknfa (fun p a q => transition p (f a) q) (initial_state (aut:=aut)) (accepting_state (aut:=aut)).
Lemma preimage_aut_correct : L_B preimage_aut =$= PreImage f (L_B aut).
Proof.
intros sigma. split; intros [rho [V [In Fin]]]; exists rho; repeat split; auto.
- intros n. rewrite map_nth. apply V.
- intros n. specialize (V n). rewrite map_nth in V. apply V.
Qed.
End PreImageNFA.
Section ImageNFA.
The image is more effort as we need to exploit constructive choice for witnesses of existential quantification over members of a finite type.
Context {Sigma_1 Sigma_2 : finType}.
Variable (f : Sigma_1 -> Sigma_2).
Variable (aut: NFA Sigma_1).
Implicit Types (p q : state aut).
Definition image_transition p a q:= exists b, f b = a /\ transition (aut:=aut) p b q.
Definition image_aut : NFA Sigma_2 := mknfa image_transition (initial_state (aut:=aut)) (accepting_state (aut:=aut)).
Definition choose_sym {x: Dummy Sigma_1} : (state image_aut * Sigma_2 * state image_aut) -> Sigma_1:=
fun t => match t with (p,a,q)=>
match (decision (exists b, f b = a/\ transition (aut:= aut) p b q)) with
| left D => proj1_sig (@finType_cc _ _ _ D)
| right _ => x
end end.
Lemma choose_sym_correct p q a {d:Dummy Sigma_1} : transition (aut:=image_aut) p a q -> f (choose_sym (p,a,q)) = a /\ transition (aut:= aut) p (choose_sym (p,a,q)) q.
Proof.
intros T. cbn. destruct decision as [D|D].
- now destruct finType_cc.
- exfalso. apply D. destruct T as [b [H1 H2]]. now exists b.
Qed.
Lemma aut_accepts_image: L_B image_aut <$= Image f (L_B aut) .
Proof.
intros tau [rho [V [I F]]].
eexists (map (@choose_sym _) (zip (zip rho tau) (tl rho))). split.
- intros n. rewrite !map_nth, !zip_nth, <-nth_step_tl. now apply choose_sym_correct.
- exists rho. repeat split; auto. intros n.
rewrite map_nth, !zip_nth. now apply choose_sym_correct.
Unshelve.
now destruct (@finType_cc _ _ _ (V 0)).
Qed.
Lemma image_accepts_aut: Image f (L_B aut) <$= L_B image_aut.
Proof.
intros sigma [tau [E [rho [V [I F]]]]].
exists rho. repeat split; auto. rewrite <-E.
intros n. rewrite map_nth. now exists (tau n).
Qed.
Lemma image_aut_correct : L_B image_aut =$= Image f (L_B aut).
Proof.
intros w. split; auto using aut_accepts_image, image_accepts_aut.
Qed.
We now show for every match in the image automaton there is a corresponding match in the original automaton.
This will be important to verify the translation pf existantial second order quantifiers to automata for UP semantics.
Lemma transforms_image_aut_transforms_aut x p q : transforms (aut:= image_aut) p q x -> exists y, transforms (aut:=aut) p q y /\ nstr_map f y = x.
Proof.
intros T. induction T as [p q a T | p p' q a x T T2].
- apply finType_cc in T; auto. destruct T as [b [E T]].
exists (sing b). repeat split.
+ now apply trans_base.
+ cbn. now f_equal.
- apply finType_cc in T; auto. destruct T as [b [E T]].
destruct IHT2 as [y [T3 E2]].
exists (ncons b y). split.
+ apply (trans_step T T3) .
+ cbn. now f_equal.
Qed.
Lemma transforms_accepting_image_aut_transforms_accepting_aut x p q : transforms_accepting (aut:= image_aut) p q x -> exists y, transforms_accepting (aut:=aut) p q y /\ nstr_map f y = x.
Proof.
intros [[F [y [T E]] % transforms_image_aut_transforms_aut]|[y [z [q' [F [C [[y' [Ty Ey]] % transforms_image_aut_transforms_aut [z' [Tz Ez]] % transforms_image_aut_transforms_aut]]]]]]] %transforms_accepting_iff.
- exists y. repeat split; auto.
now apply trans_accepting_base.
- exists (nstr_concat' y' z'). split.
+ apply transforms_accepting_iff. right.
exists y', z', q'. repeat split; auto.
+ now rewrite nstr_map_concat, Ey, Ez, C.
Qed.
Lemma image_match x y: is_match (image_aut) x y -> exists u v, is_match aut u v /\ map f (u +++ omega_iter v) == (x +++ omega_iter y).
Proof.
intros [p [q [I [[u [Tu Eu]] % transforms_image_aut_transforms_aut [v [Tv Ev]] % transforms_accepting_image_aut_transforms_accepting_aut]]]].
exists u, v. repeat split; auto.
- now exists p, q.
- now rewrite map_nstr_prepend, omega_iter_map, Ev, Eu.
Qed.
End ImageNFA.
Union
The union construction is just disjoint union of two automata. We exploit symmetry of the construction.
Section Union.
Context {Sigma : finType}.
Section Def.
Variables (aut_1 aut_2 : NFA Sigma).
Definition union_transition p a (q: state aut_1 (+) state aut_2) := match p,q with
| (inl p), (inl q) => transition p a q
| (inr p), (inr q) => transition p a q
| _ , _ => False
end.
Definition union_initial (p:state aut_1 (+) state aut_2) := match p with
| inl p => initial_state p
| inr p => initial_state p
end.
Definition union_accepting (p:state aut_1 (+) state aut_2) :=match p with
| inl p => accepting_state p
| inr p => accepting_state p
end.
Definition union:= mknfa union_transition union_initial union_accepting.
Implicit Types (sigma: Seq Sigma) (rho: Run union).
Lemma states_do_not_mix rho sigma : valid_run rho sigma -> (exists q, (rho 0) = inl q) ->
(forall n, exists q, rho n = inl q).
Proof.
intros V [q L] .
induction n.
- firstorder.
- specialize (V n). destruct (rho ( S n)) as [p |p].
+ now exists p.
+ exfalso. destruct IHn as [q' E]. now rewrite E in V.
Qed.
Context {Sigma : finType}.
Section Def.
Variables (aut_1 aut_2 : NFA Sigma).
Definition union_transition p a (q: state aut_1 (+) state aut_2) := match p,q with
| (inl p), (inl q) => transition p a q
| (inr p), (inr q) => transition p a q
| _ , _ => False
end.
Definition union_initial (p:state aut_1 (+) state aut_2) := match p with
| inl p => initial_state p
| inr p => initial_state p
end.
Definition union_accepting (p:state aut_1 (+) state aut_2) :=match p with
| inl p => accepting_state p
| inr p => accepting_state p
end.
Definition union:= mknfa union_transition union_initial union_accepting.
Implicit Types (sigma: Seq Sigma) (rho: Run union).
Lemma states_do_not_mix rho sigma : valid_run rho sigma -> (exists q, (rho 0) = inl q) ->
(forall n, exists q, rho n = inl q).
Proof.
intros V [q L] .
induction n.
- firstorder.
- specialize (V n). destruct (rho ( S n)) as [p |p].
+ now exists p.
+ exfalso. destruct IHn as [q' E]. now rewrite E in V.
Qed.
Given an accepting_for run of the union automaton, the first state of the run decides whether the sequence
is accepted by aut_1 or aut_2
Lemma autU_accepted_by_aut1 rho sigma:
accepting_for rho sigma -> (exists q, (rho 0) = inl q) -> (L_B aut_1 sigma).
Proof.
intros [V [I Fin]] B.
assert (forall n, exists q, rho n = inl q) as M by now apply (states_do_not_mix V).
destruct B as [q B].
exists (map (fun p => match p with
| inl p => p
| inr _ => q
end) rho ). repeat split.
- intros n. specialize (V n). rewrite !map_nth.
destruct (M n) as [p1 E1]. destruct (M (S n)) as [p2 E2]. simpl in *. now rewrite E1, E2 in *.
- red. red in I. rewrite map_nth. destruct (M 0) as [p E0]. simpl in *. now rewrite E0 in *.
- intros n. destruct (Fin n) as [m [P Q]].
exists m. split; auto. rewrite map_nth.
destruct (M m) as [sm Em]. simpl in *. now rewrite Em in *.
Qed.
Lemma aut1_incl_autU: L_B aut_1 <$= L_B union.
Proof.
intros sigma [rho [V [I Fin]]].
exists (map inl rho). repeat split.
- intros n. rewrite !map_nth. apply V.
- cbn. now rewrite map_nth.
- intros n. destruct (Fin n) as [m [Q P]]. exists m. now rewrite map_nth.
Qed.
End Def.
accepting_for rho sigma -> (exists q, (rho 0) = inl q) -> (L_B aut_1 sigma).
Proof.
intros [V [I Fin]] B.
assert (forall n, exists q, rho n = inl q) as M by now apply (states_do_not_mix V).
destruct B as [q B].
exists (map (fun p => match p with
| inl p => p
| inr _ => q
end) rho ). repeat split.
- intros n. specialize (V n). rewrite !map_nth.
destruct (M n) as [p1 E1]. destruct (M (S n)) as [p2 E2]. simpl in *. now rewrite E1, E2 in *.
- red. red in I. rewrite map_nth. destruct (M 0) as [p E0]. simpl in *. now rewrite E0 in *.
- intros n. destruct (Fin n) as [m [P Q]].
exists m. split; auto. rewrite map_nth.
destruct (M m) as [sm Em]. simpl in *. now rewrite Em in *.
Qed.
Lemma aut1_incl_autU: L_B aut_1 <$= L_B union.
Proof.
intros sigma [rho [V [I Fin]]].
exists (map inl rho). repeat split.
- intros n. rewrite !map_nth. apply V.
- cbn. now rewrite map_nth.
- intros n. destruct (Fin n) as [m [Q P]]. exists m. now rewrite map_nth.
Qed.
End Def.
We get the other inclusion by symmetry.
Definition swap_sum {Sigma_1 Sigma_2: Type} (v: Sigma_1 + Sigma_2) := match v with | inl l => inr l | inr r => inl r end.
Lemma union_symmetric_acc (aut_1 aut_2: NFA Sigma) rho sigma: accepting_for (aut:=union aut_1 aut_2) rho sigma -> accepting_for (aut:= union aut_2 aut_1) (map swap_sum rho) sigma.
Proof.
intros [V [I F]]. repeat split.
- intros n. rewrite !map_nth. specialize (V n). simpl in *. now destruct (rho n); destruct (rho (S n)).
- unfold initial in *. rewrite map_nth. simpl in*. now destruct (rho 0).
- intros n. destruct (F n) as [m [P Q]]. exists m. split; auto. rewrite map_nth. simpl in *. now destruct (rho m).
Qed.
Lemma union_symmetric (aut_1 aut_2 : NFA Sigma) : L_B (union aut_1 aut_2) =$= L_B (union aut_2 aut_1).
Proof.
intros sigma. split; intros [rho Acc]; exists (map swap_sum rho); now apply union_symmetric_acc.
Qed.
Lemma union_correct (aut_1 aut_2 : NFA Sigma) : L_B (union aut_1 aut_2) =$= L_B aut_1 \$/ L_B aut_2.
Proof.
intros sigma. split.
- intros L. destruct L as [rho Acc] . destruct (rho 0) as [q|q] eqn:H.
+ left. apply autU_accepted_by_aut1 with (rho:=rho); firstorder.
+ right. apply union_symmetric_acc in Acc.
eapply autU_accepted_by_aut1. apply Acc. exists q. rewrite map_nth. simpl in *. now rewrite H.
- intros [L1 | L2].
+ now apply aut1_incl_autU.
+ apply union_symmetric. now apply aut1_incl_autU.
Qed.
End Union.
Union and of finitely many NFAs.
Definition big_union (Sigma:finType) (l:list (NFA Sigma)) := fold_right union empty_aut l.
Lemma big_union_correct (Sigma:finType) (l:list (NFA Sigma)):
L_B (big_union l) =$= fun w => exists a, (a el l) /\ L_B a w.
Proof.
split.
- intros U. induction l; cbn in U.
+ exfalso. now apply empty_aut_correct in U.
+ apply union_correct in U. destruct U as [U|U].
* now exists a.
* destruct (IHl U) as [a' [H1 H2]].
exists a'; split; auto.
- intros [b [I L]]. induction l.
+ contradiction I.
+ cbn. apply union_correct.
destruct I as [I |I].
* left. now rewrite I.
* right. now apply IHl.
Qed.
Intersection
Given two Büchi automata, we use the construction that runs both automata in parallel and asserts that after one automaton visited an accepting state, the other one visits an accpeting state, too. This construction is not symmetric, as an accepting state of the intersection automaton corresponds to accepting states of one automaton, but not to accepting states of the other. Hence the verification is more difficult.
Section Intersection.
Context (Sigma:finType).
Variables (aut_1 aut_2 : NFA Sigma).
Definition intersection_state := state aut_1 (x) state aut_2 (x) finType_bool.
Implicit Types (x:Sigma)(q: intersection_state)(sigma:Seq Sigma).
Definition intersection_initial q := match q with
| (q_1, q_2, _) => initial_state q_1 /\ initial_state q_2
end.
Definition intersection_accepting q := match q with
| (_, q_2 , true) => accepting_state q_2
| _ => False
end.
Definition intersection_transition q x p := match q,p with
| (q_1, p_1, true), (q_2,p_2,b) =>
(transition q_1 x q_2) /\ (transition p_1 x p_2) /\
(b = false <-> accepting_state p_1)
| (q_1, p_1, false), (q_2,p_2,b) =>
(transition q_1 x q_2) /\ (transition p_1 x p_2) /\
(b = true <-> accepting_state q_1)
end.
Definition intersect := mknfa intersection_transition intersection_initial intersection_accepting.
Lemma between_accepting_state_intersect_is_accepting_state_aut_1 (rho: Run intersect) sigma n m: valid_run rho sigma -> accepting_state (rho n) -> accepting_state (rho m) -> n < m -> exists k, n <= k <= m /\ accepting_state (fst (fst (rho k))).
Proof.
intros V Fn Fm L. decide (exists k , k <= m /\ n <= k /\ accepting_state (fst (fst (rho k)))) as [[k [L1 [L2 F]]] | D].
- exists k. tauto.
- exfalso. enough (forall i, n < i <= m -> (snd (rho i)) = false) as H.
+ enough (snd (rho m) = true) as H'.
* now rewrite (H ( m)) in H' by omega.
* destruct (rho m) as [[? ?][|]]; cbn in *; auto.
+ intros i [L' L'']. clear L. induction L' as [| i].
* specialize (V n). destruct (rho n) as [[? ?] [|]] eqn:E; destruct (rho (S n)) as [[? ?] [|]] eqn:E'; cbn in *; try tauto.
* specialize (V i). destruct (rho i) as [[? ?] [|]] eqn:E; destruct (rho (S i)) as [[? ?] [|]] eqn:E'; cbn in *; try tauto.
-- apply IHL'. omega.
-- exfalso. apply D. exists i. rewrite E. cbn in *. repeat split; oauto. now apply V.
Qed.
Lemma intersect_incl_aut1_acc sigma rho: accepting_for (aut:=intersect) rho sigma -> accepting_for (map (fun v => fst (fst v)) rho) sigma.
Proof.
intros [V [I F]]. repeat split.
- intros n. rewrite !map_nth. specialize (V n). simpl in *. destruct (rho n) as [[? ?] [|]] ; destruct (rho (S n)) as [[? ?][|]]; cbn in *; tauto.
- unfold initial in *. rewrite map_nth. simpl in *. destruct (rho 0) as [[? ?] [|]]; cbn in *; tauto.
- intros n.
pose (Fn := F n). destruct Fn as [m1 [L1 F1]].
pose (Fm := F (S m1)). destruct Fm as [m2 [L2 F2]].
destruct (between_accepting_state_intersect_is_accepting_state_aut_1 V (n := m1) (m := m2)) as [k [L Fk]]; oauto.
exists k. rewrite map_nth. split; oauto.
Qed.
Lemma intersect_incl_aut1: L_B intersect <$= L_B aut_1.
Proof.
intros sigma [rho Acc]. exists (map (fun v => fst (fst v)) rho).
now apply intersect_incl_aut1_acc.
Qed.
Lemma intersect_incl_aut2: L_B intersect <$= L_B aut_2.
Proof.
intros sigma [rho [V [I F]]]. exists (map (fun v => snd (fst v)) rho). repeat split.
- intros n. rewrite !map_nth. specialize (V n). simpl in *. destruct (rho n) as [[? ?] [|]]; destruct (rho (S n)) as [[? ?][|]]; cbn in *; tauto.
- unfold initial in *. rewrite map_nth. simpl in *. destruct (rho 0) as [[? ?] [|]]; cbn in *; tauto.
- intros n. destruct (F n) as [m [L F']].
exists m. rewrite map_nth. split; auto. simpl in *. destruct (rho m) as [[q1 q2] [|]]; cbn in *; auto. now exfalso.
Qed.
Context (Sigma:finType).
Variables (aut_1 aut_2 : NFA Sigma).
Definition intersection_state := state aut_1 (x) state aut_2 (x) finType_bool.
Implicit Types (x:Sigma)(q: intersection_state)(sigma:Seq Sigma).
Definition intersection_initial q := match q with
| (q_1, q_2, _) => initial_state q_1 /\ initial_state q_2
end.
Definition intersection_accepting q := match q with
| (_, q_2 , true) => accepting_state q_2
| _ => False
end.
Definition intersection_transition q x p := match q,p with
| (q_1, p_1, true), (q_2,p_2,b) =>
(transition q_1 x q_2) /\ (transition p_1 x p_2) /\
(b = false <-> accepting_state p_1)
| (q_1, p_1, false), (q_2,p_2,b) =>
(transition q_1 x q_2) /\ (transition p_1 x p_2) /\
(b = true <-> accepting_state q_1)
end.
Definition intersect := mknfa intersection_transition intersection_initial intersection_accepting.
Lemma between_accepting_state_intersect_is_accepting_state_aut_1 (rho: Run intersect) sigma n m: valid_run rho sigma -> accepting_state (rho n) -> accepting_state (rho m) -> n < m -> exists k, n <= k <= m /\ accepting_state (fst (fst (rho k))).
Proof.
intros V Fn Fm L. decide (exists k , k <= m /\ n <= k /\ accepting_state (fst (fst (rho k)))) as [[k [L1 [L2 F]]] | D].
- exists k. tauto.
- exfalso. enough (forall i, n < i <= m -> (snd (rho i)) = false) as H.
+ enough (snd (rho m) = true) as H'.
* now rewrite (H ( m)) in H' by omega.
* destruct (rho m) as [[? ?][|]]; cbn in *; auto.
+ intros i [L' L'']. clear L. induction L' as [| i].
* specialize (V n). destruct (rho n) as [[? ?] [|]] eqn:E; destruct (rho (S n)) as [[? ?] [|]] eqn:E'; cbn in *; try tauto.
* specialize (V i). destruct (rho i) as [[? ?] [|]] eqn:E; destruct (rho (S i)) as [[? ?] [|]] eqn:E'; cbn in *; try tauto.
-- apply IHL'. omega.
-- exfalso. apply D. exists i. rewrite E. cbn in *. repeat split; oauto. now apply V.
Qed.
Lemma intersect_incl_aut1_acc sigma rho: accepting_for (aut:=intersect) rho sigma -> accepting_for (map (fun v => fst (fst v)) rho) sigma.
Proof.
intros [V [I F]]. repeat split.
- intros n. rewrite !map_nth. specialize (V n). simpl in *. destruct (rho n) as [[? ?] [|]] ; destruct (rho (S n)) as [[? ?][|]]; cbn in *; tauto.
- unfold initial in *. rewrite map_nth. simpl in *. destruct (rho 0) as [[? ?] [|]]; cbn in *; tauto.
- intros n.
pose (Fn := F n). destruct Fn as [m1 [L1 F1]].
pose (Fm := F (S m1)). destruct Fm as [m2 [L2 F2]].
destruct (between_accepting_state_intersect_is_accepting_state_aut_1 V (n := m1) (m := m2)) as [k [L Fk]]; oauto.
exists k. rewrite map_nth. split; oauto.
Qed.
Lemma intersect_incl_aut1: L_B intersect <$= L_B aut_1.
Proof.
intros sigma [rho Acc]. exists (map (fun v => fst (fst v)) rho).
now apply intersect_incl_aut1_acc.
Qed.
Lemma intersect_incl_aut2: L_B intersect <$= L_B aut_2.
Proof.
intros sigma [rho [V [I F]]]. exists (map (fun v => snd (fst v)) rho). repeat split.
- intros n. rewrite !map_nth. specialize (V n). simpl in *. destruct (rho n) as [[? ?] [|]]; destruct (rho (S n)) as [[? ?][|]]; cbn in *; tauto.
- unfold initial in *. rewrite map_nth. simpl in *. destruct (rho 0) as [[? ?] [|]]; cbn in *; tauto.
- intros n. destruct (F n) as [m [L F']].
exists m. rewrite map_nth. split; auto. simpl in *. destruct (rho m) as [[q1 q2] [|]]; cbn in *; auto. now exfalso.
Qed.
The following function yields an accepting run of the intersection automaton given accepting runs for aut_1 and aut_2.
Definition irun_step q p_2 (q_2: state aut_2) : (state intersect) := match q with
| (_,q_1,true) => (p_2, q_2, if (decision (accepting_state (q_1))) then false else true)
| (p_1,_,false) => (p_2, q_2, if (decision (accepting_state (p_1))) then true else false)
end.
Fixpoint seq_irun (rho_1:Run aut_1) (rho_2: Run aut_2) n := match n with
| 0 => ((rho_1 0),(rho_2 0), false)
| S n => irun_step (seq_irun rho_1 rho_2 n) (rho_1 (S n)) (rho_2 (S n))
end.
Definition irun (rho_1:Run aut_1) (rho_2: Run aut_2) : (Run intersect) :=
wrap (seq_irun rho_1 rho_2).
We verify that that is actually the case.
Section IRun.
Variables (sigma: Seq Sigma)(rho_1 : Run aut_1) (rho_2: Run aut_2).
Lemma irun_0th: irun rho_1 rho_2 0 = (rho_1 0, rho_2 0, false).
Proof.
unfold irun. now rewrite wrap_correct.
Qed.
Lemma irun_Snth n : irun rho_1 rho_2 (S n) = irun_step (irun rho_1 rho_2 n) (rho_1 (S n)) (rho_2 (S n)).
Proof.
unfold irun. now rewrite !wrap_correct.
Qed.
Lemma irun_same_states n : exists b, irun rho_1 rho_2 n = (rho_1 n, rho_2 n, b).
Proof.
induction n.
- rewrite irun_0th. now exists false.
- rewrite irun_Snth. destruct IHn as [[|] IHn];
[decide (accepting_state (rho_2 n)); [exists false | exists true] | decide (accepting_state (rho_1 n)); [exists true | exists false]];
rewrite IHn;unfold irun_step; now trivial_decision.
Qed.
Lemma irun_valid: valid_run rho_1 sigma -> valid_run rho_2 sigma -> valid_run (irun rho_1 rho_2) sigma .
Proof.
intros V1 V2 n. induction n.
- specialize (V1 0). specialize (V2 0). rewrite irun_Snth, irun_0th. unfold irun_step. cbn in *. repeat split; auto; destruct decision; congruence.
- specialize (V1 (S n)). specialize (V2 (S n)). rewrite 3irun_Snth.
destruct (irun_same_states n) as [b H]. rewrite H.
cbn in *. unfold irun_step. destruct b; simpl; repeat split; destruct decision; destruct decision; auto; repeat split; try tauto; intros H'; now discriminate.
Qed.
Lemma irun_initial: initial rho_1 -> initial rho_2 -> initial (irun rho_1 rho_2).
Proof.
intros I1 I2. unfold initial in *. now rewrite irun_0th.
Qed.
Variables (F1: accepting rho_1) (F2: accepting rho_2).
Lemma irun_step_to_true n : snd(irun rho_1 rho_2 n) = false -> exists m, m > n /\ snd (irun rho_1 rho_2 m) = true.
Proof.
intros F. exists (S (cc_nat_first_geq_exists (F1 n))). split.
- pose (cc_nat_first_geq_exists_increasing (F1 n)). omega.
- enough (forall k, n <= k <= (cc_nat_first_geq_exists (F1 n)) -> snd (irun rho_1 rho_2 k) = false) as H.
+ rewrite irun_Snth. destruct (irun_same_states (cc_nat_first_geq_exists (F1 n))) as [[|] E]; simpl in *; rewrite E in *.
* exfalso. specialize (H (cc_nat_first_geq_exists (F1 n))).
enough (true = false) by congruence. rewrite E in H. apply H.
pose (cc_nat_first_geq_exists_increasing (F1 n)). omega.
* cbn. destruct decision as [D|D]; cbn; auto.
exfalso. apply D. apply cc_nat_first_geq_exists_correct.
+ intros k. intros [L1 L2]. induction L1; auto.
cbn in *. destruct (irun_same_states m) as [[|] H]; rewrite irun_Snth; simpl in *; rewrite H in *; unfold irun_step.
* exfalso. enough (true =false ) by congruence. apply IHL1. omega.
* destruct decision as [D|D]; auto.
exfalso. apply (cc_nat_first_geq_exists_all (L:= F1 n) (k:=m)); oauto.
Qed.
Lemma irun_step_accepting n : snd(irun rho_1 rho_2 n) = true -> exists m, m >= n /\ accepting_state (irun rho_1 rho_2 m).
Proof.
intros F. exists (cc_nat_first_geq_exists (F2 n)). split.
- pose (cc_nat_first_geq_exists_increasing (F2 n)). omega.
- enough (forall k, n <= k <= (cc_nat_first_geq_exists (F2 n)) -> snd (irun rho_1 rho_2 k) = true) as H.
+ destruct (irun_same_states (cc_nat_first_geq_exists (F2 n))) as [[|] E]; rewrite E.
* cbn. apply cc_nat_first_geq_exists_correct.
* exfalso. specialize (H (cc_nat_first_geq_exists (F2 n))). rewrite E in H. cbn in H.
enough (false = true) by congruence. apply H. pose (cc_nat_first_geq_exists_increasing (F2 n)). omega.
+ intros k [L1 L2]. induction L1; auto.
cbn in *. destruct (irun_same_states m) as [[|] E]; rewrite irun_Snth; simpl in *; rewrite E in *; unfold irun_step.
* destruct decision as [D|D]; auto.
exfalso. apply (cc_nat_first_geq_exists_all (L:= F2 n) (k:=m)); oauto.
* exfalso. cbn in IHL1. enough (false = true) by congruence. apply IHL1. omega.
Qed.
Lemma irun_accepting: accepting (irun rho_1 rho_2).
Proof.
intros n. destruct (snd (irun rho_1 rho_2 n)) eqn:H.
- now apply irun_step_accepting.
- apply irun_step_to_true in H. destruct H as [n' [G T]].
apply irun_step_accepting in T. destruct T as [m [G' F]].
exists m. split; oauto.
Qed.
End IRun.
Lemma intersection_incl_intersect : L_B aut_1 /$\ L_B aut_2 <$= L_B intersect.
Proof.
intros w [[rho_1 [V1 [I1 F1]]] [rho_2 [V2 [I2 F2]]]].
exists (irun rho_1 rho_2). split; [|split].
- now apply irun_valid.
- now apply irun_initial.
- now apply irun_accepting.
Qed.
Lemma intersect_correct: L_B intersect =$= L_B aut_1 /$\ L_B aut_2.
Proof.
intros w. split.
- intros L. split; [now apply intersect_incl_aut1 | now apply intersect_incl_aut2].
- apply intersection_incl_intersect.
Qed.
Variables (sigma: Seq Sigma)(rho_1 : Run aut_1) (rho_2: Run aut_2).
Lemma irun_0th: irun rho_1 rho_2 0 = (rho_1 0, rho_2 0, false).
Proof.
unfold irun. now rewrite wrap_correct.
Qed.
Lemma irun_Snth n : irun rho_1 rho_2 (S n) = irun_step (irun rho_1 rho_2 n) (rho_1 (S n)) (rho_2 (S n)).
Proof.
unfold irun. now rewrite !wrap_correct.
Qed.
Lemma irun_same_states n : exists b, irun rho_1 rho_2 n = (rho_1 n, rho_2 n, b).
Proof.
induction n.
- rewrite irun_0th. now exists false.
- rewrite irun_Snth. destruct IHn as [[|] IHn];
[decide (accepting_state (rho_2 n)); [exists false | exists true] | decide (accepting_state (rho_1 n)); [exists true | exists false]];
rewrite IHn;unfold irun_step; now trivial_decision.
Qed.
Lemma irun_valid: valid_run rho_1 sigma -> valid_run rho_2 sigma -> valid_run (irun rho_1 rho_2) sigma .
Proof.
intros V1 V2 n. induction n.
- specialize (V1 0). specialize (V2 0). rewrite irun_Snth, irun_0th. unfold irun_step. cbn in *. repeat split; auto; destruct decision; congruence.
- specialize (V1 (S n)). specialize (V2 (S n)). rewrite 3irun_Snth.
destruct (irun_same_states n) as [b H]. rewrite H.
cbn in *. unfold irun_step. destruct b; simpl; repeat split; destruct decision; destruct decision; auto; repeat split; try tauto; intros H'; now discriminate.
Qed.
Lemma irun_initial: initial rho_1 -> initial rho_2 -> initial (irun rho_1 rho_2).
Proof.
intros I1 I2. unfold initial in *. now rewrite irun_0th.
Qed.
Variables (F1: accepting rho_1) (F2: accepting rho_2).
Lemma irun_step_to_true n : snd(irun rho_1 rho_2 n) = false -> exists m, m > n /\ snd (irun rho_1 rho_2 m) = true.
Proof.
intros F. exists (S (cc_nat_first_geq_exists (F1 n))). split.
- pose (cc_nat_first_geq_exists_increasing (F1 n)). omega.
- enough (forall k, n <= k <= (cc_nat_first_geq_exists (F1 n)) -> snd (irun rho_1 rho_2 k) = false) as H.
+ rewrite irun_Snth. destruct (irun_same_states (cc_nat_first_geq_exists (F1 n))) as [[|] E]; simpl in *; rewrite E in *.
* exfalso. specialize (H (cc_nat_first_geq_exists (F1 n))).
enough (true = false) by congruence. rewrite E in H. apply H.
pose (cc_nat_first_geq_exists_increasing (F1 n)). omega.
* cbn. destruct decision as [D|D]; cbn; auto.
exfalso. apply D. apply cc_nat_first_geq_exists_correct.
+ intros k. intros [L1 L2]. induction L1; auto.
cbn in *. destruct (irun_same_states m) as [[|] H]; rewrite irun_Snth; simpl in *; rewrite H in *; unfold irun_step.
* exfalso. enough (true =false ) by congruence. apply IHL1. omega.
* destruct decision as [D|D]; auto.
exfalso. apply (cc_nat_first_geq_exists_all (L:= F1 n) (k:=m)); oauto.
Qed.
Lemma irun_step_accepting n : snd(irun rho_1 rho_2 n) = true -> exists m, m >= n /\ accepting_state (irun rho_1 rho_2 m).
Proof.
intros F. exists (cc_nat_first_geq_exists (F2 n)). split.
- pose (cc_nat_first_geq_exists_increasing (F2 n)). omega.
- enough (forall k, n <= k <= (cc_nat_first_geq_exists (F2 n)) -> snd (irun rho_1 rho_2 k) = true) as H.
+ destruct (irun_same_states (cc_nat_first_geq_exists (F2 n))) as [[|] E]; rewrite E.
* cbn. apply cc_nat_first_geq_exists_correct.
* exfalso. specialize (H (cc_nat_first_geq_exists (F2 n))). rewrite E in H. cbn in H.
enough (false = true) by congruence. apply H. pose (cc_nat_first_geq_exists_increasing (F2 n)). omega.
+ intros k [L1 L2]. induction L1; auto.
cbn in *. destruct (irun_same_states m) as [[|] E]; rewrite irun_Snth; simpl in *; rewrite E in *; unfold irun_step.
* destruct decision as [D|D]; auto.
exfalso. apply (cc_nat_first_geq_exists_all (L:= F2 n) (k:=m)); oauto.
* exfalso. cbn in IHL1. enough (false = true) by congruence. apply IHL1. omega.
Qed.
Lemma irun_accepting: accepting (irun rho_1 rho_2).
Proof.
intros n. destruct (snd (irun rho_1 rho_2 n)) eqn:H.
- now apply irun_step_accepting.
- apply irun_step_to_true in H. destruct H as [n' [G T]].
apply irun_step_accepting in T. destruct T as [m [G' F]].
exists m. split; oauto.
Qed.
End IRun.
Lemma intersection_incl_intersect : L_B aut_1 /$\ L_B aut_2 <$= L_B intersect.
Proof.
intros w [[rho_1 [V1 [I1 F1]]] [rho_2 [V2 [I2 F2]]]].
exists (irun rho_1 rho_2). split; [|split].
- now apply irun_valid.
- now apply irun_initial.
- now apply irun_accepting.
Qed.
Lemma intersect_correct: L_B intersect =$= L_B aut_1 /$\ L_B aut_2.
Proof.
intros w. split.
- intros L. split; [now apply intersect_incl_aut1 | now apply intersect_incl_aut2].
- apply intersection_incl_intersect.
Qed.
We show that a match of the intersection automaton is a match of aut_2.
It is a match of aut_1, too, but we do not show it, as we do not need it.
Lemma intersect_transforms (x: NStr Sigma) (p q: state intersect) : p ===> q on x -> (snd (fst p)) ===> (snd (fst q)) on x.
Proof.
intros T. induction T.
- destruct p as [[p1 p2] b]; destruct q as [[q1 q2] b'].
apply trans_base. cbn in *. destruct b; apply H.
- destruct p as [[p1 p2] b]; destruct p' as [[p1' p2'] b']; destruct q as [[q1 q2] b''].
apply trans_step with (p' := p2'); cbn in *; auto.
destruct b; apply H.
Qed.
Lemma intersect_transforms_accepting (x: NStr Sigma) (p q: state intersect) : p =!=> q on x -> (snd (fst p)) =!=> (snd (fst q)) on x.
Proof.
intros T. induction T.
- apply trans_accepting_base.
+ destruct p as [[p1 p2] b]. cbn. cbn in H. destruct b; auto.
now exfalso.
+ now apply intersect_transforms.
- destruct p as [[p1 p2] b]; destruct p' as [[p1' p2'] b']; destruct q as [[q1 q2] b''].
apply trans_accepting_step with (p' := p2'); cbn in *; auto.
destruct b; apply H.
Qed.
We have no formal proof that a match of the intersection is a match of aut_1 as this is not
required for the development and more effort to prove.
Lemma intersect_match_second (x y: NStr Sigma): is_match intersect x y -> is_match aut_2 x y.
Proof.
intros [p [q [I [H1 H2]]]].
exists (snd (fst p)), (snd (fst q)). repeat split.
- destruct p as [[p1 p2] ?]. cbn. apply I.
- now apply intersect_transforms.
- now apply intersect_transforms_accepting.
Qed.
End Intersection.
Proof.
intros [p [q [I [H1 H2]]]].
exists (snd (fst p)), (snd (fst q)). repeat split.
- destruct p as [[p1 p2] ?]. cbn. apply I.
- now apply intersect_transforms.
- now apply intersect_transforms_accepting.
Qed.
End Intersection.
ω-Iteration of a Regular Language
Given an NFA accepting a regular language, we construct the Büchi automaton accepting the ω-iteration of that language, i.e. sequences obtained as flattening a sequences of nonempty strings, which all belong the the regular language.
Section NFAOmegaIteration.
Context {Sigma:finType}.
Variable (aut: NFA Sigma).
Definition oiter_transition p a q := match p, q with
| None, None => exists (p_I q_F : state aut), initial_state p_I /\ accepting_state q_F /\ transition p_I a q_F
| None, Some q => exists (p_I: state aut), initial_state p_I /\ transition p_I a q
| Some p, None => exists q_F, accepting_state q_F /\ transition p a q_F
| Some p, Some q => transition p a q
end.
Definition nfa_omega_iter := mknfa oiter_transition (fun s => s = None) (fun s => s = None).
Lemma accepted_strings_transforms' (x: NStr Sigma) (p: state aut): snaccepting_ind p x -> (Some p : state nfa_omega_iter) ===> None on x.
Proof.
intros Ac. induction Ac as [p a q|p q a].
- apply trans_base. now exists q .
- apply trans_step with (p':=Some q); auto.
Qed.
Lemma accepted_strings_transforms (x: NStr Sigma) : L_NR aut x -> (None : state nfa_omega_iter) ===> None on x.
Proof.
intros [p_I [I Ac]].
destruct Ac as [p a q|p q a].
- apply trans_base. now exists p, q.
- apply trans_step with (p' := Some q).
+ now exists p.
+ now apply accepted_strings_transforms'.
Qed.
Lemma nfa_omega_iter_accepts_aut: (L_NR aut)^00 <$= L_B nfa_omega_iter.
Proof.
intros sigma [tau [W C]]. rewrite C.
apply accepting_quasi_run_iff_accepts.
exists (const None). repeat split.
- intros n. rewrite !const_nth. apply accepted_strings_transforms, W.
- intros m. exists m. split; auto.
apply trans_accepting_base.
+ apply const_nth.
+ rewrite !const_nth. apply accepted_strings_transforms, W.
Qed.
Lemma inf_often_zip_offset (sigma: Seq Sigma) (rho: Seq (state nfa_omega_iter)) P : inf_often P rho -> inf_often (fun t => match t with (_, q) => P q end) (zip sigma (tl rho)).
Proof.
intros Inf n. destruct (Inf (S n)) as [m [H1 H2]].
exists (pred m); split; auto.
rewrite zip_nth. rewrite <-nth_step_tl.
now rewrite_eq (S (pred m) = m).
Qed.
Inductive transforms_not_accepting : state nfa_omega_iter -> state nfa_omega_iter -> NStr Sigma -> Prop :=
| trans_not_base p q a: transition p a q -> transforms_not_accepting p q (sing a)
| trans_not_step p p' q a x : ~accepting_state p' -> transition p a p' -> transforms_not_accepting p' q x -> transforms_not_accepting p q (ncons a x) .
Lemma transforms_not_accepting_is_accepted' x p q : transforms_not_accepting p q x->
match p ,q with
| Some p, None => snaccepting_ind p x
| _, _ => True end.
Proof.
intros T. induction T as [[p|] [q|] a T |[p|] [p'|] [q|] a x NF]; auto.
- destruct T as [q [F T]]. now apply naccept_sing with (q0 := q).
- now apply naccept_step with (p0 := p').
- exfalso. now apply NF.
Qed.
Lemma transforms_not_accepting_is_accepted x : transforms_not_accepting None None x-> L_NR aut x.
Proof.
intros T. inversion T; subst.
- destruct H as [p [q [I [F T']]]]. exists p. split; auto.
now apply naccept_sing with (q0 :=q).
- destruct p' as [p'|].
+ destruct H0 as [p [F T']]. exists p. split; auto.
apply naccept_step with (p0 := p'); auto.
apply (transforms_not_accepting_is_accepted' H1).
+ exfalso. now apply H.
Qed.
Lemma between_accepting_state_transforms_not_accepting' (rho : Run nfa_omega_iter) sigma m: valid_run rho sigma ->
(forall n, n <= m -> ~ accepting_state (rho n)) ->
accepting_state (rho (S m)) -> transforms_not_accepting (rho 0) None (closed_prefix sigma m).
Proof.
revert rho sigma. induction m; intros rho sigma V NF F.
- simpl closed_prefix. apply trans_not_base. specialize (NF 0). specialize (V 0). destruct (rho 0) as [p|].
+ destruct (rho 1) as [q|].
* exfalso. cbn in F. congruence.
* destruct V as [q [F' T]]. now exists q.
+ exfalso. now apply NF.
- simpl closed_prefix. pose proof (NF 0) as NF0. pose proof (NF 1) as NF1. pose proof (V 0) as V0. pose proof (V 1) as V1. destruct (rho 0) as [p|].
+ apply trans_not_step with (p' := rho 1); auto.
rewrite nth_step_tl. apply IHm.
* now apply valid_run_tl.
* intros n L. rewrite <-nth_step_tl; auto.
* now rewrite <-nth_step_tl.
+ exfalso. apply NF0; auto. reflexivity.
Qed.
Lemma between_accepting_state_transforms_not_accepting (rho : Run nfa_omega_iter) sigma m: valid_run rho sigma -> initial rho ->
(forall n, 1 <= n <= m -> ~ accepting_state (rho n)) ->
accepting_state (rho (S m)) -> transforms_not_accepting None None (closed_prefix sigma m).
Proof.
intros V I NF F.
pose proof (V 0) as V0. unfold initial in *. destruct (rho 0) as [p|].
- exfalso. now cbn in I.
- destruct m as [|m].
+ cbn. destruct (rho 1) as [q |].
* exfalso. now cbn in F.
* now apply trans_not_base.
+ simpl closed_prefix. apply trans_not_step with (p' := rho 1); auto.
rewrite nth_step_tl. apply between_accepting_state_transforms_not_accepting'.
* now apply valid_run_tl.
* intros n L. rewrite <-nth_step_tl. apply NF. omega.
* now rewrite <-nth_step_tl.
Qed.
Lemma aut_accepts_nfa_omega_iter: L_B nfa_omega_iter <$= (L_NR aut)^00.
Proof.
intros sigma [rho [V [I Fin]]].
exists (map (nstr_map fst) (@factorize _ _ _ _ (inf_often_zip_offset sigma Fin))). split.
- intros n. revert sigma rho I Fin V. induction n; intros sigma rho I Fin V.
+ rewrite factorize_correct, map_correct, hd_correct, nth_first, <-closed_prefix_map, zip_map_fst.
apply transforms_not_accepting_is_accepted.
apply between_accepting_state_transforms_not_accepting with (rho := rho); auto.
* intros [|n] L. now exfalso.
pose proof (cc_nat_first_geq_exists_all (L := (inf_often_zip_offset sigma Fin 0))) as H1.
specialize (H1 n (ltac:(omega))). now rewrite zip_nth, <-nth_step_tl in H1.
* pose proof (cc_nat_first_geq_exists_correct (inf_often_zip_offset sigma Fin 0)) as H1.
now rewrite zip_nth, <-nth_step_tl in H1.
+ rewrite factorize_correct, map_correct, nth_step, tl_correct.
erewrite factorize_proper.
2: rewrite zip_drop, <-drop_tl; reflexivity.
apply IHn.
-- pose proof (cc_nat_first_geq_exists_correct (inf_often_zip_offset sigma Fin 0)) as H2.
now rewrite zip_nth, <-nth_step_tl in H2.
-- now apply valid_run_drop.
- rewrite <-flatten_map, flatten_factorize_inv. intros n. now rewrite map_nth, zip_nth.
Unshelve.
now apply inf_often_drop.
Qed.
Lemma nfa_omega_iter_correct: L_B nfa_omega_iter =$= (L_NR aut)^00.
Proof.
split. apply aut_accepts_nfa_omega_iter. apply nfa_omega_iter_accepts_aut.
Qed.
End NFAOmegaIteration.
Context {Sigma:finType}.
Variable (aut: NFA Sigma).
Definition oiter_transition p a q := match p, q with
| None, None => exists (p_I q_F : state aut), initial_state p_I /\ accepting_state q_F /\ transition p_I a q_F
| None, Some q => exists (p_I: state aut), initial_state p_I /\ transition p_I a q
| Some p, None => exists q_F, accepting_state q_F /\ transition p a q_F
| Some p, Some q => transition p a q
end.
Definition nfa_omega_iter := mknfa oiter_transition (fun s => s = None) (fun s => s = None).
Lemma accepted_strings_transforms' (x: NStr Sigma) (p: state aut): snaccepting_ind p x -> (Some p : state nfa_omega_iter) ===> None on x.
Proof.
intros Ac. induction Ac as [p a q|p q a].
- apply trans_base. now exists q .
- apply trans_step with (p':=Some q); auto.
Qed.
Lemma accepted_strings_transforms (x: NStr Sigma) : L_NR aut x -> (None : state nfa_omega_iter) ===> None on x.
Proof.
intros [p_I [I Ac]].
destruct Ac as [p a q|p q a].
- apply trans_base. now exists p, q.
- apply trans_step with (p' := Some q).
+ now exists p.
+ now apply accepted_strings_transforms'.
Qed.
Lemma nfa_omega_iter_accepts_aut: (L_NR aut)^00 <$= L_B nfa_omega_iter.
Proof.
intros sigma [tau [W C]]. rewrite C.
apply accepting_quasi_run_iff_accepts.
exists (const None). repeat split.
- intros n. rewrite !const_nth. apply accepted_strings_transforms, W.
- intros m. exists m. split; auto.
apply trans_accepting_base.
+ apply const_nth.
+ rewrite !const_nth. apply accepted_strings_transforms, W.
Qed.
Lemma inf_often_zip_offset (sigma: Seq Sigma) (rho: Seq (state nfa_omega_iter)) P : inf_often P rho -> inf_often (fun t => match t with (_, q) => P q end) (zip sigma (tl rho)).
Proof.
intros Inf n. destruct (Inf (S n)) as [m [H1 H2]].
exists (pred m); split; auto.
rewrite zip_nth. rewrite <-nth_step_tl.
now rewrite_eq (S (pred m) = m).
Qed.
Inductive transforms_not_accepting : state nfa_omega_iter -> state nfa_omega_iter -> NStr Sigma -> Prop :=
| trans_not_base p q a: transition p a q -> transforms_not_accepting p q (sing a)
| trans_not_step p p' q a x : ~accepting_state p' -> transition p a p' -> transforms_not_accepting p' q x -> transforms_not_accepting p q (ncons a x) .
Lemma transforms_not_accepting_is_accepted' x p q : transforms_not_accepting p q x->
match p ,q with
| Some p, None => snaccepting_ind p x
| _, _ => True end.
Proof.
intros T. induction T as [[p|] [q|] a T |[p|] [p'|] [q|] a x NF]; auto.
- destruct T as [q [F T]]. now apply naccept_sing with (q0 := q).
- now apply naccept_step with (p0 := p').
- exfalso. now apply NF.
Qed.
Lemma transforms_not_accepting_is_accepted x : transforms_not_accepting None None x-> L_NR aut x.
Proof.
intros T. inversion T; subst.
- destruct H as [p [q [I [F T']]]]. exists p. split; auto.
now apply naccept_sing with (q0 :=q).
- destruct p' as [p'|].
+ destruct H0 as [p [F T']]. exists p. split; auto.
apply naccept_step with (p0 := p'); auto.
apply (transforms_not_accepting_is_accepted' H1).
+ exfalso. now apply H.
Qed.
Lemma between_accepting_state_transforms_not_accepting' (rho : Run nfa_omega_iter) sigma m: valid_run rho sigma ->
(forall n, n <= m -> ~ accepting_state (rho n)) ->
accepting_state (rho (S m)) -> transforms_not_accepting (rho 0) None (closed_prefix sigma m).
Proof.
revert rho sigma. induction m; intros rho sigma V NF F.
- simpl closed_prefix. apply trans_not_base. specialize (NF 0). specialize (V 0). destruct (rho 0) as [p|].
+ destruct (rho 1) as [q|].
* exfalso. cbn in F. congruence.
* destruct V as [q [F' T]]. now exists q.
+ exfalso. now apply NF.
- simpl closed_prefix. pose proof (NF 0) as NF0. pose proof (NF 1) as NF1. pose proof (V 0) as V0. pose proof (V 1) as V1. destruct (rho 0) as [p|].
+ apply trans_not_step with (p' := rho 1); auto.
rewrite nth_step_tl. apply IHm.
* now apply valid_run_tl.
* intros n L. rewrite <-nth_step_tl; auto.
* now rewrite <-nth_step_tl.
+ exfalso. apply NF0; auto. reflexivity.
Qed.
Lemma between_accepting_state_transforms_not_accepting (rho : Run nfa_omega_iter) sigma m: valid_run rho sigma -> initial rho ->
(forall n, 1 <= n <= m -> ~ accepting_state (rho n)) ->
accepting_state (rho (S m)) -> transforms_not_accepting None None (closed_prefix sigma m).
Proof.
intros V I NF F.
pose proof (V 0) as V0. unfold initial in *. destruct (rho 0) as [p|].
- exfalso. now cbn in I.
- destruct m as [|m].
+ cbn. destruct (rho 1) as [q |].
* exfalso. now cbn in F.
* now apply trans_not_base.
+ simpl closed_prefix. apply trans_not_step with (p' := rho 1); auto.
rewrite nth_step_tl. apply between_accepting_state_transforms_not_accepting'.
* now apply valid_run_tl.
* intros n L. rewrite <-nth_step_tl. apply NF. omega.
* now rewrite <-nth_step_tl.
Qed.
Lemma aut_accepts_nfa_omega_iter: L_B nfa_omega_iter <$= (L_NR aut)^00.
Proof.
intros sigma [rho [V [I Fin]]].
exists (map (nstr_map fst) (@factorize _ _ _ _ (inf_often_zip_offset sigma Fin))). split.
- intros n. revert sigma rho I Fin V. induction n; intros sigma rho I Fin V.
+ rewrite factorize_correct, map_correct, hd_correct, nth_first, <-closed_prefix_map, zip_map_fst.
apply transforms_not_accepting_is_accepted.
apply between_accepting_state_transforms_not_accepting with (rho := rho); auto.
* intros [|n] L. now exfalso.
pose proof (cc_nat_first_geq_exists_all (L := (inf_often_zip_offset sigma Fin 0))) as H1.
specialize (H1 n (ltac:(omega))). now rewrite zip_nth, <-nth_step_tl in H1.
* pose proof (cc_nat_first_geq_exists_correct (inf_often_zip_offset sigma Fin 0)) as H1.
now rewrite zip_nth, <-nth_step_tl in H1.
+ rewrite factorize_correct, map_correct, nth_step, tl_correct.
erewrite factorize_proper.
2: rewrite zip_drop, <-drop_tl; reflexivity.
apply IHn.
-- pose proof (cc_nat_first_geq_exists_correct (inf_often_zip_offset sigma Fin 0)) as H2.
now rewrite zip_nth, <-nth_step_tl in H2.
-- now apply valid_run_drop.
- rewrite <-flatten_map, flatten_factorize_inv. intros n. now rewrite map_nth, zip_nth.
Unshelve.
now apply inf_often_drop.
Qed.
Lemma nfa_omega_iter_correct: L_B nfa_omega_iter =$= (L_NR aut)^00.
Proof.
split. apply aut_accepts_nfa_omega_iter. apply nfa_omega_iter_accepts_aut.
Qed.
End NFAOmegaIteration.
Section PrependNFA.
Context {Sigma:finType}.
Variable (aut_1 aut_2: NFA Sigma).
Implicit Types (p q: (state aut_1) (+) (state aut_2))(a:Sigma).
Definition prepend_transition p a q := match p, q with
| inl p, inl q => transition p a q
| inl p, inr q => initial_state q /\ exists (q': state aut_1), accepting_state q' /\ transition p a q'
| inr p, inr q => transition p a q
| _, _ => False end.
Definition prepend_state_accepting p := match p with
| inr p => accepting_state p
| inl p => False end.
Definition prepend_state_initial p := match p with
| inl p => initial_state p
| inr p => L_R aut_1 [] /\ initial_state p end.
Instance dec_mem_empty : dec (L_R aut_1 []).
Proof.
decide (exists (p: state aut_1), initial_state p /\ accepting_state p) as [D|D].
- left. destruct D as [p [I F]]. exists p. split; auto.
now apply accept_empty.
- right. intros [p [I Ac]]. inversion Ac. subst. firstorder.
Qed.
Definition prepend_nfa := mknfa prepend_transition prepend_state_initial prepend_state_accepting.
Notation isleft := (fun p => match p with | inl _ => True | inr _ => False end).
Notation isright := (fun p => match p with | inl _ => False | inr _ => True end).
Definition toright (q: state aut_2) p:= match p with
| inl _ => q
| inr p => p end.
Ltac destruct_isright q p := destruct q as [p|p]; [exfalso; auto|].
Ltac destruct_isright_eqn q p H:= destruct q as [p|p] eqn:H; [exfalso; auto|].
Ltac destruct_isleft q p := destruct q as [p|p]; [|exfalso; auto].
Ltac destruct_isleft_eqn q p H:= destruct q as [p|p] eqn:H; [|exfalso; auto].
Lemma notright_is_left p : ~ isright p <-> isleft p.
Proof.
destruct p as [p|p]; split; auto.
Qed.
Lemma switch_from_V_to_W rho sigma : accepting_for (aut:=prepend_nfa) rho sigma ->
{k | (forall n, n < k -> isleft (rho n)) /\ (forall n, isright (rho (n + k)))}.
Proof.
intros [V [I F]].
assert (exists n, 0 <= n /\ isright (rho n)) as H. { destruct (F 0) as [n [P Q]]. exists n. split; auto. destruct (rho n). apply Q. trivial. }
exists (cc_nat_first_geq_exists (f:=rho)H). repeat split.
- intros n H2. apply notright_is_left. apply (cc_nat_first_geq_exists_all (L := H)). omega.
- intros n. induction n.
+ cbn. pose proof (cc_nat_first_geq_exists_correct H). cbn in *.
now destruct_isright (rho (cc_nat_first_geq_exists H)) p.
+ remember (cc_nat_first_geq_exists H) as k. specialize (V ( n +k)). rewrite plus_Sn_m.
destruct_isright (rho (n+k)) p. now destruct_isright (rho (S (n + k))) q.
Qed.
Lemma prepend_aut_is_prepend_omega: L_B prepend_nfa <$= L_R aut_1 o L_B aut_2.
Proof.
intros sigma [rho Ac].
destruct (switch_from_V_to_W Ac) as [w_begin [AV AW]].
apply prepend_lang_split_position. exists ( w_begin). destruct Ac as [V [I F]].
split.
- destruct w_begin; unfold initial in I.
+ simpl. specialize (AW 0). simpl plus in AW. destruct_isright (rho 0) p. apply I.
+ rewrite nonempty_prefix_is_closed.
apply snlanguage_ind_iff_slanguage_ind.
pose proof (AV 0 (ltac:(omega))) as I0. destruct (rho 0) as [p_I|] eqn: E0; try now exfalso.
exists p_I. split; auto. clear I.
revert E0. generalize p_I. clear p_I. revert sigma rho V F AV AW. induction w_begin; intros sigma rho V F AV AW p E.
* simpl.
specialize (AW 0). simpl plus in AW. specialize (V 0). rewrite E in V. destruct (rho 1) as [q|q].
-- now exfalso.
-- destruct V as [I' [q_F [F' T]]]. now apply naccept_sing with (q0:=q_F).
* simpl.
pose proof (AV 1 (ltac:(omega))) as AV1. pose proof (V 0) as V0. rewrite E in V0. destruct (rho 1) as [q|q] eqn:E1.
-- apply naccept_step with (p0 := q). apply V0.
apply IHw_begin with (rho := tl rho).
++ now apply valid_run_tl.
++ now apply inf_often_tl.
++ intros n L. rewrite <-nth_step_tl. apply AV. omega.
++ intros n. rewrite <-nth_step_tl, plus_n_Sm. apply (AW n).
++ apply E1.
-- now exfalso.
- pose proof (AW 0) as AW0. simpl plus in AW0. destruct_isright (rho w_begin) q0. clear AW0.
exists (drop (map (toright q0) rho) w_begin). repeat split.
+ intros k. specialize (V (k + w_begin)).
rewrite 3drop_nth', 2map_nth.
pose proof (AW k) as AWk. pose proof (AW (S k)) as AWSk.
simpl in rho, V , AWk, AWSk. simpl.
destruct_isright (rho (k + w_begin)) p. destruct_isright (rho (S (k + w_begin))) q. simpl.
apply V.
+ unfold initial. rewrite drop_nth', map_nth. simpl. destruct w_begin.
* unfold initial in I. specialize (AW 0). simpl in rho, AW, I. simpl. destruct_isright (rho 0) p.
apply I.
* specialize (V w_begin). specialize (AW 0). specialize (AV w_begin). simpl in rho, V, AW, AV.
destruct_isright (rho (S w_begin)) p. destruct_isleft(rho w_begin) q. simpl. apply V.
+ apply inf_often_drop. apply inf_often_map with (P:= accepting_state (aut:= prepend_nfa)).
* intros [p|p] Fin; simpl in *; auto. now exfalso.
* apply F.
Qed.
Lemma prepend_aut_accepts_prepend_omega: L_R aut_1 o L_B aut_2 <$= L_B prepend_nfa.
Proof.
intros sigma [x [tau [Ac [[rho [Vrho [Irho Frho]]] E]]]]. rewrite E.
destruct x as [|a x].
- simpl. exists (map inr rho). repeat split; auto.
+ intros n. simpl. rewrite 2map_nth. apply Vrho.
+ apply inf_often_map with (P:= accepting_state (aut:=aut_2)); auto.
- rewrite str_to_nstr_idem'. rewrite str_to_nstr_idem' in Ac.
remember (!a :: x) as y. clear a x E Heqy. apply snlanguage_ind_iff_slanguage_ind in Ac.
destruct Ac as [p_I[ I Ac]].
enough (forall (p: state aut_1), snaccepting_ind p y -> exists (r: Run prepend_nfa), r 0 = inl p /\ valid_run r (y +++ tau) /\ accepting r) as H.
+ destruct (H p_I Ac) as [r [B [V F]]]. exists r. repeat split; auto.
unfold initial. now rewrite B.
+ clear p_I I Ac. intros p Ac. induction Ac as [p a q T| p' q a p].
* exists (inl p ::: map inr rho). repeat split.
-- simpl. apply (valid_run_cons (aut:= prepend_nfa)).
++ rewrite map_nth. split; auto. firstorder.
++ intros n. rewrite !map_nth. apply Vrho.
-- apply inf_often_cons, inf_often_map with (P := accepting_state (aut:= aut_2)); auto.
* destruct IHAc as [r [E [V F]]]. exists (inl p' ::: r). repeat split.
-- simpl. apply (valid_run_cons (aut:= prepend_nfa)); auto.
now rewrite E.
-- now apply inf_often_cons.
Qed.
Lemma prepend_nfa_correct: L_B prepend_nfa =$= L_R aut_1 o L_B aut_2.
Proof.
split. apply prepend_aut_is_prepend_omega. apply prepend_aut_accepts_prepend_omega.
Qed.
End PrependNFA.
Context {Sigma:finType}.
Variable (aut_1 aut_2: NFA Sigma).
Implicit Types (p q: (state aut_1) (+) (state aut_2))(a:Sigma).
Definition prepend_transition p a q := match p, q with
| inl p, inl q => transition p a q
| inl p, inr q => initial_state q /\ exists (q': state aut_1), accepting_state q' /\ transition p a q'
| inr p, inr q => transition p a q
| _, _ => False end.
Definition prepend_state_accepting p := match p with
| inr p => accepting_state p
| inl p => False end.
Definition prepend_state_initial p := match p with
| inl p => initial_state p
| inr p => L_R aut_1 [] /\ initial_state p end.
Instance dec_mem_empty : dec (L_R aut_1 []).
Proof.
decide (exists (p: state aut_1), initial_state p /\ accepting_state p) as [D|D].
- left. destruct D as [p [I F]]. exists p. split; auto.
now apply accept_empty.
- right. intros [p [I Ac]]. inversion Ac. subst. firstorder.
Qed.
Definition prepend_nfa := mknfa prepend_transition prepend_state_initial prepend_state_accepting.
Notation isleft := (fun p => match p with | inl _ => True | inr _ => False end).
Notation isright := (fun p => match p with | inl _ => False | inr _ => True end).
Definition toright (q: state aut_2) p:= match p with
| inl _ => q
| inr p => p end.
Ltac destruct_isright q p := destruct q as [p|p]; [exfalso; auto|].
Ltac destruct_isright_eqn q p H:= destruct q as [p|p] eqn:H; [exfalso; auto|].
Ltac destruct_isleft q p := destruct q as [p|p]; [|exfalso; auto].
Ltac destruct_isleft_eqn q p H:= destruct q as [p|p] eqn:H; [|exfalso; auto].
Lemma notright_is_left p : ~ isright p <-> isleft p.
Proof.
destruct p as [p|p]; split; auto.
Qed.
Lemma switch_from_V_to_W rho sigma : accepting_for (aut:=prepend_nfa) rho sigma ->
{k | (forall n, n < k -> isleft (rho n)) /\ (forall n, isright (rho (n + k)))}.
Proof.
intros [V [I F]].
assert (exists n, 0 <= n /\ isright (rho n)) as H. { destruct (F 0) as [n [P Q]]. exists n. split; auto. destruct (rho n). apply Q. trivial. }
exists (cc_nat_first_geq_exists (f:=rho)H). repeat split.
- intros n H2. apply notright_is_left. apply (cc_nat_first_geq_exists_all (L := H)). omega.
- intros n. induction n.
+ cbn. pose proof (cc_nat_first_geq_exists_correct H). cbn in *.
now destruct_isright (rho (cc_nat_first_geq_exists H)) p.
+ remember (cc_nat_first_geq_exists H) as k. specialize (V ( n +k)). rewrite plus_Sn_m.
destruct_isright (rho (n+k)) p. now destruct_isright (rho (S (n + k))) q.
Qed.
Lemma prepend_aut_is_prepend_omega: L_B prepend_nfa <$= L_R aut_1 o L_B aut_2.
Proof.
intros sigma [rho Ac].
destruct (switch_from_V_to_W Ac) as [w_begin [AV AW]].
apply prepend_lang_split_position. exists ( w_begin). destruct Ac as [V [I F]].
split.
- destruct w_begin; unfold initial in I.
+ simpl. specialize (AW 0). simpl plus in AW. destruct_isright (rho 0) p. apply I.
+ rewrite nonempty_prefix_is_closed.
apply snlanguage_ind_iff_slanguage_ind.
pose proof (AV 0 (ltac:(omega))) as I0. destruct (rho 0) as [p_I|] eqn: E0; try now exfalso.
exists p_I. split; auto. clear I.
revert E0. generalize p_I. clear p_I. revert sigma rho V F AV AW. induction w_begin; intros sigma rho V F AV AW p E.
* simpl.
specialize (AW 0). simpl plus in AW. specialize (V 0). rewrite E in V. destruct (rho 1) as [q|q].
-- now exfalso.
-- destruct V as [I' [q_F [F' T]]]. now apply naccept_sing with (q0:=q_F).
* simpl.
pose proof (AV 1 (ltac:(omega))) as AV1. pose proof (V 0) as V0. rewrite E in V0. destruct (rho 1) as [q|q] eqn:E1.
-- apply naccept_step with (p0 := q). apply V0.
apply IHw_begin with (rho := tl rho).
++ now apply valid_run_tl.
++ now apply inf_often_tl.
++ intros n L. rewrite <-nth_step_tl. apply AV. omega.
++ intros n. rewrite <-nth_step_tl, plus_n_Sm. apply (AW n).
++ apply E1.
-- now exfalso.
- pose proof (AW 0) as AW0. simpl plus in AW0. destruct_isright (rho w_begin) q0. clear AW0.
exists (drop (map (toright q0) rho) w_begin). repeat split.
+ intros k. specialize (V (k + w_begin)).
rewrite 3drop_nth', 2map_nth.
pose proof (AW k) as AWk. pose proof (AW (S k)) as AWSk.
simpl in rho, V , AWk, AWSk. simpl.
destruct_isright (rho (k + w_begin)) p. destruct_isright (rho (S (k + w_begin))) q. simpl.
apply V.
+ unfold initial. rewrite drop_nth', map_nth. simpl. destruct w_begin.
* unfold initial in I. specialize (AW 0). simpl in rho, AW, I. simpl. destruct_isright (rho 0) p.
apply I.
* specialize (V w_begin). specialize (AW 0). specialize (AV w_begin). simpl in rho, V, AW, AV.
destruct_isright (rho (S w_begin)) p. destruct_isleft(rho w_begin) q. simpl. apply V.
+ apply inf_often_drop. apply inf_often_map with (P:= accepting_state (aut:= prepend_nfa)).
* intros [p|p] Fin; simpl in *; auto. now exfalso.
* apply F.
Qed.
Lemma prepend_aut_accepts_prepend_omega: L_R aut_1 o L_B aut_2 <$= L_B prepend_nfa.
Proof.
intros sigma [x [tau [Ac [[rho [Vrho [Irho Frho]]] E]]]]. rewrite E.
destruct x as [|a x].
- simpl. exists (map inr rho). repeat split; auto.
+ intros n. simpl. rewrite 2map_nth. apply Vrho.
+ apply inf_often_map with (P:= accepting_state (aut:=aut_2)); auto.
- rewrite str_to_nstr_idem'. rewrite str_to_nstr_idem' in Ac.
remember (!a :: x) as y. clear a x E Heqy. apply snlanguage_ind_iff_slanguage_ind in Ac.
destruct Ac as [p_I[ I Ac]].
enough (forall (p: state aut_1), snaccepting_ind p y -> exists (r: Run prepend_nfa), r 0 = inl p /\ valid_run r (y +++ tau) /\ accepting r) as H.
+ destruct (H p_I Ac) as [r [B [V F]]]. exists r. repeat split; auto.
unfold initial. now rewrite B.
+ clear p_I I Ac. intros p Ac. induction Ac as [p a q T| p' q a p].
* exists (inl p ::: map inr rho). repeat split.
-- simpl. apply (valid_run_cons (aut:= prepend_nfa)).
++ rewrite map_nth. split; auto. firstorder.
++ intros n. rewrite !map_nth. apply Vrho.
-- apply inf_often_cons, inf_often_map with (P := accepting_state (aut:= aut_2)); auto.
* destruct IHAc as [r [E [V F]]]. exists (inl p' ::: r). repeat split.
-- simpl. apply (valid_run_cons (aut:= prepend_nfa)); auto.
now rewrite E.
-- now apply inf_often_cons.
Qed.
Lemma prepend_nfa_correct: L_B prepend_nfa =$= L_R aut_1 o L_B aut_2.
Proof.
split. apply prepend_aut_is_prepend_omega. apply prepend_aut_accepts_prepend_omega.
Qed.
End PrependNFA.
Properties of UP Sequences
We show that acceptance of UP sequences is decidable and for every accepted UP sequence there is an equivalent match.Definition exact_up_nfa (Sigma:finType) (x: Str Sigma)(y: NStr Sigma):= prepend_nfa (os_nfa x) (nfa_omega_iter (os_nfa y)).
Lemma exact_up_nfa_correct (Sigma:finType) (x: Str Sigma)(y: NStr Sigma): L_B (exact_up_nfa x y) =$= fun sigma => sigma == x +++ omega_iter y.
Proof.
unfold exact_up_nfa.
rewrite prepend_nfa_correct, nfa_omega_iter_correct, os_nfa_correct, nstr_os_nfa_correct.
intros sigma. split.
- intros [x' [y' [E1 [[tau [H2 H3]] H]]]].
subst x'. rewrite H. apply prepend_proper; auto. rewrite H3.
unfold omega_iter. apply flatten_proper. intros n. now rewrite const_nth.
- intros E. exists x, (omega_iter y). repeat split; auto.
exists (const y). repeat split; auto. apply const_nth.
Qed.
Lemma dec_up_in_lang (Sigma: finType)(x : Str Sigma) (y: NStr Sigma)(aut: NFA Sigma): dec (L_B aut (x+++omega_iter y)).
Proof.
destruct (dec_buechi_empty_informative (intersect aut (exact_up_nfa x y))) as [D|D].
- left. destruct D as [x' [y' D]].
apply match_accepted, intersect_correct in D.
destruct D as [D1 D2]. apply exact_up_nfa_correct in D2.
now rewrite <-D2.
- right. intros L.
apply (D (x +++ omega_iter y)). apply intersect_correct. split.
+ apply L.
+ now apply exact_up_nfa_correct.
Qed.
Lemma match_for_up (Sigma: finType) (aut : NFA Sigma) ( x y : NStr Sigma) : L_B aut ( x +++ (omega_iter y)) -> exists u v, is_match aut u v /\ x +++ (omega_iter y) == u +++ (omega_iter v).
Proof.
intros H.
assert (exists sigma, L_B (intersect (exact_up_nfa x y) aut)sigma) as H'.
- exists (x +++ omega_iter y). apply intersect_correct. split; auto. now apply exact_up_nfa_correct.
- apply nonempty_iff_match in H'.
destruct H' as [u [v M]]. exists u,v.
repeat split.
+ now apply intersect_match_second in M.
+ symmetry. apply exact_up_nfa_correct.
apply match_accepted,intersect_correct in M.
apply M.
Qed.
End Buechi.
Notation "'L_B'" := accepts.