Set Implicit Arguments.
Require Import Coq.Init.Nat.
Require Import Coq.Relations.Relation_Definitions.
Require Import BA.External.
Require Import BA.FinTypes.
Require Import BasicDefs.
Require Import Seqs.
Require Import StrictlyMonotoneSeqs.
Require Import SeqOperations.
Require Import NFAs.
Require Import Buechi.
Require Import NFAConstructions.
Require Import Utils.
Require Import DecLanguageEmpty.
Require Import fin_languages.
Arguments reflexive [A] _ .
Arguments transitive [A] _ .
Arguments symmetric [A] _.
Arguments equiv [A] _.
Close Scope list_scope.
Open Scope string_scope.
Require Import Coq.Init.Nat.
Require Import Coq.Relations.Relation_Definitions.
Require Import BA.External.
Require Import BA.FinTypes.
Require Import BasicDefs.
Require Import Seqs.
Require Import StrictlyMonotoneSeqs.
Require Import SeqOperations.
Require Import NFAs.
Require Import Buechi.
Require Import NFAConstructions.
Require Import Utils.
Require Import DecLanguageEmpty.
Require Import fin_languages.
Arguments reflexive [A] _ .
Arguments transitive [A] _ .
Arguments symmetric [A] _.
Arguments equiv [A] _.
Close Scope list_scope.
Open Scope string_scope.
Section TildeEquivalenceRelation.
Context {A:finType}.
Context {aut:BuechiAut A}.
Definition transforms (w :String A) (s s': state aut) :=
∃exists r, path r w s s'.
Definition transforms_final (w:String A) (s s': state aut) :=
∃exists r, path r w s s' ∧/\ ∃exists n, n ≤<= S (|w|) ∧/\ final_state (r n).
Notation " s1 '⟹===>' s2 '·on' w" := (transforms w s₁s1 s₂s2) (at level 10).
Notation " s1 '⟹F=!=>' s2 '·on' w" := (transforms_final w s₁s1 s₂s2) (at level 10).
Lemma final_transform_implies_transform s s' w: s ⟹F=!=> s' on w →-> s ⟹===> s' on w.
Proof.
intros [r [P _]]. now exists r.
Qed.
Lemma split_transforms u w s s': s ⟹===> s' on (u ⧺++ w) →-> ∃exists s'', s ⟹===> s'' on u ∧/\ s'' ⟹===> s' on w.
Proof.
intros [r W].
destruct (split_path W) as [s'' [P₁P1 P₂P2]].
exists s''. split.
- now exists r.
- now exists ((drop (S (| u |)) r)).
Qed.
Lemma combine_transforms u v s s' s'' : s ⟹===> s'' on u →-> s'' ⟹===> s' on v →-> s ⟹===> s' on (u⧺++v).
Proof.
intros [r₁r1 W₁W1] [r₂r2 W₂W2].
exists (prepend_path (|u|) r₁r1 r₂r2).
now apply (concat_paths (aut:=aut) (s'':=s'')).
Qed.
Lemma split_final_transforms u w s s': s ⟹F=!=> s' on (u ⧺++ w) →-> ∃exists s'',
(s ⟹F=!=> s'' on u ∧/\ s'' ⟹===> s' on w) ∨\/ (s ⟹===> s'' on u ∧/\ s'' ⟹F=!=> s' on w).
Proof.
intros [r [V [n [L F]]]].
destruct (split_path V) as [s'' [P₁P1 P₂P2]].
exists s''.
decide (n ≤<= S(|u|)) as [D|D].
- left. split.
+ exists r. split; firstorder.
+ now exists (drop (S (| u |)) r) .
- right. split.
+ now exists r.
+ exists (drop (S (| u |)) r). split; auto.
exists (n - (S(|u|))). split.
* simpl in L. omega.
* rewrite drop_correct. now rewrite_eq (S(|u|) + (n - S(|u|)) = n).
Qed.
Lemma combine_final_transforms_left u w s s' s'' : s ⟹F=!=> s'' on u →-> s'' ⟹===> s' on w →-> s ⟹F=!=> s' on (u⧺++w).
Proof.
intros [r₁r1 [W₁W1 [n₁n1 [L₁L1 F₁F1]]]] [r₂r2 W₂W2].
exists (prepend_path (|u|) r₁r1 r₂r2). split.
- now apply (concat_paths (aut:=aut)) with (s'':=s'').
- exists n₁n1. split.
+ simpl. omega.
+ decide (n₁n1 ≤<= |u|) as [D|D].
* now rewrite prepend_path_begin_correct.
* rewrite prepend_path_rest_correct2 with (n:=0).
-- rewrite ←<-(adjacent_paths_agree W₁W1 W₂W2). now rewrite_eq (S (|u|) = n₁n1).
-- omega.
Qed.
Lemma combine_final_transforms_right u w s s' s'' : s ⟹===> s'' on u →-> s'' ⟹F=!=> s' on w →-> s ⟹F=!=> s' on (u⧺++w).
Proof.
intros [r₁r1 W₁W1] [r₂r2 [W₂W2 [n₂n2 [L₂L2 F₂F2]]]].
exists (prepend_path (|u|) r₁r1 r₂r2). split.
- now apply (concat_paths (aut:=aut)) with (s'':=s'').
- exists (n₂n2 + S(|u|)). split.
+ simpl. omega.
+ rewrite prepend_path_rest_correct2 with (n:=n₂n2); oauto.
Qed.
Definition tilde_equiv (w v : String A) := ∀forall s s',
(s ⟹===> s' on w ↔<-> s ⟹===> s' on v) ∧/\
(s ⟹F=!=> s' on w ↔<-> s ⟹F=!=> s' on v).
Notation "w ~~~ v" := (tilde_equiv w v) (at level 60).
Lemma tilde_reflexive : reflexive tilde_equiv.
Proof.
intros w. split; tauto.
Qed.
Lemma tilde_transitive : transitive tilde_equiv.
Proof.
intros u v w UV VW.
repeat split;
destruct (UV s s') as [[uTv vTu] [uFv vFu]];
destruct (VW s s') as [[vTw wTv] [vFw wFv]];
tauto.
Qed.
Lemma tilde_symmetric : symmetric tilde_equiv.
Proof.
intros w v WV.
repeat split; destruct (WV s s') as [[uTv vTu] [uFv vFu]]; tauto.
Qed.
Lemma tilde_equivalence : equiv tilde_equiv.
Proof.
unfold equiv. auto using tilde_reflexive, tilde_transitive, tilde_symmetric.
Qed.
~~~ is a congruence relation
Definition congruence (R : String A →-> String A →-> Prop) := ∀forall (u v w : String A), R u v →-> R (u ⧺++ w) (v ⧺++ w).
Hint Unfold tilde_equiv.
Lemma tilde_congruence : congruence tilde_equiv.
Proof.
intros u v w UV.
split.
- split; intros T; destruct (split_transforms T) as [s'' [P₁P1 P₂P2]];
apply (combine_transforms) with (s'':=s''); destruct (UV s s'') as [[? ?][? ?]]; auto.
- split; intros T; destruct (split_final_transforms T) as [s'' [[F₁F1 P₂P2]|[P₁P1 F₂F2]]];
[ apply combine_final_transforms_left with (s'':=s'') |
apply combine_final_transforms_right with (s'':=s'')|
apply combine_final_transforms_left with (s'':=s'') |
apply combine_final_transforms_right with (s'':=s'') ];
destruct (UV s s'') as [[? ?] [? ?]]; auto.
Qed.
Extensionality of ~~~
Lemma transforms_extensional w w' s s': s ⟹===> s' on w →-> w == w' →-> s ⟹===> s' on w'.
Proof.
intros [r P] EW.
exists r. now apply (path_extensional (w:=w)).
Qed.
Lemma final_transforms_extensional w w' s s': s ⟹F=!=> s' on w →-> w == w' →-> s ⟹F=!=> s' on w'.
Proof.
intros [r [P [n Q]]] EW.
exists r. split.
- now apply (path_extensional (w:=w)).
- exists n. split.
+ destruct EW as [EL _]. now rewrite ←<-EL.
+ tauto.
Qed.
Lemma tilde_extensional w v w' v': w ~~~ v →-> w == w' →-> v == v' →-> w' ~~~ v'.
Proof.
intros WV EW EV.
pose (EW' := string_equal_symmetric EW); pose (EV' := string_equal_symmetric EV).
unfold tilde_equiv.
intros s s'. repeat split; intros T.
- apply (transforms_extensional (w:=v)); auto. apply WV.
now apply (transforms_extensional (w:=w')).
- apply (transforms_extensional (w:=w)); auto. apply WV.
now apply (transforms_extensional (w:=v')).
- apply (final_transforms_extensional (w:=v)); auto. apply WV.
now apply (final_transforms_extensional (w:=w')).
- apply (final_transforms_extensional (w:=w)); auto. apply WV.
now apply (final_transforms_extensional (w:=v')).
Qed.
Decidability of ~~~
Lemma bound_path_unchanged r w (s s':state aut): path r w s s' →-> path (to_seq (to_bounded (m:=S (|w|)) r)) w s s'.
Proof.
intros [V [B E]]. repeat split.
- apply bounded_run_is_valid_path; oauto.
- rewrite bounded_unchanged; oauto.
- rewrite bounded_unchanged; oauto.
Qed.
Instance dec_transforms : ∀forall s s' w, dec (s ⟹===> s' on w).
Proof.
intros s s' w. unfold transforms.
enough (dec (∃exists r : (state aut) ^ (finType_Le_K (S (|w|))), path (to_seq r) w s s')) as H.
- destruct H as [H|H].
+ left. destruct H as [r H]. now exists (to_seq r).
+ right. intros [r E]. apply H. exists (to_bounded r).
now apply bound_path_unchanged.
- auto.
Defined.
Lemma there_is_final_index (w:String A) (r: (state aut) ^ (finType_Le_K (S (|w|)))) (L : Le_K (S (| w |))):
final_state (applyVect r L) →-> ∃exists n, n ≤<= S (| w |) ∧/\ final_state (to_seq r n).
Proof.
intros V.
destruct L as [n L'] eqn:E.
assert (n ≤<= S(|w|)) as L''. { change (le_k (S (|w|)) n). rewrite pure_equiv. apply L'. }
exists n. split;auto.
rewrite ←<-E in V.
rewrite (to_seq_unchanged r L'' ).
assert(create_Le_K L'' = L) as H. { rewrite E. unfold create_Le_K. f_equal. apply pure_eq. }
now rewrite H.
Qed.
Instance dec_transforms_final : ∀forall s s' w, dec(s ⟹F=!=> s' on w).
Proof.
intros s s' w. unfold transforms_final.
enough (dec (∃exists r : (state aut) ^ (finType_Le_K (S (|w|))), path (to_seq r) w s s' ∧/\
(∃exists L: Le_K (S (| w |)), final_state (applyVect r L)))) as H.
- destruct H as [H|H].
+ left. destruct H as [r [H₁H1 [L H₂H2]]]. exists (to_seq r). split; auto.
apply (there_is_final_index H₂H2).
+ right. intros [r [E₁E1 [n [L E₂E2]]]]. apply H. exists (to_bounded r). split.
* now apply bound_path_unchanged.
* exists (create_Le_K L). now rewrite (to_bounded_unchanged).
- auto.
Defined.
Given ⟹===> or ⟹F=!=> we can compute the run on the NFA
Lemma finType_cc_sigma (X: finType) (p: X →-> Prop) (dec_p: ∀forall x, dec (p x)): (∃exists x, p x) →-> (ΣSigma x, p x).
Proof.
intros E.
destruct (finType_cc dec_p E) as [x px].
exists x; auto.
Qed.
Arguments finType_cc [X] [p] [D] _.
Lemma compute_run_transforms s s' w : s ⟹===> s' on w →-> ΣSigma r, path r w s s'.
Proof.
intros T.
enough (ΣSigma (r: (state aut) ^ (finType_Le_K (S (|w|)))), path (to_seq r) w s s').
- destruct X as [r P]. now exists (to_seq r).
- apply finType_cc_sigma.
+ auto.
+ destruct T as [r P]. exists (to_bounded r).
now apply bound_path_unchanged.
Qed.
(* Need the products instead of conjunctions in this lemma because we will destruct it in functions later *)
Lemma compute_run_final_transforms s s' w : s ⟹F=!=> s' on w →-> ΣSigma r, prod (path r w s s') (ΣSigma n, prod (n ≤<= S (|w|)) (final_state (r n))).
Proof.
intros T.
enough (ΣSigma (r: (state aut) ^ (finType_Le_K (S (|w|)))), prod (path (to_seq r) w s s')((ΣSigma (L : Le_K (S (| w |))), final_state (applyVect r L)))).
- destruct X as [r [P₁P1 [L P₂P2]]]. destruct L as [n L'] eqn:E.
exists (to_seq r). split;auto.
assert (n ≤<= S(|w|)) as L'' by (rewrite pure_equiv; apply L').
exists n. split; auto.
rewrite ←<-E in P₂P2. rewrite (to_seq_unchanged r L'').
assert(create_Le_K L'' = L) as H. { rewrite E. unfold create_Le_K. f_equal. apply pure_eq. }
now rewrite H.
- enough (∃exists (r: (state aut) ^ (finType_Le_K (S (|w|)))), (path (to_seq r) w s s') ∧/\ (∃exists (L : Le_K (S (| w |))), final_state (applyVect r L))).
+ destruct (finType_cc H) as [r [P₁P1 P₂P2]].
exists r. split; auto.
destruct (finType_cc P₂P2) as [L P₃P3]. now exists L.
+ destruct T as [r [P₁P1 [n [P₂P2 P₃P3]]]].
exists (to_bounded r). split.
* now apply bound_path_unchanged.
* exists (create_Le_K P₂P2).
now rewrite to_bounded_unchanged.
Qed.
Definition EquivalenceClassIndex := (? finType_bool) ^ (state aut (x) state aut).
Definition TildeEquivalenceClass (i : EquivalenceClassIndex) : StringLang A := λfun w ⇒=>
∀forall s, ∀forall s', match (applyVect i (s,s')) with
| None ⇒=> ¬~ (s ⟹===> s' on w)
| Some false ⇒=> (s ⟹===> s' on w) ∧/\ ~(s ⟹F=!=> s' on w)
| Some true ⇒=> s ⟹F=!=> s' on w
end.
Notation "{[ i ]}" := (TildeEquivalenceClass i) (at level 0).
Definition tilde_eq_class w : EquivalenceClassIndex:= (vectorise (λfun z ⇒=> match z with
(s,s') ⇒=> if (decision (s ⟹===> s' on w))
then if (decision (s ⟹F=!=> s' on w))
then Some true
else Some false
else None end)).
Lemma tilde_eq_class_correct w: ⟦{[tilde_eq_class w⟧]} w.
Proof.
unfold tilde_eq_class. intros s s'.
rewrite apply_vectorise_inverse.
decide (s ⟹===> s' on w) as [D|D].
- decide (s ⟹F=!=> s' on w) as [D₂D2|D₂D2]; auto.
- auto.
Qed.
Lemma equivalence_class_closed i u w: ⟦{[i⟧]} w →-> u ~~~ w →-> ⟦{[i⟧]} u.
Proof.
intros WI UW s s'.
specialize (WI s s').
destruct (applyVect i (s,s')) as [[|]|] .
- now apply UW.
- split.
+ now apply UW.
+ intros NU. apply WI. now apply UW.
- intros NU. apply WI. now apply UW.
Qed.
Lemma equivalent_in_equivalence_class i w w': ⟦{[i⟧]} w →-> ⟦{[i⟧]} w' →-> w ~~~ w'.
Proof.
intros WI W'W'I s s'.
specialize (WI s s'). specialize (W'W'I s s').
destruct (applyVect i (s,s')) as [[|]|].
- repeat split; auto using final_transform_implies_transform.
- destruct WI;destruct W'W'I. repeat split; intros L; auto ; try (exfalso ;auto).
- repeat split; intros L; exfalso; auto using final_transform_implies_transform .
Qed.
Lemma equivalent_if_same_equivalence_class w w': tilde_eq_class w = tilde_eq_class w' →-> w ~~~ w'.
Proof.
intros E.
apply (equivalent_in_equivalence_class (i := tilde_eq_class w)).
- apply tilde_eq_class_correct.
- rewrite E. apply tilde_eq_class_correct.
Qed.
Lemma equivalent_drop n m k j v: k ≤<= n < m →->
⟦{[j⟧]} (extract n m v) →->
⟦{[j⟧]} (extract (n - k) (m - k) (drop k v)) .
Proof.
intros L E.
apply (equivalence_class_closed E).
apply (tilde_extensional (w:=(extract n m v)) (v:=(extract n m v))).
- apply tilde_reflexive.
- split.
+ simpl. omega.
+ intros i iL. simpl.
repeat rewrite drop_correct. f_equal. omega.
- apply string_equal_reflexive.
Qed.
Lemma tilde_eq_class_congruence v w u: tilde_eq_class w = tilde_eq_class v →-> tilde_eq_class (w ⧺++ u) = tilde_eq_class (v ⧺++ u).
Proof.
intros E.
pose (Q := equivalent_if_same_equivalence_class E).
pose (C:=tilde_congruence u Q).
apply vector_extensionality.
unfold tilde_eq_class. simpl. unfold getImage. apply list_eq.
induction (elem (state aut (x) state aut)); intros n.
- reflexivity.
- simpl. destruct n; simpl.
+ destruct a as [s s']. decide (s ⟹===> s' on (w ⧺++ u)) as [D|D].
* decide (s ⟹F=!=> s' on (w ⧺++ u)) as [D'|D'].
-- repeat rewrite decision_true; auto; now apply C.
-- rewrite decision_true. rewrite decision_false; auto.
++ intros T. apply C in T. tauto.
++ now apply C.
* rewrite decision_false. reflexivity.
intros T. apply C in T. tauto.
+ apply IHl.
Qed.
Instance dec_tilde_eq_class i w: dec( ⟦{[i⟧]} w).
Proof.
unfold TildeEquivalenceClass.
apply finType_forall_dec. intros s.
apply finType_forall_dec. intros s'.
destruct (applyVect i (s,s')) as [[|]|]; auto.
Defined.
Equivalence classes can be recognized by NFAs
There aretwo ways to show this: using Myhill Nerode or Closure Properties of NFAs
Myhill-Nerode is only proven for Strings including the empty String. We do not prove it here.
Quickly define EStrings (String including the empty one) and the EString language of an NFA
Definition EString := option (String A).
Definition econcat (s₁s1 s₂s2: EString) := match s₁s1,s₂s2 with
| None, None ⇒=> None
| None, Some _ ⇒=> s₂s2
| Some _ , None ⇒=> s₁s1
| Some s₁s1, Some s₂s2 ⇒=> Some (s₁s1 ⧺++ s₂s2) end.
Definition seaccepting (aut: NFA A) r s := match s with
| None ⇒=> initial_state (r 0) ∧/\ final_state (aut:=aut) (r 0)
| Some w ⇒=> saccepting r w
end.
Definition selanguage (aut:NFA A) := λfun w ⇒=> ∃exists r, seaccepting (aut:=aut) r w.
Myhill-Nerode Theorem, without proof
Definition right_congruent (X: Type) (f: EString →-> X) := ∀forall x y, f x = f y →-> ∀forall a, f (econcat x a) = f (econcat y a).
Definition classifier (X: finType) (f: EString →-> X) := right_congruent f.
Definition refines (X: finType) (f:EString →->X) (L: Language EString) := ∀forall x y, f x = f y →-> (L x ↔<-> L y).
Definition MyhillNerode (X:finType) (f: EString →-> X) (L: Language EString) :=
(∀forall s, dec (L s)) →-> classifier f →-> refines f L →-> { aut| selanguage aut =L=$= L}.
Lemma equalSELangImpliesEqualSLang (a: NFA A) (L: StringLang A) (P:Prop): selanguage a =L=$= (λfun (s:EString) ⇒=> match s with
| None ⇒=> P
| Some w ⇒=> L w
end ) →-> LSL_S a =L=$= L.
Proof.
intros E w.
now specialize (E (Some w)).
Qed.
No we obtain the desired NFA to recognize a equivalence class when we use the equivalence classes as classifier.
Lemma tilde_equiv_class_NFA_recognizable_MyhillNerode (i:EquivalenceClassIndex) : (∀forall X f L, MyhillNerode (X:=X) f L) →->
ΣSigma aut, slanguage aut =L=$= ⟦{[i⟧]}.
Proof.
intros M.
pose (f:= λfun (s:EString) ⇒=> match s with
| None ⇒=> None
| Some w ⇒=> Some (tilde_eq_class w)
end).
pose (L:= λfun(s:EString) ⇒=> match s with
| None ⇒=> False
| Some w ⇒=> ⟦{[i⟧]} w
end).
assert (∀forall s, dec (L s)) as decL. { intros s. unfold L. destruct s; auto. }
assert (classifier f) as clasF. { unfold f. intros x y E a. destruct x,y,a ;simpl; try discriminate; auto.
f_equal. apply tilde_eq_class_congruence. congruence. }
assert (refines f L) as ref. { unfold f, L. intros x y E. destruct x as [w|]; destruct y as [v|]; try discriminate.
- split.
+ intros W. apply (equivalence_class_closed W). apply equivalent_if_same_equivalence_class. congruence.
+ intros V. apply (equivalence_class_closed V). apply equivalent_if_same_equivalence_class. congruence.
- tauto. }
destruct (M (? EquivalenceClassIndex) f L decL clasF ref) as [a P].
exists a.
unfold f, L in *.
now apply (equalSELangImpliesEqualSLang (P:=False)).
Qed.
End TildeEquivalenceClassRecognizableMyhillNerode.
This Section is not as nice, but it is not as intersting. If I would use the automata of the
Doczkal library to have a proof for Myhill Nerode and to apply the section before,
but because I use the finite types of Jan's bachelor thesis it was right easy to show the equivalence of my NFAs to his
and to obtain closure properties from them
Section TildeEqivalenceClassRecognizable.
Hint Resolve final_state_dec.
Hint Resolve initial_state_dec.
Hint Resolve transition_dec.
Hint Resolve finType_exists_dec.
Section TransformsRecognizable.
Variable (startS : state aut).
Variable (endS: state aut).
Definition tf_state := (state aut).
Definition tf_state_initial s := s = startS.
Definition tf_state_final s := s = endS.
Definition tf_transition s a s' := transition (aut:=aut) s a s'.
Lemma tf_state_initial_dec s : dec(tf_state_initial s). Proof. unfold tf_state_initial. auto. Qed.
Lemma tf_state_final_dec s : dec(tf_state_final s). Proof. unfold tf_state_final. auto. Qed.
Lemma tf_transition_dec s a s': dec (tf_transition s a s'). Proof. unfold tf_transition. auto. Qed.
Definition tf_aut := mknfa tf_transition_dec tf_state_initial_dec tf_state_final_dec.
Lemma tf_accepts_tranforms w: (startS ⟹===> endS on w)-> LSL_S tf_aut w.
Proof.
intros [r [V [B E]]].
exists r.
repeat split; auto.
Qed.
Lemma tf_is_transforms w: LSL_S tf_aut w →-> (startS ⟹===> endS on w).
Proof.
intros [r [V [I F]]].
exists r. repeat split; auto.
Qed.
Lemma tf_recognizes_transforms w : startS ⟹===>endS on w ↔<-> (LSL_S tf_aut w).
Proof.
split. apply tf_accepts_tranforms. apply tf_is_transforms.
Qed.
End TransformsRecognizable.
Section TransformsFinalRecognizable.
Variable (startS : state aut).
Variable (endS: state aut).
Definition tff_state := (state aut) (x) finType_bool.
Definition tff_state_initial s := s = (startS,false) ∨\/ (s = (startS,true) ∧/\ final_state startS).
Definition tff_state_final s := s = (endS, true).
Definition tff_transition s a s' := match s,s' with
| (s, true),(s',true) ⇒=> transition (aut:=aut) s a s'
| (s, false), (s', true) ⇒=> transition (aut:=aut) s a s' ∧/\ final_state s'
| (s, false), (s', false) ⇒=> transition (aut:=aut) s a s'
| _,_ ⇒=> False
end.
Lemma tff_state_initial_dec s : dec(tff_state_initial s). Proof. unfold tff_state_initial. auto. Qed.
Lemma tff_state_final_dec s : dec(tff_state_final s). Proof. unfold tff_state_final. auto. Qed.
Lemma tff_transition_dec s a s': dec (tff_transition s a s'). Proof. unfold tff_transition. destruct s as [s [|]];destruct s' as[s' [|]]; auto. Qed.
Definition tff_aut := mknfa tff_transition_dec tff_state_initial_dec tff_state_final_dec.
Lemma tff_accepts_tranforms_final w: (startS ⟹F=!=> endS on w)-> LSL_S tff_aut w.
Proof.
intros [r [[V [B E]] [k [Lk Fk]]]].
exists (λfun n ⇒=> if (decision (n < k))
then (r n, false)
else (r n, true)).
repeat split.
- intros n L.
decide (n < k).
+ decide (S n < k).
* now apply V.
* simpl. split.
-- now apply V.
-- now rewrite_eq (S n = k).
+ rewrite decision_false by omega. simpl. now apply V.
- unfold sinitial.
decide (0 < k).
+ simpl. rewrite B. unfold tff_state_initial. tauto.
+ simpl. unfold tff_state_initial. rewrite B.
rewrite_eq (k = 0) in Fk. rewrite B in Fk. tauto.
- simpl. unfold tff_state_final.
rewrite decision_false by omega.
now rewrite E.
Qed.
Lemma tff_is_transforms_final w: LSL_S tff_aut w →-> startS ⟹F=!=> endS on w.
Proof.
intros [r [V [I F]]].
exists (seq_map fst r).
repeat split; unfold seq_map.
- intros n L.
specialize (V n).
destruct (r n) as[sn [|]]; destruct (r (S n)) as[ sSn [|]]; simpl; simpl in V; try (now apply V).
contradiction V.
- unfold sinitial in I.
destruct (r 0).
simpl in I. unfold tff_state_initial in I.
simpl. destruct I as [I | [I _]]; congruence.
- unfold sfinal in F.
destruct (r (S(|w|))).
simpl. simpl in F. unfold tff_state_final in F.
congruence.
- assert (0 ≤<= S(|w|)) as H by omega.
pose ( p := λfun (s:tff_state) ⇒=> snd s = true).
assert (p (r (S(|w|)))) as H₂H2. { unfold p. simpl in F. unfold tff_state_final in F. rewrite F. now simpl. }
assert (∀forall s, dec (p s)) as decP. { intros s. unfold p. auto. }
destruct (can_find_next_position decP H H₂H2) as [n [L [P Q]]].
exists n. split.
+ omega.
+ destruct n.
* unfold p in P.
destruct I as [I | [I₁I1 I₂I2]].
-- exfalso. destruct (r 0).
simpl in P. rewrite P in I. congruence.
-- now rewrite I₁I1.
* specialize (V n).
unfold p in P.
assert (n ≤<= |w|) as Hz by omega.
specialize (V Hz).
simpl in V. unfold tff_transition in V.
destruct (r n) as [rn [|]] eqn:N; destruct (r (S n)) as [rSn [|]] eqn:SN.
-- exfalso. apply (Q n).
++ omega.
++ now rewrite N.
-- exfalso. simpl in P. congruence.
-- now simpl.
-- exfalso. simpl in P. congruence.
Qed.
Lemma tff_recognizes_transforms_final w: (startS ⟹F=!=> endS on w) ↔<-> LSL_S tff_aut w.
Proof.
split. apply tff_accepts_tranforms_final. apply tff_is_transforms_final.
Qed.
End TransformsFinalRecognizable.
Context { V : EquivalenceClassIndex}.
Definition s_s's_s'_pair_aut (p :(state aut) (x) (state aut)):=
let (s, s') := p in
match (applyVect V (s, s')) with
| None ⇒=> scomplement (tf_aut s s')
| Some false ⇒=> sdiff (tf_aut s s') (tff_aut s s')
| Some true ⇒=> (tff_aut s s')
end.
Definition tilde_equiv_class_aut := fold_right
sintersect all_aut
(map s_s's_s'_pair_aut (elem ((state aut) (x) (state aut)))) .
Lemma tilde_equiv_class_aut_accepts_Equiv_class: ⟦{[V⟧]} ⊆<$= LSL_S tilde_equiv_class_aut.
Proof.
intros w wV. unfold TildeEquivalenceClass in wV. unfold tilde_equiv_class_aut.
induction (elem (state aut (x) state aut)).
- simpl. apply all_aut_accepts_everything.
- simpl. apply sintersect_correct. split.
+ unfold s_s's_s'_pair_aut.
destruct a as [s s'].
specialize (wV s s').
destruct (applyVect V (s, s')) as [[|]|] eqn:H.
* now apply tff_recognizes_transforms_final.
* apply sdiff_correct. split.
-- now apply tf_recognizes_transforms.
-- intros N. apply wV. now apply tff_recognizes_transforms_final.
* apply scomplement_correct.
intros T. apply wV.
now apply tf_recognizes_transforms.
+ apply IHl.
Qed.
Lemma tilde_equiv_class_aut_is_equiv_class: LSL_S tilde_equiv_class_aut ⊆<$= ⟦{[V⟧]}.
Proof.
intros w wA.
unfold tilde_equiv_class_aut in wA.
intros s s'.
assert (LSL_S (s_s's_s'_pair_aut (s,s')) w) as H. {
apply (many_aut_intersection wA).
apply in_map_iff.
exists ((s,s')).
split;auto.
}
unfold s_s's_s'_pair_aut in H.
destruct (applyVect V (s, s')) as [[|]|].
- now apply tff_recognizes_transforms_final.
- apply sdiff_correct in H. destruct H as [H₁H1 H₂H2]. split.
+ now apply tf_recognizes_transforms.
+ intros F. apply H₂H2. now apply tff_recognizes_transforms_final.
- intros F.
apply scomplement_correct in H.
apply H.
now apply tf_recognizes_transforms.
Qed.
Lemma tilde_equiv_class_NFA_recognizable: ⟦{[V⟧]} =L=$= LSL_S tilde_equiv_class_aut.
Proof.
intros w. split.
- apply tilde_equiv_class_aut_accepts_Equiv_class.
- apply tilde_equiv_class_aut_is_equiv_class.
Qed.
End TildeEqivalenceClassRecognizable.
Corollary eq_classes_extensional i: StringLang_Extensional ⟦{[i⟧]}.
Proof.
intros w w' C E.
(* Could be derived from definiton, but I showed that all i are finite
automaton recognizable and languages are extensional *)
pose (f := tilde_equiv_class_NFA_recognizable (V:=i)).
apply f.
apply (slanguage_extensional (w:=w)); auto.
now apply f.
Qed.
NFA recognizing V ·o Wω^00
Definition VW_aut i j := projT₁projT1 (sNFA_sNFA_to_omega_Buechi (tilde_equiv_class_aut (V:=i)) (tilde_equiv_class_aut (V:=j))).
Lemma VW_aut_correct i j: LBL_B (VW_aut i j) =L=$= ⟦{[i⟧]}·o⟦{[j⟧]}ω^00.
Proof.
unfold VW_aut.
destruct (sNFA_sNFA_to_omega_Buechi) as [a P]. simpl.
intros w; split.
- intros B. apply P in B. destruct B as [n [Q₁Q1 [f [Inc [Z Q₂Q2]]]]].
exists n. split.
+ now apply (tilde_equiv_class_NFA_recognizable (V:= i) (mkstring w n) ).
+ exists f; repeat split; auto. intros k.
now apply (tilde_equiv_class_NFA_recognizable (V:= j) (extract (f k) (f (S k)) (drop (S n) w))).
- intros B. apply P. destruct B as [n [B₁B1 [f [Inc [Z B₂B2]]]]].
exists n. split.
+ now apply (tilde_equiv_class_NFA_recognizable (V:= i) (mkstring w n)).
+ exists f; repeat split; auto. intros k.
now apply (tilde_equiv_class_NFA_recognizable (V:= j) (extract (f k) (f (S k)) (drop (S n) w))).
Qed.
Lemma VW_aut_correct i j: LBL_B (VW_aut i j) =L=$= ⟦{[i⟧]}·o⟦{[j⟧]}ω^00.
Proof.
unfold VW_aut.
destruct (sNFA_sNFA_to_omega_Buechi) as [a P]. simpl.
intros w; split.
- intros B. apply P in B. destruct B as [n [Q₁Q1 [f [Inc [Z Q₂Q2]]]]].
exists n. split.
+ now apply (tilde_equiv_class_NFA_recognizable (V:= i) (mkstring w n) ).
+ exists f; repeat split; auto. intros k.
now apply (tilde_equiv_class_NFA_recognizable (V:= j) (extract (f k) (f (S k)) (drop (S n) w))).
- intros B. apply P. destruct B as [n [B₁B1 [f [Inc [Z B₂B2]]]]].
exists n. split.
+ now apply (tilde_equiv_class_NFA_recognizable (V:= i) (mkstring w n)).
+ exists f; repeat split; auto. intros k.
now apply (tilde_equiv_class_NFA_recognizable (V:= j) (extract (f k) (f (S k)) (drop (S n) w))).
Qed.
Now put a lot on the table: given two sequences ow ow' and an accepting run for ow
And both strings are pointwise equivalent to some v +++ (w₁w1 ++ w₂w2 ++ ..)
Variable (v v' : String A).
Variable (w w' : Seq (String A)).
Variable (Eq: (∀forall n : ℕnat, ow n = (v ⧻+++ (concat∞concat_inf w)) n)).
Variable (Eq':(∀forall n : ℕnat, ow' n = (v' ⧻+++ (concat∞concat_inf w')) n)).
Variable (w w' : Seq (String A)).
Variable (Eq: (∀forall n : ℕnat, ow n = (v ⧻+++ (concat∞concat_inf w)) n)).
Variable (Eq':(∀forall n : ℕnat, ow' n = (v' ⧻+++ (concat∞concat_inf w')) n)).
and the v v' resp wi w'i are from the same ~ equivalence class
Variables (i j: EquivalenceClassIndex).
Variables (V: ⟦{[i⟧]} v )(V': ⟦{[i⟧]} v').
Variables (W: (∀forall n, ⟦{[j⟧]} (w n) ))(W': (∀forall n, ⟦{[j⟧]} (w' n))).
Variables (V: ⟦{[i⟧]} v )(V': ⟦{[i⟧]} v').
Variables (W: (∀forall n, ⟦{[j⟧]} (w n) ))(W': (∀forall n, ⟦{[j⟧]} (w' n))).
and r gets partitioned into r0 R according to v w
Variable (r₀r0 : String (state aut)).
Variable (R : Seq (String (state aut))).
Variable (EqR: (∀forall n, r n = (r₀r0 ⧻+++ concat∞concat_inf R) n)).
Variable (eqLengthv: (|r₀r0| = |v|)).
Variable (valid_r0: (valid_path (seq r₀r0) v)).
Variable (agree_r0: (r₀r0 [S(|r₀r0|)] = (R 0) [0])).
Variable (valid_R : (∀forall k, |R k| = |w k| ∧/\
valid_path (seq (R k)) (w k))).
Variable (agree_R: (∀forall k, (R k)[ S(|R k|)] = (R (S k)) [0])).
Variable (R : Seq (String (state aut))).
Variable (EqR: (∀forall n, r n = (r₀r0 ⧻+++ concat∞concat_inf R) n)).
Variable (eqLengthv: (|r₀r0| = |v|)).
Variable (valid_r0: (valid_path (seq r₀r0) v)).
Variable (agree_r0: (r₀r0 [S(|r₀r0|)] = (R 0) [0])).
Variable (valid_R : (∀forall k, |R k| = |w k| ∧/\
valid_path (seq (R k)) (w k))).
Variable (agree_R: (∀forall k, (R k)[ S(|R k|)] = (R (S k)) [0])).
Then we can show that there is an accepting run for ow'
(* predicate that tells whether in R k is a final state, so wether on w k there is a final state *)
Definition W_final := λfun k ⇒=> visits_final (R k).
Definition pure_W_final := pure W_final.
Lemma W_final_iff k: W_final k ↔<-> pure_W_final k.
Proof.
unfold pure_W_final. apply pure_equiv.
Qed.
Instance dec_pure_W_final: ∀forall k, dec (pure_W_final k).
Proof.
intros k. unfold pure_W_final.
decide (W_final k) as [D|D].
- left. now apply pure_equiv.
- right. intros np.
apply D. rewrite pure_equiv. apply np.
Qed.
Lemma v_transforms: (r₀r0 [0]) ⟹===> (R 0) [0] on v .
Proof.
exists (seq r₀r0).
rewrite ←<-agree_r0. split; auto.
Qed.
Lemma W_transforms: ∀forall k, (R k)[0] ⟹===> (R (S k)) [0] on (w k) ∧/\
(W_final k →-> (R k)[0] ⟹F=!=> (R (S k)) [0] on (w k)).
Proof.
intros k. specialize (agree_R k). destruct (valid_R k) as [E P]. split.
- exists (seq (R k)). split.
+ trivial.
+ now rewrite ←<-E.
- intros F. exists (seq (R k)). repeat split.
+ assumption.
+ now rewrite ←<-E.
+ destruct F as [m [L F]]. exists m. split; oauto.
Qed.
Lemma v'_transforms: (r₀r0 [0]) ⟹===> (R 0) [0] on v'.
Proof.
apply (equivalent_in_equivalence_class V V').
apply v_transforms.
Qed.
Lemma W'_transforms :
∀forall k, (R k)[0] ⟹===> (R (S k)) [0] on (w' k) ∧/\
(pure_W_final k →-> (R k)[0] ⟹F=!=> (R (S k)) [0] on (w' k)).
Proof.
intros k. split.
- apply (equivalent_in_equivalence_class (W k) (W' k)). apply W_transforms.
- intros F. rewrite ←<-W_final_iff in F.
apply (equivalent_in_equivalence_class (W k) (W' k)). now apply W_transforms.
Qed.
Build the accepting run for ow' Runs for the strings in W'. Need to check whether W is final to ensure that the run for W' is final, too
Definition R' : Seq (String (state aut)):= λfun k ⇒=> match (dec_pure_W_final k) with
| left B ⇒=> match (W'_transforms k ) with
| conj _ Z ⇒=> mkstring (projT₁projT1 (compute_run_final_transforms (Z B))) (|w' k|) end
| _ ⇒=> match (W'_transforms k) with
| conj Z _ ⇒=> mkstring (projT₁projT1 (compute_run_transforms Z)) (|w' k|) end end.
| left B ⇒=> match (W'_transforms k ) with
| conj _ Z ⇒=> mkstring (projT₁projT1 (compute_run_final_transforms (Z B))) (|w' k|) end
| _ ⇒=> match (W'_transforms k) with
| conj Z _ ⇒=> mkstring (projT₁projT1 (compute_run_transforms Z)) (|w' k|) end end.
Run on ow' is obtained from concatting the run on v' to R'
Definition r' : (Run aut):= (mkstring (projT₁projT1 (compute_run_transforms v'_transforms)) (|v'|)) ⧻+++ (concat∞concat_inf R').
Ltac destruct_compute_run_maybe_final_transforms := try (destruct compute_run_final_transforms); try (destruct compute_run_transforms).
Ltac destruct_in_R' := destruct dec_pure_W_final; destruct W'W'_transforms; destruct_compute_run_maybe_final_transforms.
Lemma R'k0_eq_Rk0: ∀forall k, (R' k) [0] = (R k) [0].
Proof.
intros k. unfold R'.
destruct_in_R'; simpl; unfold path in *; tauto.
Qed.
Lemma valid_r' : valid_run r' ow'.
Proof.
apply (valid_run_extensional (r:=r') (w:=v' ⧻+++ concat∞concat_inf w')); auto.
unfold r'. apply prepend_string_is_valid.
- reflexivity.
- destruct (compute_run_transforms v'_transforms) as [x P]. simpl. apply P.
- destruct (compute_run_transforms v'_transforms) as [x P].
unfold concat∞concat_inf. simpl. rewrite R'k0_eq_Rk0. apply P.
- unfold R'. apply concat_inf_is_valid. intros n. repeat split.
+ now destruct_in_R'.
+ destruct_in_R'; unfold path in *; simpl; tauto.
+ assert (∀forall x y, x (S (| w' n |)) = (R (S n)) [0] →-> y 0 = (R (S n)) [0] →-> x (S (| w' n |)) = y 0) as T. {
intros x y E₁E1 E₂E2. now rewrite E₁E1, E₂E2. }
repeat destruct_in_R'; simpl; unfold path in *; apply T; tauto.
Qed.
Lemma initial_r' : initial r'.
Proof.
unfold initial, r'. simpl.
destruct (compute_run_transforms v'_transforms) as [x [? [B E]]]. simpl.
rewrite prepend_path_begin_correct by omega.
rewrite B.
specialize (EqR 0). unfold concat∞concat_inf in EqR. simpl in EqR.
rewrite prepend_path_begin_correct in EqR by omega.
rewrite ←<-EqR. apply Acc.
Qed.
Ltac destruct_compute_run_maybe_final_transforms := try (destruct compute_run_final_transforms); try (destruct compute_run_transforms).
Ltac destruct_in_R' := destruct dec_pure_W_final; destruct W'W'_transforms; destruct_compute_run_maybe_final_transforms.
Lemma R'k0_eq_Rk0: ∀forall k, (R' k) [0] = (R k) [0].
Proof.
intros k. unfold R'.
destruct_in_R'; simpl; unfold path in *; tauto.
Qed.
Lemma valid_r' : valid_run r' ow'.
Proof.
apply (valid_run_extensional (r:=r') (w:=v' ⧻+++ concat∞concat_inf w')); auto.
unfold r'. apply prepend_string_is_valid.
- reflexivity.
- destruct (compute_run_transforms v'_transforms) as [x P]. simpl. apply P.
- destruct (compute_run_transforms v'_transforms) as [x P].
unfold concat∞concat_inf. simpl. rewrite R'k0_eq_Rk0. apply P.
- unfold R'. apply concat_inf_is_valid. intros n. repeat split.
+ now destruct_in_R'.
+ destruct_in_R'; unfold path in *; simpl; tauto.
+ assert (∀forall x y, x (S (| w' n |)) = (R (S n)) [0] →-> y 0 = (R (S n)) [0] →-> x (S (| w' n |)) = y 0) as T. {
intros x y E₁E1 E₂E2. now rewrite E₁E1, E₂E2. }
repeat destruct_in_R'; simpl; unfold path in *; apply T; tauto.
Qed.
Lemma initial_r' : initial r'.
Proof.
unfold initial, r'. simpl.
destruct (compute_run_transforms v'_transforms) as [x [? [B E]]]. simpl.
rewrite prepend_path_begin_correct by omega.
rewrite B.
specialize (EqR 0). unfold concat∞concat_inf in EqR. simpl in EqR.
rewrite prepend_path_begin_correct in EqR by omega.
rewrite ←<-EqR. apply Acc.
Qed.
In order to prove that r' is final, we prove that infinitely many strings in R' visit a final state.
This may switch the next string in R', if the final state in run for (W' k) is the last state,
because this is cut off because it is equal to the first in the run of (W' (S k)).
Lemma string_final_R' k: visits_final (R k) →-> visits_final (R' k) ∨\/ visits_final (R' (S k)).
Proof.
intros WF. unfold R'. destruct dec_pure_W_final.
- unfold visits_final.
destruct W'_transforms.
destruct compute_run_final_transforms as [? [P [n F]]]. simpl.
decide (n = S (|w' k|)) as [D|D].
+ right. exists 0.
assert (∀forall y , y 0 = (R (S k)) [0] →-> final_state (y 0 )) as T. {
intros y E. rewrite E. destruct P as [_ [_ H]]. rewrite ←<-H, ←<- D. tauto. }
destruct_in_R'; simpl; split; try omega; unfold path in *; apply T; tauto.
+ left. exists n. destruct F. split; oauto.
- exfalso. apply n. now apply W_final_iff.
Qed.
Lemma infinite_final_strings_R: ∀forall n, ∃exists m, m ≥>= n ∧/\ visits_final (R m).
Proof.
assert (final (concat∞concat_inf R)) as FR. {
apply final_extensional with (r:= drop (S(|r₀r0|)) r).
- apply final_drop. apply Acc.
- intros n. rewrite drop_correct.
specialize (EqR (S(|r₀r0|) + n)).
now rewrite prepend_path_rest_correct in EqR by omega. }
apply (final_concat_inf_infinite_final_strings (aut:=aut) (runs:=R) FR ).
Qed.
Proof.
intros WF. unfold R'. destruct dec_pure_W_final.
- unfold visits_final.
destruct W'_transforms.
destruct compute_run_final_transforms as [? [P [n F]]]. simpl.
decide (n = S (|w' k|)) as [D|D].
+ right. exists 0.
assert (∀forall y , y 0 = (R (S k)) [0] →-> final_state (y 0 )) as T. {
intros y E. rewrite E. destruct P as [_ [_ H]]. rewrite ←<-H, ←<- D. tauto. }
destruct_in_R'; simpl; split; try omega; unfold path in *; apply T; tauto.
+ left. exists n. destruct F. split; oauto.
- exfalso. apply n. now apply W_final_iff.
Qed.
Lemma infinite_final_strings_R: ∀forall n, ∃exists m, m ≥>= n ∧/\ visits_final (R m).
Proof.
assert (final (concat∞concat_inf R)) as FR. {
apply final_extensional with (r:= drop (S(|r₀r0|)) r).
- apply final_drop. apply Acc.
- intros n. rewrite drop_correct.
specialize (EqR (S(|r₀r0|) + n)).
now rewrite prepend_path_rest_correct in EqR by omega. }
apply (final_concat_inf_infinite_final_strings (aut:=aut) (runs:=R) FR ).
Qed.
There are infinite final strings in r', so there are infinite final states in r',
with infinite combinatorics there is a final state occuring infinitely often
Lemma final_r' : final r'.
Proof.
unfold r'.
apply concat_inf_final_step.
apply concat_inf_is_final_not_constructive.
intros n.
destruct (infinite_final_strings_R n) as [m [L P]]; destruct (string_final_R' P).
- now exists m.
- exists (S m). split; oauto.
Qed.
Proof.
unfold r'.
apply concat_inf_final_step.
apply concat_inf_is_final_not_constructive.
intros n.
destruct (infinite_final_strings_R n) as [m [L P]]; destruct (string_final_R' P).
- now exists m.
- exists (S m). split; oauto.
Qed.
So we obtain that r' is accepting
Lemma accepting_run_for_W': ΣSigma r', accepting (aut:=aut) r' ow'.
Proof.
exists r'. repeat split; auto using valid_r', initial_r', final_r'.
Qed.
End Compatibility.
Theorem compatibility i j w: (⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ∩/$\ LBL_B aut) w →-> (⟦{[i⟧]}·o⟦{[j⟧]}ω^00) ⊆<$= LBL_B aut.
Proof.
intros [wVW [r Acc]] w' w'w'VW.
(* To get the accepting run for w', we need to cut everything *)
apply prepend_on_omega_iteration in wVW. apply prepend_on_omega_iteration in w'w'VW.
destruct wVW as [v [fw [ V [ W E]]]]. destruct w'w'VW as [v' [fw' [ V' [ W' E']]]].
assert (valid_run r (v ⧻+++ concat∞concat_inf fw)) as H. {
apply (valid_run_extensional (r:= r) (w:= w)); auto. apply Acc. }
destruct (partition_run_on_prepend_string H) as [r₀r0 [R' [P₁P1 [P₂P2 [P₃P3 [P₄P4 P₅P5] ]]]]].
destruct (partition_run_on_concat_inf P₅P5) as [R [P₆P6 [P₇P7 P₈P8]]].
destruct (accepting_run_for_W' Acc E' V V' W W' (ow:=w) (ow' := w') (r:=r) (v:=v) (v':=v') (w:=fw)(w':=fw') (i:=i)(j:=j) (r₀r0 := r₀r0) (R := R) ) as [r' A']; auto.
- intros n. decide (n ≤<= |r₀r0|).
+ rewrite prepend_path_begin_correct by omega.
specialize (P₁P1 n). now rewrite prepend_path_begin_correct in P₁P1 by omega.
+ rewrite_eq (n = S(|r₀r0|) + (n - S(|r₀r0|))).
rewrite prepend_path_rest_correct by omega.
rewrite (P₆P6 (n - S(|r₀r0|))).
specialize (P₁P1 (S(|r₀r0|) + (n - S(|r₀r0|)))).
now rewrite prepend_path_rest_correct in P₁P1 by omega.
- rewrite P₃P3. specialize (P₆P6 0). now rewrite ←<-P₆P6.
- now exists r'.
Qed.
Corollary compatibilityComplement i j w: (⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ∩/$\ (LBL_B aut)C)^$~) w →-> (⟦{[i⟧]}·o⟦{[j⟧]}ω^00) ⊆<$= (LBL_B aut)C)^$~.
Proof.
intros [IJw Cw] v IJv Bv. autounfold in *. apply Cw.
now apply (compatibility (i:=i) (j:=j) (w:=v)).
Qed.
Corollary compatibility2 i j: ⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ⊆<$= LBL_B aut ∨\/ ⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ⊆<$= (LBL_B aut)C)^$~.
Proof.
destruct (dec_language_empty_informative (aut:=(intersect (VW_aut i j) aut) )) as [D|D].
- left. destruct D as [w' L]. apply intersect_correct in L.
apply (compatibility (w:=w') (i:=i)(j:=j)).
destruct L as [L₁L1 L₂L2]. now apply VW_aut_correct in L₁L1.
- right. intros w VW.
autounfold in *. specialize (D w). intros B.
apply D. apply intersect_correct. split.
+ now apply VW_aut_correct.
+ assumption.
Qed.
Proof.
exists r'. repeat split; auto using valid_r', initial_r', final_r'.
Qed.
End Compatibility.
Theorem compatibility i j w: (⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ∩/$\ LBL_B aut) w →-> (⟦{[i⟧]}·o⟦{[j⟧]}ω^00) ⊆<$= LBL_B aut.
Proof.
intros [wVW [r Acc]] w' w'w'VW.
(* To get the accepting run for w', we need to cut everything *)
apply prepend_on_omega_iteration in wVW. apply prepend_on_omega_iteration in w'w'VW.
destruct wVW as [v [fw [ V [ W E]]]]. destruct w'w'VW as [v' [fw' [ V' [ W' E']]]].
assert (valid_run r (v ⧻+++ concat∞concat_inf fw)) as H. {
apply (valid_run_extensional (r:= r) (w:= w)); auto. apply Acc. }
destruct (partition_run_on_prepend_string H) as [r₀r0 [R' [P₁P1 [P₂P2 [P₃P3 [P₄P4 P₅P5] ]]]]].
destruct (partition_run_on_concat_inf P₅P5) as [R [P₆P6 [P₇P7 P₈P8]]].
destruct (accepting_run_for_W' Acc E' V V' W W' (ow:=w) (ow' := w') (r:=r) (v:=v) (v':=v') (w:=fw)(w':=fw') (i:=i)(j:=j) (r₀r0 := r₀r0) (R := R) ) as [r' A']; auto.
- intros n. decide (n ≤<= |r₀r0|).
+ rewrite prepend_path_begin_correct by omega.
specialize (P₁P1 n). now rewrite prepend_path_begin_correct in P₁P1 by omega.
+ rewrite_eq (n = S(|r₀r0|) + (n - S(|r₀r0|))).
rewrite prepend_path_rest_correct by omega.
rewrite (P₆P6 (n - S(|r₀r0|))).
specialize (P₁P1 (S(|r₀r0|) + (n - S(|r₀r0|)))).
now rewrite prepend_path_rest_correct in P₁P1 by omega.
- rewrite P₃P3. specialize (P₆P6 0). now rewrite ←<-P₆P6.
- now exists r'.
Qed.
Corollary compatibilityComplement i j w: (⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ∩/$\ (LBL_B aut)C)^$~) w →-> (⟦{[i⟧]}·o⟦{[j⟧]}ω^00) ⊆<$= (LBL_B aut)C)^$~.
Proof.
intros [IJw Cw] v IJv Bv. autounfold in *. apply Cw.
now apply (compatibility (i:=i) (j:=j) (w:=v)).
Qed.
Corollary compatibility2 i j: ⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ⊆<$= LBL_B aut ∨\/ ⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ⊆<$= (LBL_B aut)C)^$~.
Proof.
destruct (dec_language_empty_informative (aut:=(intersect (VW_aut i j) aut) )) as [D|D].
- left. destruct D as [w' L]. apply intersect_correct in L.
apply (compatibility (w:=w') (i:=i)(j:=j)).
destruct L as [L₁L1 L₂L2]. now apply VW_aut_correct in L₁L1.
- right. intros w VW.
autounfold in *. specialize (D w). intros B.
apply D. apply intersect_correct. split.
+ now apply VW_aut_correct.
+ assumption.
Qed.
Lemma ramseyTotality: (∀forall (f : ℕnat →-> ℕnat →-> EquivalenceClassIndex), Ramsey f) →-> (∃exists i j, (⟦{[i⟧]}·o⟦{[j⟧]}ω^00) w).
Proof.
intros R.
destruct (R (λfun n m ⇒=> tilde_eq_class (extract (min n m) (max n m) w))) as [x [g [Inc P]]].
- intros n m. simpl.
now rewrite Nat.max_comm, Nat.min_comm.
- exists (tilde_eq_class (mkstring w (pred (g 1)) )), x, (pred (g 1)). split.
+ apply tilde_eq_class_correct.
+ exists (seq_map (λfun n ⇒=> n - (g 1)) (drop 1 g)). repeat split; unfold seq_map.
* simpl. intros n. pose (Inc (S n)). destruct n.
-- omega.
-- assert (1 < (S (S n))) as H by omega. assert (1 < S (S (S n))) as H' by omega.
pose (s_monotone_strict_order_preserving Inc H).
pose (s_monotone_strict_order_preserving Inc H'). omega.
* simpl. omega.
* intros n.
pose (Inc 0). rewrite_eq (S (pred (g 1)) = g 1).
apply equivalent_drop.
-- repeat rewrite drop_correct. split.
++ apply s_monotone_order_preserving; oauto.
++ rewrite_eq (1 + S n = S(1 + n)). apply Inc.
-- repeat rewrite drop_correct.
rewrite ←<- (P (1 + n) (1 + S n)) by omega.
assert (g (1 + n ) ≤<= g (1 + S n)) . { rewrite_eq (1 + S n = S (1 + n)). pose (Inc (1 + n)). omega. }
rewrite max_r, min_l by auto.
apply tilde_eq_class_correct.
Qed.
Proof.
intros R.
destruct (R (λfun n m ⇒=> tilde_eq_class (extract (min n m) (max n m) w))) as [x [g [Inc P]]].
- intros n m. simpl.
now rewrite Nat.max_comm, Nat.min_comm.
- exists (tilde_eq_class (mkstring w (pred (g 1)) )), x, (pred (g 1)). split.
+ apply tilde_eq_class_correct.
+ exists (seq_map (λfun n ⇒=> n - (g 1)) (drop 1 g)). repeat split; unfold seq_map.
* simpl. intros n. pose (Inc (S n)). destruct n.
-- omega.
-- assert (1 < (S (S n))) as H by omega. assert (1 < S (S (S n))) as H' by omega.
pose (s_monotone_strict_order_preserving Inc H).
pose (s_monotone_strict_order_preserving Inc H'). omega.
* simpl. omega.
* intros n.
pose (Inc 0). rewrite_eq (S (pred (g 1)) = g 1).
apply equivalent_drop.
-- repeat rewrite drop_correct. split.
++ apply s_monotone_order_preserving; oauto.
++ rewrite_eq (1 + S n = S(1 + n)). apply Inc.
-- repeat rewrite drop_correct.
rewrite ←<- (P (1 + n) (1 + S n)) by omega.
assert (g (1 + n ) ≤<= g (1 + S n)) . { rewrite_eq (1 + S n = S (1 + n)). pose (Inc (1 + n)). omega. }
rewrite max_r, min_l by auto.
apply tilde_eq_class_correct.
Qed.
Notation "k1 '~~~@' k2 'at' m" :=((m > k₁k1 ∧/\ m > k₂k2) ∧/\ (extract k₁k1 m w) ~~~ (extract k₂k2 m w)) (at level 58).
Instance dec_merge_at k₁k1 k₂k2 m : dec (k₁k1 ~w~~@ k₂k2 at m).
Proof. auto. Defined.
Definition tilde_w_equiv (k k' : ℕnat) := ∃exists m, k ~w~~@ k' at m.
Notation "k1 '~w~~#' k2" := (tilde_w_equiv k₁k1 k₂k2) (at level 60).
Lemma tilde_w_extend k k' m: (k ~w~~@ k' at m) →-> ∀forall m', m' ≥>= m →-> k ~w~~@ k' at m'.
Proof.
intros W m' L.
decide (m = m').
- now subst m'.
- split.
+ omega.
+ apply (tilde_extensional (w:= (extract k m w) ⧺++ (extract m m' w)) (v:= (extract k' m w) ⧺++ (extract m m' w))).
* now apply tilde_congruence.
* apply concat_extract; omega.
* apply concat_extract; omega.
Qed.
Lemma tilde_w_index_reflexive k n : k < n →-> k ~w~~@ k at n.
Proof.
split.
- omega.
- apply tilde_reflexive.
Qed.
Lemma tilde_w_reflexive: reflexive tilde_w_equiv.
Proof.
intros s. exists (S s). apply tilde_w_index_reflexive. omega.
Qed.
Lemma tilde_w_index_symmetric k₁k1 k₂k2 m: k₁k1 ~w~~@ k₂k2 at m →-> k₂k2 ~w~~@ k₁k1 at m.
Proof.
split.
- omega.
- now apply tilde_symmetric.
Qed.
Lemma tilde_w_symmetric: symmetric tilde_w_equiv.
Proof.
intros s₁s1 s₂s2 [m [P Q]].
exists m. apply tilde_w_index_symmetric. split;auto.
Qed.
Lemma tilde_w_index_transitive k₁k1 k₂k2 k₃k3 m₁m1 m₂m2:
k₁k1 ~w~~@ k₂k2 at m₁m1 →-> k₂k2 ~w~~@ k₃k3 at m₂m2 →-> k₁k1 ~w~~@ k₃k3 at (max m₁m1 m₂m2).
Proof.
intros P₁P1 P₂P2. split.
- split.
+ apply max_le_left. omega.
+ apply max_le_right. omega.
- apply tilde_w_extend with (m':= max m₁m1 m₂m2) in P₁P1.
apply tilde_w_extend with (m':= max m₁m1 m₂m2) in P₂P2.
+ destruct P₁P1; destruct P₂P2.
apply (tilde_transitive (y:= extract k₂k2 (max m₁m1 m₂m2) w)); auto.
+ now apply max_le_right.
+ now apply max_le_left.
Qed.
Lemma tilde_w_transitive: transitive tilde_w_equiv.
Proof.
intros k₁k1 k₂k2 k₃k3 [m₁m1 P₁P1] [m₂m2 P₂P2].
exists (max m₁m1 m₂m2).
apply (tilde_w_index_transitive P₁P1 P₂P2).
Qed.
Lemma tilde_w_equivalence : equiv tilde_w_equiv.
Proof.
repeat split; auto using tilde_w_reflexive, tilde_w_transitive, tilde_w_symmetric.
Qed.
Excluded Middle for ~w~~#
Because of the unbounded quantifier in ~w~~# we cannot decide it. However, we have XM for it
Section PropositionalDecidability.
Variables k₁k1 k₂k2: ℕnat.
(* Sequence which is true if k₁k1 ~w~~# k₂k2 at n *)
Definition tilde_w_equiv_bool := λfun n ⇒=> if (decision (k₁k1 ~w~~@ k₂k2 at n)) then true else false.
Lemma tilde_w_index_equiv_iff m : k₁k1 ~w~~@ k₂k2 at m ↔<-> tilde_w_equiv_bool m = true.
Proof.
split; unfold tilde_w_equiv_bool; intros E.
- now rewrite decision_true by auto.
- decide (k₁k1 ~w~~@ k₂k2 at m).
+ auto.
+ discriminate.
Qed.
Lemma tilde_w_equiv_iff: k₁k1 ~w~~# k₂k2 ↔<-> ∃exists n, tilde_w_equiv_bool n = true.
Proof.
split; intros [m E]; exists m; now apply tilde_w_index_equiv_iff.
Qed.
Lemma tilde_w_equiv_bool_remains_true m: tilde_w_equiv_bool m = true →-> ∀forall n, n ≥>= m →-> tilde_w_equiv_bool n = true.
Proof.
intros P n L.
apply tilde_w_index_equiv_iff.
apply tilde_w_index_equiv_iff in P.
now apply (tilde_w_extend P).
Qed.
Lemma tilde_w_equiv_bool_infinite_false: infinite false tilde_w_equiv_bool ↔<-> ∀forall n, tilde_w_equiv_bool n = false.
Proof.
split.
- intros Inf n.
destruct (tilde_w_equiv_bool n ) eqn:H.
+ exfalso. destruct (Inf n) as [m [L F]].
now rewrite (tilde_w_equiv_bool_remains_true H L) in F.
+ reflexivity.
- intros F. intros n. exists n. auto.
Qed.
End PropositionalDecidability.
Lemma tilde_w_equiv_XM: rel_XM tilde_w_equiv.
Proof.
intros k₁k1 k₂k2.
destruct (finite_type_seq (tilde_w_equiv_bool k₁k1 k₂k2) ) as [[|] Inf].
- left. apply tilde_w_equiv_iff. destruct (Inf 0) as [k T]. now exists k.
- right. intros E. apply tilde_w_equiv_iff in E.
destruct E as [n T].
destruct (tilde_w_equiv_bool_infinite_false k₁k1 k₂k2) as [F _].
specialize (F Inf n).
now rewrite T in F.
Qed.
Hint Resolve dupfree_dec.
Hint Resolve nat_eq_dec.
Hint Resolve list_exists_dec.
Lemma not_tilde_w_extend k₁k1 k₂k2: ¬~ k₁k1 ~w~~# k₂k2 →-> ∀forall m, ¬~ k₁k1 ~w~~@ k₂k2 at m.
Proof.
intros NE m Em. apply NE. now exists m.
Qed.
Variables k₁k1 k₂k2: ℕnat.
(* Sequence which is true if k₁k1 ~w~~# k₂k2 at n *)
Definition tilde_w_equiv_bool := λfun n ⇒=> if (decision (k₁k1 ~w~~@ k₂k2 at n)) then true else false.
Lemma tilde_w_index_equiv_iff m : k₁k1 ~w~~@ k₂k2 at m ↔<-> tilde_w_equiv_bool m = true.
Proof.
split; unfold tilde_w_equiv_bool; intros E.
- now rewrite decision_true by auto.
- decide (k₁k1 ~w~~@ k₂k2 at m).
+ auto.
+ discriminate.
Qed.
Lemma tilde_w_equiv_iff: k₁k1 ~w~~# k₂k2 ↔<-> ∃exists n, tilde_w_equiv_bool n = true.
Proof.
split; intros [m E]; exists m; now apply tilde_w_index_equiv_iff.
Qed.
Lemma tilde_w_equiv_bool_remains_true m: tilde_w_equiv_bool m = true →-> ∀forall n, n ≥>= m →-> tilde_w_equiv_bool n = true.
Proof.
intros P n L.
apply tilde_w_index_equiv_iff.
apply tilde_w_index_equiv_iff in P.
now apply (tilde_w_extend P).
Qed.
Lemma tilde_w_equiv_bool_infinite_false: infinite false tilde_w_equiv_bool ↔<-> ∀forall n, tilde_w_equiv_bool n = false.
Proof.
split.
- intros Inf n.
destruct (tilde_w_equiv_bool n ) eqn:H.
+ exfalso. destruct (Inf n) as [m [L F]].
now rewrite (tilde_w_equiv_bool_remains_true H L) in F.
+ reflexivity.
- intros F. intros n. exists n. auto.
Qed.
End PropositionalDecidability.
Lemma tilde_w_equiv_XM: rel_XM tilde_w_equiv.
Proof.
intros k₁k1 k₂k2.
destruct (finite_type_seq (tilde_w_equiv_bool k₁k1 k₂k2) ) as [[|] Inf].
- left. apply tilde_w_equiv_iff. destruct (Inf 0) as [k T]. now exists k.
- right. intros E. apply tilde_w_equiv_iff in E.
destruct E as [n T].
destruct (tilde_w_equiv_bool_infinite_false k₁k1 k₂k2) as [F _].
specialize (F Inf n).
now rewrite T in F.
Qed.
Hint Resolve dupfree_dec.
Hint Resolve nat_eq_dec.
Hint Resolve list_exists_dec.
Lemma not_tilde_w_extend k₁k1 k₂k2: ¬~ k₁k1 ~w~~# k₂k2 →-> ∀forall m, ¬~ k₁k1 ~w~~@ k₂k2 at m.
Proof.
intros NE m Em. apply NE. now exists m.
Qed.
Lemma tilde_equiv_finite_index: finiteIndex tilde_equiv.
Proof.
exists (Cardinality EquivalenceClassIndex).
intros L G.
pose (L' := seq_map (λfun w ⇒=> tilde_eq_class w) L ).
destruct (can_find_duplicate (|L|) L') as [D|D].
- destruct D as [i [j [P Q]]]. exists i,j. split; auto.
apply (equivalent_in_equivalence_class (i := tilde_eq_class (L [i]))).
+ apply tilde_eq_class_correct.
+ unfold L', seq_map in *. simpl in Q. rewrite Q. apply tilde_eq_class_correct.
- exfalso. omega.
Qed.
Lemma tilde_equiv_finite_index_neq: finiteIndexNeg tilde_equiv.
Proof.
apply finiteIndexImpliesFiniteIndexNeg. apply tilde_equiv_finite_index.
Qed.
Lemma tilde_w_equiv_finite_index_neq : finiteIndexNeg tilde_w_equiv.
Proof.
destruct tilde_equiv_finite_index_neq as [n P]. exists n.
intros L G NE.
pose (m := S (max_of_nat_string (seq L) (|L|))).
pose (L' := seq_map (λfun k ⇒=> extract k m w) L).
apply P with (L:= mkstring L' (|L|)).
- now simpl.
- intros x y O E. simpl in O.
apply (NE x y O). exists m. split.
+ subst m. split.
* assert (L [x] ≤<= max_of_nat_string (seq L) (| L |)). { apply max_of_nat_string_correct. omega. } omega.
* assert (L [y] ≤<= max_of_nat_string (seq L) (| L |)). { apply max_of_nat_string_correct. omega. } omega.
+ assumption.
Qed.
Lemma tilde_w_equiv_finite_index: finiteIndex tilde_w_equiv.
Proof.
apply finiteIndexNegAndXMImpliesFiniteIndex.
- apply tilde_w_equiv_XM.
- apply tilde_w_equiv_finite_index_neq.
Qed.
Construction of V and W
We will refine strictly monotone sequences such that in the end the sequence gives the partition of w.- they are equivalent
Lemma infinite_equiv_indices : ∃exists g, s_monotone g ∧/\ g 0 > 0 ∧/\ ∀forall n, (g 0) ~w~~# (g n).
Proof.
destruct (finite_equiv_classes tilde_w_equivalence tilde_w_equiv_XM tilde_w_equiv_finite_index (λfun n ⇒=> n)) as [g [Inc E]].
exists (drop 1 g). repeat split.
- now apply s_monotone_drop.
- simpl. now apply s_monotone_ge.
- intros n. repeat rewrite drop_correct.
apply (tilde_w_transitive (tilde_w_symmetric (E (1 + 0))) (E (1 + n))).
Qed.
Arguments cc_nat [p] [p_dec] _.
There are infinitely many indices such that
- they are equivalent
- the strings extract (g 0) (g n) w are equivalent forall n
Lemma infinite_equiv_indices_equiv_begin: ∃exists g,
s_monotone g ∧/\ g 0 > 0 ∧/\ (∀forall n, (g 0) ~w~~# (g n)) ∧/\ (∀forall n m, n > 0 →-> m > 0 →-> extract (g 0) (g n) w ~~~ extract (g 0) (g m) w).
Proof.
destruct infinite_equiv_indices as [g [GZ [I WE]]].
pose (g' := λfun n ⇒=> tilde_eq_class (extract (g 0) (g n) w)).
destruct (finite_type_seq g') as [i Inf].
pose (f := filter∞infinite_filter (P:=λfun j ⇒=> j = i) (λfun j ⇒=> decision (j = i)) Inf ).
assert (∀forall n, g' (f n) = i) as H. { intros k. subst f. apply infinite_filter_correct. }
assert (∀forall n, n > 0 →-> ⟦{[i⟧]} (extract (g 0) (g (fix_first_zero f n)) w)) as H'. {
intros k Lk. destruct k.
- exfalso. omega.
- specialize (H (S k)). unfold g' in H. unfold fix_first_zero.
rewrite ←<-H. apply tilde_eq_class_correct. }
exists (λfun n ⇒=> g (fix_first_zero f n)). split.
- unfold f. auto using compose_s_monotone, fix_first_zero_s_monotone, infinite_filter_s_monotone.
- split; [|split] .
+ now apply s_monotone_ge_zero.
+ intros n. simpl. apply WE.
+ intros n m Ln Lm. simpl.
apply equivalent_in_equivalence_class with (i:=i); now apply H'.
Qed.
There are infinitely many indices such that
- they are equivalent
- the strings extract (g 0) (g n) w are equivalent forall n
- for all j<=i we have (g j) ~~~@ (g i) at (g (S i))
Definition merge_at_next (w: String ℕnat) := ∀forall i j, j≤<=i < |w| →-> w [j] ~w~~@ w[i] at (w [S i]).
Instance dec_merge_at_next: ∀forall w, dec(merge_at_next w).
Proof.
intros v. unfold merge_at_next.
enough (dec (∀forall i, i < |v| →-> (∀forall j, j ≤<= i →-> v[j]~w~~@ v[i] at (v[S i])))) as [H|H].
- left. intros i j L. apply H; omega.
- right. intros N. apply H. intros i L j L'. apply N; omega.
- auto.
Defined.
Lemma merge_at_next_extensional v v': merge_at_next v →-> v == v' →-> merge_at_next v'.
Proof.
intros M [E₁E1 E₂E2] i j L.
rewrite ←<-E₁E1 in L. specialize (M i j L). split.
- destruct M as [M M']. now repeat rewrite ←<-E₂E2 by omega.
- apply (tilde_extensional (w:= extract (v [j]) (v [S i]) w) (v:= (extract (v [i]) (v [S i]) w))).
+ apply M.
+ split; intros *; simpl; repeat rewrite E₂E2 by omega; oauto.
+ split; intros *; simpl; repeat rewrite E₂E2 by omega; oauto.
Qed.
Lemma common_merge_index g g' : g' 0 = 0 →-> (∀forall n : ℕnat, g 0 ~w~~# g n) →-> ∀forall k, ∃exists m, ∀forall i, i ≤<= k →-> g 0 ~w~~@ g (g' i) at m.
Proof.
intros Z WE k.
induction k.
- exists (S (g 0)). intros i L. rewrite_eq (i = 0). rewrite Z. apply tilde_w_index_reflexive. omega.
- destruct IHk as [m P]. destruct (WE (g' (S k))) as [m' Q].
exists (max m m'). intros i L.
pose (Nat.le_max_r m m'); pose (Nat.le_max_l m m'). decide (i = S k).
+ subst i. apply tilde_w_extend with (m := m'); auto.
+ apply tilde_w_extend with (m := m); try(apply P); oauto.
Qed.
Lemma merge_at_next_append g g' m : s_monotone g →-> merge_at_next (substring g g')→-> m > g' [| g' |] →-> (∀forall i, i < |g'| →-> g (g' [i]) ~w~~@ g (g' [|g'|]) at (g m))
→-> merge_at_next (substring g (g' ⧺++ mkstring (λfun _ : ℕnat ⇒=> m) 0)).
Proof.
intros Inc M G MS i j.
decide (i = |g'|); intros O; simpl in *.
- subst i. rewrite_eq (S(|g'|) = S(|g'|) + 0). rewrite prepend_path_rest_correct.
repeat rewrite prepend_path_begin_correct by omega.
decide (j = |g'|).
+ subst j. apply tilde_w_index_reflexive. simpl. apply s_monotone_strict_order_preserving; auto.
+ apply MS. omega.
- repeat rewrite prepend_path_begin_correct by omega.
apply tilde_w_extend with (m:= g(g' [S i])).
+ apply M. simpl. omega.
+ omega.
Qed.
Lemma there_is_bigger_merging_index g: s_monotone g →-> (∀forall n, (g 0) ~w~~# (g n)) →->
∀forall g', g' [0] = 0 →-> merge_at_next (substring g g') →-> ∃exists m, m > g' [| g' |] ∧/\ merge_at_next (substring g (g' ⧺++ mkstring (λfun _ : ℕnat ⇒=> m) 0)).
Proof.
intros Inc WE [g' l] Z M. induction l.
- simpl. exists (S (g' 0)). split.
+ omega.
+ apply merge_at_next_append; auto; simpl. intros i L . omega.
- destruct (common_merge_index Z WE (S l)) as [m P].
destruct (s_monotone_unbouded Inc m) as [k Q].
assert (g k > g' (S l)) as H. { destruct (P (S l)) as [H _]. { omega. } simpl in H. pose (s_monotone_ge Inc (g' (S l))). omega. }
exists (g k). split.
+ auto.
+ apply merge_at_next_append; auto.
simpl. intros i G. simpl in *.
apply tilde_w_extend with (m:=m).
* assert (max m m = m) as H' by now apply max_l. rewrite ←<-H'.
apply (tilde_w_index_transitive (k₁k1:=g(g' i)) (k₂k2:=g 0) (k₃k3:=g(g' (S l))) (m₁m1 := m) (m₂m2 := m)).
-- apply tilde_w_index_symmetric. apply P. omega.
-- apply P. omega.
* pose (s_monotone_order_preserving Inc Q). pose (s_monotone_ge Inc m). omega.
Qed.
Lemma infinite_equiv_indices_merging: ∃exists g, s_monotone g ∧/\ g 0 > 0 ∧/\
(∀forall n, (g 0) ~w~~# (g n)) ∧/\ (∀forall n m, n > 0 →-> m > 0 →-> extract (g 0) (g n) w ~~~ extract (g 0) (g m) w) ∧/\
(∀forall j i, j ≤<= i →-> (g j) ~w~~@ (g i) at (g (S i))).
Proof.
destruct infinite_equiv_indices_equiv_begin as [g [Inc [GZ [WE BE]]]].
assert (merge_at_next (mkstring g 0)) as baseP. {intros i j L. simpl in L. exfalso. omega. }
pose (stepP := there_is_bigger_merging_index Inc WE).
assert (s_monotone (filterhistoryhistory_filter dec_merge_at_next merge_at_next_extensional baseP stepP)) as Inc₂Inc2 by apply history_filter_s_monotone.
exists (λfun n ⇒=> g (filterhistoryhistory_filter dec_merge_at_next merge_at_next_extensional baseP stepP n)). split.
- apply compose_s_monotone; auto.
- split; [|split]; [| |split].
+ now apply s_monotone_ge_zero.
+ intros n. rewrite history_filter_zero. apply WE.
+ intros n m Ln Lm. repeat rewrite history_filter_zero. apply BE.
-- pose (s_monotone_ge Inc₂Inc2 n). omega.
-- pose (s_monotone_ge Inc₂Inc2 m). omega.
+ intros j i L. split.
-- split; apply s_monotone_strict_order_preserving; auto; apply s_monotone_strict_order_preserving; oauto.
-- specialize (history_filter_correct dec_merge_at_next merge_at_next_extensional baseP stepP (S i)).
intros E. specialize (E i j). simpl in E. apply E. omega.
Qed.
Finally we can give the desired V and W
Lemma totality: ∃exists i j, (⟦{[i⟧]}·o⟦{[j⟧]}ω^00) w.
Proof.
destruct infinite_equiv_indices_merging as [g [Inc [GZ [WE [BE M]]]]].
exists (tilde_eq_class (extract 0 (g 0) w)), (tilde_eq_class (extract (g 0) (g 1) w)), (pred (g 0)).
split.
- unfold extract. simpl. rewrite_eq (pred (g 0) = g 0 -1). apply tilde_eq_class_correct.
- rewrite_eq (S (pred (g 0)) = g 0).
exists (fix_first_zero (seq_map (λfun n ⇒=> n - g 0 ) g)). split.
+ apply fix_first_zero_s_monotone. intros n. destruct n; simpl; unfold seq_map.
* specialize (Inc 0). omega.
* pose (s_monotone_strict_order_preserving Inc (k:=0) (n:= S n) ).
pose (s_monotone_strict_order_preserving Inc (k:=0) (n:= S (S n)) ).
pose (Inc (S n)). omega.
+ split.
* reflexivity.
* intros n. unfold seq_map. simpl. destruct n; simpl.
-- unfold extract. simpl. rewrite_eq (g 1 - g 0 - 1 = g 1 - S(g 0)). apply tilde_eq_class_correct.
-- apply equivalent_drop. { split.
- apply s_monotone_order_preserving; oauto.
- apply Inc. }
destruct (M 0 (S n) ) as [_ M']. { omega. }
assert (1 > 0) as H' by omega. assert (S (S n) > 0) as H'' by omega.
specialize (BE 1 (S (S n)) H' H'').
apply (equivalence_class_closed (tilde_eq_class_correct ((extract (g 0) (g 1) w)) )).
apply tilde_symmetric.
apply (tilde_transitive BE M').
Qed.
End Totality.
NFAs recognizing all V ·o Wω^00
V ·o Wω^00 is part of the complement if its intersection with the Buechi language is empty
Definition VW_part_of_complement (vw : VW) := LBL_B (intersect (VW_aut (fst vw) (snd vw)) aut) =L=$= ∅{}.
Instance dec_VW_part_of_complement vw: dec (VW_part_of_complement vw).
Proof.
unfold VW_part_of_complement.
apply dec_language_empty.
Qed.
Definition complement_auts := map (λfun vw ⇒=> VW_aut (fst vw) (snd vw)) (filter (DecPred VW_part_of_complement ) (elem VW)).
Instance dec_VW_part_of_complement vw: dec (VW_part_of_complement vw).
Proof.
unfold VW_part_of_complement.
apply dec_language_empty.
Qed.
Definition complement_auts := map (λfun vw ⇒=> VW_aut (fst vw) (snd vw)) (filter (DecPred VW_part_of_complement ) (elem VW)).
The complement automaton is the union of all these automata
Lemma autC_disjoint: LBL_B aut ∩/$\ LBL_B autC =L=$= ∅{}.
Proof.
apply language_empty_iff. intros w [LA LC].
destruct (totality w) as [i [j P]].
unfold autC in LC. apply many_aut_union 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 [Q₁Q1 Q₂Q2].
apply (Q₂Q2 w).
apply intersect_correct. split.
- now rewrite AVW.
- assumption.
Qed.
Lemma part_of_complement_implies_complement i j: VW_part_of_complement (i,j) →-> ⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ⊆<$= LBL_B autC.
Proof.
intros PC w VW.
apply many_aut_union.
exists (VW_aut i j). split.
- unfold complement_auts.
apply in_map_iff.
exists (i,j). 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 i j: ¬~VW_part_of_complement (i,j) →-> ⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ⊆<$= LBL_B aut.
Proof.
intros nPC w VW.
unfold VW_part_of_complement in nPC.
destruct (dec_language_empty_informative (aut:=(intersect (VW_aut i j) aut) )) as [D|D].
- destruct D as [w' L]. apply intersect_correct in L.
apply (compatibility (w:=w') (i:=i)(j:=j)).
+ destruct L as [L₁L1 L₂L2]. now apply VW_aut_correct in L₁L1.
+ assumption.
- exfalso. auto.
Qed.
Lemma complement_complete : LBL_B autC ∪\$/ LBL_B aut =L=$= Aω^0$0.
Proof.
apply language_universal_iff. intros w.
destruct (totality w) as [i [j P]].
decide (VW_part_of_complement (i,j)) 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: LBL_B autC =L=$= (LBL_B aut)C)^$~.
Proof.
intros w. destruct (complement_complete w). pose (autC_disjoint w).
autounfold in *. tauto.
Qed.
Lemma complement_correct2: (LBL_B autC)C)^$~ =L=$= LBL_B aut.
Proof.
intros w. destruct (complement_complete w). pose (autC_disjoint w).
autounfold in *. tauto.
Qed.
Definition complement := autC.
End Complement.
End TildeEquivalenceRelation.
Proof.
apply language_empty_iff. intros w [LA LC].
destruct (totality w) as [i [j P]].
unfold autC in LC. apply many_aut_union 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 [Q₁Q1 Q₂Q2].
apply (Q₂Q2 w).
apply intersect_correct. split.
- now rewrite AVW.
- assumption.
Qed.
Lemma part_of_complement_implies_complement i j: VW_part_of_complement (i,j) →-> ⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ⊆<$= LBL_B autC.
Proof.
intros PC w VW.
apply many_aut_union.
exists (VW_aut i j). split.
- unfold complement_auts.
apply in_map_iff.
exists (i,j). 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 i j: ¬~VW_part_of_complement (i,j) →-> ⟦{[i⟧]}·o⟦{[j⟧]}ω^00 ⊆<$= LBL_B aut.
Proof.
intros nPC w VW.
unfold VW_part_of_complement in nPC.
destruct (dec_language_empty_informative (aut:=(intersect (VW_aut i j) aut) )) as [D|D].
- destruct D as [w' L]. apply intersect_correct in L.
apply (compatibility (w:=w') (i:=i)(j:=j)).
+ destruct L as [L₁L1 L₂L2]. now apply VW_aut_correct in L₁L1.
+ assumption.
- exfalso. auto.
Qed.
Lemma complement_complete : LBL_B autC ∪\$/ LBL_B aut =L=$= Aω^0$0.
Proof.
apply language_universal_iff. intros w.
destruct (totality w) as [i [j P]].
decide (VW_part_of_complement (i,j)) 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: LBL_B autC =L=$= (LBL_B aut)C)^$~.
Proof.
intros w. destruct (complement_complete w). pose (autC_disjoint w).
autounfold in *. tauto.
Qed.
Lemma complement_correct2: (LBL_B autC)C)^$~ =L=$= LBL_B aut.
Proof.
intros w. destruct (complement_complete w). pose (autC_disjoint w).
autounfold in *. tauto.
Qed.
Definition complement := autC.
End Complement.
End TildeEquivalenceRelation.
Section ComplementCorollaries.
Context {A: finType}.
Corollary dec_language_universal (aut:BuechiAut A) : dec(LBL_B aut =L=$= Aω^0$0).
Proof.
destruct (dec_language_empty (aut:= (complement (aut:= aut)))) as [D|D].
- left. apply language_universal_iff. intros w. specialize (D w).
destruct (complement_complete (aut:=aut) w). autounfold in *. tauto.
- right. intros L. apply D. intros w. pose (complement_correct2 (aut:=aut) w).
autounfold in *. specialize (L w). tauto.
Qed.
Corollary dec_language_inclusion (aut₁aut1 aut₂aut2:BuechiAut A): dec (LBL_B aut₁aut1 ⊆<$= LBL_B aut₂aut2).
Proof.
destruct (dec_language_empty (aut:= (intersect aut₁aut1 (complement (aut:= aut₂aut2))))) as [D|D].
- left. intros w L. specialize (D w).
destruct (complement_complete (aut:=aut₂aut2) w) as [_ [D'| D']].
+ auto.
+ exfalso. apply D. now apply intersect_correct.
+ assumption.
- right. intros I. apply D. apply language_empty_iff.
intros w L. apply intersect_correct in L. destruct L as [L₁L1 L₂L2].
apply complement_correct in L₂L2. auto.
Qed.
Corollary dec_language_eq (aut₁aut1 aut₂aut2:BuechiAut A): dec (LBL_B aut₁aut1 =L=$= LBL_B aut₂aut2).
Proof.
pose (language_eq_iff (LBL_B aut₁aut1) (LBL_B aut₂aut2)) as P.
apply dec_trans with (P:=language_inclusion (LBL_B aut₁aut1) (LBL_B aut₂aut2) ∧/\ language_inclusion (LBL_B aut₂aut2) (LBL_B aut₁aut1)).
- auto using and_dec, dec_language_inclusion.
- split; apply language_eq_iff.
Qed.
End ComplementCorollaries.
Context {A: finType}.
Corollary dec_language_universal (aut:BuechiAut A) : dec(LBL_B aut =L=$= Aω^0$0).
Proof.
destruct (dec_language_empty (aut:= (complement (aut:= aut)))) as [D|D].
- left. apply language_universal_iff. intros w. specialize (D w).
destruct (complement_complete (aut:=aut) w). autounfold in *. tauto.
- right. intros L. apply D. intros w. pose (complement_correct2 (aut:=aut) w).
autounfold in *. specialize (L w). tauto.
Qed.
Corollary dec_language_inclusion (aut₁aut1 aut₂aut2:BuechiAut A): dec (LBL_B aut₁aut1 ⊆<$= LBL_B aut₂aut2).
Proof.
destruct (dec_language_empty (aut:= (intersect aut₁aut1 (complement (aut:= aut₂aut2))))) as [D|D].
- left. intros w L. specialize (D w).
destruct (complement_complete (aut:=aut₂aut2) w) as [_ [D'| D']].
+ auto.
+ exfalso. apply D. now apply intersect_correct.
+ assumption.
- right. intros I. apply D. apply language_empty_iff.
intros w L. apply intersect_correct in L. destruct L as [L₁L1 L₂L2].
apply complement_correct in L₂L2. auto.
Qed.
Corollary dec_language_eq (aut₁aut1 aut₂aut2:BuechiAut A): dec (LBL_B aut₁aut1 =L=$= LBL_B aut₂aut2).
Proof.
pose (language_eq_iff (LBL_B aut₁aut1) (LBL_B aut₂aut2)) as P.
apply dec_trans with (P:=language_inclusion (LBL_B aut₁aut1) (LBL_B aut₂aut2) ∧/\ language_inclusion (LBL_B aut₂aut2) (LBL_B aut₁aut1)).
- auto using and_dec, dec_language_inclusion.
- split; apply language_eq_iff.
Qed.
End ComplementCorollaries.