Set Implicit Arguments.
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Require Import Ramsey.
Require Import NFAs.
Require Import Buechi.
Require Import Complement.
Open Scope list_scope.
Close Scope string_scope.
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Require Import Ramsey.
Require Import NFAs.
Require Import Buechi.
Require Import Complement.
Open Scope list_scope.
Close Scope string_scope.
Class SequenceStructure := mkSequenceStructure {
ASeq: finType -> Type;
aseq_to_seq: forall (X:finType), ASeq X -> Seq X;
azip: forall (X Y: finType), ASeq X -> ASeq Y -> ASeq (X (x) Y);
amap: forall (X Y:finType), (X -> Y) -> ASeq X -> ASeq Y;
exact_at: forall (X: finType), X -> X -> nat -> ASeq X;
azip_correct: forall (X Y: finType) (w:ASeq X) (w':ASeq Y),(aseq_to_seq (azip w w')) === seq_zip(aseq_to_seq w)(aseq_to_seq w');
amap_correct : forall (X Y: finType) (f: X -> Y) (w: ASeq X), aseq_to_seq (amap f w) === seq_map f (aseq_to_seq w);
exact_at_correct: forall (X:finType) (x y : X) (n : nat), x <> y -> forall m, aseq_to_seq (exact_at x y n) m = x <-> m = n
}.
Arguments ASeq {A} X : rename.
Arguments aseq_to_seq {A} {X} : rename.
Arguments azip {A}{X}{Y} : rename.
Arguments azip_correct {A}{X}{Y} w w': rename.
Arguments amap {A}{X}{Y}: rename.
Arguments amap_correct {A}{X}{Y}:rename.
Coercion aseq_to_seq: ASeq >-> Seq .
Identity Coercion applySeq: Seq >-> Funclass .
Section BigZip.
Context {CC: SequenceStructure}.
Definition aseq_equal (A: finType) : ASeq A -> ASeq A -> Prop := @seq_equal A.
Instance aseq_equal_equiv (A:finType): Equivalence (@aseq_equal A).
Proof.
repeat split; unfold aseq_equal.
- intros w w' E. symmetry. apply E.
- intros w1 w2 w3 E1 E2. now rewrite E1, <-E2.
Qed.
Instance amap_proper (A B:finType)(f: A-> B): Proper ((@aseq_equal A ) ==> (@aseq_equal B)) (amap f).
Proof.
intros w w' E n. rewrite !amap_correct. unfold seq_map. now rewrite E.
Qed.
Notation "w ==== w'" := (aseq_equal w w') (at level 71).
Lemma test (A B: finType) (w w': ASeq A) (f: A -> B) : w ==== w' -> (amap f w) ==== (amap f w').
Proof.
intros E. now rewrite E.
Qed.
Context{X:finType}{Y:finType}.
Implicit Types (x:X)(y:Y)(L:list Y).
Definition const (X:finType) (x:X) := amap (fun _ => x) (exact_at x x 0).
Lemma const_correct x: const x === fun _ => x.
Proof.
intros n. unfold const. now rewrite amap_correct.
Qed.
Definition zipFinTypes y L: (X * X^^L) -> X^^(y::L).
Proof.
intros [C V].
apply vectorise. intros [x P].
decide (x = y) as [<-|D].
- exact C.
- apply (applyVect V). exists x. apply pure_equiv in P. destruct P as [P|P].
+ exfalso. auto.
+ now apply pure_equiv.
Defined.
Fixpoint bigzip' L (f: (finType_fromList L)-> ASeq X) {struct L}: ASeq (X^^L).
Proof.
destruct L as [| y L].
- apply const. apply vectorise. intros [x P]. exfalso. now apply pure_equiv in P.
-apply (amap (@zipFinTypes y L)).
apply azip.
+ apply f. exists y. apply pure_equiv. now left.
+ apply bigzip'. intros [x P]. apply f. exists x. apply pure_equiv. right. now apply pure_equiv in P.
Defined.
Definition elemToFinType : X^^(elem Y) -> X^Y.
Proof.
intros Z. apply vectorise. intros i.
apply (applyVect Z). exists i. apply pure_equiv. auto.
Defined.
Definition bigzip (f: Y -> ASeq X): (ASeq (X^Y)).
Proof.
apply (amap elemToFinType). apply bigzip'.
intros [i _]. exact (f i).
Defined.
Lemma bigzip_correct' L (f: (finType_fromList L)-> ASeq X) (Z:finType_fromList L) n: applyVect ((bigzip' f) n) Z = (f Z) n.
Proof.
induction L as [|x L].
- exfalso. destruct Z as [x P]. now apply pure_equiv in P.
- cbn. rewrite amap_correct.
destruct Z as [z P].
unfold seq_map, zipFinTypes. cbn. rewrite azip_correct. unfold seq_zip.
rewrite apply_vectorise_inverse. destruct decision as [<- | D].
+ cbn. repeat f_equal. apply pure_eq.
+ rewrite IHL. repeat f_equal. apply pure_eq.
Qed.
Lemma bigzip_correct (f : Y -> ASeq X) y n: applyVect ((bigzip f) n) y = (f y) n.
Proof.
unfold bigzip. rewrite amap_correct. unfold seq_map, elemToFinType.
now rewrite apply_vectorise_inverse, bigzip_correct'.
Qed.
Definition bigpi : ASeq (X^Y) -> Y -> ASeq X.
Proof.
intros w i.
apply (amap (fun v => applyVect v i)). exact w.
Defined.
Lemma bigpi_correct (w: ASeq (X^Y)) y n : (bigpi w y) n = applyVect (w n) y.
Proof.
unfold bigpi. now rewrite amap_correct.
Qed.
End BigZip.
Notation "w ==== w'" := (aseq_equal w w') (at level 71).
Definition L_A {CC: SequenceStructure} (A:finType) (aut : NFA A) : Language (ASeq A) := fun w => L_B aut (aseq_to_seq w).
Definition LAmap {CC: SequenceStructure} (X Y :finType) (f: X->Y) (L : Language (ASeq X)) : Language (ASeq Y) := fun w => exists w', amap f w' ==== w /\ L w'.
Definition APreImage {CC: SequenceStructure} (X Y: finType) (f: X -> Y) (L: Language (ASeq Y )) : Language (ASeq X) := fun w => L (amap f w).
Notation "{[ V ]}" := (eqClass V) (at level 0).
Class AdmissibleSequenceStructure := mkAdmissibleSequenceStructure {
CC :> SequenceStructure;
dec_alanguage_empty_informative: forall (A: finType) (aut: NFA A), {exists w, L_A aut w} + {L_A aut =$= {}};
totality: forall (A:finType) (aut: NFA A) (w : ASeq A), exists (V W:EqClass(aut:=aut)), ({[V]}o({[W]})^00 )(aseq_to_seq w);
aseq_run: forall (A:finType) (aut: NFA A) (w: ASeq A), L_A aut w -> (exists (r: ASeq (state aut)), accepting (aseq_to_seq r) (aseq_to_seq w));
map_aut_acorrect : forall (X Y:finType) (f: X ->Y) (aut: NFA X) , L_A (image_aut f aut) =$= LAmap f (L_A aut)
}.
Section ClosureProperties.
Variable (AC: AdmissibleSequenceStructure).
Variable (X Y: finType).
Lemma empty_aut_acorrect: L_A (empty_aut (X:=X)) =$= {}.
Proof.
intros a. split; intros B; exfalso.
- now apply empty_aut_correct in B.
- assumption.
Qed.
Lemma preimage_aut_acorrect (f: X-> Y) (aut: NFA Y): L_A (preimage_aut f aut) =$= APreImage f (L_A aut).
Proof.
split.
- intros LA. apply preimage_aut_correct in LA. unfold APreImage,L_A. now rewrite amap_correct.
- intros LA. unfold L_A, APreImage in *. apply preimage_aut_correct.
now rewrite amap_correct in LA.
Qed.
Lemma union_acorrect (aut_1 aut_2 :NFA X): L_A (union aut_1 aut_2) =$= L_A aut_1 \$/ L_A aut_2.
Proof.
intros w. split; eauto using union_correct.
- intros [B|B] % union_correct; [now left | now right].
- intros [B|B]; apply union_correct; [now left| now right].
Qed.
Lemma intersect_acorrect (aut_1 aut_2 :NFA X): L_A (intersect aut_1 aut_2) =$= L_A aut_1 /$\ L_A aut_2.
Proof.
intros w. split.
- intros B % intersect_correct. split; apply B.
- intros [B1 B2]. apply intersect_correct. now split.
Qed.
Lemma big_union_acorrect (l:list (NFA X)) :
L_A (big_union l) =$= fun w => exists a, (a el l) /\ L_A a w.
Proof.
intros w. split.
- intros [a [P Q]] % big_union_correct. exists a. split; auto.
- intros [a [P Q]]. apply big_union_correct. exists a. split; auto.
Qed.
Lemma dec_alanguage_empty (aut: NFA X): dec (L_A aut =$= {}).
Proof.
destruct (dec_alanguage_empty_informative aut) as [D|D].
- right. intros E. destruct D as [w D]. now apply E in D.
- now left.
Qed.
Section Complement.
Variable (aut: NFA X).
Implicit Types ( V W : EqClass (aut:=aut)).
Lemma autC_disjoint: L_A aut /$\ L_A (complement aut) =$= {}.
Proof.
apply language_empty_iff. intros w [LA LC].
destruct (totality aut w) as [V [W P]].
unfold complement in LC. apply big_union_acorrect in LC. destruct LC as [b [IC LB]].
unfold complement_auts in IC. apply in_map_iff in IC. destruct IC as [vw [AVW Q]].
apply in_filter_iff in Q. destruct Q as [Q1 Q2].
apply (Q2 (aseq_to_seq w)).
apply intersect_acorrect. split.
- now rewrite AVW.
- assumption.
Qed.
Definition toL_A (L : SeqLang X) := fun (aseq : ASeq X) => (L (aseq_to_seq aseq)).
Lemma part_of_complement_implies_complement V W: VW_part_of_complement (V,W) -> toL_A ({[V]}o{[W]}^00) <$= L_A (complement aut).
Proof.
intros PC w VW.
apply big_union_acorrect.
exists (VW_aut V W). split.
- unfold complement_auts.
apply in_map_iff.
exists (V,W). split;auto.
apply in_filter_iff. split.
+ apply elementIn.
+ unfold VW_part_of_complement. simpl.
apply language_empty_iff. intros w' L. now apply (PC w').
- now apply VW_aut_correct.
Qed.
Lemma not_part_of_complement_implies_aut V W: ~VW_part_of_complement (V,W) -> toL_A ({[V]}o{[W]}^00) <$= L_A aut.
Proof.
intros nPC w VW.
unfold VW_part_of_complement in nPC.
destruct (dec_language_empty_informative (intersect (VW_aut V W) aut )) as [D|D].
- destruct D as [w' L]. apply intersect_correct in L.
apply (compatibility (w:=w') (V:=V)(W:=W)).
+ destruct L as [L1 L2]. now apply VW_aut_correct in L1.
+ assumption.
- cbn in nPC. exfalso. apply nPC. intros w'. split.
+ intros B. specialize (D w'). exfalso. apply D. auto.
+ intros E. exfalso. auto.
Qed.
Lemma complement_complete : L_A (complement aut) \$/ L_A aut =$= universal_language.
Proof.
apply language_universal_iff. intros w.
destruct (totality aut w) as [V [W P]].
destruct (dec_VW_part_of_complement (V,W)) as [D|D].
- left. now apply (part_of_complement_implies_complement D).
- right. now apply (not_part_of_complement_implies_aut D).
Qed.
Lemma complement_correct: L_A (complement aut) =$= (L_A aut)^$~.
Proof.
intros w. destruct (complement_complete w). pose (autC_disjoint w).
autounfold in *. tauto.
Qed.
Lemma complement_correct2: (L_A (complement aut))^$~ =$= L_A aut.
Proof.
intros w. destruct (complement_complete w). pose (autC_disjoint w).
autounfold in *. tauto.
Qed.
End Complement.
Variable (aut: NFA X).
Implicit Types ( V W : EqClass (aut:=aut)).
Lemma autC_disjoint: L_A aut /$\ L_A (complement aut) =$= {}.
Proof.
apply language_empty_iff. intros w [LA LC].
destruct (totality aut w) as [V [W P]].
unfold complement in LC. apply big_union_acorrect in LC. destruct LC as [b [IC LB]].
unfold complement_auts in IC. apply in_map_iff in IC. destruct IC as [vw [AVW Q]].
apply in_filter_iff in Q. destruct Q as [Q1 Q2].
apply (Q2 (aseq_to_seq w)).
apply intersect_acorrect. split.
- now rewrite AVW.
- assumption.
Qed.
Definition toL_A (L : SeqLang X) := fun (aseq : ASeq X) => (L (aseq_to_seq aseq)).
Lemma part_of_complement_implies_complement V W: VW_part_of_complement (V,W) -> toL_A ({[V]}o{[W]}^00) <$= L_A (complement aut).
Proof.
intros PC w VW.
apply big_union_acorrect.
exists (VW_aut V W). split.
- unfold complement_auts.
apply in_map_iff.
exists (V,W). split;auto.
apply in_filter_iff. split.
+ apply elementIn.
+ unfold VW_part_of_complement. simpl.
apply language_empty_iff. intros w' L. now apply (PC w').
- now apply VW_aut_correct.
Qed.
Lemma not_part_of_complement_implies_aut V W: ~VW_part_of_complement (V,W) -> toL_A ({[V]}o{[W]}^00) <$= L_A aut.
Proof.
intros nPC w VW.
unfold VW_part_of_complement in nPC.
destruct (dec_language_empty_informative (intersect (VW_aut V W) aut )) as [D|D].
- destruct D as [w' L]. apply intersect_correct in L.
apply (compatibility (w:=w') (V:=V)(W:=W)).
+ destruct L as [L1 L2]. now apply VW_aut_correct in L1.
+ assumption.
- cbn in nPC. exfalso. apply nPC. intros w'. split.
+ intros B. specialize (D w'). exfalso. apply D. auto.
+ intros E. exfalso. auto.
Qed.
Lemma complement_complete : L_A (complement aut) \$/ L_A aut =$= universal_language.
Proof.
apply language_universal_iff. intros w.
destruct (totality aut w) as [V [W P]].
destruct (dec_VW_part_of_complement (V,W)) as [D|D].
- left. now apply (part_of_complement_implies_complement D).
- right. now apply (not_part_of_complement_implies_aut D).
Qed.
Lemma complement_correct: L_A (complement aut) =$= (L_A aut)^$~.
Proof.
intros w. destruct (complement_complete w). pose (autC_disjoint w).
autounfold in *. tauto.
Qed.
Lemma complement_correct2: (L_A (complement aut))^$~ =$= L_A aut.
Proof.
intros w. destruct (complement_complete w). pose (autC_disjoint w).
autounfold in *. tauto.
Qed.
End Complement.
Section ComplementCorollaries.
Corollary dec_language_universal (aut:NFA X) : dec(L_A aut =$= universal_language).
Proof.
destruct (dec_alanguage_empty (complement aut)) as [D|D].
- left. apply language_universal_iff. intros w. specialize (D w).
destruct (complement_complete aut w). autounfold in *. tauto.
- right. intros L. apply D. intros w. pose (complement_correct2 aut w).
autounfold in *. specialize (L w). tauto.
Qed.
Corollary dec_language_inclusion (aut1 aut2:NFA X): dec (L_A aut1 <$= L_A aut2).
Proof.
destruct (dec_alanguage_empty (intersect aut1 (complement aut2))) as [D|D].
- left. intros w L. specialize (D w).
destruct (complement_complete aut2 w) as [_ [D'| D']].
+ auto.
+ exfalso. apply D. now apply intersect_acorrect.
+ assumption.
- right. intros I. apply D. apply language_empty_iff.
intros w L. apply intersect_acorrect in L. destruct L as [L1 L2].
apply complement_correct in L2. auto.
Qed.
Corollary dec_language_eq (aut1 aut2:NFA X): dec (L_A aut1 =$= L_A aut2).
Proof.
pose (language_eq_iff (L_A aut1) (L_A aut2)) as P.
apply dec_trans with (P:=language_inclusion (L_A aut1) (L_A aut2) /\ language_inclusion (L_A aut2) (L_A aut1)).
- auto using and_dec, dec_language_inclusion.
- split; apply language_eq_iff.
Qed.
Corollary xm_word_problem (aut: NFA X) w : L_A aut w \/ ~ L_A aut w.
Proof.
destruct (complement_complete aut w) as [_ H].
destruct (H I).
- right. now apply complement_correct.
- left. assumption.
Qed.
End ComplementCorollaries.
End ClosureProperties.
Corollary dec_language_universal (aut:NFA X) : dec(L_A aut =$= universal_language).
Proof.
destruct (dec_alanguage_empty (complement aut)) as [D|D].
- left. apply language_universal_iff. intros w. specialize (D w).
destruct (complement_complete aut w). autounfold in *. tauto.
- right. intros L. apply D. intros w. pose (complement_correct2 aut w).
autounfold in *. specialize (L w). tauto.
Qed.
Corollary dec_language_inclusion (aut1 aut2:NFA X): dec (L_A aut1 <$= L_A aut2).
Proof.
destruct (dec_alanguage_empty (intersect aut1 (complement aut2))) as [D|D].
- left. intros w L. specialize (D w).
destruct (complement_complete aut2 w) as [_ [D'| D']].
+ auto.
+ exfalso. apply D. now apply intersect_acorrect.
+ assumption.
- right. intros I. apply D. apply language_empty_iff.
intros w L. apply intersect_acorrect in L. destruct L as [L1 L2].
apply complement_correct in L2. auto.
Qed.
Corollary dec_language_eq (aut1 aut2:NFA X): dec (L_A aut1 =$= L_A aut2).
Proof.
pose (language_eq_iff (L_A aut1) (L_A aut2)) as P.
apply dec_trans with (P:=language_inclusion (L_A aut1) (L_A aut2) /\ language_inclusion (L_A aut2) (L_A aut1)).
- auto using and_dec, dec_language_inclusion.
- split; apply language_eq_iff.
Qed.
Corollary xm_word_problem (aut: NFA X) w : L_A aut w \/ ~ L_A aut w.
Proof.
destruct (complement_complete aut w) as [_ H].
destruct (H I).
- right. now apply complement_correct.
- left. assumption.
Qed.
End ComplementCorollaries.
End ClosureProperties.
Definition OmegaSequenceStructure : SequenceStructure.
Proof.
apply (mkSequenceStructure
(ASeq := Seq)
(aseq_to_seq := fun (X:finType) (w:Seq X) => w)
(azip := fun(X Y:finType) => @seq_zip X Y)
(amap := fun(X Y:finType) => @seq_map X Y)
(exact_at := fun (X:finType)(x y : X) n m => if (decision (n = m)) then x else y)).
- now reflexivity.
- now reflexivity.
- intros X x y n D m. destruct decision; split ;intros K; congruence.
Defined.
Definition OmegaStructure (AR: forall C, AdditiveRamsey C): AdmissibleSequenceStructure.
Proof.
apply (mkAdmissibleSequenceStructure (CC:=OmegaSequenceStructure)).
- intros A aut. apply dec_language_empty_informative.
- intros A aut w. apply ramseyTotality. apply AR.
- eauto.
- intros A B aut. unfold LAmap, L_A. apply image_aut_correct.
Defined.
Proof.
apply (mkSequenceStructure
(ASeq := Seq)
(aseq_to_seq := fun (X:finType) (w:Seq X) => w)
(azip := fun(X Y:finType) => @seq_zip X Y)
(amap := fun(X Y:finType) => @seq_map X Y)
(exact_at := fun (X:finType)(x y : X) n m => if (decision (n = m)) then x else y)).
- now reflexivity.
- now reflexivity.
- intros X x y n D m. destruct decision; split ;intros K; congruence.
Defined.
Definition OmegaStructure (AR: forall C, AdditiveRamsey C): AdmissibleSequenceStructure.
Proof.
apply (mkAdmissibleSequenceStructure (CC:=OmegaSequenceStructure)).
- intros A aut. apply dec_language_empty_informative.
- intros A aut w. apply ramseyTotality. apply AR.
- eauto.
- intros A B aut. unfold LAmap, L_A. apply image_aut_correct.
Defined.
Definition UPSequenceStructure : SequenceStructure.
Proof.
apply (mkSequenceStructure
(ASeq := UPSeq)
(aseq_to_seq := unfold)
(amap := fun (X Y:finType) => @up_map X Y)
(azip := fun (X Y:finType) => @up_zip X Y)
(exact_at := fun (X:finType) (x y : X) (n : nat) => mkUPSeq (mkstring (fun m => if (decision (m = n)) then x else y) n)( mkstring (fun n => y) 0))).
- intros X Y w w'. now apply up_zip_correct.
- intros X Y f w. now apply up_map_correct.
- intros X x y n D m. unfold unfold; rewrite up_prefix, up_loop. decide (m <= n).
+ rewrite prepend_string_begin by comega. cbn. destruct decision as [<-|D']. tauto. split; intros Z; exfalso; auto.
+ rewrite prepend_string_rest by comega. cbn. split; intros Z; exfalso. auto. omega.
Defined.
Instance seq_dec_exists_bounded (X: Type)(P: X -> Prop) (decP: forall n, dec (P n)) (w : Seq X) n: dec( exists k, k <= n /\ P (w k)).
Proof. auto.
Defined.
Section UPAdmissible.
Existing Instance UPSequenceStructure.
Every accepted UP Sequence has an accepting UP run
Section PeriodicRun.
Open Scope string_scope.
Context{A:finType}.
Variable (aut: NFA A).
Lemma prepend_string_valid_run q r v w: |q| = (|v|) -> valid_path (seq q) v -> transition (q [(|q|)]) (v[(|v|)]) (r 0) -> valid_run (aut:=aut) r w -> valid_run (q +++ r) (v +++ w).
Proof.
intros E VP T VR.
intros n. decide (n < |v|) as [D|D].
- repeat rewrite prepend_string_begin by omega. apply VP. omega.
- decide (n = |v|) as [D' | D'].
+ repeat rewrite prepend_string_begin by omega. rewrite prepend_string_rest by omega.
rewrite E. subst n. rewrite_eq (S(|v|) - S(|v|) = 0). rewrite E in T. apply T.
+ repeat rewrite prepend_string_rest by omega. rewrite_eq (S n - S (| q |) = S (n - S(|q|))). rewrite E. apply VR.
Qed.
Lemma valid_path_prepended_string (r: Run aut) v w: valid_run r (v +++ w) -> valid_path r v.
Proof.
intros V n L. specialize (V n). now rewrite prepend_string_begin in V.
Qed.
Lemma omega_iteration_valid_run (r: String (state aut)) w: |r| = |w| -> valid_path (seq r) w -> transition (r [(|r|)]) (w[(|w|)]) (r [0]) -> valid_run (r to_omega) (w to_omega).
Proof.
(* This proof is kind of duplicated as in NFA, but I do not want to depent on these old proofs anymore *)
intros E V P n. unfold omega_iteration, concat_inf.
rewrite (concat_inf_index_equal (f:=(fun _ : nat => w)) (g:=(fun _ : nat => r))) by auto.
destruct (concat_inf_indices (fun _ : nat => r)) as [wi i] eqn:H.
destruct (concat_inf_index_step_correct H) as [J|J]; cbn; cbn in J; rewrite H in J; rewrite H; cbn.
- rewrite J. cbn. apply V. rewrite <-E. apply (concat_inf_index_in_bounds H).
- destruct decision; cbn.
+ subst i. now rewrite <-E in P.
+ apply V. omega.
Qed.
Lemma valid_periodic_run v w (q r : String (state aut)) : |q| = |v| -> |r| = |w| -> valid_path (seq q) v -> transition (q [(|q|)]) (v[(|v|)]) (r [0])
-> valid_path (seq r) w -> transition (r [(|r|)]) (w[(|w|)]) (r [0])
-> valid_run (q +++ r to_omega) (v +++ w to_omega).
Proof.
intros E1 E2 V1 T1 V2 T2.
apply prepend_string_valid_run, omega_iteration_valid_run; auto.
Qed.
Variable (vw : UPSeq A).
Definition critical_index_unfold (r:Run aut) n k k' := k' <= |loop vw| /\ (final_state (r (n + k')) /\ S(|prefix vw|) + k * (S(|loop vw|)) = n) .
Definition critical_index (r: Run aut) n := exists k k', critical_index_unfold r n k k'.
Instance dec_critical_index_unfold r n k k': dec (critical_index_unfold r n k k').
Proof. auto. Qed.
Lemma critical_index_unfold_bound r n k k': critical_index_unfold r n k k' -> k <= n.
Proof.
intros [_ [_ C]]. rewrite <-C.
enough (k <= k * S(|loop vw|)) by omega.
rewrite <-Nat.mul_1_r with (n := k) at 1.
apply Nat.mul_le_mono_nonneg_l; omega.
Qed.
Instance dec_ciritcal_index r n : dec (critical_index r n).
Proof.
apply dec_trans with (P:= exists k, k <= n /\ exists k', critical_index_unfold r n k k').
- apply (seq_dec_exists_bounded (P:=fun k => (exists k' : nat, critical_index_unfold r n k k'))). intros k.
unfold critical_index_unfold.
apply (seq_dec_exists_bounded (P:= fun k' => final_state (r (n + k')) /\ S(| prefix vw |) + k * S (| loop vw |) = n)). intros k'. auto.
- split.
+ firstorder.
+ intros [k [k' C]]. exists k. split.
* apply (critical_index_unfold_bound C).
* firstorder.
Qed.
Lemma critical_index_unfold_monotone r n1 n2 k1 k2 k'1 k'2: critical_index_unfold r n1 k1 k'1 -> critical_index_unfold r n2 k2 k'2 -> n1 < n2 -> k1 < k2.
Proof.
intros [_[_ C1]] [_[_ C2]] L.
enough (k1 * S(|loop vw|) < k2 * S(|loop vw|)).
- rewrite Nat.mul_lt_mono_pos_r with (p:= S(|loop vw|)); oauto.
- omega.
Qed.
Lemma critical_index_unfold_ge_zero r n k k': critical_index_unfold r n k k' -> S (| prefix vw |) < n -> 0 < k.
Proof.
intros [_ [_ C]] L.
enough (0 < k * S(|loop vw|)).
- rewrite Nat.mul_pos_cancel_r in H; omega.
- omega.
Qed.
Lemma critical_index_unfold_pred_index r n k k': critical_index_unfold r n k k' -> 0 < k -> unfold vw (n - 1) = (loop vw) [|loop vw|].
Proof.
intros [C1 [_ C2]] L.
unfold unfold. subst n.
assert (0 < k * S(|loop vw|)). { rewrite Nat.mul_pos_cancel_r; omega. }
rewrite prepend_string_rest.
- rewrite_eq (S (| prefix vw |) + k * S (| loop vw |) - 1 - S (| prefix vw |) = k * S (| loop vw |) - 1).
rewrite omega_iter_unfold with (n := k). rewrite prepend_string_begin.
+ apply fin_iter_last_index. omega.
+ rewrite fin_iter_length. enough (k * S (| loop vw |) <= S k * S (| loop vw |) ) by omega. apply Nat.mul_le_mono_nonneg_r; omega.
- omega.
Qed.
Lemma critical_index_unfold_distance r n1 n2 k1 k2 k'1 k'2: critical_index_unfold r n1 k1 k'1 -> critical_index_unfold r n2 k2 k'2 -> k1 < k2 -> |loop vw| <= n2 - S n1.
Proof.
intros [_ [_ C1]] [_ [_ C2]] L.
subst n1 n2.
enough (| loop vw | <= k2 * S (| loop vw |) - S (k1 * S (| loop vw |))) by omega.
destruct k2.
- exfalso. omega.
- rewrite Nat.mul_succ_l.
enough (k1 * S(|loop vw|) <= k2 * S(|loop vw|)) by omega.
apply Nat.mul_le_mono_nonneg_r; omega.
Qed.
Lemma critical_index_unfold_distance' r n1 n2 k1 k2 k'1 k'2: critical_index_unfold r n1 k1 k'1 -> critical_index_unfold r n2 k2 k'2 -> k1 < k2 -> k'1 <= n2 - S n1.
Proof.
intros C1 C2 L. assert ( k'1 <= |loop vw|) by apply C1.
enough (|loop vw| <= n2 - S n1) by omega.
now apply (critical_index_unfold_distance C1 C2).
Qed.
Lemma find_multiplicative n m : 0 < m -> exists k, k <= S n /\ n < k * m <= n + m.
intros L.
decide (m = 1).
- subst m. exists (S n). omega.
- destruct n.
+ exists 1. repeat split; omega.
+ exists (S(S n / m)). repeat split.
* enough ((S n / m) < (S n)) by omega. apply Nat.div_lt ; omega.
* rewrite Nat.mul_comm. apply (Nat.mul_succ_div_gt (S n) m). omega.
* rewrite Nat.mul_comm, Nat.mul_succ_r. cbn. enough (m * (S n / m) <= S n) by omega. apply (Nat.mul_div_le (S n) m). omega.
Qed.
Lemma final_state_eq (r:Run aut) n m : final_state (r n) -> n = m -> final_state (r m).
Proof.
intros Fs E. now rewrite <-E.
Qed.
Lemma final_to_critical r n : final_state (r (n + S(|prefix vw|) + S(|loop vw|))) -> exists m, m >= n /\ critical_index r m.
Proof.
intros F.
destruct (find_multiplicative (n) (m:=S(|loop vw|))) as [k [L M]]. { omega. }
exists (S(|prefix vw|) + k * (S (|loop vw|))). repeat split.
- omega.
- exists k, ((n + S (|loop vw|)) - k * (S(|loop vw|))).
repeat split.
+ omega.
+ apply (final_state_eq F). omega.
Qed.
Lemma infinite_final_implies_infinite_critical r : final r -> forall n, exists m, m >= n /\ critical_index r m.
Proof.
intros F n.
destruct (F (n + S(|prefix vw|) + S (|loop vw|))) as [m' [L' F']].
pose (n' := m' - S(|prefix vw|) - S (|loop vw|)).
enough (exists m, m >= n' /\ critical_index r m).
- destruct H as [m'' C]. exists m''. split.
+ subst n'. omega.
+ tauto.
- apply final_to_critical. subst n'.
apply (final_state_eq F'). omega.
Qed.
Lemma split_critical_index_begin r n k k': critical_index_unfold r n k k' -> k > 0 -> S(|prefix vw|) + S (|(fin_iter (loop vw) (pred k))|) = n.
Proof.
intros [_ [_ C]] G.
cbn. rewrite fin_iter_length. rewrite_eq (S (pred k) = k). subst n. remember (k * S (|loop vw|)) as Z.
enough (0 < Z) by omega.
subst Z. apply Nat.mul_pos_cancel_r; omega.
Qed.
Lemma periodic_run: L_B aut (unfold vw) -> exists rs, accepting (aut:=aut) (unfold rs) (unfold vw).
Proof.
intros [r [V [I F]]].
pose (r_f := infinite_filter (infinite_final_implies_infinite_critical F)).
destruct (can_find_duplicate' (S(S(|prefix vw|))) (S (Cardinality (state aut))+ S(S(|prefix vw|))) (fun n => r (r_f n))) as [[n1 [n2 [P Q]]]|D].
- unfold unfold. exists (mkUPSeq (extract 0 (r_f n1) r) (extract (r_f n1) (r_f n2) r)).
destruct (infinite_filter_correct (infinite_final_implies_infinite_critical F) n1) as [k1 [k1' H1]].
destruct (infinite_filter_correct (infinite_final_implies_infinite_critical F) n2) as [k2 [k2' H2]].
assert (0 < n1 < n2) by omega.
assert (0 < k1 < k2). {split.
- apply (critical_index_unfold_ge_zero H1).
enough (n1 <= infinite_filter (infinite_final_implies_infinite_critical F) n1) by omega.
apply s_monotone_ge, infinite_filter_s_monotone.
- apply (critical_index_unfold_monotone H1 H2). apply s_monotone_strict_order_preserving.
+ apply infinite_filter_s_monotone.
+ omega. }
repeat split.
+ rewrite (omega_iter_unfold (loop vw) (pred k1) ).
rewrite <-concat_prepend_string_associative.
apply prepend_string_valid_run.
* cbn. enough (r_f n1 > 0) as Z.
-- subst r_f. pose (split_critical_index_begin H1) as Eq. cbn in Eq. omega.
-- enough (n1 <= r_f n1) by omega. apply s_monotone_ge. subst r_f. apply infinite_filter_s_monotone.
* cbn. intros n L. specialize (V n). cbn in V. unfold unfold in V. rewrite (omega_iter_unfold (loop vw) (pred k1)) in V.
rewrite <-concat_prepend_string_associative in V. rewrite prepend_string_begin in V by auto. apply V.
* rewrite concat_string_rest by comega. cbn. rewrite drop_correct.
enough (((| prefix vw |) + S (| fin_iter (loop vw) (pred k1) |))= r_f n1 - 1) as Q'.
-- rewrite Q'.
assert ( (fin_iter (loop vw) (pred k1)) [r_f n1 -1- S (| prefix vw |)] = (unfold vw (r_f n1 -1 ))) as H'. {
unfold unfold. rewrite prepend_string_rest by omega.
rewrite (omega_iter_unfold (loop vw) (pred k1)).
now rewrite prepend_string_begin by omega.
}
rewrite H'. assert (r_f n1 > 0). { enough (r_f n1 >= n1) by omega. apply s_monotone_ge, infinite_filter_s_monotone. }
rewrite_eq (r_f n1 + 0 = S(r_f n1 - 1)). apply V.
-- subst r_f. rewrite <-(proj2 (proj2 H1)). rewrite fin_iter_length. rewrite_eq (S(pred k1) = k1).
remember (k1 * S (|loop vw|)) as Z. enough (0 < Z ) by omega. subst Z. apply Nat.mul_pos_cancel_r; omega.
* cbn. rewrite (fin_iter_to_omega (loop vw) (pred (k2 - k1))). apply omega_iteration_valid_run.
-- cbn. rewrite fin_iter_length. rewrite_eq (S (pred (k2 - k1)) = k2 - k1).
pose (split_critical_index_begin H1) as Eq1.
pose (split_critical_index_begin H2) as Eq2. cbn in Eq1,Eq2. rewrite fin_iter_length in Eq1,Eq2.
rewrite_eq (S (pred k1) = k1) in Eq1. rewrite_eq (S (pred k2) = k2) in Eq2.
subst r_f. rewrite <-Eq1, <-Eq2 by oauto. rewrite (Nat.mul_sub_distr_r).
remember (k2 * S (| loop vw |)) as Z2. remember (k1 * S (| loop vw |)) as Z1.
enough (0 < Z1 /\ 0 < Z2) by omega.
split; [subst Z1 | subst Z2]; apply Nat.mul_pos_cancel_r; omega.
-- intros n L.
cbn. repeat rewrite drop_correct.
enough ((fin_iter (loop vw) (pred (k2 - k1))) [n] = (unfold vw) (r_f n1 + n)) as H'.
++ rewrite H'. rewrite_eq (r_f n1 + S n = S (r_f n1 + n)). apply V.
++ unfold unfold. rewrite prepend_string_rest. destruct H1 as [_ [_ H1]].
unfold r_f. rewrite <-H1. rewrite (omega_iter_unfold (loop vw) (pred k1)).
rewrite prepend_string_rest.
** rewrite (omega_iter_unfold (loop vw) (pred (k2 - k1))).
rewrite prepend_string_begin.
--- f_equal. rewrite fin_iter_length.
rewrite_eq (S (pred k1) = k1). remember (k1 * (S(|loop vw|))) as C.
enough (0 < C) by omega. subst C. apply Nat.mul_pos_cancel_r; omega.
--- rewrite fin_iter_length in L. repeat rewrite fin_iter_length.
rewrite_eq (S(pred (k2 - k1)) = k2 - k1). rewrite_eq (S(pred (k2 - k1)) = k2 - k1) in L.
rewrite_eq (S (pred k1) = k1).
remember (k1 * S(|loop vw|)) as C.
enough (0 < C) by (rewrite_eq (S(C-1) = C); omega).
subst C. apply Nat.mul_pos_cancel_r; omega.
** rewrite fin_iter_length. rewrite_eq (S (pred k1) = k1). remember (k1 * S(|loop vw|)) as C.
enough (0 < C) by omega. subst C. apply Nat.mul_pos_cancel_r; omega.
** subst r_f. destruct H1 as [_ [_ H1]]. rewrite <-H1. remember (k1 * S(|loop vw|)) as C. omega.
-- cbn. rewrite drop_correct. rewrite fin_iter_length. rewrite drop_correct.
remember (r_f n1) as N1. remember (r_f n2) as N2.
assert (N1 < N2). { subst N1 N2. apply s_monotone_strict_order_preserving. subst r_f. apply infinite_filter_s_monotone. omega. }
rewrite_eq (N1 + (N2 - S N1) = N2 - 1). rewrite_eq (S (pred (k2 - k1)) = k2 - k1).
rewrite fin_iter_last_index.
++ destruct Q as [_ Q]. rewrite_eq (N1 + 0 = N1). rewrite Q.
specialize (V (N2 -1)). rewrite_eq (S (N2 -1) = N2) in V.
enough (unfold vw (N2 -1) = (loop vw)[|loop vw|]) as H'.
** now rewrite <-H'.
** subst N2 r_f. apply ( critical_index_unfold_pred_index H2). omega.
++ omega.
+ unfold initial. rewrite prepend_string_begin by omega. cbn. apply I.
+ apply final_prepend. cbn. apply omega_iteration_final with (k := k1').
* cbn. subst r_f. now apply (critical_index_unfold_distance' H1 H2).
* cbn. unfold critical_index_unfold in H1. subst r_f. rewrite drop_correct. tauto.
- exfalso. omega.
Qed.
End PeriodicRun.
Close Scope list_scope.
Open Scope string_scope.
Lemma periodic_run_matching_pseq_size (A:finType) (aut: NFA A) (w : UPSeq A) (r: UPSeq (state aut)) : accepting (unfold r) (unfold w) ->
exists r' w', accepting (unfold r') (unfold w') /\
r ==== r' /\ w ==== w' /\
|prefix r'| = |prefix w'| /\ |loop r'| = |loop w'|.
Proof.
intros Acc.
exists (up_map fst (up_zip r w)), (up_map snd (up_zip r w)). split; [|repeat split].
- apply (accepting_extensional (r := unfold r) (w:= unfold w)); auto.
+ now rewrite up_zip_proj1.
+ now rewrite up_zip_proj2.
- now rewrite up_zip_proj1.
- now rewrite up_zip_proj2.
Qed.
Open Scope string_scope.
Context{A:finType}.
Variable (aut: NFA A).
Lemma prepend_string_valid_run q r v w: |q| = (|v|) -> valid_path (seq q) v -> transition (q [(|q|)]) (v[(|v|)]) (r 0) -> valid_run (aut:=aut) r w -> valid_run (q +++ r) (v +++ w).
Proof.
intros E VP T VR.
intros n. decide (n < |v|) as [D|D].
- repeat rewrite prepend_string_begin by omega. apply VP. omega.
- decide (n = |v|) as [D' | D'].
+ repeat rewrite prepend_string_begin by omega. rewrite prepend_string_rest by omega.
rewrite E. subst n. rewrite_eq (S(|v|) - S(|v|) = 0). rewrite E in T. apply T.
+ repeat rewrite prepend_string_rest by omega. rewrite_eq (S n - S (| q |) = S (n - S(|q|))). rewrite E. apply VR.
Qed.
Lemma valid_path_prepended_string (r: Run aut) v w: valid_run r (v +++ w) -> valid_path r v.
Proof.
intros V n L. specialize (V n). now rewrite prepend_string_begin in V.
Qed.
Lemma omega_iteration_valid_run (r: String (state aut)) w: |r| = |w| -> valid_path (seq r) w -> transition (r [(|r|)]) (w[(|w|)]) (r [0]) -> valid_run (r to_omega) (w to_omega).
Proof.
(* This proof is kind of duplicated as in NFA, but I do not want to depent on these old proofs anymore *)
intros E V P n. unfold omega_iteration, concat_inf.
rewrite (concat_inf_index_equal (f:=(fun _ : nat => w)) (g:=(fun _ : nat => r))) by auto.
destruct (concat_inf_indices (fun _ : nat => r)) as [wi i] eqn:H.
destruct (concat_inf_index_step_correct H) as [J|J]; cbn; cbn in J; rewrite H in J; rewrite H; cbn.
- rewrite J. cbn. apply V. rewrite <-E. apply (concat_inf_index_in_bounds H).
- destruct decision; cbn.
+ subst i. now rewrite <-E in P.
+ apply V. omega.
Qed.
Lemma valid_periodic_run v w (q r : String (state aut)) : |q| = |v| -> |r| = |w| -> valid_path (seq q) v -> transition (q [(|q|)]) (v[(|v|)]) (r [0])
-> valid_path (seq r) w -> transition (r [(|r|)]) (w[(|w|)]) (r [0])
-> valid_run (q +++ r to_omega) (v +++ w to_omega).
Proof.
intros E1 E2 V1 T1 V2 T2.
apply prepend_string_valid_run, omega_iteration_valid_run; auto.
Qed.
Variable (vw : UPSeq A).
Definition critical_index_unfold (r:Run aut) n k k' := k' <= |loop vw| /\ (final_state (r (n + k')) /\ S(|prefix vw|) + k * (S(|loop vw|)) = n) .
Definition critical_index (r: Run aut) n := exists k k', critical_index_unfold r n k k'.
Instance dec_critical_index_unfold r n k k': dec (critical_index_unfold r n k k').
Proof. auto. Qed.
Lemma critical_index_unfold_bound r n k k': critical_index_unfold r n k k' -> k <= n.
Proof.
intros [_ [_ C]]. rewrite <-C.
enough (k <= k * S(|loop vw|)) by omega.
rewrite <-Nat.mul_1_r with (n := k) at 1.
apply Nat.mul_le_mono_nonneg_l; omega.
Qed.
Instance dec_ciritcal_index r n : dec (critical_index r n).
Proof.
apply dec_trans with (P:= exists k, k <= n /\ exists k', critical_index_unfold r n k k').
- apply (seq_dec_exists_bounded (P:=fun k => (exists k' : nat, critical_index_unfold r n k k'))). intros k.
unfold critical_index_unfold.
apply (seq_dec_exists_bounded (P:= fun k' => final_state (r (n + k')) /\ S(| prefix vw |) + k * S (| loop vw |) = n)). intros k'. auto.
- split.
+ firstorder.
+ intros [k [k' C]]. exists k. split.
* apply (critical_index_unfold_bound C).
* firstorder.
Qed.
Lemma critical_index_unfold_monotone r n1 n2 k1 k2 k'1 k'2: critical_index_unfold r n1 k1 k'1 -> critical_index_unfold r n2 k2 k'2 -> n1 < n2 -> k1 < k2.
Proof.
intros [_[_ C1]] [_[_ C2]] L.
enough (k1 * S(|loop vw|) < k2 * S(|loop vw|)).
- rewrite Nat.mul_lt_mono_pos_r with (p:= S(|loop vw|)); oauto.
- omega.
Qed.
Lemma critical_index_unfold_ge_zero r n k k': critical_index_unfold r n k k' -> S (| prefix vw |) < n -> 0 < k.
Proof.
intros [_ [_ C]] L.
enough (0 < k * S(|loop vw|)).
- rewrite Nat.mul_pos_cancel_r in H; omega.
- omega.
Qed.
Lemma critical_index_unfold_pred_index r n k k': critical_index_unfold r n k k' -> 0 < k -> unfold vw (n - 1) = (loop vw) [|loop vw|].
Proof.
intros [C1 [_ C2]] L.
unfold unfold. subst n.
assert (0 < k * S(|loop vw|)). { rewrite Nat.mul_pos_cancel_r; omega. }
rewrite prepend_string_rest.
- rewrite_eq (S (| prefix vw |) + k * S (| loop vw |) - 1 - S (| prefix vw |) = k * S (| loop vw |) - 1).
rewrite omega_iter_unfold with (n := k). rewrite prepend_string_begin.
+ apply fin_iter_last_index. omega.
+ rewrite fin_iter_length. enough (k * S (| loop vw |) <= S k * S (| loop vw |) ) by omega. apply Nat.mul_le_mono_nonneg_r; omega.
- omega.
Qed.
Lemma critical_index_unfold_distance r n1 n2 k1 k2 k'1 k'2: critical_index_unfold r n1 k1 k'1 -> critical_index_unfold r n2 k2 k'2 -> k1 < k2 -> |loop vw| <= n2 - S n1.
Proof.
intros [_ [_ C1]] [_ [_ C2]] L.
subst n1 n2.
enough (| loop vw | <= k2 * S (| loop vw |) - S (k1 * S (| loop vw |))) by omega.
destruct k2.
- exfalso. omega.
- rewrite Nat.mul_succ_l.
enough (k1 * S(|loop vw|) <= k2 * S(|loop vw|)) by omega.
apply Nat.mul_le_mono_nonneg_r; omega.
Qed.
Lemma critical_index_unfold_distance' r n1 n2 k1 k2 k'1 k'2: critical_index_unfold r n1 k1 k'1 -> critical_index_unfold r n2 k2 k'2 -> k1 < k2 -> k'1 <= n2 - S n1.
Proof.
intros C1 C2 L. assert ( k'1 <= |loop vw|) by apply C1.
enough (|loop vw| <= n2 - S n1) by omega.
now apply (critical_index_unfold_distance C1 C2).
Qed.
Lemma find_multiplicative n m : 0 < m -> exists k, k <= S n /\ n < k * m <= n + m.
intros L.
decide (m = 1).
- subst m. exists (S n). omega.
- destruct n.
+ exists 1. repeat split; omega.
+ exists (S(S n / m)). repeat split.
* enough ((S n / m) < (S n)) by omega. apply Nat.div_lt ; omega.
* rewrite Nat.mul_comm. apply (Nat.mul_succ_div_gt (S n) m). omega.
* rewrite Nat.mul_comm, Nat.mul_succ_r. cbn. enough (m * (S n / m) <= S n) by omega. apply (Nat.mul_div_le (S n) m). omega.
Qed.
Lemma final_state_eq (r:Run aut) n m : final_state (r n) -> n = m -> final_state (r m).
Proof.
intros Fs E. now rewrite <-E.
Qed.
Lemma final_to_critical r n : final_state (r (n + S(|prefix vw|) + S(|loop vw|))) -> exists m, m >= n /\ critical_index r m.
Proof.
intros F.
destruct (find_multiplicative (n) (m:=S(|loop vw|))) as [k [L M]]. { omega. }
exists (S(|prefix vw|) + k * (S (|loop vw|))). repeat split.
- omega.
- exists k, ((n + S (|loop vw|)) - k * (S(|loop vw|))).
repeat split.
+ omega.
+ apply (final_state_eq F). omega.
Qed.
Lemma infinite_final_implies_infinite_critical r : final r -> forall n, exists m, m >= n /\ critical_index r m.
Proof.
intros F n.
destruct (F (n + S(|prefix vw|) + S (|loop vw|))) as [m' [L' F']].
pose (n' := m' - S(|prefix vw|) - S (|loop vw|)).
enough (exists m, m >= n' /\ critical_index r m).
- destruct H as [m'' C]. exists m''. split.
+ subst n'. omega.
+ tauto.
- apply final_to_critical. subst n'.
apply (final_state_eq F'). omega.
Qed.
Lemma split_critical_index_begin r n k k': critical_index_unfold r n k k' -> k > 0 -> S(|prefix vw|) + S (|(fin_iter (loop vw) (pred k))|) = n.
Proof.
intros [_ [_ C]] G.
cbn. rewrite fin_iter_length. rewrite_eq (S (pred k) = k). subst n. remember (k * S (|loop vw|)) as Z.
enough (0 < Z) by omega.
subst Z. apply Nat.mul_pos_cancel_r; omega.
Qed.
Lemma periodic_run: L_B aut (unfold vw) -> exists rs, accepting (aut:=aut) (unfold rs) (unfold vw).
Proof.
intros [r [V [I F]]].
pose (r_f := infinite_filter (infinite_final_implies_infinite_critical F)).
destruct (can_find_duplicate' (S(S(|prefix vw|))) (S (Cardinality (state aut))+ S(S(|prefix vw|))) (fun n => r (r_f n))) as [[n1 [n2 [P Q]]]|D].
- unfold unfold. exists (mkUPSeq (extract 0 (r_f n1) r) (extract (r_f n1) (r_f n2) r)).
destruct (infinite_filter_correct (infinite_final_implies_infinite_critical F) n1) as [k1 [k1' H1]].
destruct (infinite_filter_correct (infinite_final_implies_infinite_critical F) n2) as [k2 [k2' H2]].
assert (0 < n1 < n2) by omega.
assert (0 < k1 < k2). {split.
- apply (critical_index_unfold_ge_zero H1).
enough (n1 <= infinite_filter (infinite_final_implies_infinite_critical F) n1) by omega.
apply s_monotone_ge, infinite_filter_s_monotone.
- apply (critical_index_unfold_monotone H1 H2). apply s_monotone_strict_order_preserving.
+ apply infinite_filter_s_monotone.
+ omega. }
repeat split.
+ rewrite (omega_iter_unfold (loop vw) (pred k1) ).
rewrite <-concat_prepend_string_associative.
apply prepend_string_valid_run.
* cbn. enough (r_f n1 > 0) as Z.
-- subst r_f. pose (split_critical_index_begin H1) as Eq. cbn in Eq. omega.
-- enough (n1 <= r_f n1) by omega. apply s_monotone_ge. subst r_f. apply infinite_filter_s_monotone.
* cbn. intros n L. specialize (V n). cbn in V. unfold unfold in V. rewrite (omega_iter_unfold (loop vw) (pred k1)) in V.
rewrite <-concat_prepend_string_associative in V. rewrite prepend_string_begin in V by auto. apply V.
* rewrite concat_string_rest by comega. cbn. rewrite drop_correct.
enough (((| prefix vw |) + S (| fin_iter (loop vw) (pred k1) |))= r_f n1 - 1) as Q'.
-- rewrite Q'.
assert ( (fin_iter (loop vw) (pred k1)) [r_f n1 -1- S (| prefix vw |)] = (unfold vw (r_f n1 -1 ))) as H'. {
unfold unfold. rewrite prepend_string_rest by omega.
rewrite (omega_iter_unfold (loop vw) (pred k1)).
now rewrite prepend_string_begin by omega.
}
rewrite H'. assert (r_f n1 > 0). { enough (r_f n1 >= n1) by omega. apply s_monotone_ge, infinite_filter_s_monotone. }
rewrite_eq (r_f n1 + 0 = S(r_f n1 - 1)). apply V.
-- subst r_f. rewrite <-(proj2 (proj2 H1)). rewrite fin_iter_length. rewrite_eq (S(pred k1) = k1).
remember (k1 * S (|loop vw|)) as Z. enough (0 < Z ) by omega. subst Z. apply Nat.mul_pos_cancel_r; omega.
* cbn. rewrite (fin_iter_to_omega (loop vw) (pred (k2 - k1))). apply omega_iteration_valid_run.
-- cbn. rewrite fin_iter_length. rewrite_eq (S (pred (k2 - k1)) = k2 - k1).
pose (split_critical_index_begin H1) as Eq1.
pose (split_critical_index_begin H2) as Eq2. cbn in Eq1,Eq2. rewrite fin_iter_length in Eq1,Eq2.
rewrite_eq (S (pred k1) = k1) in Eq1. rewrite_eq (S (pred k2) = k2) in Eq2.
subst r_f. rewrite <-Eq1, <-Eq2 by oauto. rewrite (Nat.mul_sub_distr_r).
remember (k2 * S (| loop vw |)) as Z2. remember (k1 * S (| loop vw |)) as Z1.
enough (0 < Z1 /\ 0 < Z2) by omega.
split; [subst Z1 | subst Z2]; apply Nat.mul_pos_cancel_r; omega.
-- intros n L.
cbn. repeat rewrite drop_correct.
enough ((fin_iter (loop vw) (pred (k2 - k1))) [n] = (unfold vw) (r_f n1 + n)) as H'.
++ rewrite H'. rewrite_eq (r_f n1 + S n = S (r_f n1 + n)). apply V.
++ unfold unfold. rewrite prepend_string_rest. destruct H1 as [_ [_ H1]].
unfold r_f. rewrite <-H1. rewrite (omega_iter_unfold (loop vw) (pred k1)).
rewrite prepend_string_rest.
** rewrite (omega_iter_unfold (loop vw) (pred (k2 - k1))).
rewrite prepend_string_begin.
--- f_equal. rewrite fin_iter_length.
rewrite_eq (S (pred k1) = k1). remember (k1 * (S(|loop vw|))) as C.
enough (0 < C) by omega. subst C. apply Nat.mul_pos_cancel_r; omega.
--- rewrite fin_iter_length in L. repeat rewrite fin_iter_length.
rewrite_eq (S(pred (k2 - k1)) = k2 - k1). rewrite_eq (S(pred (k2 - k1)) = k2 - k1) in L.
rewrite_eq (S (pred k1) = k1).
remember (k1 * S(|loop vw|)) as C.
enough (0 < C) by (rewrite_eq (S(C-1) = C); omega).
subst C. apply Nat.mul_pos_cancel_r; omega.
** rewrite fin_iter_length. rewrite_eq (S (pred k1) = k1). remember (k1 * S(|loop vw|)) as C.
enough (0 < C) by omega. subst C. apply Nat.mul_pos_cancel_r; omega.
** subst r_f. destruct H1 as [_ [_ H1]]. rewrite <-H1. remember (k1 * S(|loop vw|)) as C. omega.
-- cbn. rewrite drop_correct. rewrite fin_iter_length. rewrite drop_correct.
remember (r_f n1) as N1. remember (r_f n2) as N2.
assert (N1 < N2). { subst N1 N2. apply s_monotone_strict_order_preserving. subst r_f. apply infinite_filter_s_monotone. omega. }
rewrite_eq (N1 + (N2 - S N1) = N2 - 1). rewrite_eq (S (pred (k2 - k1)) = k2 - k1).
rewrite fin_iter_last_index.
++ destruct Q as [_ Q]. rewrite_eq (N1 + 0 = N1). rewrite Q.
specialize (V (N2 -1)). rewrite_eq (S (N2 -1) = N2) in V.
enough (unfold vw (N2 -1) = (loop vw)[|loop vw|]) as H'.
** now rewrite <-H'.
** subst N2 r_f. apply ( critical_index_unfold_pred_index H2). omega.
++ omega.
+ unfold initial. rewrite prepend_string_begin by omega. cbn. apply I.
+ apply final_prepend. cbn. apply omega_iteration_final with (k := k1').
* cbn. subst r_f. now apply (critical_index_unfold_distance' H1 H2).
* cbn. unfold critical_index_unfold in H1. subst r_f. rewrite drop_correct. tauto.
- exfalso. omega.
Qed.
End PeriodicRun.
Close Scope list_scope.
Open Scope string_scope.
Lemma periodic_run_matching_pseq_size (A:finType) (aut: NFA A) (w : UPSeq A) (r: UPSeq (state aut)) : accepting (unfold r) (unfold w) ->
exists r' w', accepting (unfold r') (unfold w') /\
r ==== r' /\ w ==== w' /\
|prefix r'| = |prefix w'| /\ |loop r'| = |loop w'|.
Proof.
intros Acc.
exists (up_map fst (up_zip r w)), (up_map snd (up_zip r w)). split; [|repeat split].
- apply (accepting_extensional (r := unfold r) (w:= unfold w)); auto.
+ now rewrite up_zip_proj1.
+ now rewrite up_zip_proj2.
- now rewrite up_zip_proj1.
- now rewrite up_zip_proj2.
Qed.
Correctness of image NFA
Lemma map_aut_up_correct (X Y:finType) (f: X ->Y) (aut: NFA X) : L_A (CC:=UPSequenceStructure) (image_aut f aut) =$= LAmap f (L_A aut).
Proof.
unfold L_A, LAmap, ASeq, azip, amap. simpl. split.
- intros [r [r' [w' [[V [I F]] [Er [Ew [Ef Es]]]]]] % periodic_run_matching_pseq_size] % periodic_run.
assert (forall n, {x : X | f x = (unfold w' n)/\ transition (aut:=aut) (unfold r' n) x (unfold r' (S n))}) as H. {
intros n. apply finType_cc.
- auto.
- apply V.
}
pose (w1 := mkstring (fun n => proj1_sig (H n)) (|prefix r'|)).
pose (w2 := mkstring (fun n => proj1_sig (H ((S (|prefix r'|))+n ))) (| loop r' |)).
exists (mkUPSeq w1 w2). rewrite Ew. split.
{
unfold up_map. rewrite !up_prefix, !up_loop.
apply prepend_string_proper; unfold string_map, seq_map.
- split; auto. intros n L. cbn in *. destruct H as [x [E T]]. cbn. unfold unfold in E. now rewrite prepend_string_begin in E by comega.
- apply omega_iteration_proper.
split; auto. intros n L. cbn in *. rewrite_eq (S (|prefix r'| +n) = S(|prefix r'|) + n). destruct H as [x [E T]]. cbn. unfold unfold in E. rewrite Ef in E. rewrite prepend_string_rest' in E.
now rewrite omega_iter_first in E by omega.
}
exists (unfold r'). repeat split; auto.
destruct r' as [r1 r2]. simpl in Ef,Es. unfold unfold. simpl prefix. simpl loop.
simpl in r1 , r2.
apply (valid_prepend_path' (X:=X) (aut:=aut)); auto.
+ intros n L. subst w1. simpl. destruct (H n) as[x T]. simpl. simpl in L.
unfold unfold in T. now rewrite 3prepend_string_begin in T by comega.
+ simpl. destruct (H (|r1|)) as [x T]. simpl.
unfold unfold in T. rewrite 2prepend_string_begin in T by comega.
rewrite_eq (S(|r1|) = S(|r1|)+0) in T.
now rewrite prepend_string_rest' in T.
+ unfold omega_iteration. apply (concat_inf_is_valid'' (X:=X)).
intros _. repeat split.
* intros n L. subst w2. simpl seq. rewrite_eq (S(|r1| + n) = S(|r1|) + n).
destruct (H ((S (| r1 |))+ n)) as [x [E T]].
unfold unfold in T. simpl in L. simpl prefix in T. simpl loop in T. simpl.
rewrite_eq (S(S (|r1|) + n) = S (|r1|) + S n) in T.
rewrite 2prepend_string_rest' in T.
now rewrite 2omega_iter_first in T by comega.
* subst w2. simpl. rewrite_eq (S(|r1| + |r2|) = S(|r1|) + |r2|). destruct (H ((S (| r1 |)) + |r2|)) as [x [E T]].
unfold unfold in T. simpl prefix in T. simpl loop in T. simpl.
rewrite_eq (S(S (|r1|) + |r2|) = S (|r1|) + S (|r2|)) in T.
rewrite 2prepend_string_rest' in T.
rewrite omega_iter_first in T by auto.
simpl. now rewrite omega_iter_first_new in T.
- intros [w' [E [r [V [In Fin]]]]].
exists r. repeat split; auto.
intros n. exists (unfold w' n). split.
+ unfold aseq_equal, aseq_to_seq in E. simpl in E. rewrite up_map_correct in E. apply E.
+ apply V.
Qed.
End UPAdmissible.
Definition UPStructure : AdmissibleSequenceStructure.
Proof.
apply ( mkAdmissibleSequenceStructure (CC:=UPSequenceStructure)).
- intros A aut. unfold L_A. simpl. destruct (dec_language_empty_informative_periodic aut ) as [D|D].
+ left. destruct D as [v [w L]]. exists (mkUPSeq v w). auto.
+ right. intros vw. apply (D (unfold vw)).
- intros A aut [v w]. exists (buechi_eq_class v), (buechi_eq_class w). simpl. unfold unfold.
auto using in_lang_prepend, eq_classes_extensional, lang_omega_iteration_extensional, buechi_eq_class_correct, string_omega_omega_iteration.
- intros *. apply periodic_run.
- apply map_aut_up_correct.
Defined.
Proof.
unfold L_A, LAmap, ASeq, azip, amap. simpl. split.
- intros [r [r' [w' [[V [I F]] [Er [Ew [Ef Es]]]]]] % periodic_run_matching_pseq_size] % periodic_run.
assert (forall n, {x : X | f x = (unfold w' n)/\ transition (aut:=aut) (unfold r' n) x (unfold r' (S n))}) as H. {
intros n. apply finType_cc.
- auto.
- apply V.
}
pose (w1 := mkstring (fun n => proj1_sig (H n)) (|prefix r'|)).
pose (w2 := mkstring (fun n => proj1_sig (H ((S (|prefix r'|))+n ))) (| loop r' |)).
exists (mkUPSeq w1 w2). rewrite Ew. split.
{
unfold up_map. rewrite !up_prefix, !up_loop.
apply prepend_string_proper; unfold string_map, seq_map.
- split; auto. intros n L. cbn in *. destruct H as [x [E T]]. cbn. unfold unfold in E. now rewrite prepend_string_begin in E by comega.
- apply omega_iteration_proper.
split; auto. intros n L. cbn in *. rewrite_eq (S (|prefix r'| +n) = S(|prefix r'|) + n). destruct H as [x [E T]]. cbn. unfold unfold in E. rewrite Ef in E. rewrite prepend_string_rest' in E.
now rewrite omega_iter_first in E by omega.
}
exists (unfold r'). repeat split; auto.
destruct r' as [r1 r2]. simpl in Ef,Es. unfold unfold. simpl prefix. simpl loop.
simpl in r1 , r2.
apply (valid_prepend_path' (X:=X) (aut:=aut)); auto.
+ intros n L. subst w1. simpl. destruct (H n) as[x T]. simpl. simpl in L.
unfold unfold in T. now rewrite 3prepend_string_begin in T by comega.
+ simpl. destruct (H (|r1|)) as [x T]. simpl.
unfold unfold in T. rewrite 2prepend_string_begin in T by comega.
rewrite_eq (S(|r1|) = S(|r1|)+0) in T.
now rewrite prepend_string_rest' in T.
+ unfold omega_iteration. apply (concat_inf_is_valid'' (X:=X)).
intros _. repeat split.
* intros n L. subst w2. simpl seq. rewrite_eq (S(|r1| + n) = S(|r1|) + n).
destruct (H ((S (| r1 |))+ n)) as [x [E T]].
unfold unfold in T. simpl in L. simpl prefix in T. simpl loop in T. simpl.
rewrite_eq (S(S (|r1|) + n) = S (|r1|) + S n) in T.
rewrite 2prepend_string_rest' in T.
now rewrite 2omega_iter_first in T by comega.
* subst w2. simpl. rewrite_eq (S(|r1| + |r2|) = S(|r1|) + |r2|). destruct (H ((S (| r1 |)) + |r2|)) as [x [E T]].
unfold unfold in T. simpl prefix in T. simpl loop in T. simpl.
rewrite_eq (S(S (|r1|) + |r2|) = S (|r1|) + S (|r2|)) in T.
rewrite 2prepend_string_rest' in T.
rewrite omega_iter_first in T by auto.
simpl. now rewrite omega_iter_first_new in T.
- intros [w' [E [r [V [In Fin]]]]].
exists r. repeat split; auto.
intros n. exists (unfold w' n). split.
+ unfold aseq_equal, aseq_to_seq in E. simpl in E. rewrite up_map_correct in E. apply E.
+ apply V.
Qed.
End UPAdmissible.
Definition UPStructure : AdmissibleSequenceStructure.
Proof.
apply ( mkAdmissibleSequenceStructure (CC:=UPSequenceStructure)).
- intros A aut. unfold L_A. simpl. destruct (dec_language_empty_informative_periodic aut ) as [D|D].
+ left. destruct D as [v [w L]]. exists (mkUPSeq v w). auto.
+ right. intros vw. apply (D (unfold vw)).
- intros A aut [v w]. exists (buechi_eq_class v), (buechi_eq_class w). simpl. unfold unfold.
auto using in_lang_prepend, eq_classes_extensional, lang_omega_iteration_extensional, buechi_eq_class_correct, string_omega_omega_iteration.
- intros *. apply periodic_run.
- apply map_aut_up_correct.
Defined.