Set Implicit Arguments.
Require Import Coq.Init.Nat.
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Require Import NFAs.
Require Import RegularLanguages.
Open Scope string_scope.
Require Import Coq.Init.Nat.
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Require Import NFAs.
Require Import RegularLanguages.
Open Scope string_scope.
Section BuechiAutomaton.
Context {X:finType}.
Variable (aut: NFA X).
Implicit Types (r: Run aut) (w: Seq X).
Definition initial r := initial_state (r 0).
Definition final r := infiniteP (final_state (aut:=aut)) r.
Definition accepting r w := (valid_run r w) /\ (initial r) /\ (final r).
Definition buechi_language : SeqLang X := fun w => exists r, accepting r w.
Lemma accepting_extensional r r' w w' : r === r' -> w === w' -> accepting r w -> accepting r' w'.
Proof.
intros Er Ew [V [In Fin]]. repeat split.
- now rewrite <-Er, <- Ew.
- red. now rewrite <-Er.
- now rewrite <-Er.
Qed.
Global Instance accepting_proper: Proper (@seq_equal (state aut) ==> @seq_equal X ==> iff) accepting.
Proof.
intros r r' Er w w' Ew. split; apply accepting_extensional; auto.
Qed.
Global Instance buechi_language_proper : Proper (@seq_equal X ==> iff) buechi_language.
Proof.
intros w w' E; split; intros [r A]; exists r. now rewrite <-E. now rewrite E.
Qed.
Lemma final_drop r n : final r -> final (drop n r).
Proof. now apply drop_preserves_infiniteP. Qed.
Lemma final_prepend (r' : String (state aut)) r : final r -> final (r' +++ r).
Proof. now apply finite_prefix_preserves_infiniteP. Qed.
Lemma omega_iteration_final (r: String (state aut)) k: k <= |r| -> final_state (r [k]) -> final (r to_omega).
Proof. intros L F. apply omega_iteration_infiniteP. firstorder. Qed.
Lemma final_iff_step r: (exists n, final_state (r n)) -> (forall n, final_state (r n) -> exists m, n < m /\ final_state (r m)) -> final r.
Proof.
intros B S n. induction n.
- destruct B as [n F]. exists n; split; oauto.
- destruct IHn as [m [G F]].
destruct (S m F) as [m' [G' F']].
exists m'. split; oauto.
Qed.
End BuechiAutomaton.
Notation "'L_B'" := buechi_language.
Context {X:finType}.
Variable (aut: NFA X).
Implicit Types (r: Run aut) (w: Seq X).
Definition initial r := initial_state (r 0).
Definition final r := infiniteP (final_state (aut:=aut)) r.
Definition accepting r w := (valid_run r w) /\ (initial r) /\ (final r).
Definition buechi_language : SeqLang X := fun w => exists r, accepting r w.
Lemma accepting_extensional r r' w w' : r === r' -> w === w' -> accepting r w -> accepting r' w'.
Proof.
intros Er Ew [V [In Fin]]. repeat split.
- now rewrite <-Er, <- Ew.
- red. now rewrite <-Er.
- now rewrite <-Er.
Qed.
Global Instance accepting_proper: Proper (@seq_equal (state aut) ==> @seq_equal X ==> iff) accepting.
Proof.
intros r r' Er w w' Ew. split; apply accepting_extensional; auto.
Qed.
Global Instance buechi_language_proper : Proper (@seq_equal X ==> iff) buechi_language.
Proof.
intros w w' E; split; intros [r A]; exists r. now rewrite <-E. now rewrite E.
Qed.
Lemma final_drop r n : final r -> final (drop n r).
Proof. now apply drop_preserves_infiniteP. Qed.
Lemma final_prepend (r' : String (state aut)) r : final r -> final (r' +++ r).
Proof. now apply finite_prefix_preserves_infiniteP. Qed.
Lemma omega_iteration_final (r: String (state aut)) k: k <= |r| -> final_state (r [k]) -> final (r to_omega).
Proof. intros L F. apply omega_iteration_infiniteP. firstorder. Qed.
Lemma final_iff_step r: (exists n, final_state (r n)) -> (forall n, final_state (r n) -> exists m, n < m /\ final_state (r m)) -> final r.
Proof.
intros B S n. induction n.
- destruct B as [n F]. exists n; split; oauto.
- destruct IHn as [m [G F]].
destruct (S m F) as [m' [G' F']].
exists m'. split; oauto.
Qed.
End BuechiAutomaton.
Notation "'L_B'" := buechi_language.
Empty and Universal Büchi Automataon
Section EmptyBuechiAutomaton.
Context {X:finType}.
Definition empty_aut := mknfa (fun (s : finType_False)(x:X) (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 seq_in_empty_aut_contradicts w: L_B empty_aut w -> False.
Proof. apply (empty_aut_correct w). Qed.
End EmptyBuechiAutomaton.
Section UniversalBuechiAutomaton.
Context {X:finType}.
Lemma univ_aut_correct: L_B (univ_aut (X:=X)) =$= universal_language.
Proof.
intros w. split; firstorder.
exists (fun n => tt); repeat split.
intros n. exists n; oauto.
Qed.
End UniversalBuechiAutomaton.
Context {X:finType}.
Definition empty_aut := mknfa (fun (s : finType_False)(x:X) (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 seq_in_empty_aut_contradicts w: L_B empty_aut w -> False.
Proof. apply (empty_aut_correct w). Qed.
End EmptyBuechiAutomaton.
Section UniversalBuechiAutomaton.
Context {X:finType}.
Lemma univ_aut_correct: L_B (univ_aut (X:=X)) =$= universal_language.
Proof.
intros w. split; firstorder.
exists (fun n => tt); repeat split.
intros n. exists n; oauto.
Qed.
End UniversalBuechiAutomaton.
Section DecBuechiAutomatonEmpty.
Context {X: finType}.
Variable (aut: NFA X).
Implicit Types (w: Seq X) (s: state aut).
Definition final_loop_exists := exists (s_i s_f: state aut), initial_state s_i /\ final_state s_f /\ reachable s_i s_f /\ reachable s_f s_f.
Lemma seq_implies_final_loop : (exists w, L_B aut w) -> final_loop_exists.
Proof.
intros [w [r [V [I F]]]]. exists (r 0).
pose (r_f := infinite_filter F).
destruct (can_find_duplicate' 1 (S(S (Cardinality (state aut)))) (seq_map r r_f)) as [[i [j [L [_ E]]]]|D].
- exists (r (r_f i)). repeat split; auto.
+ subst r_f. apply infinite_filter_correct.
+ exists r, (mkstring w (pred (r_f i))). repeat split.
* now apply valid_run_is_path_from_begin.
* cbn. f_equal. enough (r_f i > 0) by omega.
subst r_f. enough (1 <= i); try omega.
apply s_monotone_ge_zero'; auto. apply infinite_filter_s_monotone.
+ exists (drop (r_f i) r), (extract (r_f i) (r_f j) w). repeat split.
* now apply valid_run_is_path_everywhere.
* rewrite drop_correct. f_equal. omega.
* unfold seq_map in E. rewrite E.
rewrite drop_correct. cbn. f_equal.
enough (r_f j > (r_f i)) by omega.
apply s_monotone_strict_order_preserving; oauto.
apply infinite_filter_s_monotone.
- exfalso. omega.
Qed.
Lemma final_loop_implies_up_seq : final_loop_exists -> (exists u v, L_B aut (u +++ v to_omega)).
Proof.
intros [s_i [s_f [I [F [[r_i [u [Vi [Bi Ei]]]] [r_f [v Pf]]]]]]].
exists u, v, ((mkstring r_i (|u|)) +++ (mkstring r_f (|v|)) to_omega). repeat split.
- apply valid_prepend_path; auto.
+ cbn. destruct Pf as [_ [Bf _]]. now rewrite Bf, <-Ei.
+ now apply cycle_omega_is_valid_run with (s:=s_f).
- unfold initial. rewrite prepend_string_begin by omega.
cbn. now rewrite Bi.
- apply final_prepend. apply omega_iteration_final with (k := 0). omega.
cbn. destruct Pf as [_ [Bf _]]. now rewrite Bf.
Qed.
Theorem dec_language_empty_informative_periodic : {exists u v, L_B aut (u +++ v to_omega)} + {L_B aut =$= {}}.
Proof.
decide (final_loop_exists) as [D|D].
- left. now apply final_loop_implies_up_seq.
- right. intros w. split.
+ intros M. apply D, seq_implies_final_loop. now exists w.
+ intros M. exfalso. apply M.
Qed.
Corollary dec_language_empty_informative : {exists w, L_B aut w} + {L_B aut =$= {}}.
Proof.
destruct (dec_language_empty_informative_periodic) as [D|D].
- left. destruct D as [v [w L]]. now exists (v +++ w to_omega).
- now right.
Qed.
Corollary dec_language_empty: dec(L_B aut =$= {}).
Proof.
destruct dec_language_empty_informative as [D|D].
- right. intros E. destruct D as [w Lw]. now apply (E w).
- now left.
Qed.
End DecBuechiAutomatonEmpty.
Section ImageNFA.
Context {X Y : finType}.
Variable (f : X -> Y).
Variable (aut: NFA X).
Definition image_transition (s: state aut) (y: Y) (s': state aut) := exists x, f x = y /\ transition (aut:=aut) s x s'.
Definition image_aut := mknfa image_transition (initial_state (aut:=aut)) (final_state (aut:=aut)).
Lemma aut_accepts_image: L_B image_aut <$= Image f (L_B aut) .
Proof.
intros w' [r [V [I F]]].
assert (forall n, { x | f x = w' n /\ transition (aut:=aut) (r n) x (r (S n))}) as W. {
intros n . apply finType_cc; auto. now specialize (V n). }
exists (fun n => proj1_sig (W n)). split.
- intros n. unfold seq_map. now destruct (W n) as [x [P Q]].
- exists r. repeat split; auto.
intros n. now destruct (W n).
Qed.
Lemma image_accepts_aut: Image f (L_B aut) <$= L_B image_aut.
Proof.
intros w [w' [E [r [V [I F]]]]].
exists r. repeat split; auto. rewrite <-E.
intros n. cbn. now exists (w' 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.
End ImageNFA.
Section PreImageNFA.
Context {X Y:finType}.
Variable (f: X -> Y).
Variable (aut: NFA Y).
Implicit Types (p q : state aut).
Definition preimage_aut := mknfa (fun p a q => transition p (f a) q) (initial_state (aut:=aut)) (final_state (aut:=aut)).
Lemma preimage_aut_correct : L_B preimage_aut =$= PreImage f (L_B aut).
Proof.
intros w. split; intros [r [V [In Fin]]]; exists r; repeat split; auto.
Qed.
End PreImageNFA.
Context {X Y : finType}.
Variable (f : X -> Y).
Variable (aut: NFA X).
Definition image_transition (s: state aut) (y: Y) (s': state aut) := exists x, f x = y /\ transition (aut:=aut) s x s'.
Definition image_aut := mknfa image_transition (initial_state (aut:=aut)) (final_state (aut:=aut)).
Lemma aut_accepts_image: L_B image_aut <$= Image f (L_B aut) .
Proof.
intros w' [r [V [I F]]].
assert (forall n, { x | f x = w' n /\ transition (aut:=aut) (r n) x (r (S n))}) as W. {
intros n . apply finType_cc; auto. now specialize (V n). }
exists (fun n => proj1_sig (W n)). split.
- intros n. unfold seq_map. now destruct (W n) as [x [P Q]].
- exists r. repeat split; auto.
intros n. now destruct (W n).
Qed.
Lemma image_accepts_aut: Image f (L_B aut) <$= L_B image_aut.
Proof.
intros w [w' [E [r [V [I F]]]]].
exists r. repeat split; auto. rewrite <-E.
intros n. cbn. now exists (w' 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.
End ImageNFA.
Section PreImageNFA.
Context {X Y:finType}.
Variable (f: X -> Y).
Variable (aut: NFA Y).
Implicit Types (p q : state aut).
Definition preimage_aut := mknfa (fun p a q => transition p (f a) q) (initial_state (aut:=aut)) (final_state (aut:=aut)).
Lemma preimage_aut_correct : L_B preimage_aut =$= PreImage f (L_B aut).
Proof.
intros w. split; intros [r [V [In Fin]]]; exists r; repeat split; auto.
Qed.
End PreImageNFA.
Section UnionClosure.
Context {X : finType}.
Section Def.
Variables (aut_1 aut_2 : NFA X).
Definition union_state : finType := (state aut_1) (+) (state aut_2).
Definition union_transition (s1:union_state) (x:X) (s2:union_state) := match s1,s2 with
| (inl s1), (inl s2) => transition s1 x s2
| (inr s1), (inr s2) => transition s1 x s2
| _ , _ => False
end.
Definition union_initial (s:union_state) := match s with
| inl s => initial_state s
| inr s => initial_state s
end.
Definition union_final (s : union_state) :=match s with
| inl s => final_state s
| inr s => final_state s
end.
Instance dec_union_transition: forall s1 x s2, dec(union_transition s1 x s2).
Proof.
intros s1 x s2. destruct s1,s2; simpl; auto.
Qed.
Instance dec_union_initial: forall s, dec(union_initial s).
Proof.
intros s. destruct s; auto.
Qed.
Instance dec_union_final: forall s, dec(union_final s).
Proof.
intros s. destruct s; simpl; auto.
Qed.
Definition union:= mknfa union_transition union_initial union_final.
Implicit Types (w: Seq X) (r: Run union).
Context {X : finType}.
Section Def.
Variables (aut_1 aut_2 : NFA X).
Definition union_state : finType := (state aut_1) (+) (state aut_2).
Definition union_transition (s1:union_state) (x:X) (s2:union_state) := match s1,s2 with
| (inl s1), (inl s2) => transition s1 x s2
| (inr s1), (inr s2) => transition s1 x s2
| _ , _ => False
end.
Definition union_initial (s:union_state) := match s with
| inl s => initial_state s
| inr s => initial_state s
end.
Definition union_final (s : union_state) :=match s with
| inl s => final_state s
| inr s => final_state s
end.
Instance dec_union_transition: forall s1 x s2, dec(union_transition s1 x s2).
Proof.
intros s1 x s2. destruct s1,s2; simpl; auto.
Qed.
Instance dec_union_initial: forall s, dec(union_initial s).
Proof.
intros s. destruct s; auto.
Qed.
Instance dec_union_final: forall s, dec(union_final s).
Proof.
intros s. destruct s; simpl; auto.
Qed.
Definition union:= mknfa union_transition union_initial union_final.
Implicit Types (w: Seq X) (r: Run union).
Because states from aut1 can only go the states of aut1
Lemma states_do_not_mix r w : valid_run r w -> (exists s, (r 0) = inl s) ->
(forall n, exists s, r n = inl s).
Proof.
intros V [s L] .
induction n.
- firstorder.
- specialize (V n). destruct (r ( S n)) as [s2 |s2].
+ now exists s2.
+ exfalso. destruct IHn as [s1 E]. now rewrite E in V.
Qed.
(forall n, exists s, r n = inl s).
Proof.
intros V [s L] .
induction n.
- firstorder.
- specialize (V n). destruct (r ( S n)) as [s2 |s2].
+ now exists s2.
+ exfalso. destruct IHn as [s1 E]. now rewrite E in V.
Qed.
Given an accepting run of the union aut, the first state of the run decides whether the sequence
is accepted by aut1 or aut2
Lemma autU_accepted_by_aut1 r w:
accepting r w -> (exists s, (r 0) = inl s) -> (L_B aut_1 w).
Proof.
intros [V [I Fin]] B.
assert (forall n, exists s, r n = inl s) as M by now apply (states_do_not_mix V).
destruct B as [s B].
exists (seq_map (fun s' => match s' with
| inl s' => s'
| inr _ => s
end) r ). repeat split; unfold seq_map.
- intros n. specialize (V n).
destruct (M n) as [s1 E1]. destruct (M (S n)) as [s2 E2]. now rewrite E1, E2 in *.
- red. red in I. destruct (M 0) as [s0 E0]. now rewrite E0 in *.
- intros n. destruct (Fin n) as [m [P Q]].
exists m. split; auto.
destruct (M m) as [sm Em]. now rewrite Em in *.
Qed.
Lemma aut1_incl_autU: L_B aut_1 <$= L_B union.
Proof.
intros w [r [V [I Fin]]].
exists (fun n => inl (r n)). repeat split; auto.
Qed.
End Def.
Definition swap_sum (X Y: Type) (v: X + Y) := match v with | inl l => inr l | inr r => inl r end.
Arguments swap_sum {X} {Y} _.
Lemma union_symmetric_acc (aut_1 aut_2: NFA X) r w: accepting (aut:=union aut_1 aut_2) r w -> accepting (aut:= union aut_2 aut_1) (seq_map swap_sum r) w.
Proof.
intros [V [I F]]. repeat split; unfold seq_map.
- intros n. specialize (V n). now destruct (r n); destruct (r (S n)).
- unfold initial in *. now destruct (r 0).
- intros n. destruct (F n) as [m [P Q]]. exists m. split; auto. now destruct (r m).
Qed.
Lemma union_symmetric (aut_1 aut_2 : NFA X) : L_B (union aut_1 aut_2) =$= L_B (union aut_2 aut_1).
Proof.
intros w. split; intros [r Acc]; exists (seq_map swap_sum r); now apply union_symmetric_acc.
Qed.
Lemma union_correct (aut_1 aut_2 : NFA X) : L_B (union aut_1 aut_2) =$= L_B aut_1 \$/ L_B aut_2.
Proof.
intros w. split.
- intros L. destruct L as [r Acc] . destruct (r 0) eqn:H.
+ left. apply autU_accepted_by_aut1 with (r:=r); firstorder.
+ right. apply union_symmetric_acc in Acc.
eapply autU_accepted_by_aut1. apply Acc. exists e. unfold seq_map. now rewrite H.
- intros [L1 | L2].
+ now apply aut1_incl_autU.
+ apply union_symmetric. now apply aut1_incl_autU.
Qed.
End UnionClosure.
accepting r w -> (exists s, (r 0) = inl s) -> (L_B aut_1 w).
Proof.
intros [V [I Fin]] B.
assert (forall n, exists s, r n = inl s) as M by now apply (states_do_not_mix V).
destruct B as [s B].
exists (seq_map (fun s' => match s' with
| inl s' => s'
| inr _ => s
end) r ). repeat split; unfold seq_map.
- intros n. specialize (V n).
destruct (M n) as [s1 E1]. destruct (M (S n)) as [s2 E2]. now rewrite E1, E2 in *.
- red. red in I. destruct (M 0) as [s0 E0]. now rewrite E0 in *.
- intros n. destruct (Fin n) as [m [P Q]].
exists m. split; auto.
destruct (M m) as [sm Em]. now rewrite Em in *.
Qed.
Lemma aut1_incl_autU: L_B aut_1 <$= L_B union.
Proof.
intros w [r [V [I Fin]]].
exists (fun n => inl (r n)). repeat split; auto.
Qed.
End Def.
Definition swap_sum (X Y: Type) (v: X + Y) := match v with | inl l => inr l | inr r => inl r end.
Arguments swap_sum {X} {Y} _.
Lemma union_symmetric_acc (aut_1 aut_2: NFA X) r w: accepting (aut:=union aut_1 aut_2) r w -> accepting (aut:= union aut_2 aut_1) (seq_map swap_sum r) w.
Proof.
intros [V [I F]]. repeat split; unfold seq_map.
- intros n. specialize (V n). now destruct (r n); destruct (r (S n)).
- unfold initial in *. now destruct (r 0).
- intros n. destruct (F n) as [m [P Q]]. exists m. split; auto. now destruct (r m).
Qed.
Lemma union_symmetric (aut_1 aut_2 : NFA X) : L_B (union aut_1 aut_2) =$= L_B (union aut_2 aut_1).
Proof.
intros w. split; intros [r Acc]; exists (seq_map swap_sum r); now apply union_symmetric_acc.
Qed.
Lemma union_correct (aut_1 aut_2 : NFA X) : L_B (union aut_1 aut_2) =$= L_B aut_1 \$/ L_B aut_2.
Proof.
intros w. split.
- intros L. destruct L as [r Acc] . destruct (r 0) eqn:H.
+ left. apply autU_accepted_by_aut1 with (r:=r); firstorder.
+ right. apply union_symmetric_acc in Acc.
eapply autU_accepted_by_aut1. apply Acc. exists e. unfold seq_map. now rewrite H.
- intros [L1 | L2].
+ now apply aut1_incl_autU.
+ apply union_symmetric. now apply aut1_incl_autU.
Qed.
End UnionClosure.
Section IntersectionClosure.
Context (X:finType).
Variables (aut_1 aut_2 : NFA X).
Definition intersection_state := state aut_1 (x) state aut_2 (x) finType_bool.
Implicit Types (x:X)(s: intersection_state)(w:Seq X).
Definition intersection_initial s := match s with
| (s_1, s_2, _) => initial_state s_1 /\ initial_state s_2
end.
Definition intersection_final s := match s with
| (_, s_2 , true) => final_state s_2
| _ => False
end.
Definition intersection_transition s x s' := match s,s' with
| (s_1, s_2, true), (s_1',s_2',b) =>
(transition s_1 x s_1') /\ (transition s_2 x s_2') /\
(b = false <-> final_state s_2)
| (s_1, s_2, false), (s_1',s_2',b) =>
(transition s_1 x s_1') /\ (transition s_2 x s_2') /\
(b = true <-> final_state s_1)
end.
Instance dec_intersection_initial s : dec(intersection_initial s).
Proof. destruct s as [[? ?] ?]; auto. Qed.
Instance dec_intersection_final s : dec (intersection_final s).
Proof. destruct s as [[? ?] [|]]; auto. Qed.
Instance dec_intersection_transition s x s': dec(intersection_transition s x s').
Proof. destruct s as [[? ?] [|]]; destruct s' as [[? ?] [|]]; auto. Qed.
Definition intersect := mknfa intersection_transition intersection_initial intersection_final.
Lemma between_final_state_intersect_is_final_state_aut_1 (r: Run intersect) w n m: valid_run r w -> final_state (r n) -> final_state (r m) -> n < m -> exists k, n <= k <= m /\ final_state (fst (fst (r k))).
Proof.
intros V Fn Fm L. decide (exists k , k <= m /\ n <= k /\ final_state (fst (fst (r k)))) as [[k [L1 [L2 F]]] | D].
- exists k. tauto.
- exfalso. enough (forall i, n < i <= m -> (snd (r ( i))) = false) as H.
+ enough (snd (r m) = true) as H'.
* now rewrite (H ( m)) in H' by omega.
* destruct (r m) as [[? ?][|]]; cbn in *; auto.
+ intros i [L' L'']. clear L. induction L' as [| i].
* specialize (V n). destruct (r n) as [[? ?] [|]] eqn:E; destruct (r (S n)) as [[? ?] [|]] eqn:E'; cbn in *; try tauto.
* specialize (V i). destruct (r i) as [[? ?] [|]] eqn:E; destruct (r (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: L_B intersect <$= L_B aut_1.
Proof.
intros w [r [V [I F]]]. exists (seq_map (fun v => fst (fst v)) r). unfold seq_map. repeat split.
- intros n. specialize (V n). destruct (r n) as [[? ?] [|]]; destruct (r (S n)) as [[? ?][|]]; cbn in *; tauto.
- unfold initial in *. destruct (r 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_final_state_intersect_is_final_state_aut_1 V (n := m1) (m := m2)) as [k [L Fk]]; oauto.
exists k. split; oauto.
Qed.
Lemma intersect_incl_aut2: L_B intersect <$= L_B aut_2.
Proof.
intros w [r [V [I F]]]. exists (seq_map (fun v => snd (fst v)) r). unfold seq_map. repeat split.
- intros n. specialize (V n). destruct (r n) as [[? ?] [|]]; destruct (r (S n)) as [[? ?][|]]; cbn in *; tauto.
- unfold initial in *. destruct (r 0) as [[? ?] [|]]; cbn in *; tauto.
- intros n. destruct (F n) as [m [L F']].
exists m. split; auto. destruct (r m) as [[q1 q2] [|]]; cbn in *; auto. now exfalso.
Qed.
Fixpoint irun (r_1:Run aut_1) (r_2: Run aut_2) n: (state intersect) := match n with
| 0 => ((r_1 0),(r_2 0), false)
| S n => match (irun r_1 r_2 n) with
| (_,_,true) => (r_1 (S n), r_2 (S n), if (decision (final_state (r_2 n))) then false else true)
| (_,_,false) => (r_1 (S n), r_2 (S n), if (decision (final_state (r_1 n))) then true else false)
end end.
Section IRun.
Variables (w: Seq X)(r_1 : Run aut_1) (r_2: Run aut_2).
Lemma irun_valid: valid_run r_1 w -> valid_run r_2 w -> valid_run (irun r_1 r_2) w .
Proof.
intros V1 V2 n. induction n.
- specialize (V1 0). specialize (V2 0). cbn in *. repeat split; auto; destruct decision; congruence.
- specialize (V1 (S n)). specialize (V2 (S n)). cbn in *. destruct (irun r_1 r_2 n)as [[? ?][|]]; cbn in *;
destruct decision; destruct decision; auto; repeat split; congruence.
Qed.
Lemma irun_initial: initial r_1 -> initial r_2 -> initial (irun r_1 r_2).
Proof.
intros I1 I2. unfold initial in *. cbn. tauto.
Qed.
Variables (F1: final r_1) (F2: final r_2).
Lemma irun_step_to_true n : snd(irun r_1 r_2 n) = false -> exists m, m > n /\ snd (irun r_1 r_2 m) = true.
Proof.
intros F. exists (S (next_position_exists (F1 n))). split.
- pose (next_position_exists_increasing (F1 n)). omega.
- enough (forall k, n <= k <= (next_position_exists (F1 n)) -> snd (irun r_1 r_2 k) = false) as H.
+ destruct (irun r_1 r_2 (next_position_exists (F1 n))) as [[? ?][|]] eqn:E.
* exfalso. specialize (H (next_position_exists (F1 n))).
rewrite E in H. cbn in H. enough (true = false) by congruence. apply H.
pose (next_position_exists_increasing (F1 n)). omega.
* cbn. rewrite E. destruct decision as [D|D]; cbn; auto.
exfalso. apply D. apply next_position_exists_correct.
+ intros k. intros [L1 L2]. induction L1; auto.
cbn in *. destruct (irun r_1 r_2 m) as [[? ?][|]] eqn :H.
* exfalso. cbn in IHL1. enough (true =false ) by congruence. apply IHL1. omega.
* destruct decision as [D|D]; auto.
exfalso. apply (next_position_exists_all (L:= F1 n) (k:=m)); oauto.
Qed.
Lemma irun_same_states n : fst (irun r_1 r_2 n) = (r_1 n, r_2 n).
Proof.
induction n; auto. cbn.
destruct (irun r_1 r_2 n) as [[? ?] [|]]; auto.
Qed.
Lemma irun_step_final n : snd(irun r_1 r_2 n) = true -> exists m, m >= n /\ final_state (irun r_1 r_2 m).
Proof.
intros F. exists (next_position_exists (F2 n)). split.
- pose (next_position_exists_increasing (F2 n)). omega.
- enough (forall k, n <= k <= (next_position_exists (F2 n)) -> snd (irun r_1 r_2 k) = true) as H.
+ destruct (irun r_1 r_2 (next_position_exists (F2 n))) as [[? s2][|]] eqn:E.
* cbn. enough (s2 = r_2 (next_position_exists (F2 n))) as -> by apply next_position_exists_correct.
pose (H' := irun_same_states (next_position_exists (F2 n))). rewrite E in H'. cbn in H'. congruence.
* exfalso. specialize (H (next_position_exists (F2 n))). rewrite E in H. cbn in H.
enough (false = true) by congruence. apply H. pose (next_position_exists_increasing (F2 n)). omega.
+ intros k [L1 L2]. induction L1; auto.
cbn in *. destruct (irun r_1 r_2 m) as [[? ?][|]] eqn :H.
* destruct decision as [D|D]; auto.
exfalso. apply (next_position_exists_all (L:= F2 n) (k:=m)); oauto.
* exfalso. cbn in IHL1. enough (false = true) by congruence. apply IHL1. omega.
Qed.
Lemma irun_final: final (irun r_1 r_2).
Proof.
intros n. destruct (snd (irun r_1 r_2 n)) eqn:H.
- now apply irun_step_final.
- apply irun_step_to_true in H. destruct H as [n' [G T]].
apply irun_step_final 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 [[r_1 [V1 [I1 F1]]] [r_2 [V2 [I2 F2]]]].
exists (irun r_1 r_2). split; [|split].
- now apply irun_valid.
- now apply irun_initial.
- now apply irun_final.
Qed.
Lemma intersect_correct: L_B intersect =$= L_B aut_1 /$\ L_B aut_2.
Proof.
intros w. split.
- intros A. split; [now apply intersect_incl_aut1 | now apply intersect_incl_aut2].
- apply intersection_incl_intersect.
Qed.
End IntersectionClosure.
Context (X:finType).
Variables (aut_1 aut_2 : NFA X).
Definition intersection_state := state aut_1 (x) state aut_2 (x) finType_bool.
Implicit Types (x:X)(s: intersection_state)(w:Seq X).
Definition intersection_initial s := match s with
| (s_1, s_2, _) => initial_state s_1 /\ initial_state s_2
end.
Definition intersection_final s := match s with
| (_, s_2 , true) => final_state s_2
| _ => False
end.
Definition intersection_transition s x s' := match s,s' with
| (s_1, s_2, true), (s_1',s_2',b) =>
(transition s_1 x s_1') /\ (transition s_2 x s_2') /\
(b = false <-> final_state s_2)
| (s_1, s_2, false), (s_1',s_2',b) =>
(transition s_1 x s_1') /\ (transition s_2 x s_2') /\
(b = true <-> final_state s_1)
end.
Instance dec_intersection_initial s : dec(intersection_initial s).
Proof. destruct s as [[? ?] ?]; auto. Qed.
Instance dec_intersection_final s : dec (intersection_final s).
Proof. destruct s as [[? ?] [|]]; auto. Qed.
Instance dec_intersection_transition s x s': dec(intersection_transition s x s').
Proof. destruct s as [[? ?] [|]]; destruct s' as [[? ?] [|]]; auto. Qed.
Definition intersect := mknfa intersection_transition intersection_initial intersection_final.
Lemma between_final_state_intersect_is_final_state_aut_1 (r: Run intersect) w n m: valid_run r w -> final_state (r n) -> final_state (r m) -> n < m -> exists k, n <= k <= m /\ final_state (fst (fst (r k))).
Proof.
intros V Fn Fm L. decide (exists k , k <= m /\ n <= k /\ final_state (fst (fst (r k)))) as [[k [L1 [L2 F]]] | D].
- exists k. tauto.
- exfalso. enough (forall i, n < i <= m -> (snd (r ( i))) = false) as H.
+ enough (snd (r m) = true) as H'.
* now rewrite (H ( m)) in H' by omega.
* destruct (r m) as [[? ?][|]]; cbn in *; auto.
+ intros i [L' L'']. clear L. induction L' as [| i].
* specialize (V n). destruct (r n) as [[? ?] [|]] eqn:E; destruct (r (S n)) as [[? ?] [|]] eqn:E'; cbn in *; try tauto.
* specialize (V i). destruct (r i) as [[? ?] [|]] eqn:E; destruct (r (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: L_B intersect <$= L_B aut_1.
Proof.
intros w [r [V [I F]]]. exists (seq_map (fun v => fst (fst v)) r). unfold seq_map. repeat split.
- intros n. specialize (V n). destruct (r n) as [[? ?] [|]]; destruct (r (S n)) as [[? ?][|]]; cbn in *; tauto.
- unfold initial in *. destruct (r 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_final_state_intersect_is_final_state_aut_1 V (n := m1) (m := m2)) as [k [L Fk]]; oauto.
exists k. split; oauto.
Qed.
Lemma intersect_incl_aut2: L_B intersect <$= L_B aut_2.
Proof.
intros w [r [V [I F]]]. exists (seq_map (fun v => snd (fst v)) r). unfold seq_map. repeat split.
- intros n. specialize (V n). destruct (r n) as [[? ?] [|]]; destruct (r (S n)) as [[? ?][|]]; cbn in *; tauto.
- unfold initial in *. destruct (r 0) as [[? ?] [|]]; cbn in *; tauto.
- intros n. destruct (F n) as [m [L F']].
exists m. split; auto. destruct (r m) as [[q1 q2] [|]]; cbn in *; auto. now exfalso.
Qed.
Fixpoint irun (r_1:Run aut_1) (r_2: Run aut_2) n: (state intersect) := match n with
| 0 => ((r_1 0),(r_2 0), false)
| S n => match (irun r_1 r_2 n) with
| (_,_,true) => (r_1 (S n), r_2 (S n), if (decision (final_state (r_2 n))) then false else true)
| (_,_,false) => (r_1 (S n), r_2 (S n), if (decision (final_state (r_1 n))) then true else false)
end end.
Section IRun.
Variables (w: Seq X)(r_1 : Run aut_1) (r_2: Run aut_2).
Lemma irun_valid: valid_run r_1 w -> valid_run r_2 w -> valid_run (irun r_1 r_2) w .
Proof.
intros V1 V2 n. induction n.
- specialize (V1 0). specialize (V2 0). cbn in *. repeat split; auto; destruct decision; congruence.
- specialize (V1 (S n)). specialize (V2 (S n)). cbn in *. destruct (irun r_1 r_2 n)as [[? ?][|]]; cbn in *;
destruct decision; destruct decision; auto; repeat split; congruence.
Qed.
Lemma irun_initial: initial r_1 -> initial r_2 -> initial (irun r_1 r_2).
Proof.
intros I1 I2. unfold initial in *. cbn. tauto.
Qed.
Variables (F1: final r_1) (F2: final r_2).
Lemma irun_step_to_true n : snd(irun r_1 r_2 n) = false -> exists m, m > n /\ snd (irun r_1 r_2 m) = true.
Proof.
intros F. exists (S (next_position_exists (F1 n))). split.
- pose (next_position_exists_increasing (F1 n)). omega.
- enough (forall k, n <= k <= (next_position_exists (F1 n)) -> snd (irun r_1 r_2 k) = false) as H.
+ destruct (irun r_1 r_2 (next_position_exists (F1 n))) as [[? ?][|]] eqn:E.
* exfalso. specialize (H (next_position_exists (F1 n))).
rewrite E in H. cbn in H. enough (true = false) by congruence. apply H.
pose (next_position_exists_increasing (F1 n)). omega.
* cbn. rewrite E. destruct decision as [D|D]; cbn; auto.
exfalso. apply D. apply next_position_exists_correct.
+ intros k. intros [L1 L2]. induction L1; auto.
cbn in *. destruct (irun r_1 r_2 m) as [[? ?][|]] eqn :H.
* exfalso. cbn in IHL1. enough (true =false ) by congruence. apply IHL1. omega.
* destruct decision as [D|D]; auto.
exfalso. apply (next_position_exists_all (L:= F1 n) (k:=m)); oauto.
Qed.
Lemma irun_same_states n : fst (irun r_1 r_2 n) = (r_1 n, r_2 n).
Proof.
induction n; auto. cbn.
destruct (irun r_1 r_2 n) as [[? ?] [|]]; auto.
Qed.
Lemma irun_step_final n : snd(irun r_1 r_2 n) = true -> exists m, m >= n /\ final_state (irun r_1 r_2 m).
Proof.
intros F. exists (next_position_exists (F2 n)). split.
- pose (next_position_exists_increasing (F2 n)). omega.
- enough (forall k, n <= k <= (next_position_exists (F2 n)) -> snd (irun r_1 r_2 k) = true) as H.
+ destruct (irun r_1 r_2 (next_position_exists (F2 n))) as [[? s2][|]] eqn:E.
* cbn. enough (s2 = r_2 (next_position_exists (F2 n))) as -> by apply next_position_exists_correct.
pose (H' := irun_same_states (next_position_exists (F2 n))). rewrite E in H'. cbn in H'. congruence.
* exfalso. specialize (H (next_position_exists (F2 n))). rewrite E in H. cbn in H.
enough (false = true) by congruence. apply H. pose (next_position_exists_increasing (F2 n)). omega.
+ intros k [L1 L2]. induction L1; auto.
cbn in *. destruct (irun r_1 r_2 m) as [[? ?][|]] eqn :H.
* destruct decision as [D|D]; auto.
exfalso. apply (next_position_exists_all (L:= F2 n) (k:=m)); oauto.
* exfalso. cbn in IHL1. enough (false = true) by congruence. apply IHL1. omega.
Qed.
Lemma irun_final: final (irun r_1 r_2).
Proof.
intros n. destruct (snd (irun r_1 r_2 n)) eqn:H.
- now apply irun_step_final.
- apply irun_step_to_true in H. destruct H as [n' [G T]].
apply irun_step_final 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 [[r_1 [V1 [I1 F1]]] [r_2 [V2 [I2 F2]]]].
exists (irun r_1 r_2). split; [|split].
- now apply irun_valid.
- now apply irun_initial.
- now apply irun_final.
Qed.
Lemma intersect_correct: L_B intersect =$= L_B aut_1 /$\ L_B aut_2.
Proof.
intros w. split.
- intros A. split; [now apply intersect_incl_aut1 | now apply intersect_incl_aut2].
- apply intersection_incl_intersect.
Qed.
End IntersectionClosure.
Union and Intersection of Finitely Many NFAs
Definition big_union (A:finType) (l:list (NFA A)) := fold_right union empty_aut l.
Lemma big_union_correct (A:finType) (l:list (NFA A)):
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.
Definition big_intersection (A:finType) (l:list (NFA A)) := fold_right (intersect (X:=A)) univ_aut l.
Lemma big_intersection_correct (A:finType) (l:list (NFA A)):
L_B (big_intersection l) =$= fun w => forall a, (a el l) -> L_B a w.
Proof.
intros w. split.
- intros I a L. induction l.
+ now exfalso.
+ cbn in I. apply intersect_correct in I. destruct I as [I1 I2].
destruct L.
* now subst a.
* now apply IHl.
- intros I. induction l.
+ cbn. now apply univ_aut_correct.
+ cbn. apply intersect_correct. split.
* now apply I.
* apply IHl. auto.
Qed.
Section NFAOmegaIteration.
Context {X:finType}.
Section OmegaIterNormalized.
Variable (aut: NFA X).
Variables (initialW finalW : state aut).
Variable (normW: sautomaton_normalized initialW finalW).
Definition oiter_transition s a s' := (s' <> initialW /\ transition s a s') \/ (s' = initialW /\ transition s a finalW).
Definition nfa_omega_iter' := mknfa oiter_transition (fun s => s = initialW) (fun s => s = initialW).
Lemma nfa_omega_iter'_accepts_aut: (L_S aut)^00 <$= L_B nfa_omega_iter'.
Proof.
intros w W.
destruct W as [ws [W C]].
pose (R:= fun (n:nat) => mkstring ( fun k =>(proj1_sig (nfa_string_lang_cc (W n))) k) (|ws n|) : String (state nfa_omega_iter')).
exists (concat_inf R).
repeat split.
- rewrite C. apply concat_inf_is_valid. repeat split.
+ intros k L. left. unfold R. destruct (nfa_string_lang_cc (W n)) as [r [Vn [In Fn]]]. cbn. split.
* specialize (Vn k L). decide (r (S k) = initialW) as [D|D]; auto.
exfalso. rewrite D in Vn. now apply normW in Vn.
* now apply Vn.
+ right. unfold R. destruct (nfa_string_lang_cc (W n)) as [r [V [I F]]]; destruct (nfa_string_lang_cc (W (S n))) as [r' [V' [I' F']]]. cbn. split.
* now apply normW in I'.
* apply normW in F. rewrite <-F. now apply V.
- cbn. destruct (nfa_string_lang_cc (W 0)) as [r [V [I F]]]. cbn.
apply normW in I. now rewrite I.
- intros n. exists (begin_in R n). split.
+ apply s_monotone_ge, s_monotone_begin_in.
+ unfold concat_inf. rewrite concat_inf_index_begin. cbn.
destruct (nfa_string_lang_cc (W n)) as [r [V [I F]]]. cbn.
now apply normW in I.
Qed.
Lemma initialW_partitions_in_W r w n m: accepting (aut:=nfa_omega_iter') r w
-> n < m -> r n = initialW -> r m = initialW
-> (forall k, n < k < m -> r k <> initialW )
-> (L_S aut) (extract n m w).
Proof.
intros [V [I F]] L nW mW kNW.
exists ((extract n m r) +++ (fun _ => finalW)).
repeat split.
- intros k B. simpl.
decide (k < m - S n).
+ rewrite 2prepend_string_begin by comega. cbn.
repeat rewrite drop_correct. rewrite_eq (n + S k = S(n+k)).
specialize (V (n + k)). simpl in V. unfold oiter_transition in V.
enough (r (S (n + k)) <> initialW) by tauto. apply kNW. omega.
+ cbn in B.
rewrite prepend_string_begin by comega.
rewrite prepend_string_rest by comega. cbn.
rewrite 2drop_correct.
specialize (V (n + k)). simpl in V. unfold oiter_transition in V.
enough (r (S (n + k)) = initialW) by tauto.
rewrite <-mW. f_equal. omega.
- unfold sinitial. rewrite prepend_string_begin by comega. cbn.
rewrite drop_correct. rewrite_eq ( (n + 0) = n).
rewrite nW. apply normW.
- unfold sfinal. simpl.
rewrite prepend_string_rest by comega.
apply normW.
Qed.
Arguments infinite_filter [X] _ _ _ _ _.
Lemma aut_accepts_nfa_omega_iter': L_B nfa_omega_iter' <$= (L_S aut)^00.
Proof.
intros w [r A].
pose (A' := A). destruct A' as [V [I Fin]].
apply lang_o_iter_extract.
exists (infinite_filter r (fun s => s = initialW) (fun s=> decision (s = initialW)) Fin). repeat split.
- apply infinite_filter_s_monotone.
- apply infinite_filter_zero, I.
- intros n. apply (initialW_partitions_in_W A).
+ apply infinite_filter_s_monotone.
+ apply infinite_filter_correct.
+ apply infinite_filter_correct.
+ apply infinite_filter_all.
Qed.
Lemma nfa_omega_iter'_correct: L_B nfa_omega_iter' =$= (L_S aut)^00.
Proof.
split. apply aut_accepts_nfa_omega_iter'. apply nfa_omega_iter'_accepts_aut.
Qed.
End OmegaIterNormalized.
Definition nfa_omega_iter aut := nfa_omega_iter' (normalize_inital aut) (normalize_final aut).
Lemma nfa_omega_iter_correct aut: L_B (nfa_omega_iter aut) =$= (L_S aut)^00.
Proof.
unfold nfa_omega_iter. rewrite nfa_omega_iter'_correct, <-normalize_correct.
reflexivity. apply normalize_is_normalized.
Qed.
End NFAOmegaIteration.
Context {X:finType}.
Section OmegaIterNormalized.
Variable (aut: NFA X).
Variables (initialW finalW : state aut).
Variable (normW: sautomaton_normalized initialW finalW).
Definition oiter_transition s a s' := (s' <> initialW /\ transition s a s') \/ (s' = initialW /\ transition s a finalW).
Definition nfa_omega_iter' := mknfa oiter_transition (fun s => s = initialW) (fun s => s = initialW).
Lemma nfa_omega_iter'_accepts_aut: (L_S aut)^00 <$= L_B nfa_omega_iter'.
Proof.
intros w W.
destruct W as [ws [W C]].
pose (R:= fun (n:nat) => mkstring ( fun k =>(proj1_sig (nfa_string_lang_cc (W n))) k) (|ws n|) : String (state nfa_omega_iter')).
exists (concat_inf R).
repeat split.
- rewrite C. apply concat_inf_is_valid. repeat split.
+ intros k L. left. unfold R. destruct (nfa_string_lang_cc (W n)) as [r [Vn [In Fn]]]. cbn. split.
* specialize (Vn k L). decide (r (S k) = initialW) as [D|D]; auto.
exfalso. rewrite D in Vn. now apply normW in Vn.
* now apply Vn.
+ right. unfold R. destruct (nfa_string_lang_cc (W n)) as [r [V [I F]]]; destruct (nfa_string_lang_cc (W (S n))) as [r' [V' [I' F']]]. cbn. split.
* now apply normW in I'.
* apply normW in F. rewrite <-F. now apply V.
- cbn. destruct (nfa_string_lang_cc (W 0)) as [r [V [I F]]]. cbn.
apply normW in I. now rewrite I.
- intros n. exists (begin_in R n). split.
+ apply s_monotone_ge, s_monotone_begin_in.
+ unfold concat_inf. rewrite concat_inf_index_begin. cbn.
destruct (nfa_string_lang_cc (W n)) as [r [V [I F]]]. cbn.
now apply normW in I.
Qed.
Lemma initialW_partitions_in_W r w n m: accepting (aut:=nfa_omega_iter') r w
-> n < m -> r n = initialW -> r m = initialW
-> (forall k, n < k < m -> r k <> initialW )
-> (L_S aut) (extract n m w).
Proof.
intros [V [I F]] L nW mW kNW.
exists ((extract n m r) +++ (fun _ => finalW)).
repeat split.
- intros k B. simpl.
decide (k < m - S n).
+ rewrite 2prepend_string_begin by comega. cbn.
repeat rewrite drop_correct. rewrite_eq (n + S k = S(n+k)).
specialize (V (n + k)). simpl in V. unfold oiter_transition in V.
enough (r (S (n + k)) <> initialW) by tauto. apply kNW. omega.
+ cbn in B.
rewrite prepend_string_begin by comega.
rewrite prepend_string_rest by comega. cbn.
rewrite 2drop_correct.
specialize (V (n + k)). simpl in V. unfold oiter_transition in V.
enough (r (S (n + k)) = initialW) by tauto.
rewrite <-mW. f_equal. omega.
- unfold sinitial. rewrite prepend_string_begin by comega. cbn.
rewrite drop_correct. rewrite_eq ( (n + 0) = n).
rewrite nW. apply normW.
- unfold sfinal. simpl.
rewrite prepend_string_rest by comega.
apply normW.
Qed.
Arguments infinite_filter [X] _ _ _ _ _.
Lemma aut_accepts_nfa_omega_iter': L_B nfa_omega_iter' <$= (L_S aut)^00.
Proof.
intros w [r A].
pose (A' := A). destruct A' as [V [I Fin]].
apply lang_o_iter_extract.
exists (infinite_filter r (fun s => s = initialW) (fun s=> decision (s = initialW)) Fin). repeat split.
- apply infinite_filter_s_monotone.
- apply infinite_filter_zero, I.
- intros n. apply (initialW_partitions_in_W A).
+ apply infinite_filter_s_monotone.
+ apply infinite_filter_correct.
+ apply infinite_filter_correct.
+ apply infinite_filter_all.
Qed.
Lemma nfa_omega_iter'_correct: L_B nfa_omega_iter' =$= (L_S aut)^00.
Proof.
split. apply aut_accepts_nfa_omega_iter'. apply nfa_omega_iter'_accepts_aut.
Qed.
End OmegaIterNormalized.
Definition nfa_omega_iter aut := nfa_omega_iter' (normalize_inital aut) (normalize_final aut).
Lemma nfa_omega_iter_correct aut: L_B (nfa_omega_iter aut) =$= (L_S aut)^00.
Proof.
unfold nfa_omega_iter. rewrite nfa_omega_iter'_correct, <-normalize_correct.
reflexivity. apply normalize_is_normalized.
Qed.
End NFAOmegaIteration.
Section PrependNFA.
Context {X:finType}.
Section PrependNormalizedNFA.
Variable (aut_1 aut_2: NFA X).
Variables (initialV finalV : state aut_1).
Variable (norm: sautomaton_normalized initialV finalV).
Definition prepend_state := (state aut_1) (x) (state aut_2).
Implicit Types (s: prepend_state)(x:X).
Definition prepend_transition s x s' := match s,s' with
| (p, q) , (p',q') => (~ final_state p -> transition p x p' /\ initial_state q') /\
( final_state p -> transition q x q' /\ p' = finalV)
end.
Definition prepend_state_final s := match s with (p, q) => final_state p /\ final_state q end.
Definition prepend_state_initial s := match s with (p,q) => p = initialV /\ initial_state q end.
Instance dec_prepend_transition s x s': dec (prepend_transition s x s'). Proof. destruct s,s'; simpl; auto. Qed.
Instance dec_prepend_state_final s : dec (prepend_state_final s). Proof. destruct s; auto. Qed.
Instance dev_prepend_state_initial s : dec (prepend_state_initial s). Proof. destruct s; auto. Qed.
Definition prepend_nfa' := mknfa prepend_transition prepend_state_initial prepend_state_final.
Arguments can_find_next_position [X] _ _ [w] [n] [m] _ _.
Definition activeW (s:prepend_state) := match s with (q, _) => final_state q end.
Instance decActivW s: dec (activeW s). Proof. destruct s. auto. Qed.
Lemma switch_from_V_to_W r w : accepting (aut:=prepend_nfa') r w -> Sigma k, k > 0 /\ (forall n, n < k -> ~ activeW (r n)) /\ (forall n, activeW (r (n + k))).
Proof.
intros [V [I F]].
assert (exists n, 0 <= n /\ activeW (r n)) as H. { destruct (F 0) as [n [P Q]]. exists n. split; auto. destruct (r n). apply Q. }
exists (next_position_exists H). repeat split.
- decide (next_position_exists H > 0); auto. exfalso.
assert (next_position_exists H = 0) as H' by omega.
pose proof (next_position_exists_correct H) as Q. rewrite H' in Q.
unfold initial in I. destruct (r 0). apply norm. cbn in *. rewrite <-(proj1 I). now apply norm in Q.
- intros n L. intros A. specialize (V n). destruct (r n) eqn:En. cbn in A.
apply (next_position_exists_all (n:=0) (k:=n) (L:=H)).
+ split; oauto.
+ now rewrite En.
- intros n. induction n.
+ cbn. pose proof (next_position_exists_correct H).
destruct (r (next_position_exists H)) eqn:H'. cbn in *. now rewrite H'.
+ remember (next_position_exists H) as k. specialize (V ( n +k)). cbn.
destruct (r (n+k)) as [s1 s2]. destruct (r (S (n +k))) as [s3 s4]. cbn in *.
enough (s3 = finalV) as H2.
* rewrite H2. apply norm.
* now apply V.
Qed.
Lemma prepend_aut_is_prepend_omega: L_B prepend_nfa' <$= L_S aut_1 o L_B aut_2.
Proof.
intros w [r A].
destruct (switch_from_V_to_W A) as [w_begin [G0 [AV AW]]].
apply split_position_lang_prepend. exists (pred w_begin). destruct A as [V [I F]].
split.
- exists (fun n => match (r n) with (q,_) => q end).
repeat split.
+ intros k L. simpl in L. specialize (V k). specialize (AV k).
destruct (r k), (r (S k)). apply V, AV. omega.
+ unfold sinitial. compute in I. destruct (r 0). destruct I as [I _]. rewrite I. apply norm.
+ unfold sfinal. cbn. specialize (AW 0).
rewrite_eq (S (pred w_begin) = w_begin). cbn in AW.
destruct (r w_begin). apply AW.
- exists (drop w_begin (fun n => match (r n) with (_,q) => q end)).
repeat split.
+ intros k. specialize (V (k + w_begin)). specialize (AW k).
rewrite_eq (S (pred w_begin) = w_begin). rewrite 3drop_correct'. cbn.
destruct (r (k + w_begin)). destruct (r (S (k + w_begin ))). apply V, AW.
+ unfold initial. rewrite drop_correct'. specialize (V (pred w_begin)).
rewrite_eq (S(pred w_begin) = w_begin) in V. cbn.
specialize (AV (pred w_begin)). destruct (r w_begin).
destruct (r (pred (w_begin))). cbn in V. apply V, AV. omega.
+ apply final_drop. intros n. destruct (F n) as [m [P Q]]. exists m. split; oauto.
destruct (r m). apply Q.
Qed.
Lemma prepend_aut_accepts_prepend_omega: L_S aut_1 o L_B aut_2 <$= L_B prepend_nfa'.
Proof.
intros w [v [w' [E [[rv [Vv [Iv Fv]]] [rw [Vw [Iw Fw]]]]]]]. rewrite E.
exists (mkstring (seq_zip rv (fun _ => rw 0)) (|v|) +++ (seq_zip (fun _ => finalV) rw)).
split; [|split].
- intros n. decide (n <= |v| ) as[D'|D'].
+ rewrite prepend_string_begin by comega.
decide (S n <= |v|) as [D|D].
* rewrite !prepend_string_begin by comega. cbn. split.
-- intros nF. split. apply Vv. comega. apply Iw.
-- intros F. exfalso. specialize (Vv n D'). apply norm in F. rewrite F in Vv. now apply norm in Vv.
* assert (n = |v|) by omega. subst n. rewrite prepend_string_begin, prepend_string_rest by comega. cbn. split.
-- intros nF. split.
++ unfold sfinal in Fv. cbn in Fv. apply norm in Fv. rewrite <-Fv. apply Vv. comega.
++ rewrite_eq (|v| - (|v|) = 0). apply Iw.
-- intros F. exfalso. specialize (Vv (|v|) D'). apply norm in F. rewrite F in Vv. now apply norm in Vv.
+ rewrite 3prepend_string_rest by comega. cbn. split.
* intros F. exfalso. apply F. apply norm.
* specialize (E (n )). rewrite prepend_string_rest in E by omega. rewrite <-E.
intros F. split; auto. specialize (Vw (n - S (|v|))).
rewrite <-E in Vw.
now rewrite_eq (S (n - S (|v|)) = n - (|v|)) in Vw.
- unfold initial. rewrite prepend_string_begin by omega. cbn. split.
apply norm, Iv. apply Iw.
- apply final_prepend. intros n. destruct (Fw n) as [m [P Q]]. exists m. repeat split; oauto. apply norm.
Qed.
Lemma prepend_nfa'_correct: L_B prepend_nfa' =$= L_S aut_1 o L_B aut_2.
Proof.
split. apply prepend_aut_is_prepend_omega. apply prepend_aut_accepts_prepend_omega.
Qed.
End PrependNormalizedNFA.
Definition prepend_nfa aut_1 aut_2 := prepend_nfa' aut_2 (normalize_inital aut_1) (normalize_final aut_1).
Lemma prepend_nfa_correct aut_1 aut_2 : L_B (prepend_nfa aut_1 aut_2) =$= (L_S aut_1) o (L_B aut_2).
Proof.
unfold prepend_nfa. rewrite prepend_nfa'_correct, <-normalize_correct.
reflexivity. apply normalize_is_normalized.
Qed.
End PrependNFA.
Section ConcatInfPrependNFA.
Context {X:finType}.
Context {aut: NFA X}.
Variable strings: Seq (String X).
Variable runs: Seq (String (state aut)).
Context {X:finType}.
Section PrependNormalizedNFA.
Variable (aut_1 aut_2: NFA X).
Variables (initialV finalV : state aut_1).
Variable (norm: sautomaton_normalized initialV finalV).
Definition prepend_state := (state aut_1) (x) (state aut_2).
Implicit Types (s: prepend_state)(x:X).
Definition prepend_transition s x s' := match s,s' with
| (p, q) , (p',q') => (~ final_state p -> transition p x p' /\ initial_state q') /\
( final_state p -> transition q x q' /\ p' = finalV)
end.
Definition prepend_state_final s := match s with (p, q) => final_state p /\ final_state q end.
Definition prepend_state_initial s := match s with (p,q) => p = initialV /\ initial_state q end.
Instance dec_prepend_transition s x s': dec (prepend_transition s x s'). Proof. destruct s,s'; simpl; auto. Qed.
Instance dec_prepend_state_final s : dec (prepend_state_final s). Proof. destruct s; auto. Qed.
Instance dev_prepend_state_initial s : dec (prepend_state_initial s). Proof. destruct s; auto. Qed.
Definition prepend_nfa' := mknfa prepend_transition prepend_state_initial prepend_state_final.
Arguments can_find_next_position [X] _ _ [w] [n] [m] _ _.
Definition activeW (s:prepend_state) := match s with (q, _) => final_state q end.
Instance decActivW s: dec (activeW s). Proof. destruct s. auto. Qed.
Lemma switch_from_V_to_W r w : accepting (aut:=prepend_nfa') r w -> Sigma k, k > 0 /\ (forall n, n < k -> ~ activeW (r n)) /\ (forall n, activeW (r (n + k))).
Proof.
intros [V [I F]].
assert (exists n, 0 <= n /\ activeW (r n)) as H. { destruct (F 0) as [n [P Q]]. exists n. split; auto. destruct (r n). apply Q. }
exists (next_position_exists H). repeat split.
- decide (next_position_exists H > 0); auto. exfalso.
assert (next_position_exists H = 0) as H' by omega.
pose proof (next_position_exists_correct H) as Q. rewrite H' in Q.
unfold initial in I. destruct (r 0). apply norm. cbn in *. rewrite <-(proj1 I). now apply norm in Q.
- intros n L. intros A. specialize (V n). destruct (r n) eqn:En. cbn in A.
apply (next_position_exists_all (n:=0) (k:=n) (L:=H)).
+ split; oauto.
+ now rewrite En.
- intros n. induction n.
+ cbn. pose proof (next_position_exists_correct H).
destruct (r (next_position_exists H)) eqn:H'. cbn in *. now rewrite H'.
+ remember (next_position_exists H) as k. specialize (V ( n +k)). cbn.
destruct (r (n+k)) as [s1 s2]. destruct (r (S (n +k))) as [s3 s4]. cbn in *.
enough (s3 = finalV) as H2.
* rewrite H2. apply norm.
* now apply V.
Qed.
Lemma prepend_aut_is_prepend_omega: L_B prepend_nfa' <$= L_S aut_1 o L_B aut_2.
Proof.
intros w [r A].
destruct (switch_from_V_to_W A) as [w_begin [G0 [AV AW]]].
apply split_position_lang_prepend. exists (pred w_begin). destruct A as [V [I F]].
split.
- exists (fun n => match (r n) with (q,_) => q end).
repeat split.
+ intros k L. simpl in L. specialize (V k). specialize (AV k).
destruct (r k), (r (S k)). apply V, AV. omega.
+ unfold sinitial. compute in I. destruct (r 0). destruct I as [I _]. rewrite I. apply norm.
+ unfold sfinal. cbn. specialize (AW 0).
rewrite_eq (S (pred w_begin) = w_begin). cbn in AW.
destruct (r w_begin). apply AW.
- exists (drop w_begin (fun n => match (r n) with (_,q) => q end)).
repeat split.
+ intros k. specialize (V (k + w_begin)). specialize (AW k).
rewrite_eq (S (pred w_begin) = w_begin). rewrite 3drop_correct'. cbn.
destruct (r (k + w_begin)). destruct (r (S (k + w_begin ))). apply V, AW.
+ unfold initial. rewrite drop_correct'. specialize (V (pred w_begin)).
rewrite_eq (S(pred w_begin) = w_begin) in V. cbn.
specialize (AV (pred w_begin)). destruct (r w_begin).
destruct (r (pred (w_begin))). cbn in V. apply V, AV. omega.
+ apply final_drop. intros n. destruct (F n) as [m [P Q]]. exists m. split; oauto.
destruct (r m). apply Q.
Qed.
Lemma prepend_aut_accepts_prepend_omega: L_S aut_1 o L_B aut_2 <$= L_B prepend_nfa'.
Proof.
intros w [v [w' [E [[rv [Vv [Iv Fv]]] [rw [Vw [Iw Fw]]]]]]]. rewrite E.
exists (mkstring (seq_zip rv (fun _ => rw 0)) (|v|) +++ (seq_zip (fun _ => finalV) rw)).
split; [|split].
- intros n. decide (n <= |v| ) as[D'|D'].
+ rewrite prepend_string_begin by comega.
decide (S n <= |v|) as [D|D].
* rewrite !prepend_string_begin by comega. cbn. split.
-- intros nF. split. apply Vv. comega. apply Iw.
-- intros F. exfalso. specialize (Vv n D'). apply norm in F. rewrite F in Vv. now apply norm in Vv.
* assert (n = |v|) by omega. subst n. rewrite prepend_string_begin, prepend_string_rest by comega. cbn. split.
-- intros nF. split.
++ unfold sfinal in Fv. cbn in Fv. apply norm in Fv. rewrite <-Fv. apply Vv. comega.
++ rewrite_eq (|v| - (|v|) = 0). apply Iw.
-- intros F. exfalso. specialize (Vv (|v|) D'). apply norm in F. rewrite F in Vv. now apply norm in Vv.
+ rewrite 3prepend_string_rest by comega. cbn. split.
* intros F. exfalso. apply F. apply norm.
* specialize (E (n )). rewrite prepend_string_rest in E by omega. rewrite <-E.
intros F. split; auto. specialize (Vw (n - S (|v|))).
rewrite <-E in Vw.
now rewrite_eq (S (n - S (|v|)) = n - (|v|)) in Vw.
- unfold initial. rewrite prepend_string_begin by omega. cbn. split.
apply norm, Iv. apply Iw.
- apply final_prepend. intros n. destruct (Fw n) as [m [P Q]]. exists m. repeat split; oauto. apply norm.
Qed.
Lemma prepend_nfa'_correct: L_B prepend_nfa' =$= L_S aut_1 o L_B aut_2.
Proof.
split. apply prepend_aut_is_prepend_omega. apply prepend_aut_accepts_prepend_omega.
Qed.
End PrependNormalizedNFA.
Definition prepend_nfa aut_1 aut_2 := prepend_nfa' aut_2 (normalize_inital aut_1) (normalize_final aut_1).
Lemma prepend_nfa_correct aut_1 aut_2 : L_B (prepend_nfa aut_1 aut_2) =$= (L_S aut_1) o (L_B aut_2).
Proof.
unfold prepend_nfa. rewrite prepend_nfa'_correct, <-normalize_correct.
reflexivity. apply normalize_is_normalized.
Qed.
End PrependNFA.
Section ConcatInfPrependNFA.
Context {X:finType}.
Context {aut: NFA X}.
Variable strings: Seq (String X).
Variable runs: Seq (String (state aut)).
Facts showing that Composing the Sequence carry over to the Run
If the sequence is obtained by prepending, we can split the run accordingly.
Lemma partition_run_on_prepend_string w0 w r : valid_run (aut:=aut) r (w0 +++ w) ->
exists r0 r', (r0 +++ r') === r /\ (|r0| = |w0|) /\ (r0 [S(|r0|)] = r' 0) /\ valid_path (seq r0) w0 /\ valid_run r' w.
Proof.
intros V.
exists (mkstring r (|w0|)); exists (drop (S(|w0|)) r). repeat split.
- now rewrite revert_drop.
- cbn. rewrite drop_correct. f_equal. omega.
- assert (w0 == mkstring (w0 +++w) (|w0|)) as H. { split;cbn;oauto. intros n L. now rewrite prepend_string_begin. }
rewrite H. now apply valid_run_is_path_from_begin.
- rewrite <-revert_prepend_string with (v:= w0). now apply valid_run_drop.
Qed.
exists r0 r', (r0 +++ r') === r /\ (|r0| = |w0|) /\ (r0 [S(|r0|)] = r' 0) /\ valid_path (seq r0) w0 /\ valid_run r' w.
Proof.
intros V.
exists (mkstring r (|w0|)); exists (drop (S(|w0|)) r). repeat split.
- now rewrite revert_drop.
- cbn. rewrite drop_correct. f_equal. omega.
- assert (w0 == mkstring (w0 +++w) (|w0|)) as H. { split;cbn;oauto. intros n L. now rewrite prepend_string_begin. }
rewrite H. now apply valid_run_is_path_from_begin.
- rewrite <-revert_prepend_string with (v:= w0). now apply valid_run_drop.
Qed.
Likewise, if the sequence was obtained by infinite concattenation, the run can be partitioned
into infinitely many strings
Lemma partition_run_on_concat_inf W r : valid_run (aut:=aut) r (concat_inf W) ->
exists R, concat_inf R === r /\
(forall k, |R k| = |W k| /\ valid_path (seq (R k)) (W k)) /\
(forall k, (R k)[ S(|R k|)] = (R (S k)) [0]) .
Proof.
intros V.
exists (fun n => extract (begin_in W n) (begin_in W (S n)) r). repeat split.
- intros n.
unfold concat_inf.
destruct (concat_inf_indices) as [w i] eqn:H.
simpl. rewrite drop_correct.
apply concat_inf_index_to_begin in H. destruct H as [H _].
rewrite H. f_equal. f_equal. apply begin_in_equal. intros k. comega.
- comega.
- cbn. intros n L.
rewrite 2drop_correct', <-concat_inf_correct by auto. cbn. apply V.
- intros k. cbn. rewrite 2drop_correct. f_equal. omega.
Qed.
End ConcatInfPrependNFA.
exists R, concat_inf R === r /\
(forall k, |R k| = |W k| /\ valid_path (seq (R k)) (W k)) /\
(forall k, (R k)[ S(|R k|)] = (R (S k)) [0]) .
Proof.
intros V.
exists (fun n => extract (begin_in W n) (begin_in W (S n)) r). repeat split.
- intros n.
unfold concat_inf.
destruct (concat_inf_indices) as [w i] eqn:H.
simpl. rewrite drop_correct.
apply concat_inf_index_to_begin in H. destruct H as [H _].
rewrite H. f_equal. f_equal. apply begin_in_equal. intros k. comega.
- comega.
- cbn. intros n L.
rewrite 2drop_correct', <-concat_inf_correct by auto. cbn. apply V.
- intros k. cbn. rewrite 2drop_correct. f_equal. omega.
Qed.
End ConcatInfPrependNFA.
Definition exact_up_nfa (X:finType) (u v : String X):= prepend_nfa (os_nfa u) (nfa_omega_iter (os_nfa v)).
Lemma exact_up_nfa_correct (X:finType) (u v : String X): L_B (exact_up_nfa u v) =$= fun w => w === u +++ v to_omega.
Proof.
unfold exact_up_nfa.
rewrite prepend_nfa_correct, nfa_omega_iter_correct, 2os_nfa_correct.
intros w. split.
- intros [u' [w' [E1 [E2 [w'' [E3 E4]]]]]].
now rewrite E1, E2, E4, (concat_inf_extensional E3).
- intros E. exists u, (v to_omega). repeat split; auto.
exists (fun _ => v). repeat split; auto.
Qed.
Lemma dec_up_in_lang (X: finType)(v w : String X) (A: NFA X): dec (L_B A (v+++w to_omega)).
Proof.
destruct (dec_language_empty_informative (intersect A (exact_up_nfa v w))) as [D|D].
- left. destruct D as [w' [L1 L2%exact_up_nfa_correct] % intersect_correct].
now rewrite <-L2.
- right. intros L.
apply (D (v +++ w to_omega)). apply intersect_correct. split.
+ apply L.
+ now apply exact_up_nfa_correct.
Qed.