Set Implicit Arguments.
Require Import Utils.
Require Import FinSets.
Require Import Strings.
Require Import Sequences.
Require Import NFAs.
Require Import Buechi.
Require Import Complement.
Require Import MinimalS1S.
Require Import FullS1S.
Require Import RegularLanguages.
Require Import FiniteSemigroups.
Require Import RamseyanFactorizations.
Require Import AdditiveRamsey.
Require Import RamseyanPigeonholePrinciple.
Require Import Utils.
Require Import FinSets.
Require Import Strings.
Require Import Sequences.
Require Import NFAs.
Require Import Buechi.
Require Import Complement.
Require Import MinimalS1S.
Require Import FullS1S.
Require Import RegularLanguages.
Require Import FiniteSemigroups.
Require Import RamseyanFactorizations.
Require Import AdditiveRamsey.
Require Import RamseyanPigeonholePrinciple.
Necessity of RF
We show that RF was necessary for complementation and FX by showing RF equivalent to- AC: Complement automata exist
- AX: Büchi acceptance satisfies XM
- AU: UP equivalent Büchi automata are equivalent
- FX: Satisfaction in S1S satisfies XM
Definition AC := forall Sigma (aut: NFA Sigma), exists aut', forall sigma, (L_B aut sigma -> ~ L_B aut' sigma) /\ (L_B aut sigma \/ L_B aut' sigma).
Definition AX := forall Sigma (aut: NFA Sigma), forall sigma, L_B aut sigma \/ ~ L_B aut sigma.
Definition AU := forall Sigma (aut1 aut2 : NFA Sigma), (forall (x y : NStr Sigma), L_B aut1 (x +++ omega_iter y) <-> L_B aut2 (x +++ omega_iter y)) -> (L_B aut1 =$= L_B aut2).
Lemma AC_implies_AX : AC -> AX.
Proof.
intros ac X aut sigma.
destruct (ac X aut) as [aut' H].
destruct (H sigma). tauto.
Qed.
We construct an automaton that accepts exactly the sequences admitting a Ramseyan factorization.
The automaton first guesses the color of the factorization and
then the positions where the factors begin and verifies the guesses.
To do that, we construct an automaton accepting sequences that have a Ramseyan factorization of given color
and take the union over all colors.
Section RamseyNFA.
Context (Gamma: FiniteSemigroup).
Definition ramsey_nfa_color a := prepend_nfa univ_aut (nfa_omega_iter (one_color_nfa a SUM)).
Lemma ramsey_nfa_color_correct a: L_B (ramsey_nfa_color a) =$= (fun sigma => exists (tau: Seq (NStr Gamma)), SUM ( tau 1) = a /\ is_ramseyan_factorization sigma tau).
Proof.
unfold ramsey_nfa_color.
rewrite prepend_nfa_correct, nfa_omega_iter_correct, one_color_nfa_correct, univ_aut_scorrect by apply SUM_is_homomorphism.
intros sigma. split.
- intros [y [sigma' [_ [[tau [L1 E1]] E2]]]]. destruct y as [|b y].
+ exists tau. repeat split; cbn in *; auto.
* now rewrite E2.
* intros n _. now rewrite !L1.
+ exists ((!(b :: y)) ::: tau). repeat split.
* now rewrite nth_step.
* rewrite E2, E1. symmetry. rewrite flatten_correct, tl_correct, hd_correct. now rewrite <-str_to_nstr_idem'.
* intros [|n] L; try now exfalso. now rewrite !nth_step, !L1.
- intros [tau [H1 [H2 H3]]]. exists (hd tau), (flatten (tl tau)). repeat split; auto.
+ exists (tl tau). split; try reflexivity.
intros n. rewrite <-nth_step_tl, H3; auto.
+ now rewrite H2, flatten_correct.
Qed.
Definition ramsey_nfa := big_union (List.map ramsey_nfa_color (elem Gamma) ).
Lemma ramsey_nfa_correct: L_B ramsey_nfa =$= admits_ramseyan_factorization.
Proof.
intros w. unfold ramsey_nfa. split.
- intros [nfa [[x [E _]]%in_map_iff L]] % big_union_correct.
subst nfa. apply ramsey_nfa_color_correct in L .
destruct L as [tau [_ RF]]. now exists tau.
- intros [tau RF]. apply big_union_correct. exists (ramsey_nfa_color (SUM (tau 1))). split.
+ apply in_map_iff. exists (SUM (tau 1)). split; auto.
+ apply ramsey_nfa_color_correct. exists tau. split; auto.
Qed.
End RamseyNFA.
Context (Gamma: FiniteSemigroup).
Definition ramsey_nfa_color a := prepend_nfa univ_aut (nfa_omega_iter (one_color_nfa a SUM)).
Lemma ramsey_nfa_color_correct a: L_B (ramsey_nfa_color a) =$= (fun sigma => exists (tau: Seq (NStr Gamma)), SUM ( tau 1) = a /\ is_ramseyan_factorization sigma tau).
Proof.
unfold ramsey_nfa_color.
rewrite prepend_nfa_correct, nfa_omega_iter_correct, one_color_nfa_correct, univ_aut_scorrect by apply SUM_is_homomorphism.
intros sigma. split.
- intros [y [sigma' [_ [[tau [L1 E1]] E2]]]]. destruct y as [|b y].
+ exists tau. repeat split; cbn in *; auto.
* now rewrite E2.
* intros n _. now rewrite !L1.
+ exists ((!(b :: y)) ::: tau). repeat split.
* now rewrite nth_step.
* rewrite E2, E1. symmetry. rewrite flatten_correct, tl_correct, hd_correct. now rewrite <-str_to_nstr_idem'.
* intros [|n] L; try now exfalso. now rewrite !nth_step, !L1.
- intros [tau [H1 [H2 H3]]]. exists (hd tau), (flatten (tl tau)). repeat split; auto.
+ exists (tl tau). split; try reflexivity.
intros n. rewrite <-nth_step_tl, H3; auto.
+ now rewrite H2, flatten_correct.
Qed.
Definition ramsey_nfa := big_union (List.map ramsey_nfa_color (elem Gamma) ).
Lemma ramsey_nfa_correct: L_B ramsey_nfa =$= admits_ramseyan_factorization.
Proof.
intros w. unfold ramsey_nfa. split.
- intros [nfa [[x [E _]]%in_map_iff L]] % big_union_correct.
subst nfa. apply ramsey_nfa_color_correct in L .
destruct L as [tau [_ RF]]. now exists tau.
- intros [tau RF]. apply big_union_correct. exists (ramsey_nfa_color (SUM (tau 1))). split.
+ apply in_map_iff. exists (SUM (tau 1)). split; auto.
+ apply ramsey_nfa_color_correct. exists tau. split; auto.
Qed.
End RamseyNFA.
Given AC we show that this automaton accepts all sequences.
Lemma AC_equiv_RF : AC <-> RF.
Proof.
split.
- intros ac Gamma sigma.
destruct (ac Gamma (ramsey_nfa Gamma)) as [aut H].
destruct (H sigma) as [H1 [H2|H2]].
+ apply ramsey_nfa_correct; auto.
+ exfalso. destruct (dec_buechi_empty_informative aut) as [[u [v L % match_accepted]]|D'].
* pose proof (up_admits_ramseyan_fac u v) as H'.
apply ramsey_nfa_correct in H'.
apply H in H'; auto.
* now apply D' in H2.
- intros rf X aut.
exists (complement aut). intros sigma. split.
+ intros H1 H2. eapply complement_disjoint; eauto.
+ now apply complement_exhaustive.
Qed.
End ACIffRF.
Lemma AU_equiv_AC: AC <-> AU.
Proof.
split.
- intros ac Sigma.
enough (forall (aut1 aut2 : NFA Sigma), (forall (x y:NStr Sigma), L_B aut1 (x +++ omega_iter y ) <-> L_B aut2 (x +++ omega_iter y )) -> (L_B aut1 <$= L_B aut2)) as H.
+ intros aut1 aut2 UPEq. split.
* apply H, UPEq.
* apply H. intros x y. symmetry. apply UPEq.
+ intros aut1 aut2 UPEq sigma.
destruct (ac Sigma aut2 ) as [aut2C Compl].
destruct (dec_buechi_empty_informative (intersect aut1 aut2C)) as [[u [v [L1 L2C] % match_accepted % intersect_correct]]|D].
* exfalso.
apply (Compl (u +++ omega_iter v)); auto.
now apply UPEq.
* intros L1. destruct (Compl sigma) as [H[ L2|NL2]]; auto.
exfalso. apply (D sigma), intersect_correct. split; auto.
- intros au Sigma aut. exists (complement aut). intros sigma. split.
+ intros LA LC. now apply (complement_disjoint aut sigma).
+ enough (L_B (union aut (complement aut) ) =$= L_B univ_aut) as H'.
* rewrite union_correct in H'. apply H', univ_aut_correct, I.
* apply au.
intros x y. split.
-- intros _. now apply univ_aut_correct.
-- intros _. apply union_correct.
apply complement_exhaustive_up.
Qed.
FX (S1S Satisfaction satisfies XM) Implies RP
To show that FX implies RF, we use FX to show that RP <-> RPc. We encode RP into an S1S formula and using FX can show it equivalent to the encoding of RPc.
Section FXImpliesRP.
Existing Instance Sequence.
Variable (MSO_XM : FX).
Arguments decision _ : simpl never.
Context (Gamma:FiniteSemigroup).
Implicit Types (a b c : Gamma).
Definition V_2 := Gamma (+) Gamma.
Instance V_1 : finTypeCardAtLeast3 := {|
V := finType_unit (+) finType_unit (+) finType_unit;
x1 := inr (tt);
x2 := inl (inr tt);
x3 := inl (inl tt) |}.
Proof.
all: congruence.
Qed.
Notation NatSet := (Seq finType_bool).
Implicit Types (I : V_1 -> nat) (J : V_2 -> NatSet) (phi : Form V_1 V_2).
Implicit Types (x y z : V_1) (n m : nat).
Instance sat_xm_satis I J phi: sat_xm (I # J |== phi).
Proof. apply MSO_XM. Qed.
Existing Instance Sequence.
Variable (MSO_XM : FX).
Arguments decision _ : simpl never.
Context (Gamma:FiniteSemigroup).
Implicit Types (a b c : Gamma).
Definition V_2 := Gamma (+) Gamma.
Instance V_1 : finTypeCardAtLeast3 := {|
V := finType_unit (+) finType_unit (+) finType_unit;
x1 := inr (tt);
x2 := inl (inr tt);
x3 := inl (inl tt) |}.
Proof.
all: congruence.
Qed.
Notation NatSet := (Seq finType_bool).
Implicit Types (I : V_1 -> nat) (J : V_2 -> NatSet) (phi : Form V_1 V_2).
Implicit Types (x y z : V_1) (n m : nat).
Instance sat_xm_satis I J phi: sat_xm (I # J |== phi).
Proof. apply MSO_XM. Qed.
Second order Variables to encode a sequence and the sums
Encoding Sequences as Sets
Definition seq_to_sets (sigma : Seq Gamma) a := (map (fun b => if (decision (b = a)) then true else false) sigma).
Lemma seq_to_sets_nth sigma a n: n elS (seq_to_sets sigma a) <-> sigma n = a.
Proof.
unfold seq_to_sets. simpl. unfold memSet. rewrite map_nth. destruct decision.
- tauto.
- split; intros H; now exfalso.
Qed.
Lemma seq_to_sets_nth sigma a n: n elS (seq_to_sets sigma a) <-> sigma n = a.
Proof.
unfold seq_to_sets. simpl. unfold memSet. rewrite map_nth. destruct decision.
- tauto.
- split; intros H; now exfalso.
Qed.
Definition phi_unique := all1 x1, AND { a | True} AND {b | a <> b } x1 el2 (Y a) ==>2 ~2 x1 el2 (Y b).
Lemma phi_unique_correct I J : I # J |== phi_unique <-> forall n a b, n elS (J (Y a)) -> n elS (J (Y b)) -> a = b.
Proof.
unfold phi_unique. rewrite all1_correct. apply iff_all. intros n.
rewrite finBigAndCorrect. apply iff_all. intros a.
rewrite iff_impl_true, finBigAndCorrect. apply iff_all. intros b.
rewrite !impl_correct, neg_correct, !el_correct. trivial_decision. split.
- intros D M1 M2. decide (a = b); auto. tauto.
- tauto.
Qed.
Definition phi_first x := AND { a | True} x el2 (X a) ==>2 x el2 (Y a).
Lemma phi_first_correct x I J : I # J |== phi_first x <-> forall a, (I x) elS (J (X a)) -> (I x) elS (J (Y a)).
Proof.
unfold phi_first. rewrite finBigAndCorrect.
apply iff_all. intros a. rewrite impl_correct; tauto.
Qed.
Definition phi_step x y := let z := fresh x y in
all1 z, (x <=2 z ==>2 z <=2 y ==>2
AND { a | True} AND {b | True} (z el2 (Y a)) ==>2
(IsSuccMem z (X b)) ==>2 (IsSuccMem z (Y (add a b)))).
Lemma phi_step_correct x y I J : I # J |== phi_step x y <-> forall n, I x <= n -> n <= I y ->
forall a b, n elS J (Y a) -> (S n) elS (J (X b)) -> (S n) elS (J (Y (add a b))).
Proof.
pose proof (fresh_correct x y) as [H1 H2]. unfold phi_step.
rewrite all1_correct.
apply iff_all. intros n.
rewrite !impl_correct, finBigAndCorrect, !leq_correct. trivial_decision.
apply iff_impl. reflexivity. apply iff_impl. reflexivity.
apply iff_all. intros a. rewrite finBigAndCorrect. rewrite iff_impl_true.
apply iff_all. intros b. rewrite iff_impl_true, !impl_correct, !isSuccMemCorrect, !el_correct.
now trivial_decision.
Qed.
Definition phi_last y c := y el2 (Y c).
Lemma phi_last_correct y c I J : I # J |== phi_last y c <-> I y elS J (Y c).
Proof. reflexivity. Qed.
Definition phi_sum_eq x y c := finBigEx2 Y (phi_unique /\2 phi_first x /\2 phi_step x y /\2 phi_last y c).
Encoding a sequence into an interpretation
Definition encode_seq J (sigma: Seq Gamma) := (finBigUpdate2 X (seq_to_sets sigma) J).
Lemma encode_seq_nth J sigma a n: n elS (encode_seq J sigma (X a)) <-> sigma n = a.
Proof.
unfold encode_seq. rewrite finBigUpdate2_changed.
- now rewrite seq_to_sets_nth.
- intros b c. unfold X. congruence.
Qed.
Lemma phi_sum_eq_correct x y c I J sigma : I x <= I y -> (I # (encode_seq J sigma) |== phi_sum_eq x y c <-> SUM (closed_substr sigma (I x) (I y)) = c).
Proof.
assert (injective Y)as InY. { intros a b. unfold Y. congruence. }
assert (forall a b, Y a <> X b) as YdifX. { intros a b. unfold X,Y . congruence. }
intros L. unfold phi_sum_eq. rewrite finBigEx2_correct; auto. split.
- intros [f Sat]. rewrite !and_correct, phi_unique_correct, phi_first_correct, phi_step_correct, phi_last_correct in Sat.
destruct Sat as [Un [In [St Ls]]].
enough (forall j, (I x) <= j <= (I y) -> j elS f (SUM (closed_substr sigma (I x) ( j) ))) as H.
+ apply Un with (n := I y); auto.
rewrite finBigUpdate2_changed by assumption.
apply H. omega.
+ clear Ls. induction L as [| m L2 IHL]; intros j L'.
* assert (j = I x) by omega. subst j.
rewrite closed_substr_singleton. cbn.
specialize (In (sigma (I x))). rewrite finBigUpdate2_changed, finBigUpdate2_unchanged in In; auto.
apply In. now rewrite encode_seq_nth.
* decide (j <= m) as [D|D].
-- apply IHL; auto.
-- assert (j = S m) by omega. subst j.
rewrite closed_substr_step_last, SUM_concat by auto. simpl.
pose proof (St m L2 (ltac:(omega)) ((SUM (closed_substr sigma (I x) m))) (sigma (S m))) as H.
rewrite !finBigUpdate2_changed, finBigUpdate2_unchanged, encode_seq_nth in H by auto.
apply H; auto.
- intros E. exists (seq_to_sets (wrap (fun k => SUM (closed_substr sigma (I x) k)))).
rewrite !and_correct, phi_unique_correct, phi_first_correct, phi_step_correct, phi_last_correct. repeat split.
+ intros n a b. rewrite !finBigUpdate2_changed, !seq_to_sets_nth by auto. congruence.
+ intros a. now rewrite !finBigUpdate2_changed, finBigUpdate2_unchanged, seq_to_sets_nth, encode_seq_nth, wrap_correct, closed_substr_singleton by auto.
+ intros n L1 L2 a b.
rewrite !finBigUpdate2_changed, finBigUpdate2_unchanged, !seq_to_sets_nth, encode_seq_nth, !wrap_correct by auto.
rewrite closed_substr_step_last, SUM_concat by assumption. cbn. congruence.
+ now rewrite finBigUpdate2_changed, seq_to_sets_nth, wrap_correct by auto.
Qed.
Definition phi_merge x y := let z := fresh x y in
ex1 z, ((x <=2 z /\2 y <=2 z) /\2 OR {a|True} (phi_sum_eq x z a /\2 phi_sum_eq y z a)).
Hint Resolve D1 D2 D3.
Lemma phi_merge_correct sigma x y I J: x <> y -> merge sigma (I x) (I y) <-> I # (encode_seq J sigma) |== phi_merge x y.
Proof.
pose proof (fresh_correct x y) as [H1 H2]. intros D.
unfold phi_merge. rewrite ex1_correct.
apply iff_ex. intros k. rewrite !and_correct, finBigOrCorrect, !leq_correct. trivial_decision. split.
- intros [[L1 L2] E]. repeat split; auto.
exists (SUM (closed_substr sigma (I x) k)). rewrite !and_correct, !phi_sum_eq_correct; trivial_decision; auto.
- intros [[L1 L2] [a E]]. repeat split; auto.
rewrite !and_correct, !phi_sum_eq_correct in E; trivial_decision; auto.
destruct E as [[E1 E2] _]. now rewrite E1, E2.
Qed.
Lemma FX_implies_RP_sigma sigma : RP_sigma sigma .
Proof.
destruct (MSO_XM (ex1 x1, all1 x3, ex1 x2, x3 <=2 x2 /\2 phi_merge x1 x2) (fun x => 0) (encode_seq (fun X => singletonSet 0) sigma)) as [D|D].
- destruct D as [i D]. exists i. intros j.
rewrite all1_correct in D. specialize (D j). destruct D as [k [L % leq_correct E]]. trivial_decision.
exists k. split; auto.
apply phi_merge_correct in E; auto. now trivial_decision.
- exfalso. apply (RPc_holds (sigma:= sigma)).
intros i.
rewrite <-neg_correct, s1s_DM_exist_neg, all1_correct in D.
specialize (D i).
apply s1s_DM_forall_neg in D. destruct D as [j D].
exists j. intros k.
apply s1s_DM_exist_neg in D. rewrite all1_correct in D.
specialize (D k).
apply s1s_DM_neg_and, or_correct in D. destruct D as [D|D].
+ left. rewrite neg_correct, leq_correct in D. trivial_decision. omega.
+ right. intros NE. apply D, phi_merge_correct; auto.
now trivial_decision.
Qed.
End FXImpliesRP.
Lemma FX_implies_RP: FX -> RP.
Proof.
intros fx Gamma sigma.
now apply FX_implies_RP_sigma.
Qed.
ex1 z, ((x <=2 z /\2 y <=2 z) /\2 OR {a|True} (phi_sum_eq x z a /\2 phi_sum_eq y z a)).
Hint Resolve D1 D2 D3.
Lemma phi_merge_correct sigma x y I J: x <> y -> merge sigma (I x) (I y) <-> I # (encode_seq J sigma) |== phi_merge x y.
Proof.
pose proof (fresh_correct x y) as [H1 H2]. intros D.
unfold phi_merge. rewrite ex1_correct.
apply iff_ex. intros k. rewrite !and_correct, finBigOrCorrect, !leq_correct. trivial_decision. split.
- intros [[L1 L2] E]. repeat split; auto.
exists (SUM (closed_substr sigma (I x) k)). rewrite !and_correct, !phi_sum_eq_correct; trivial_decision; auto.
- intros [[L1 L2] [a E]]. repeat split; auto.
rewrite !and_correct, !phi_sum_eq_correct in E; trivial_decision; auto.
destruct E as [[E1 E2] _]. now rewrite E1, E2.
Qed.
Lemma FX_implies_RP_sigma sigma : RP_sigma sigma .
Proof.
destruct (MSO_XM (ex1 x1, all1 x3, ex1 x2, x3 <=2 x2 /\2 phi_merge x1 x2) (fun x => 0) (encode_seq (fun X => singletonSet 0) sigma)) as [D|D].
- destruct D as [i D]. exists i. intros j.
rewrite all1_correct in D. specialize (D j). destruct D as [k [L % leq_correct E]]. trivial_decision.
exists k. split; auto.
apply phi_merge_correct in E; auto. now trivial_decision.
- exfalso. apply (RPc_holds (sigma:= sigma)).
intros i.
rewrite <-neg_correct, s1s_DM_exist_neg, all1_correct in D.
specialize (D i).
apply s1s_DM_forall_neg in D. destruct D as [j D].
exists j. intros k.
apply s1s_DM_exist_neg in D. rewrite all1_correct in D.
specialize (D k).
apply s1s_DM_neg_and, or_correct in D. destruct D as [D|D].
+ left. rewrite neg_correct, leq_correct in D. trivial_decision. omega.
+ right. intros NE. apply D, phi_merge_correct; auto.
now trivial_decision.
Qed.
End FXImpliesRP.
Lemma FX_implies_RP: FX -> RP.
Proof.
intros fx Gamma sigma.
now apply FX_implies_RP_sigma.
Qed.
AX (Büchi Acceptance Satisfies XM) Implies RP
Here we cannot simply encode RP into an automaton because this would require complementation, which need RF (or RP) already. We give a more fine grained analysis on which predicates need to satisfy XM such that RP is equivalent to RPc. We then encode this predicates into automata.
The following predicates need to satisfy XM:
Implicit Types (Gamma: FiniteSemigroup).
Definition P1 Gamma sigma i k:= exists j, j >= k /\ merge sigma i j.
Definition P2 Gamma sigma := exists i, forall k, exists j, j >= k /\ merge sigma i j.
Definition P3 Gamma sigma i:= exists k, ~exists j,j >= k /\ merge sigma i j.
Lemma RP_iff_RPc_pred Gamma sigma:
(forall i k, sat_xm (P1 sigma i k)) -> sat_xm (P2 sigma) -> (forall i, sat_xm (P3 sigma i)) ->
RPc_sigma sigma <-> RP_sigma sigma.
Proof.
intros H1 H2 H3.
unfold RPc_sigma, RP_sigma.
rewrite <-deMorgan_exists; auto.
apply iff_neg, iff_all. intros i.
rewrite <-deMorgan_exists.
- apply iff_neg, iff_all. intros k.
setoid_rewrite double_negation at 4; auto.
apply iff_neg. rewrite deMorgan_all.
apply iff_all. intros j.
apply bounded_pred.
- apply (sat_xm_iff (P:= P3 sigma i)).
+ apply iff_ex. intros k.
rewrite deMorgan_all.
apply iff_all. intros j.
symmetry. apply bounded_pred.
+ apply H3.
Qed.
Corollary pred_xm_RP Gamma sigma :
(forall i k, sat_xm (P1 sigma i k)) -> sat_xm (P2 sigma) -> (forall i, sat_xm (P3 sigma i)) ->
RP_sigma sigma.
Proof.
intros X1 X2 X3.
apply RP_iff_RPc_pred; auto.
apply RPc_holds.
Qed.
Basic Automata for the Predicates
Instead of building for each predicate a specific automaton, we define some more general automata and compose them using closure operations forall each prediacte. This differs from the approach in the paper, but allows a more compositional approach and verification.
Section ExAut.
Context {Sigma: finType}.
Variable (P: Sigma -> Prop).
Context {decP: forall x, dec (P x)}.
Definition ex_aut := mknfa (fun p b q => match q with
| false => True
| true => p = true \/ (P b) end)
(fun p => p = false)
(fun p => p = true).
Lemma ex_aut_correct: L_B ex_aut =$= fun sigma => exists n, P (sigma n).
Proof.
intros sigma. split.
- intros [rho [V [I F]]].
specialize (F 0).
pose proof (cc_nat_first_geq_exists_correct F) as H.
pose proof (cc_nat_first_geq_exists_all (L:=F)) as H2.
revert H H2. generalize (cc_nat_first_geq_exists F).
intros k Fk N. destruct k.
+ exfalso. unfold initial in I. congruence.
+ exists k.
specialize (V k). rewrite Fk in V.
specialize (N k).
destruct (rho k).
* exfalso. apply N; auto. reflexivity.
* cbn in V. destruct V; auto. now exfalso.
- intros [n H]. revert sigma H. induction n; intros sigma H.
+ exists (false ::: const true). repeat split.
* intros [|n]; cbn; rewrite ?nth_step, ?nth_first, ?const_nth; auto.
* intros n. exists (S n). repeat split; auto. now rewrite nth_step, const_nth.
+ destruct (IHn (tl sigma)) as [rho [V [I F]]].
* now rewrite <-nth_step_tl.
* exists (false ::: rho). repeat split; auto.
-- intros [| m]; cbn; rewrite ?nth_step, ?nth_first, ?const_nth; auto.
++ cbn in I. now rewrite I.
++ apply V.
-- now apply inf_often_cons.
Qed.
End ExAut.
Context {Sigma: finType}.
Variable (P: Sigma -> Prop).
Context {decP: forall x, dec (P x)}.
Definition ex_aut := mknfa (fun p b q => match q with
| false => True
| true => p = true \/ (P b) end)
(fun p => p = false)
(fun p => p = true).
Lemma ex_aut_correct: L_B ex_aut =$= fun sigma => exists n, P (sigma n).
Proof.
intros sigma. split.
- intros [rho [V [I F]]].
specialize (F 0).
pose proof (cc_nat_first_geq_exists_correct F) as H.
pose proof (cc_nat_first_geq_exists_all (L:=F)) as H2.
revert H H2. generalize (cc_nat_first_geq_exists F).
intros k Fk N. destruct k.
+ exfalso. unfold initial in I. congruence.
+ exists k.
specialize (V k). rewrite Fk in V.
specialize (N k).
destruct (rho k).
* exfalso. apply N; auto. reflexivity.
* cbn in V. destruct V; auto. now exfalso.
- intros [n H]. revert sigma H. induction n; intros sigma H.
+ exists (false ::: const true). repeat split.
* intros [|n]; cbn; rewrite ?nth_step, ?nth_first, ?const_nth; auto.
* intros n. exists (S n). repeat split; auto. now rewrite nth_step, const_nth.
+ destruct (IHn (tl sigma)) as [rho [V [I F]]].
* now rewrite <-nth_step_tl.
* exists (false ::: rho). repeat split; auto.
-- intros [| m]; cbn; rewrite ?nth_step, ?nth_first, ?const_nth; auto.
++ cbn in I. now rewrite I.
++ apply V.
-- now apply inf_often_cons.
Qed.
End ExAut.
An automaton that asserts that every position of accepted sequences satisfy a predicate.
Section AutAll.
Context {Sigma: finType}.
Variable (P: Sigma -> Prop).
Context {decP: forall x, dec (P x)}.
Definition all_aut := mknfa (fun p a q => match p, q with
| false, false => True
| true, true => P a
| true, false => ~ P a
| _, _ => False end)
(fun p => p = true)
(fun p => p = true).
Lemma all_aut_correct: L_B all_aut =$= fun sigma => forall n, P (sigma n).
Proof.
intros sigma. split.
- intros [r [V [I F]]].
assert (forall n, r n =true) as H. {
intros n. revert r sigma V I F. induction n; intros r sigma V I F.
- apply I.
- rewrite nth_step_tl. apply IHn with (sigma := tl sigma).
+ now apply valid_run_tl.
+ specialize (V 0) as V0. unfold initial. rewrite <-nth_step_tl.
rewrite I in V0. destruct (r 1) eqn:H; try reflexivity.
exfalso. destruct (F 1) as [m [Q1 Q2]]. enough (r m = false) as H2.
* rewrite Q2 in H2. congruence.
* clear Q2. induction Q1; auto.
specialize (V m). rewrite IHQ1 in V. destruct (r (S m)); auto. now exfalso.
+ now apply inf_often_tl.
}
intros n. specialize (V n). now rewrite !H in V.
- intros H. exists (const true). repeat split.
+ intros n. rewrite !const_nth. apply H.
+ intros n. exists n. repeat split; auto. now rewrite const_nth.
Qed.
End AutAll.
Context {Sigma: finType}.
Variable (P: Sigma -> Prop).
Context {decP: forall x, dec (P x)}.
Definition all_aut := mknfa (fun p a q => match p, q with
| false, false => True
| true, true => P a
| true, false => ~ P a
| _, _ => False end)
(fun p => p = true)
(fun p => p = true).
Lemma all_aut_correct: L_B all_aut =$= fun sigma => forall n, P (sigma n).
Proof.
intros sigma. split.
- intros [r [V [I F]]].
assert (forall n, r n =true) as H. {
intros n. revert r sigma V I F. induction n; intros r sigma V I F.
- apply I.
- rewrite nth_step_tl. apply IHn with (sigma := tl sigma).
+ now apply valid_run_tl.
+ specialize (V 0) as V0. unfold initial. rewrite <-nth_step_tl.
rewrite I in V0. destruct (r 1) eqn:H; try reflexivity.
exfalso. destruct (F 1) as [m [Q1 Q2]]. enough (r m = false) as H2.
* rewrite Q2 in H2. congruence.
* clear Q2. induction Q1; auto.
specialize (V m). rewrite IHQ1 in V. destruct (r (S m)); auto. now exfalso.
+ now apply inf_often_tl.
}
intros n. specialize (V n). now rewrite !H in V.
- intros H. exists (const true). repeat split.
+ intros n. rewrite !const_nth. apply H.
+ intros n. exists n. repeat split; auto. now rewrite const_nth.
Qed.
End AutAll.
An automaton that computes the sum of the seen prefix in a semigroup. For sake of composition,
the automaton just runs on some finite type Sigma for which it has a projection base
yielding the symbols of the semigroup and a projection sum yielding the sum. The automaton
asserts that the sum is actually correct. Because the sum is part of the input alphabet,
other automata can use the sum, too, which will be important for composition.
Section SumAut.
Context (Gamma: FiniteSemigroup) (Sigma: finType) (base : Sigma -> Gamma) (sum: Sigma -> Gamma).
Definition sum_aut_trans p a q := match p, q with
| None , Some c => c = base a /\ base a = sum a
| Some b, Some c => c = add b (base a) /\ sum a = c
| _ , _ => False
end.
Definition sum_aut := mknfa sum_aut_trans
(fun p => p = None)
(fun q => True).
Lemma sum_aut_trans_correct : L_B sum_aut =$= fun (sigma:Seq Sigma) => map sum sigma == wrap (fun n => SUM (closed_prefix (map base sigma) n)).
Proof.
intros sigma. split.
- intros [rho [V [I F]]].
assert (forall n, rho (S n) = Some (SUM (closed_prefix (map base sigma) n)) /\ rho (S n) = Some (sum (sigma n))) as H.
+ intros n. induction n.
* specialize (V 0). rewrite I in V. simpl. rewrite <-nth_first_hd. rewrite map_nth. simpl eqtype in * .
destruct (rho 1); cbn in V.
-- destruct V as [V1 V2]. now rewrite V1, V2.
-- now exfalso.
* specialize (V (S n)). destruct IHn as [IHn _]. rewrite IHn in V. simpl eqtype in *. simpl in V. destruct (rho (S (S n))).
-- destruct V as [V1 V2]. split.
++ rewrite V1. f_equal. rewrite_eq (S n = S(n+ 0)) at 2.
rewrite closed_prefix_plus. simpl. rewrite SUM_concat, <-nth_first_hd, drop_nth, <-nth_step_tl, map_nth.
now rewrite_eq (n + 0 = n).
++ now rewrite V2.
-- now exfalso.
+ intros n. destruct (H n) as [H1 H2]. rewrite H2 in H1. rewrite map_nth.
symmetry. rewrite wrap_correct. congruence.
- intros H.
exists (None ::: (map Some (wrap (fun n => (SUM (closed_prefix (map base sigma) n)))))). repeat split.
+ intros [|n].
* rewrite nth_first, nth_step, map_nth, wrap_correct. simpl. split; auto.
specialize (H 0). now rewrite map_nth, !wrap_correct in H.
* rewrite !nth_step, !map_nth. rewrite !wrap_correct. split.
-- rewrite_eq (S n = S(n+ 0)) . rewrite closed_prefix_plus. simpl. rewrite SUM_concat, <-nth_first_hd, drop_nth, <-nth_step_tl, map_nth.
now rewrite_eq (n + 0 = n).
-- specialize (H (S n) ). now rewrite map_nth, !wrap_correct in H.
+ intros n. exists n. split; auto. reflexivity.
Qed.
End SumAut.
An automaton that computes the the of sum of all suffixes of the seen prefix in a semigroup.
It is build similarly to the automaton before using some finite type as input alphabet with
projections for the elements of the semigroup and the set of sums.
Section SuffixSumsAut.
Context (Gamma: FiniteSemigroup )(Sigma: finType) (base : Sigma -> Gamma) (suffix_sums: Sigma -> finSet Gamma).
Definition suffixsums_aut_trans p (a: Sigma) q := match p, q with
| None , Some N => N = singleton (base a) /\ suffix_sums a = N
| Some M, Some N => N = FinSets.union (singleton (base a)) (set_map M (fun b => add b (base a))) /\ suffix_sums a = N
| _ , _ => False
end.
Definition suffixsums_aut := mknfa suffixsums_aut_trans
(fun p => p = None)
(fun q => True).
Lemma suffixsums_aut_trans_correct : L_B suffixsums_aut =$= fun (sigma:Seq Sigma) => map suffix_sums sigma == wrap (fun n => makeSet (fun a => exists j, j <= n /\ a = SUM (closed_substr (map base sigma) j n))).
Proof.
intros sigma. split.
- intros [rho [V [I F]]].
assert (forall n, rho (S n) = Some (makeSet (fun a => exists j, j <= n /\ a = SUM (closed_substr (map base sigma) j n))) /\ rho (S n) = Some (suffix_sums (sigma n))) as H.
+ intros n. induction n.
* specialize (V 0). rewrite I in V. simpl. simpl eqtype in * .
destruct (rho 1) as[v|]; cbn in V.
-- destruct V as [V1 V2]. subst v. split; f_equal.
++ apply set_eq. intros x. rewrite makeSet_correct. split.
** intros H %singleton_correct. exists 0. repeat split; auto.
** intros [j [H1 H2]]. apply singleton_correct'. subst x. destruct j; auto.
++ now symmetry.
-- now exfalso.
* specialize (V (S n)). destruct IHn as [IHn _]. rewrite IHn in V. simpl eqtype in *. simpl in V. destruct (rho (S (S n))) as [v|].
-- destruct V as [V1 V2]. subst v. split.
++ f_equal. apply set_eq. intros x. rewrite FinSets.union_correct, makeSet_correct, set_map_correct. split.
** intros [h % singleton_correct | [y [[j [H1 H2]]%makeSet_correct H3]]].
--- exists (S n). split; auto. now rewrite closed_substr_singleton, map_nth.
--- exists j. split; auto.
now rewrite closed_substr_step_last, SUM_concat, <-H2, map_nth by auto.
** intros [j [H1 H2]]. decide (j = S n).
--- left. apply singleton_correct'. subst j. now rewrite closed_substr_singleton, map_nth in H2.
--- right. exists ( SUM (closed_substr (map base sigma) j n)). split.
+++ rewrite makeSet_correct. exists j. split; auto.
+++ now rewrite closed_substr_step_last, SUM_concat, map_nth in H2 by auto.
++ now rewrite V2.
-- now exfalso.
+ intros n. destruct (H n) as [H1 H2]. rewrite H2 in H1. rewrite map_nth.
symmetry. rewrite wrap_correct. congruence.
- intros H.
exists (None ::: (map Some (wrap (fun n => makeSet (fun a => exists j, j <= n /\ a = SUM (closed_substr (map base sigma) j n)))))). repeat split.
+ intros [|n].
* rewrite nth_first, nth_step, map_nth, !wrap_correct. simpl. split.
-- apply set_eq. intros x. rewrite makeSet_correct. split.
++ intros [j [H1 H2]]. apply singleton_correct'. subst x. destruct j; auto.
++ intros H2 %singleton_correct. exists 0. split; auto.
-- specialize (H 0). rewrite map_nth, wrap_correct in H. rewrite H.
apply set_eq. intros x. rewrite !makeSet_correct.
split; intros [j [H1 H2]]; exists j; split; auto.
* rewrite !nth_step, !map_nth. rewrite !wrap_correct. split.
-- apply set_eq. intros x. rewrite FinSets.union_correct, set_map_correct, !makeSet_correct. split.
++ intros [j [H1 H2]]. decide (j = S n).
** subst j. left. apply singleton_correct'. subst x. now rewrite closed_substr_singleton, map_nth.
** right. exists (SUM (closed_substr (map base sigma) j n)). split.
--- apply makeSet_correct. exists j; split; auto.
--- subst x. now rewrite closed_substr_step_last, SUM_concat, map_nth by auto.
++ intros [H1 %singleton_correct | [y [[j [H1 H2]]%makeSet_correct H3]]].
** subst x. exists (S n). split; auto. now rewrite closed_substr_singleton, map_nth.
** subst x. exists j. split; auto. subst y. now rewrite closed_substr_step_last, SUM_concat, map_nth.
-- specialize (H (S n)). rewrite map_nth, !wrap_correct in H. now rewrite H.
+ intros n. exists n. split; auto. reflexivity.
Qed.
End SuffixSumsAut.
We now encode the predicates into automata. Using AX the predicates satisfy XM.
Lemma sat_xm_nat_dec_exists (P: nat -> Prop): (forall n, dec (P n)) -> sat_xm (exists n, P n).
Proof.
intros Dec.
pose (sigma := wrap (X := finType_bool) (fun n => if (decision (P n)) then true else false) ).
apply sat_xm_iff with (P:= L_B (ex_aut (P:=fun b => b = true) ) sigma).
- rewrite (ex_aut_correct sigma).
split; intros [n H]; exists n; subst sigma; rewrite wrap_correct in *; now destruct decision.
- apply ax.
Qed.
Lemma sat_xm_exists_merging Gamma sigma i k: sat_xm (P1 sigma i k).
Proof.
unfold merge.
apply sat_xm_iff with (P := (exists m, exists j,
j <= m /\ k <= j /\ m >= i /\
SUM (closed_substr sigma i m) = SUM (closed_substr sigma j m))).
- split.
+ intros [m [j [H1 [H2 [H3 H4]]]]]. exists j. split; auto. now exists m.
+ intros [j [H1 [m [[H2 H3] H4]]]]. now exists m, j.
- apply sat_xm_nat_dec_exists. auto.
Qed.
We build an automaton that accepts the regular language consisting of all strings x such that
exists k, sum x = sum (nstr_drop x k). This corresponds to the substring from i to k in a sequence
sigma if for some j with i <= j <=k, i merges with j at k.
Again we generalize the alphabet such that sum x is part of the alphabet. This allows
to take the ω-iteration of the automaton to obtain a Büchi automaton that assert that there
are infinitely merging positions.
Section MergesAut.
Context (Sigma: finType) (base: Sigma -> Gamma) (sum : Sigma -> Gamma).
Definition merges_aut := mknfa (fun (p: ? Gamma (x) finType_bool ) a (q: ? Gamma (x) finType_bool ) => match p,q with
| (None, false), ( None , false) => True
| (None, false), (Some b, false) => b = base a
| (None, false), (Some b, true ) => b = base a /\ sum a = b
| (Some c, _ ), (Some b, false) => b = add c (base a)
| (Some c, _ ), (Some b, true ) => b = add c (base a) /\ sum a = b
| _, _ => False end)
(fun p => p = (None, false))
(fun p => match p with
| (Some _, true ) => True
| _ => False end).
Lemma intermediate_sum c b x: snaccepting_ind (aut:= merges_aut) (Some c, b) x -> add c (SUM (nstr_map base x)) = sum (x (delta x)).
Proof.
enough (forall (q: state merges_aut), (exists c b, q = (Some c ,b)) -> snaccepting_ind q x ->
match q with
| (Some c, b) => add c (SUM (nstr_map base x)) = sum (nstr_nth x (delta x))
| _ => False end).
{ apply H. now exists c, b. }
clear c b. intros q E H. induction H as [p a q | p q a x T A]; destruct E as [c [b E]]; subst p.
- destruct q as [[q|] [|]]; try now exfalso. cbn in *.
destruct H as [H1 H2]. now subst q.
- cbn. destruct q as [[q|] b']; try (now exfalso).
rewrite <-IHA.
+ cbn in T. destruct b'; [destruct T as [T _]| idtac]; subst q; now rewrite Assoc.
+ now exists q, b'.
Qed.
Lemma intermediate_sum_rev c b x: add c (SUM (nstr_map base x)) = sum (x (delta x)) -> snaccepting_ind (aut:= merges_aut) (Some c, b) x .
Proof.
revert c b. induction x; intros c b H.
- apply naccept_sing with (q := (Some (add c (base a)), true)).
+ cbn. split; auto.
+ reflexivity.
- cbn in H. apply naccept_step with (p := (Some (add c (base a)), false)).
+ now cbn.
+ apply IHx. now rewrite <-Assoc.
Qed.
Lemma transition_from_none a q b : transition (aut:= merges_aut) (None, false) a (Some q, b) -> q = base a.
Proof.
destruct b; simpl; tauto.
Qed.
Lemma guess_sum x: snaccepting_ind (aut:= merges_aut) (None, false) x -> exists k, k <= delta x /\ SUM (nstr_map base (nstr_drop x k)) = sum (x (delta x)).
Proof.
enough (forall (q: state merges_aut), q = (None, false) -> snaccepting_ind q x ->
match q with
| (None, false) => exists k, k <= delta x /\ SUM (nstr_map base (nstr_drop x k)) = sum (x (delta x))
| _ => False end).
{ now apply H. }
intros q E H. induction H as [p a q | p q a x T A]; subst p.
- destruct q as [[q|] [|]]; try now exfalso. cbn in *.
destruct H as [H1 H2]. subst q. exists 0. split; auto.
- cbn. destruct q as [[q|] b'].
+ apply transition_from_none in T.
apply intermediate_sum in A. subst q.
exists 0. split; auto.
+ destruct b'; try now exfalso.
destruct IHA as [k [H1 H2]]; auto.
exists (S k). split; auto.
Qed.
Lemma guess_sum_rev x:(exists k, k <= delta x /\ SUM (nstr_map base (nstr_drop x k)) = sum (x (delta x))) -> snaccepting_ind (aut:= merges_aut) (None, false) x.
Proof.
induction x; intros [k [H1 H2]].
- cbn in H1. destruct k; try now exfalso.
cbn in H2. now apply naccept_sing with (q:= (Some (base a), true)).
- destruct k.
+ cbn in H2. apply naccept_step with (p:= (Some (base a), false)).
* reflexivity.
* now apply intermediate_sum_rev.
+ cbn in H1. apply naccept_step with (p:= (None, false)).
* reflexivity.
* apply IHx. exists k. split; auto.
Qed.
Lemma merges_aut_correct: L_NR merges_aut =$= fun x => exists k, k <= delta x /\ SUM (nstr_map base (nstr_drop x k)) = sum (x (delta x)).
Proof.
intros x. split.
- intros [q [H1 H2]].
apply guess_sum.
cbn in H1. now subst q.
- intros H.
exists (None, false). split.
* reflexivity.
* now apply guess_sum_rev.
Qed.
End MergesAut.
The automaton asserting that there are infinitely many merging positions is obtained by the
ω$-iteration of the pervious NFA, intersection with the automaton that asserts that
the [sum] component of the input alphabet is actually correct, and then projection the [sum]
component out.
Definition aut_inf_merging := image_aut fst
(intersect
(nfa_omega_iter (merges_aut fst snd))
(sum_aut fst snd)).
Lemma map_fst_omega (X Y : Type) (f: Seq X) (g : nat -> Y): map fst (wrap (fun n => (f n, g n)) ) == f.
Proof.
intros n. now rewrite !map_nth, !wrap_correct.
Qed.
Lemma aut_exists_inf_merging_correct: exists aut, L_B aut =$= fun sigma => forall k, exists j, k <= j /\ merge sigma 0 j.
Proof.
exists aut_inf_merging.
unfold aut_inf_merging. rewrite image_aut_correct, intersect_correct, nfa_omega_iter_correct, sum_aut_trans_correct, merges_aut_correct.
intros sigma. split.
- intros [tau [H1 [[tau' [H2 H4]] H3]]].
intros k.
rewrite !H4 in H3, H1.
assert (map snd (flatten tau') == wrap (fun n => SUM (closed_prefix (map fst (flatten tau')) n))) as H7.
{ intros n. rewrite H3. apply nth_proper; auto. intros m. rewrite !wrap_correct. now rewrite H4. }
clear H3 H4 tau. enough (exists j : nat, k <= j /\ exists k, k >= j /\ SUM (closed_substr (map fst (flatten tau')) j k) = snd (flatten tau' k)).
+ destruct H as [j [H3 [n [H4 H5]]]].
exists j. split; auto. exists n. repeat split; auto. rewrite <-H1.
simpl eqtype in *. rewrite H5.
specialize (H7 n). rewrite map_nth in H7. rewrite wrap_correct in H7. rewrite H7.
now rewrite closed_substr_begin.
+ clear H1 sigma H7. revert tau' H2. induction k; intros tau' H2.
* destruct (H2 0) as [j [H3 H4]]. exists j. repeat split; auto.
exists (delta (tau' 0)). repeat split; auto.
assert (SUM (closed_substr (map fst (flatten tau')) j (delta (tau' 0))) = SUM (nstr_map fst (nstr_drop (tau' 0) j))) as H5.
-- simpl eqtype in *.
unfold closed_substr. rewrite drop_map, closed_prefix_map.
rewrite <-closed_substr_begin, closed_substr_shift.
rewrite_eq (j + 0 = j). rewrite_eq (j + (delta (tau' 0) - j) = delta (tau' 0)).
f_equal. rewrite flatten_correct, <-nth_first_hd.
now rewrite closed_substr_prepend.
-- rewrite H5. simpl eqtype in *. rewrite H4.
rewrite flatten_correct, <-nth_first_hd, prepend_nstr_nth_first; auto.
* destruct (IHk (tl tau')) as [n[ H3 H4]].
-- intros n. apply (H2 (S n)).
-- exists (S (delta (tau' 0)) + n). split; auto.
destruct H4 as [m [H5 H6]].
exists (S (delta (tau' 0)) + m). repeat split; auto.
simpl eqtype in *. rewrite flatten_correct.
rewrite <-nth_first_hd, prepend_nstr_nth_rest, <-H6.
f_equal. rewrite <-closed_substr_shift, map_nstr_prepend.
rewrite <-nstr_map_delta with (f:= fst). now rewrite revert_nstr_prepend.
- intros E. exists (wrap (fun n => (sigma n, SUM (closed_prefix sigma n)))). repeat split.
+ intros n. now rewrite map_nth, wrap_correct.
+ destruct (inf_merging_to_function E) as [f [H0 H1]].
exists (wrap (fun n => closed_substr (wrap (fun n => (sigma n, SUM (closed_prefix sigma n)))) ( (f n)) (pred (f (S n))))). split.
* intros n. destruct (H1 n) as [k [H2 H3]]. exists (k - ( f n)). repeat split.
-- rewrite wrap_correct, closed_substr_delta. omega.
-- rewrite wrap_correct, closed_substr_delta, closed_substr_nth', wrap_correct by auto.
rewrite_eq (f n + (pred (f (S n)) - f n) = pred (f (S n))). rewrite <-closed_substr_begin. rewrite H3. simpl snd.
unfold closed_substr. rewrite <-closed_substr_nstr_drop, closed_substr_shift by auto.
rewrite_eq (f n + (k - f n) = k). rewrite_eq (f n + (pred (f (S n)) - (f n)) = pred ( f (S n))).
unfold closed_substr. rewrite <-closed_prefix_map.
f_equal. rewrite closed_prefix_proper. 1, 3: reflexivity.
intros m. now rewrite map_nth, !drop_nth, !wrap_correct.
* apply factorize_monotone. split; auto.
intros n. destruct (H1 n) as [k [H2 _]]. omega.
+ intros n. rewrite map_nth, !wrap_correct. cbn. f_equal. apply closed_prefix_proper; auto.
intros m. now rewrite map_nth, wrap_correct.
Qed.
Lemma aut_inf_merging_correct: exists aut, L_B aut =$= fun sigma => exists i, forall k, exists j, k <= j /\ merge (drop sigma i) 0 j.
Proof.
destruct aut_exists_inf_merging_correct as [aut H].
exists (prepend_nfa univ_aut aut).
rewrite prepend_nfa_correct, H, univ_aut_scorrect. intros sigma. split.
- intros [x [tau [_ [H1 H2]]]].
exists (length x). intros k.
destruct (H1 k) as [j [Q1 Q2]].
exists j. split; auto.
now rewrite H2, revert_prepend.
- intros [i H1].
exists (prefix sigma i), (drop sigma i). repeat split; auto.
apply revert_drop.
Qed.
(intersect
(nfa_omega_iter (merges_aut fst snd))
(sum_aut fst snd)).
Lemma map_fst_omega (X Y : Type) (f: Seq X) (g : nat -> Y): map fst (wrap (fun n => (f n, g n)) ) == f.
Proof.
intros n. now rewrite !map_nth, !wrap_correct.
Qed.
Lemma aut_exists_inf_merging_correct: exists aut, L_B aut =$= fun sigma => forall k, exists j, k <= j /\ merge sigma 0 j.
Proof.
exists aut_inf_merging.
unfold aut_inf_merging. rewrite image_aut_correct, intersect_correct, nfa_omega_iter_correct, sum_aut_trans_correct, merges_aut_correct.
intros sigma. split.
- intros [tau [H1 [[tau' [H2 H4]] H3]]].
intros k.
rewrite !H4 in H3, H1.
assert (map snd (flatten tau') == wrap (fun n => SUM (closed_prefix (map fst (flatten tau')) n))) as H7.
{ intros n. rewrite H3. apply nth_proper; auto. intros m. rewrite !wrap_correct. now rewrite H4. }
clear H3 H4 tau. enough (exists j : nat, k <= j /\ exists k, k >= j /\ SUM (closed_substr (map fst (flatten tau')) j k) = snd (flatten tau' k)).
+ destruct H as [j [H3 [n [H4 H5]]]].
exists j. split; auto. exists n. repeat split; auto. rewrite <-H1.
simpl eqtype in *. rewrite H5.
specialize (H7 n). rewrite map_nth in H7. rewrite wrap_correct in H7. rewrite H7.
now rewrite closed_substr_begin.
+ clear H1 sigma H7. revert tau' H2. induction k; intros tau' H2.
* destruct (H2 0) as [j [H3 H4]]. exists j. repeat split; auto.
exists (delta (tau' 0)). repeat split; auto.
assert (SUM (closed_substr (map fst (flatten tau')) j (delta (tau' 0))) = SUM (nstr_map fst (nstr_drop (tau' 0) j))) as H5.
-- simpl eqtype in *.
unfold closed_substr. rewrite drop_map, closed_prefix_map.
rewrite <-closed_substr_begin, closed_substr_shift.
rewrite_eq (j + 0 = j). rewrite_eq (j + (delta (tau' 0) - j) = delta (tau' 0)).
f_equal. rewrite flatten_correct, <-nth_first_hd.
now rewrite closed_substr_prepend.
-- rewrite H5. simpl eqtype in *. rewrite H4.
rewrite flatten_correct, <-nth_first_hd, prepend_nstr_nth_first; auto.
* destruct (IHk (tl tau')) as [n[ H3 H4]].
-- intros n. apply (H2 (S n)).
-- exists (S (delta (tau' 0)) + n). split; auto.
destruct H4 as [m [H5 H6]].
exists (S (delta (tau' 0)) + m). repeat split; auto.
simpl eqtype in *. rewrite flatten_correct.
rewrite <-nth_first_hd, prepend_nstr_nth_rest, <-H6.
f_equal. rewrite <-closed_substr_shift, map_nstr_prepend.
rewrite <-nstr_map_delta with (f:= fst). now rewrite revert_nstr_prepend.
- intros E. exists (wrap (fun n => (sigma n, SUM (closed_prefix sigma n)))). repeat split.
+ intros n. now rewrite map_nth, wrap_correct.
+ destruct (inf_merging_to_function E) as [f [H0 H1]].
exists (wrap (fun n => closed_substr (wrap (fun n => (sigma n, SUM (closed_prefix sigma n)))) ( (f n)) (pred (f (S n))))). split.
* intros n. destruct (H1 n) as [k [H2 H3]]. exists (k - ( f n)). repeat split.
-- rewrite wrap_correct, closed_substr_delta. omega.
-- rewrite wrap_correct, closed_substr_delta, closed_substr_nth', wrap_correct by auto.
rewrite_eq (f n + (pred (f (S n)) - f n) = pred (f (S n))). rewrite <-closed_substr_begin. rewrite H3. simpl snd.
unfold closed_substr. rewrite <-closed_substr_nstr_drop, closed_substr_shift by auto.
rewrite_eq (f n + (k - f n) = k). rewrite_eq (f n + (pred (f (S n)) - (f n)) = pred ( f (S n))).
unfold closed_substr. rewrite <-closed_prefix_map.
f_equal. rewrite closed_prefix_proper. 1, 3: reflexivity.
intros m. now rewrite map_nth, !drop_nth, !wrap_correct.
* apply factorize_monotone. split; auto.
intros n. destruct (H1 n) as [k [H2 _]]. omega.
+ intros n. rewrite map_nth, !wrap_correct. cbn. f_equal. apply closed_prefix_proper; auto.
intros m. now rewrite map_nth, wrap_correct.
Qed.
Lemma aut_inf_merging_correct: exists aut, L_B aut =$= fun sigma => exists i, forall k, exists j, k <= j /\ merge (drop sigma i) 0 j.
Proof.
destruct aut_exists_inf_merging_correct as [aut H].
exists (prepend_nfa univ_aut aut).
rewrite prepend_nfa_correct, H, univ_aut_scorrect. intros sigma. split.
- intros [x [tau [_ [H1 H2]]]].
exists (length x). intros k.
destruct (H1 k) as [j [Q1 Q2]].
exists j. split; auto.
now rewrite H2, revert_prepend.
- intros [i H1].
exists (prefix sigma i), (drop sigma i). repeat split; auto.
apply revert_drop.
Qed.
Finally P2 can be encoded into automata.
Lemma sat_xm_exists_index_inf_merging sigma : sat_xm (P2 sigma).
Proof.
destruct aut_inf_merging_correct as [aut H].
apply sat_xm_iff with (P := L_B aut sigma).
2: apply ax.
rewrite (H sigma). split.
- intros [i H1]. exists i.
intros k. destruct (H1 k) as [j [H2 H3]].
exists (j+i). split; auto. apply merging_shift; auto.
now rewrite_eq (j + i -i = j).
- intros [i H1]. exists i.
intros k. destruct (H1 (i + k)) as [j [H2 H3]].
exists (j - i). split; auto.
rewrite <-merging_shift; auto.
Qed.
P3 Satisfies XM
Definition aut_all_sums_different := image_aut fst
(intersect
(prepend_nfa univ_aut
(intersect
(all_aut (P:= fun (t: Gamma (x) (Gamma (x) finSet Gamma)) =>
match t with (a, (s, N)) => ~ s mem N end))
(suffixsums_aut fst (fun t => snd (snd t)))))
(sum_aut fst (fun t => fst (snd t)))).
Lemma not_merge_iff sigma n: (forall j, ~(n <= j /\ merge sigma 0 j)) <-> (forall k j, j<n \/ j > k \/ SUM (closed_substr sigma 0 k) <> SUM (closed_substr sigma j k)).
Proof.
split.
- intros H k j. specialize (H j).
unfold merge in H. generalize k. apply deMorgan_all_neg; auto.
intros [x Q]. apply H. split; auto. exists x.
apply deMorgan_or; auto. intros [Q2|Q2]; apply Q.
+ left. omega.
+ right. now right.
- intros H j [L [k [Q1 Q2]]].
destruct (H k j) as [H1 |H1]; auto.
destruct H1 as [H1 | H1]; auto.
Qed.
Lemma aut_forall_sums_different: L_B aut_all_sums_different =$= (fun sigma => exists k, forall j, ~ (k <= j /\ merge sigma 0 j)).
Proof.
unfold aut_all_sums_different.
rewrite image_aut_correct, intersect_correct, prepend_nfa_correct, intersect_correct, all_aut_correct, sum_aut_trans_correct, suffixsums_aut_trans_correct, univ_aut_scorrect. intros sigma. split.
- intros [tau [H1 [[x [tau' [_ [[H2 H3] H4]]]] H5]]].
exists (length x). apply not_merge_iff. intros k j.
decide (j < length x) as [D1|D1]. { now left. }
decide (j > k) as [D2 | D2]. {right. now left. }
right. right.
rewrite !H4 in H5, H1.
specialize (H3 (k - length x)). specialize (H5 k). specialize (H2 (k-length x)).
rewrite map_nth, prepend_nth_rest_sub, !wrap_correct in H5 by omega.
rewrite map_nth, !wrap_correct in H3.
rewrite H4 in H5. clear tau H4.
assert (tau' (k -length x) = (fst (tau' (k -length x)), (fst (snd (tau' (k -length x))), snd (snd (tau' (k -length x)))))) as H.
{ now destruct (tau' (k -length x)) as [a [b c]]. }
intros Q. destruct (tau' (k - (| x |))) as [a [s N]]. apply H2. cbn in *. subst.
apply makeSet_correct. exists (j - length x). repeat split; auto.
rewrite H1, <-closed_substr_begin, Q, <-H1.
rewrite_eq (j = (length x) + (j - (length x))) at 1.
rewrite_eq (k = (length x) + (k - (length x))) at 1.
rewrite <-closed_substr_shift.
now rewrite drop_map, revert_prepend.
- intros [k H]. exists (wrap (fun n => (sigma n,( SUM (closed_prefix sigma n), makeSet (fun a => exists j, j <= n /\ k <= j /\ a = SUM (closed_substr sigma j n)))))). repeat split; auto.
{ intros n. now rewrite map_nth, wrap_correct. }
exists (prefix (wrap (fun n => (sigma n,( SUM (closed_prefix sigma n), makeSet (fun a =>exists j, j <= n /\ k <= j/\ a = SUM (closed_substr sigma j n)))))) k).
exists (drop (wrap (fun n => (sigma n,( SUM (closed_prefix sigma n), makeSet (fun a => exists j, j <= n /\ k <= j /\ a = SUM (closed_substr sigma j n)))))) k). repeat split.
+ intros n. rewrite drop_nth, wrap_correct. intros [j [H1 H2]] % makeSet_correct.
apply (H j). split; auto.
exists (k + n). repeat split; auto. now rewrite closed_substr_begin.
+ intros n. rewrite map_nth, drop_nth, !wrap_correct. simpl snd. apply set_eq. intros x.
rewrite !makeSet_correct. split; intros [j [H1 H2]].
* exists (j-k). repeat split; auto. rewrite <-drop_map. rewrite (map_fst_omega sigma), closed_substr_shift. now rewrite_eq (k + (j - k) = j).
* exists (k+ j). repeat split; auto.
now rewrite <-drop_map, (map_fst_omega sigma),closed_substr_shift in H2.
+ intros n. rewrite wrap_correct. decide (n < k).
* rewrite prepend_nth_first by now rewrite prefix_length.
rewrite prefix_nth by auto. now rewrite wrap_correct.
* rewrite prepend_nth_rest_sub by (rewrite prefix_length; auto).
rewrite drop_nth, wrap_correct, prefix_length. f_equal; f_equal; auto.
-- f_equal; f_equal. omega.
-- apply set_eq. intros x. rewrite 2makeSet_correct; split; intros [j H2]; exists j; repeat split; auto.
++ now rewrite_eq (k + (n - k ) = n).
++ now rewrite_eq (k + (n - k ) = n) in H2.
+ intros n. rewrite map_nth, !wrap_correct. cbn. now rewrite map_fst_omega.
Qed.
P3 can be encoded in this automaton.
Lemma sat_xm_exists_not_merging sigma i: sat_xm (P3 sigma i).
Proof.
apply (sat_xm_iff (P:= L_B aut_all_sums_different (drop sigma i))).
2: apply ax.
rewrite (aut_forall_sums_different (drop sigma i)).
split; intros [k H].
- exists (k +i). apply deMorgan_all.
intros j [H1 H2].
apply (H (j-i)). split; auto.
rewrite <-merging_shift; auto.
- exists k. intros j [H1 H2]. apply H.
exists (j+i). split; auto.
rewrite merging_shift; auto.
now rewrite_eq (j + i - i = j).
Qed.
End SatXM_RP.
Remember that AX is an assumption in this section.
Lemma AX_implies_RP: RP.
Proof.
intros Gamma sigma.
apply pred_xm_RP.
- apply sat_xm_exists_merging.
- apply sat_xm_exists_index_inf_merging.
- apply sat_xm_exists_not_merging.
Qed.
End AXImpliesRP.
Proof.
intros Gamma sigma.
apply pred_xm_RP.
- apply sat_xm_exists_merging.
- apply sat_xm_exists_index_inf_merging.
- apply sat_xm_exists_not_merging.
Qed.
End AXImpliesRP.
The main theorem: equivalent characterizations of RF.
Theorem main_all_equiv:
(FX <-> AX) /\
(AX <-> AC) /\
(AC <-> AU) /\
(AU <-> RF) /\
(RF <-> RA) /\
(RA <-> RP).
Proof.
pose proof RF_implies_RP.
pose proof RF_implies_RP.
pose proof RF_implies_RA.
pose proof RA_implies_RF.
pose proof AC_equiv_RF.
pose proof AU_equiv_AC.
pose proof FX_implies_RP.
pose proof AX_implies_RP.
pose proof RP_implies_RF.
pose proof AC_implies_AX.
pose proof RF_implies_FX.
tauto.
Qed.