Set Implicit Arguments.
Require Import Utils.
Require Import FinSets.
Require Import Strings.
Require Import Sequences.
Require Import NFAs.
Require Import RegularLanguages.
Require Import Buechi.
Require Import FiniteSemigroups.
Require Import RamseyanFactorizations.
Require Import Utils.
Require Import FinSets.
Require Import Strings.
Require Import Sequences.
Require Import NFAs.
Require Import RegularLanguages.
Require Import Buechi.
Require Import FiniteSemigroups.
Require Import RamseyanFactorizations.
Complementation of Büchi Automata
We follow Büchi's complement construction and need RF for verification.Section Complement.
Context {Sigma:finType}.
Variable (aut:NFA Sigma).
Implicit Types (x y z: NStr Sigma)(p q : state aut).
Semigroup of Colors
We define a semigroup Gamma capturing the important information of a string part of a sequence. We call the element of Gamma colors.Definition Gamma := (finSet (state aut (x) state aut)) (x) (finSet (state aut (x) state aut)).
Implicit Types (V W U : Gamma).
We define a semigroup homomorphism NStr Sigma -> Gamma computing the color of a string.
Definition gamma x : Gamma:=
( makeSet (fun t => match t with (p,q) => p ===> q on x end) ,
makeSet (fun t => match t with (p,q) => p =!=> q on x end)).
Notation "{[ V ]}" := (fun x => gamma x = V) (at level 0).
Lemma same_color_transforms x y p q: gamma x = gamma y -> p ===> q on x -> p ===> q on y.
Proof.
unfold gamma.
intros E. apply (f_equal fst) in E.
simpl in E; apply set_eq' with (x:=(p,q)) in E; rewrite !makeSet_correct in E. tauto.
Qed.
Lemma same_color_transforms_accepting x y p q: gamma x = gamma y -> p =!=> q on x -> p =!=> q on y.
Proof.
unfold gamma.
intros E. apply (f_equal snd) in E.
simpl in E; apply set_eq' with (x:=(p,q)) in E; rewrite !makeSet_correct in E. tauto.
Qed.
We define an addition operation on Gamma turning it into a finite semigroup.
Definition addGamma V W: Gamma :=
(makeSet (fun t => match t with (p,q) => exists s, (p,s) mem (fst V) /\ (s,q) mem (fst W) end),
makeSet (fun t => match t with (p,q) => exists s, (p,s) mem (fst V) /\ (s,q) mem (snd W) \/
(p,s) mem (snd V) /\ (s,q) mem (fst W) end)).
This simple lemma should be provable in the following lemma by congruence, but it is in the
concrete instance there incredible slow.
Lemma pair_eq (Y Z: Type)(y1 y2:Y)(z1 z2:Z) : y1 = y2 -> z1 = z2 -> (y1,z1) = (y2,z2).
Proof.
intros. congruence.
Qed.
Lemma addGamma_is_associative : associative addGamma.
Proof.
intros U V W.
unfold addGamma. apply pair_eq.
- apply makeSet_eq. intros [p q]. split; intros [s [H1 H2]]; cbn in *; rewrite makeSet_correct in *.
1: destruct H2 as [s' [H2 H3]].
2: destruct H1 as [s' [H1 H3]].
all: exists s'; split; auto; cbn; rewrite makeSet_correct; exists s; split; auto.
- apply makeSet_eq. intros [p q]. split; intros [s [[H1 H2] | [H1 H2]]]; cbn in *; rewrite makeSet_correct in *.
1,2: destruct H2 as [s' H2].
3,4: destruct H1 as [s' H1].
all: exists s'; rewrite !makeSet_correct.
+ destruct H2 as [[H2 H3]|[H2 H3]].
* left. split; auto. now exists s.
* right. split; auto. exists s. now left.
+ right. destruct H2 as [H2 H3]. split; auto. exists s. now right.
+ left. destruct H1 as [H1 H3]. split; auto. exists s. now left.
+ destruct H1 as [[H1 H3]|[H1 H3]].
* left. split; auto. exists s. now right.
* right. split; auto. now exists s.
Qed.
Lemma gamma_is_homomorphisms: is_homomorphism (Gamma:= mkSG addGamma_is_associative) gamma.
Proof.
intros v u.
unfold addGamma, gamma. cbn. f_equal; apply makeSet_eq; intros [p q].
- rewrite transforms_concat. erewrite iff_ex.
apply iff_equivalence.
intros s. cbn. rewrite !makeSet_correct. tauto.
- rewrite transforms_accepting_concat. erewrite iff_ex.
apply iff_equivalence.
intros s. cbn. rewrite !makeSet_correct. tauto.
Qed.
Lemma same_color_same_accepting_quasi (tau tau': Seq (NStr Sigma)) (rho: Seq (state aut)):
(forall n, gamma (tau n) = gamma (tau' n)) ->
accepting_quasi_run rho tau -> accepting_quasi_run rho tau'.
Proof.
intros E [Va [I F]]. repeat split; auto.
- intros n. apply (same_color_transforms (E n)), Va.
- intros m. destruct (F m) as [n [H1 H2]]. exists n; split; auto.
apply (same_color_transforms_accepting (E n)), H2.
Qed.
Proof.
intros. congruence.
Qed.
Lemma addGamma_is_associative : associative addGamma.
Proof.
intros U V W.
unfold addGamma. apply pair_eq.
- apply makeSet_eq. intros [p q]. split; intros [s [H1 H2]]; cbn in *; rewrite makeSet_correct in *.
1: destruct H2 as [s' [H2 H3]].
2: destruct H1 as [s' [H1 H3]].
all: exists s'; split; auto; cbn; rewrite makeSet_correct; exists s; split; auto.
- apply makeSet_eq. intros [p q]. split; intros [s [[H1 H2] | [H1 H2]]]; cbn in *; rewrite makeSet_correct in *.
1,2: destruct H2 as [s' H2].
3,4: destruct H1 as [s' H1].
all: exists s'; rewrite !makeSet_correct.
+ destruct H2 as [[H2 H3]|[H2 H3]].
* left. split; auto. now exists s.
* right. split; auto. exists s. now left.
+ right. destruct H2 as [H2 H3]. split; auto. exists s. now right.
+ left. destruct H1 as [H1 H3]. split; auto. exists s. now left.
+ destruct H1 as [[H1 H3]|[H1 H3]].
* left. split; auto. exists s. now right.
* right. split; auto. now exists s.
Qed.
Lemma gamma_is_homomorphisms: is_homomorphism (Gamma:= mkSG addGamma_is_associative) gamma.
Proof.
intros v u.
unfold addGamma, gamma. cbn. f_equal; apply makeSet_eq; intros [p q].
- rewrite transforms_concat. erewrite iff_ex.
apply iff_equivalence.
intros s. cbn. rewrite !makeSet_correct. tauto.
- rewrite transforms_accepting_concat. erewrite iff_ex.
apply iff_equivalence.
intros s. cbn. rewrite !makeSet_correct. tauto.
Qed.
Lemma same_color_same_accepting_quasi (tau tau': Seq (NStr Sigma)) (rho: Seq (state aut)):
(forall n, gamma (tau n) = gamma (tau' n)) ->
accepting_quasi_run rho tau -> accepting_quasi_run rho tau'.
Proof.
intros E [Va [I F]]. repeat split; auto.
- intros n. apply (same_color_transforms (E n)), Va.
- intros m. destruct (F m) as [n [H1 H2]]. exists n; split; auto.
apply (same_color_transforms_accepting (E n)), H2.
Qed.
Kinds of Sequences
A kind of a sequence corresponds to a Ramseyan factorisation of the sequence in Gamma with given color of the first and second factor. We express this using language operations and hence will be able to use closure operations on Büchi automata to builds NFAs later.Definition has_kind sigma V W := ({[V]}o'{[W]}^00) sigma.
Definition has_some_kind sigma := exists V W, has_kind sigma V W.
Definition kind_compatible V W := exists sigma, has_kind sigma V W /\ L_B aut sigma.
If a kind is compatible, aut accepts all sequences of that kind.
Theorem compatibility V W: kind_compatible V W -> ({[V]}o'{[W]}^00) <$= L_B aut.
Proof.
intros [sigma [[x [sigma'' [Vx [[sigma' [Wsigma E2]] E1]] ]] L]].
rewrite E1, E2 in *. clear E1 sigma E2 sigma''.
intros tau [y [tau'' [Vy [[tau' [Wtau E3]] E4]]]].
rewrite E3, E4 in *. clear E3 tau E4 tau''.
rewrite flatten_prepend in L. rewrite flatten_prepend.
apply accepting_quasi_run_iff_accepts.
apply accepting_quasi_run_iff_accepts in L. destruct L as [rho Acc].
exists rho.
eapply same_color_same_accepting_quasi. 2: apply Acc.
intros [|n].
- cbn. now rewrite !nth_first, Vx, Vy.
- cbn. now rewrite !nth_step, Wsigma, Wtau.
Qed.
Proof.
intros [sigma [[x [sigma'' [Vx [[sigma' [Wsigma E2]] E1]] ]] L]].
rewrite E1, E2 in *. clear E1 sigma E2 sigma''.
intros tau [y [tau'' [Vy [[tau' [Wtau E3]] E4]]]].
rewrite E3, E4 in *. clear E3 tau E4 tau''.
rewrite flatten_prepend in L. rewrite flatten_prepend.
apply accepting_quasi_run_iff_accepts.
apply accepting_quasi_run_iff_accepts in L. destruct L as [rho Acc].
exists rho.
eapply same_color_same_accepting_quasi. 2: apply Acc.
intros [|n].
- cbn. now rewrite !nth_first, Vx, Vy.
- cbn. now rewrite !nth_step, Wsigma, Wtau.
Qed.
UP sequences always have some kind and given RF all sequences have a kind.
Lemma totality_up (x y : NStr Sigma) : has_some_kind (x +++ omega_iter y).
Proof.
exists (gamma x), (gamma y), x, (omega_iter y). repeat split; auto.
exists (const y). split. intros n. rewrite const_nth. now cbn. reflexivity.
Qed.
Lemma totality sigma : RF-> has_some_kind sigma.
Proof.
intros Ramsey % RamseyFac_iff_RamseyFac'.
destruct (Ramsey (mkSG addGamma_is_associative) _ gamma sigma) as [tau [F R]].
- intros x y. now rewrite gamma_is_homomorphisms.
- exists (gamma (hd tau)), (gamma (tau 1)), (hd tau), (flatten (tl tau)). repeat split.
+ exists (tl tau). split.
* intros n. specialize (R (S n)).
rewrite <-nth_step_tl.
rewrite 2map_nth in R.
rewrite <-R; auto.
* reflexivity.
+ rewrite flatten_prepend. simpl. now rewrite <-scons_correct.
Qed.
The Complement Automaton
The complement automaton is obtained by union of all incompatible kinds. We first need an automation accepting V o W^00:Definition VW_aut (V W:mkSG addGamma_is_associative) := prepend_nfa (one_color_nfa (V:mkSG addGamma_is_associative) gamma) (nfa_omega_iter (one_color_nfa (W:mkSG addGamma_is_associative) gamma)).
Lemma VW_aut_correct (V W: mkSG addGamma_is_associative): L_B (VW_aut V W) =$= {[V]}o'{[W]}^00.
Proof.
unfold VW_aut.
rewrite prepend_nfa_correct, nfa_omega_iter_correct, (one_color_nfa_correct W), (one_color_nfa_correct' V) by now apply gamma_is_homomorphisms.
intros sigma. split.
- intros [x [sigma' [[x' [E L1]] [L2 E2]] ]]. exists x', sigma'. repeat split; auto; now subst.
- intros [x [sigma' [L1 [L2 E]]]]. exists x, sigma'. repeat split; auto. now exists x.
Qed.
It is decidable whether a kinds is compatible or not.
Instance dec_kind_compatible V W : dec (kind_compatible V W).
Proof.
eapply dec_trans.
- apply (dec_is_buechi_nonempty (intersect (VW_aut V W) aut)).
- split.
+ intros [sigma [VW % VW_aut_correct H] % intersect_correct]. now exists sigma.
+ intros [sigma [H1%VW_aut_correct H2]]. exists sigma. now apply intersect_correct.
Qed.
Lemma VW_part_of_complement_iff V W : ~ kind_compatible V W <-> L_B (VW_aut V W) /$\ L_B aut =$= {}.
Proof.
rewrite VW_aut_correct.
split.
- intros N sigma. split.
+ intros H. apply N. now exists sigma.
+ now intros.
- intros N [sigma C]. now apply (N sigma).
Qed.
The complement NFA is the union of all the automata for incompatible kinds.
Definition complement := big_union (List.map (fun vw => VW_aut (fst vw) (snd vw)) (FinTypes.External.filter (DecPred (fun VW => ~ kind_compatible (fst VW) (snd VW)) ) (elem (Gamma (x) Gamma)))).
Lemma in_complement_nfa_iff sigma : L_B complement sigma <-> exists V W, ~ kind_compatible V W /\ has_kind sigma V W.
Proof.
unfold complement. rewrite (big_union_correct _ sigma). split.
- intros [B [[[V W] [E H % in_filter_iff]]% in_map_iff D]]. subst B. apply VW_aut_correct in D. now exists V, W.
- intros [V [W [C K % VW_aut_correct]]]. exists (VW_aut V W). split; auto.
apply in_map_iff. exists (V,W). split; auto. now apply in_filter_iff.
Qed.
Lemma complement_disjoint: L_B aut /$\ L_B complement =$= {}.
Proof.
apply language_empty_iff. intros sigma [LA [V [W [H1% VW_part_of_complement_iff H2]]] % in_complement_nfa_iff].
apply (H1 sigma). split; auto. now apply VW_aut_correct.
Qed.
Lemma complement_kind_exhaustive sigma: has_some_kind sigma -> (L_B aut \$/ L_B complement) sigma.
Proof.
intros [V [W K]].
decide (~ kind_compatible V W) as [D |D].
- right. apply in_complement_nfa_iff. exists V,W. split; auto.
- left. rewrite VW_part_of_complement_iff in D.
destruct (dec_buechi_empty_informative (intersect (VW_aut V W) aut )) as
[[x [y [D1 % VW_aut_correct D2] % match_accepted % intersect_correct]]|D' ].
+ eapply compatibility. 2: apply K. now exists(x +++ omega_iter y).
+ exfalso. now rewrite intersect_correct in D'.
Qed.
Lemma complement_exhaustive : RF -> L_B aut \$/ L_B complement =$= universal_language.
Proof.
intros Ramsey sigma. split; auto. intros _.
now apply complement_kind_exhaustive, totality.
Qed.
Lemma complement_exhaustive_up (x y : NStr Sigma) : L_B aut (x +++ omega_iter y) \/ L_B complement (x +++ omega_iter y).
Proof.
apply complement_kind_exhaustive, totality_up.
Qed.
End Complement.
Global Arguments complement {Sigma} aut.
Lemma in_complement_nfa_iff sigma : L_B complement sigma <-> exists V W, ~ kind_compatible V W /\ has_kind sigma V W.
Proof.
unfold complement. rewrite (big_union_correct _ sigma). split.
- intros [B [[[V W] [E H % in_filter_iff]]% in_map_iff D]]. subst B. apply VW_aut_correct in D. now exists V, W.
- intros [V [W [C K % VW_aut_correct]]]. exists (VW_aut V W). split; auto.
apply in_map_iff. exists (V,W). split; auto. now apply in_filter_iff.
Qed.
Lemma complement_disjoint: L_B aut /$\ L_B complement =$= {}.
Proof.
apply language_empty_iff. intros sigma [LA [V [W [H1% VW_part_of_complement_iff H2]]] % in_complement_nfa_iff].
apply (H1 sigma). split; auto. now apply VW_aut_correct.
Qed.
Lemma complement_kind_exhaustive sigma: has_some_kind sigma -> (L_B aut \$/ L_B complement) sigma.
Proof.
intros [V [W K]].
decide (~ kind_compatible V W) as [D |D].
- right. apply in_complement_nfa_iff. exists V,W. split; auto.
- left. rewrite VW_part_of_complement_iff in D.
destruct (dec_buechi_empty_informative (intersect (VW_aut V W) aut )) as
[[x [y [D1 % VW_aut_correct D2] % match_accepted % intersect_correct]]|D' ].
+ eapply compatibility. 2: apply K. now exists(x +++ omega_iter y).
+ exfalso. now rewrite intersect_correct in D'.
Qed.
Lemma complement_exhaustive : RF -> L_B aut \$/ L_B complement =$= universal_language.
Proof.
intros Ramsey sigma. split; auto. intros _.
now apply complement_kind_exhaustive, totality.
Qed.
Lemma complement_exhaustive_up (x y : NStr Sigma) : L_B aut (x +++ omega_iter y) \/ L_B complement (x +++ omega_iter y).
Proof.
apply complement_kind_exhaustive, totality_up.
Qed.
End Complement.
Global Arguments complement {Sigma} aut.