(* Set Implicit Arguments. *)
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Open Scope string_scope.
Require Import BasicDefs.
Require Import FinType.
Require Import Seqs.
Open Scope string_scope.
Definition associative (X: finType) (add: X -> X -> X) := forall x y z, add x (add y z) = add (add x y) z.
Class FiniteSemigroup := mkSG {
elements : finType;
add : elements -> elements -> elements;
Assoc: associative add
}.
Coercion elements : FiniteSemigroup >-> finType.
Section FiniteSemiGroup.
Context {X : FiniteSemigroup}.
Implicit Types (x y z : X).
Fixpoint ADD' (w: Seq X)(l : nat) : X := match l with
| 0 => w 0
| S n => add (w 0) (ADD' ( drop 1 w) n)
end.
Definition ADD (v:String X) := ADD' (seq v) (|v|).
Lemma ADD'_extensional w w' l : (forall n, n <= l -> w n = w' n) -> ADD' w l = ADD' w' l.
Proof.
revert w w'. induction l; intros w w' Ew.
- cbn. apply Ew. comega.
- cbn. specialize (IHl (drop 1 w) (drop 1 w')). cbn in IHl. rewrite IHl.
+ f_equal. apply Ew. comega.
+ intros n L. cbn. apply Ew. cbn in L. comega.
Qed.
Global Instance ADD_Proper: Proper (strings_equal ==> eq) ADD.
Proof.
intros [w l] [w' l'] [El Ew]. unfold ADD. cbn in El. subst l'. now apply ADD'_extensional.
Qed.
Lemma ADD_split u v : ADD (u ++ v) = add (ADD u) (ADD v).
Proof.
revert v. destruct u as [w l]. revert w. induction l; intros w v.
- now cbn.
- unfold ADD. simpl lastindex. simpl.
specialize (IHl (drop 1 w) v). unfold ADD in IHl. simpl in IHl. rewrite <-Assoc. rewrite <- IHl.
f_equal.
+ now rewrite prepend_string_begin by omega.
+ apply ADD'_extensional. intros n L. decide (n <= l).
* now rewrite !prepend_string_begin by comega.
* now rewrite !prepend_string_rest by comega.
Qed.
Lemma ADD'_last w n : ADD' w (S n) = add (ADD' w n) (w (S n)).
Proof.
revert w. induction n; intros w; auto.
cbn. specialize (IHn (drop 1 w)). cbn in IHn.
rewrite IHn. now rewrite Assoc.
Qed.
Fixpoint mul (x:X) n {struct n} := match n with
| 0 => x
| 1 => x
| S n => add x (mul x n)
end.
Lemma mul_step x n : n > 0 -> mul x (S n) = add x (mul x n).
Proof.
intros L. cbn. destruct n; auto. exfalso. omega.
Qed.
Lemma mul_comm x n : n > 0 -> add (mul x n) x = add x (mul x n).
Proof.
intros L. induction n; auto.
destruct n; auto. remember (S n) as N.
rewrite mul_step by omega. rewrite <-IHn at 2 by omega. now rewrite Assoc.
Qed.
Lemma mul_distr x n m : n > 0 -> m > 0 -> (mul x (n + m)) = add (mul x n) (mul x m).
Proof.
intros Ln Lm.
induction m.
- exfalso. omega.
- destruct m.
+ cbn. rewrite_eq (n+1 = S n). rewrite mul_step by omega.
now rewrite mul_comm.
+ rewrite_eq (n + S(S m) = S (n + S m)). rewrite !mul_step by omega.
rewrite IHm by omega. rewrite !Assoc. f_equal.
now rewrite mul_comm.
Qed.
Lemma mul_mult x n m : n > 0 -> m > 0 -> (mul x (n * m)) = (mul (mul x n) m).
Proof.
intros Ln Lm.
induction m.
- exfalso. omega.
- destruct m.
+ cbn. now rewrite Nat.mul_1_r.
+ remember (S m) as M. rewrite mul_step by omega.
rewrite <-IHm by omega.
rewrite Nat.mul_succ_r.
rewrite_eq (n*M + n = n + n* M). rewrite mul_distr; auto.
apply mul_ge_0; omega.
Qed.
Context {X : FiniteSemigroup}.
Implicit Types (x y z : X).
Fixpoint ADD' (w: Seq X)(l : nat) : X := match l with
| 0 => w 0
| S n => add (w 0) (ADD' ( drop 1 w) n)
end.
Definition ADD (v:String X) := ADD' (seq v) (|v|).
Lemma ADD'_extensional w w' l : (forall n, n <= l -> w n = w' n) -> ADD' w l = ADD' w' l.
Proof.
revert w w'. induction l; intros w w' Ew.
- cbn. apply Ew. comega.
- cbn. specialize (IHl (drop 1 w) (drop 1 w')). cbn in IHl. rewrite IHl.
+ f_equal. apply Ew. comega.
+ intros n L. cbn. apply Ew. cbn in L. comega.
Qed.
Global Instance ADD_Proper: Proper (strings_equal ==> eq) ADD.
Proof.
intros [w l] [w' l'] [El Ew]. unfold ADD. cbn in El. subst l'. now apply ADD'_extensional.
Qed.
Lemma ADD_split u v : ADD (u ++ v) = add (ADD u) (ADD v).
Proof.
revert v. destruct u as [w l]. revert w. induction l; intros w v.
- now cbn.
- unfold ADD. simpl lastindex. simpl.
specialize (IHl (drop 1 w) v). unfold ADD in IHl. simpl in IHl. rewrite <-Assoc. rewrite <- IHl.
f_equal.
+ now rewrite prepend_string_begin by omega.
+ apply ADD'_extensional. intros n L. decide (n <= l).
* now rewrite !prepend_string_begin by comega.
* now rewrite !prepend_string_rest by comega.
Qed.
Lemma ADD'_last w n : ADD' w (S n) = add (ADD' w n) (w (S n)).
Proof.
revert w. induction n; intros w; auto.
cbn. specialize (IHn (drop 1 w)). cbn in IHn.
rewrite IHn. now rewrite Assoc.
Qed.
Fixpoint mul (x:X) n {struct n} := match n with
| 0 => x
| 1 => x
| S n => add x (mul x n)
end.
Lemma mul_step x n : n > 0 -> mul x (S n) = add x (mul x n).
Proof.
intros L. cbn. destruct n; auto. exfalso. omega.
Qed.
Lemma mul_comm x n : n > 0 -> add (mul x n) x = add x (mul x n).
Proof.
intros L. induction n; auto.
destruct n; auto. remember (S n) as N.
rewrite mul_step by omega. rewrite <-IHn at 2 by omega. now rewrite Assoc.
Qed.
Lemma mul_distr x n m : n > 0 -> m > 0 -> (mul x (n + m)) = add (mul x n) (mul x m).
Proof.
intros Ln Lm.
induction m.
- exfalso. omega.
- destruct m.
+ cbn. rewrite_eq (n+1 = S n). rewrite mul_step by omega.
now rewrite mul_comm.
+ rewrite_eq (n + S(S m) = S (n + S m)). rewrite !mul_step by omega.
rewrite IHm by omega. rewrite !Assoc. f_equal.
now rewrite mul_comm.
Qed.
Lemma mul_mult x n m : n > 0 -> m > 0 -> (mul x (n * m)) = (mul (mul x n) m).
Proof.
intros Ln Lm.
induction m.
- exfalso. omega.
- destruct m.
+ cbn. now rewrite Nat.mul_1_r.
+ remember (S m) as M. rewrite mul_step by omega.
rewrite <-IHm by omega.
rewrite Nat.mul_succ_r.
rewrite_eq (n*M + n = n + n* M). rewrite mul_distr; auto.
apply mul_ge_0; omega.
Qed.
Definition idempotent x := add x x = x.
Lemma idempotent_mul x n : idempotent x -> mul x n = x.
Proof.
intros Idem. induction n; auto.
cbn. destruct n; auto.
now rewrite IHn.
Qed.
Lemma mul_yields_idempotent x : Sigma k, k > 0 /\ idempotent (mul x k).
Proof.
unfold idempotent.
destruct (can_find_duplicate (S(Cardinality X)) (fun n => (mul x (Nat.pow 2 n)))) as [[i [j [L D]]]|D].
- remember (j - i) as k. assert (j = i + k) by omega. subst j. assert (k > 0) by omega.
decide (k = 1).
+ subst k. exists (Nat.pow 2 i). split. apply pow_ge_zero.
rewrite Nat.pow_add_r in D. rewrite mul_mult in D; auto; apply pow_ge_zero.
+ exists ( (Nat.pow 2 i) * ((Nat.pow 2 k)-1)). rewrite Nat.pow_add_r in D.
remember (Nat.pow 2 i) as I. remember (Nat.pow 2 k) as K.
assert (K > 2). { subst K. destruct k.
- exfalso. omega.
- cbn. enough (Nat.pow 2 k >1 ) by omega.
destruct k.
+ exfalso. omega.
+ cbn. enough(Nat.pow 2 k > 0) by omega. apply pow_ge_zero. }
assert (I > 0). { subst I. apply pow_ge_zero. } clear HeqI HeqK.
split. { apply mul_ge_0; omega. }
rewrite <-mul_distr; auto.
* rewrite <-Nat.mul_add_distr_l. rewrite_eq ((K-1) +(K-1) = K + (K -2) ).
rewrite Nat.mul_add_distr_l. rewrite mul_distr; auto.
-- rewrite <-D. rewrite <-mul_distr; auto.
++ f_equal. enough ( I = I * 1) as H'.
** rewrite H' at 1. rewrite <-Nat.mul_add_distr_l. f_equal. omega.
** symmetry. apply Nat.mul_1_r.
++ apply mul_ge_0; omega.
-- apply mul_ge_0; omega.
-- apply mul_ge_0; omega.
* apply mul_ge_0; omega.
* apply mul_ge_0; omega.
- exfalso. omega.
Qed.
Lemma ADD_iter v k : ADD (fin_iter v k) = mul (ADD v) (S k).
Proof.
induction k; auto. destruct k.
- simpl fin_iter. rewrite ADD_split; auto.
- remember (S k) as K. assert (K > 0). { subst K. omega. }
simpl fin_iter. rewrite mul_step; auto. rewrite <-IHk; auto.
rewrite ADD_split; auto.
Qed.
Lemma ADD_single_extract w i: (ADD (extract i (S i) w)) = w i.
Proof.
cbn. rewrite_eq (i - i = 0). cbn. rewrite drop_correct'. now cbn.
Qed.
Lemma ADD_extract_last w n m : n < m -> ADD (extract n (S m) w) = add (ADD (extract n m w)) (w m).
Proof.
intros L. unfold ADD. cbn.
remember (m - S n) as k. rewrite_eq (m - n = S k).
rewrite_eq ( m = n + S k).
rewrite <-drop_correct.
apply ADD'_last.
Qed.
End FiniteSemiGroup.
Definition InfinitePigeonholePrinciple (X: finType) := forall (f: Seq X), exists (x:X), infinite x f.
Section AdditiveRamsey.
Context {X:FiniteSemigroup}.
Implicit Types (f: nat -> nat -> X).
Implicit Types (g: nat -> X).
Definition coloring_additive (f: nat -> nat -> X):= (forall i j k, i < j < k -> add (f i j) (f j k) = f i k).
Definition has_monochromatic_subsequence f := exists h, s_monotone h /\ forall n m, n < m -> f(h 0) (h 1) = f (h n) (h m).
Definition AdditiveRamsey : Prop := forall f, coloring_additive f -> has_monochromatic_subsequence f.
Definition is_ramseyan_factorization g h:= s_monotone h /\ forall n, ADD (extract (h 0)(h 1) g) = ADD (extract (h n) (h (S n)) g).
Definition admits_ramseyan_factorization g := exists h, is_ramseyan_factorization g h.
Definition admits_idempotent_ramseyan_factorization g := exists h, is_ramseyan_factorization g h /\ idempotent (ADD (extract (h 0)(h 1) g)).
Lemma sum_ramseyan_fac g h n m: n < m -> is_ramseyan_factorization g h -> mul (ADD (extract (h 0) (h 1) g)) (m - n) = ADD (extract (h n) (h m) g).
Proof.
intros L [Mon RF].
remember (m - n) as k. assert (m = n + k) by omega. subst m. clear Heqk. induction k.
- exfalso. omega.
- decide (k > 0).
+ rewrite <-concat_extract with (i_1 := h n) (i_2 := h(n + k)).
* rewrite ADD_split.
rewrite_eq ( n + (S k) = S(n + k)). rewrite <-(RF (n + k)).
rewrite_eq (S k = k +1). rewrite mul_distr by omega.
simpl. now rewrite IHk by omega.
* apply s_monotone_strict_order_preserving; oauto.
* apply s_monotone_strict_order_preserving; oauto.
+ rewrite_eq (k = 0). rewrite_eq (n + 1 = S n). simpl. apply RF.
Qed.
Hint Unfold is_ramseyan_factorization.
Lemma admits_ramseyan_fac_iff_idem_ramseyan_fac g : admits_ramseyan_factorization g <-> admits_idempotent_ramseyan_factorization g.
Proof.
split.
- intros [h [Mon RF]].
destruct (mul_yields_idempotent (ADD (extract (h 0)(h 1) g))) as [k [G Idem]].
exists (fun n => h (k * n)). split.
+ split.
* apply compose_s_monotone.
-- intros n. rewrite Nat.mul_comm. setoid_rewrite Nat.mul_comm at 2. simpl. omega.
-- apply Mon.
* clear Idem. intros n. setoid_rewrite Nat.mul_comm at 1 2 3 4.
rewrite <-sum_ramseyan_fac; oauto.
setoid_rewrite <-sum_ramseyan_fac at 2; oauto.
f_equal. simpl. omega.
+ rewrite <-sum_ramseyan_fac; oauto.
setoid_rewrite Nat.mul_comm at 1 2. simpl.
now rewrite_eq (k + 0 - 0 = k).
- intros [h [RF _]]. now exists h.
Qed.
Definition RamseyFac: Prop:=forall g, admits_ramseyan_factorization g.
Lemma compact_f f n m : coloring_additive f -> n < m -> ADD (extract n m (fun n => f n (S n))) = f n m.
Proof.
intros Col L; unfold ADD. induction L; unfold extract.
- rewrite_eq (S n - S n = 0). cbn. now rewrite drop_correct'.
- cbn. cbn in IHL. remember (m - S n) as k. rewrite_eq (m - n = S k).
rewrite ADD'_last; auto. rewrite <-(Col n m (S m)) by omega.
rewrite IHL, drop_correct. f_equal. f_equal; subst k; omega.
Qed.
Lemma RamseyFac_iff_AdditiveRamsey : RamseyFac <-> AdditiveRamsey.
Proof.
split.
- intros RF f Additive.
specialize (RF (fun n => f n (S n))).
apply admits_ramseyan_fac_iff_idem_ramseyan_fac in RF.
destruct RF as [h [[Mon RF] Idem]].
exists h. split; auto.
intros n m L. rewrite <-2compact_f; auto.
+ setoid_rewrite <-sum_ramseyan_fac at 2; auto.
now rewrite idempotent_mul by assumption.
+ apply s_monotone_strict_order_preserving; oauto.
- intros AR g.
specialize (AR (fun n m => ADD (extract n m g))).
destruct AR as [h [Mon Mono]].
+ intros i j k L. now rewrite <-ADD_split, concat_extract.
+ exists h. split; auto.
Qed.
Lemma loop_admits_ramseyan_fac v: admits_ramseyan_factorization (v to_omega).
Proof.
exists (fun n => n* S(|v|)). split.
- intros n. simpl. setoid_rewrite Nat.mul_comm at 1 2. simpl. omega.
- intros n. now rewrite 2extract_omega_iter.
Qed.
Lemma prefix_admits_ramseyan_fac v w: admits_ramseyan_factorization w -> admits_ramseyan_factorization (v +++ w).
Proof.
intros [h [Mon RF]].
exists (fun n => h n + S(|v|)). split.
- intros n. specialize (Mon n). omega.
- intros n. rewrite 2extract_prepend. apply RF.
Qed.
Lemma up_admits_ramseyan_fac v w: admits_ramseyan_factorization (v +++ w to_omega).
Proof.
apply prefix_admits_ramseyan_fac, loop_admits_ramseyan_fac.
Qed.
End AdditiveRamsey.
Arguments AdditiveRamsey X : clear implicits.
Arguments RamseyFac X : clear implicits.
Constructive Choice for (i,j) with i < j
Section ConstructiveChoiceNcrossN.
Definition Pairs := drop 1 (fun j => mkstring (fun i => (j, i)) (pred j)).
Lemma find_pos_begin i j : i < j -> exists n, concat_inf Pairs n = (j, i).
Proof.
intros L. destruct j.
- exfalso. omega.
- exists (i + begin_in Pairs j).
rewrite concat_inf_correct; cbn; oauto.
Qed.
Definition pair_to_nat : (nat * nat ) -> nat.
Proof.
intros [i j]. decide (i < j) as [D|D].
- apply find_pos_begin in D. apply cc_nat in D.
+ destruct D as [n _]. exact n.
+ auto.
- exact 0.
Defined.
Definition nat_to_pair : nat -> (nat*nat) := fun n => swap (concat_inf Pairs n).
Lemma nat_to_pair_halfspace n : fst (nat_to_pair n) < snd (nat_to_pair n).
Proof.
unfold nat_to_pair. unfold concat_inf.
destruct (concat_inf_indices Pairs n) as [i j] eqn:H.
apply concat_inf_index_to_begin in H. destruct H as [H1 H2].
cbn. rewrite H1 in H2. cbn in H2.
remember (begin_in (fun n : nat => mkstring (fun i : nat => (S n, i)) n) i) as K.
omega.
Qed.
Lemma inv_nat_to_pair i j : i < j -> nat_to_pair (pair_to_nat (i,j)) = (i,j).
Proof.
intros L. unfold pair_to_nat, nat_to_pair, swap.
destruct decision as [D|D].
- destruct cc_nat as[n P]. now rewrite P.
- exfalso. auto.
Qed.
Lemma pair_nat_choice (P : nat -> nat -> Prop ) (decP: forall i j, dec (P i j)):
(exists i j , i < j /\ P i j) -> Sigma i, {j |i < j /\ P i j}.
Proof.
intros E.
enough (exists k, P (fst (nat_to_pair k)) (snd (nat_to_pair k))) as H.
- apply cc_nat in H; auto. destruct H as [k Q].
exists (fst (nat_to_pair k)), (snd (nat_to_pair k)). split; auto.
apply nat_to_pair_halfspace.
- destruct E as [i [j Q]].
exists (pair_to_nat (i, j)). now rewrite inv_nat_to_pair by omega.
Qed.
End ConstructiveChoiceNcrossN.
Context (X:FiniteSemigroup).
Variable (f: nat -> X).
Implicit Types (x y : X)(n m : nat).
Notation F i j := (ADD (extract i j f)).
Notation "i '~~@' j 'at' m" :=((m > i /\ m > j) /\ F i m = F j m) (at level 58).
Instance dec_merge_at k1 k2 m : dec (k1 ~~@ k2 at m).
Proof. auto. Qed.
Definition tilde_w_equiv (k k' : nat) := exists m, k ~~@ k' at m.
Notation "k1 '~~#' k2" := (tilde_w_equiv k1 k2) (at level 60).
Variable (IPP_DM: forall (w: Seq X), (exists x, infinite x w) \/ (forall x, exists n, forall i, n < i -> w i <> x)).
Variable (INF_DM: (exists i, forall j, exists k, j < k /\ i ~~# k) \/ (forall i, exists j, forall k, j >= k \/ ~ i~~# k)).
Lemma tilde_w_extend k k' m: (k ~~@ k' at m) -> forall m', m' >= m -> k ~~@ k' at m'.
Proof.
intros [G W] m' L. destruct L; auto.
repeat split; oauto.
rewrite <-(concat_extract f (i_1 := k)(i_2 := m)(i_3:=S m0)); oauto.
rewrite <-(concat_extract f (i_1 := k')(i_2 := m)(i_3:=S m0)); oauto.
rewrite !ADD_split; auto.
rewrite W. f_equal.
Qed.
Lemma tilde_w_index_reflexive k n : k < n -> k ~~@ k at n.
Proof. split; oauto. Qed.
Lemma tilde_w_index_symmetric k1 k2 m: k1 ~~@ k2 at m -> k2 ~~@ k1 at m.
Proof. split. omega. now symmetry. Qed.
Lemma tilde_w_index_transitive i j k m n:
i ~~@ j at m -> j ~~@ k at n -> i ~~@ k at (max m n).
Proof.
intros P1 P2. split.
- split; [apply max_le_left | apply max_le_right]; omega.
- apply tilde_w_extend with (m':= max m n) in P1.
apply tilde_w_extend with (m':= max m n) in P2.
+ destruct P2 as [H H']. now rewrite <-H'.
+ now apply max_le_right.
+ now apply max_le_left.
Qed.
Instance tilde_w_equivalence: Equivalence tilde_w_equiv.
Proof.
repeat split.
- intros n. exists (S n). apply tilde_w_index_reflexive. omega.
- intros i j [m E]. exists m. now apply tilde_w_index_symmetric.
- intros i j k [m Em] [n En]. exists (max m n). now apply tilde_w_index_transitive with (j:=j).
Qed.
Definition finiteIndex (X:Type) (R: X -> X -> Prop) := (exists n, forall (L : String X), |L| > n -> exists i j, i < j < |L| /\ R (L[i]) (L[j])).
Fixpoint max_of_nat_string w l:= match l with
| 0 => w 0
| S l => max (w (S l)) (max_of_nat_string w l) end.
Lemma max_of_nat_string_correct v l: forall n , n<=l -> (v n) <= max_of_nat_string v l.
Proof.
induction l; intros n L.
- now rewrite_eq (n = 0).
- simpl. decide (n = S l) as[D|D].
+ apply max_le_left. rewrite D. omega.
+ apply max_le_right. apply IHl. omega.
Qed.
Lemma tilde_w_equiv_finite_index: finiteIndex tilde_w_equiv.
Proof.
exists (S(Cardinality X)). intros L O.
destruct (can_find_duplicate (S(Cardinality X)) (fun n => F (L[n]) (S(max_of_nat_string (seq L) (|L|) )))) as [[i [j [G E]]]|N].
- exists i , j. split.
+ omega.
+ exists (S (max_of_nat_string (seq L) (| L |))). repeat split.
* enough (L [i] <= max_of_nat_string (seq L) (| L |)) by omega. apply max_of_nat_string_correct. omega.
* enough (L [j] <= max_of_nat_string (seq L) (| L |)) by omega. apply max_of_nat_string_correct. omega.
* assumption.
- exfalso. omega.
Qed.
Lemma not_tilde_w_equiv_sym i j :~ i ~~# j -> ~ j ~~# i.
Proof.
intros N [n [[O1 O2] E]]. apply N. exists n. repeat split; auto.
Qed.
Lemma infinite_equiv_indices' :exists i, forall j, exists k, j < k /\ i ~~# k.
Proof.
destruct INF_DM as [D|D].
- exact D.
- exfalso.
enough (forall i, exists j, i < j /\ forall k, j < k -> ~ i~~# k) as H.
+ enough (forall n, exists (l: String nat) m,
| l| >= n /\
(forall i j, i < j < |l| -> ~ l[i] ~~# l[j]) /\
(forall j k, j < |l| -> m <= k -> ~ k ~~# l[j]) ) as H'.
* destruct tilde_w_equiv_finite_index as [m FinIn].
destruct (H' (S m)) as [l [m' [G [NEq _]]]].
specialize (FinIn l G). destruct FinIn as [i [j [O E]]].
apply (NEq i j); oauto.
* intros n. induction n.
-- exists (mkstring (fun n => 0) 0), 0. simpl; repeat split; auto; intros * I; exfalso; omega.
-- destruct IHn as [l [m [L [P N]]]].
specialize (H m). destruct H as [j [H1 H2]].
exists ( mkstring (prepend m l) (S(|l|))), (S j). repeat split.
++ cbn. omega.
++ simpl. intros i k R. destruct i.
** simpl. destruct k. {exfalso. omega. } simpl. apply N; omega.
** destruct k. {exfalso. omega. } simpl. apply P. omega.
++ simpl. intros i k L1 L2. destruct i.
** simpl. apply not_tilde_w_equiv_sym. apply H2. omega.
** simpl. apply N; omega.
+ intros i. destruct (D i) as [j P]. exists (i + S j). split; oauto.
intros k L. specialize (P k). destruct P as [P|P]; auto. exfalso. omega.
Qed.
Lemma tilde_w_equiv_cc_nat i n : (exists j, n < j /\ i ~~# j) -> Sigma j, {k | n < j < k /\ i ~~@ j at k}.
Proof.
intros E.
enough (exists j k, j < k /\ i < k /\ n < j /\ F i k = F j k) as H.
- apply pair_nat_choice in H; auto.
destruct H as [j [k [O1 [O2 [O3 P]]]]].
exists j. exists k. split; auto.
- destruct E as [j [O1 [k [[O2 O3] P]]]].
exists j,k. repeat split; oauto.
Qed.
Fixpoint equiv_merge_subseq i (P : forall j, exists k, j < k /\ i ~~# k) (n:nat) {struct n} : nat * nat :=
match n with
| 0 => (i, S i)
| S n => match (equiv_merge_subseq P n) with (j, k) =>
match (tilde_w_equiv_cc_nat (P k)) with (existT _ j' (exist _ k' _)) => (j', k') end
end
end.
Lemma equiv_merge_subseq_s_monotone i (P : forall j, exists k, j < k /\ i ~~# k) : s_monotone (seq_map fst (equiv_merge_subseq P)).
Proof.
unfold seq_map. intros n. destruct n; cbn.
- destruct tilde_w_equiv_cc_nat as [j [k Q]]. simpl. omega.
- destruct (equiv_merge_subseq P n) as [j k].
destruct tilde_w_equiv_cc_nat as [j' [k' Q]].
destruct tilde_w_equiv_cc_nat as [j'' [k'' Q']]. simpl. omega.
Qed.
Lemma equiv_merge_subseq_merge_at_next i (P : forall j, exists k, j < k /\ i ~~# k):
forall n, (seq_map fst (equiv_merge_subseq P)) 0 ~~@ (seq_map fst (equiv_merge_subseq P)) n at ((seq_map fst (equiv_merge_subseq P)) (S n)).
Proof.
intros n. unfold seq_map. destruct n.
- simpl. destruct tilde_w_equiv_cc_nat as [j [k Q]]. apply tilde_w_index_reflexive. comega.
- simpl. destruct equiv_merge_subseq as [j k].
destruct tilde_w_equiv_cc_nat as [j' [k' [O Q]]]. simpl.
destruct tilde_w_equiv_cc_nat as [j'' [k'' [O' Q']]]. simpl.
apply (tilde_w_extend Q). omega.
Qed.
Lemma infinite_merge_at_next : exists g, s_monotone g /\ forall n, forall m, m > n -> g 0 ~~@ g n at g m.
Proof.
destruct infinite_equiv_indices' as [i P].
exists (seq_map fst (equiv_merge_subseq P)). split.
- apply equiv_merge_subseq_s_monotone.
- intros n m L. apply tilde_w_extend with (m:= (seq_map fst (equiv_merge_subseq P)) (S n)).
+ apply equiv_merge_subseq_merge_at_next.
+ apply s_monotone_order_preserving.
* apply equiv_merge_subseq_s_monotone.
* omega.
Qed.
Lemma ipp : InfinitePigeonholePrinciple X.
Proof.
intros w.
destruct (IPP_DM w) as [D|D].
- assumption.
- exfalso.
enough (exists n, forall m, m > n -> forall x, x el (elem X) -> w m <> x) as H'''.
+ destruct H''' as [n H'''].
specialize (H''' (S n)). assert (S n > n) as G by omega.
now apply (H''' G (w (S n))).
+ induction (elem X).
* exists 0. intros m G x L. now exfalso.
* destruct IHl as [n IHl]; auto.
specialize (D a). destruct D as [m H].
exists (max n m). intros k G x [P | P].
-- subst x. apply H. pose (Nat.le_max_r n m). omega.
-- apply IHl; auto. pose (Nat.le_max_l n m). omega.
Qed.
Lemma infinite_merge_at_next_same_color: exists g, s_monotone g /\ (forall n, g 0 ~~@ g n at g (S n)) /\ (forall n, F(g 0) (g 1) = F (g 0) (g (S n))).
Proof.
destruct infinite_merge_at_next as [g [Mon Merge]].
destruct (ipp (fun n => F (g 0) (g ( n)))) as [x Inf].
exists (fun n => g (fix_first_zero (infinite_filter Inf) n)). split.
- apply compose_s_monotone.
+ apply fix_first_zero_s_monotone. apply infinite_filter_s_monotone.
+ apply Mon.
- split.
+ intros n. simpl fix_first_zero. apply Merge. destruct n.
* simpl. pose proof (next_position_exists_increasing (Inf (S (next_position_exists (Inf 0))))). omega.
* simpl. pose proof (next_position_exists_increasing (Inf (S (next_position_exists (Inf (S (infinite_filter Inf n))))))). omega.
+ intros n. unfold fix_first_zero.
now rewrite 2(infinite_filter_correct Inf).
Qed.
Lemma ramseyan_factorization : admits_ramseyan_factorization f.
Proof.
destruct infinite_merge_at_next_same_color as [g [Mon [Merge Same]]].
exists g. split.
- apply Mon.
- intros n. destruct (Merge n) as [M1 M2]. rewrite <-M2.
apply Same.
Qed.
End DeriveRamseyFac.
Corollary XM_implies_RamseyFac: (forall p, p \/ ~ p) -> (forall X, RamseyFac X).
Proof.
Require Import Classical.
intros XM X f.
apply ramseyan_factorization.
- intros w. destruct (XM (exists x, infinite x w)) as [D|D].
+ now left.
+ right. unfold infinite in D.
intros x. apply not_all_not_ex. intros D'.
apply D. exists x. intros n.
apply not_all_not_ex. intros D''.
specialize (D' n). apply D'. intros i L.
specialize (D'' i). apply not_and_or in D''.
destruct D'' as [H|H].
* exfalso. omega.
* assumption.
- destruct (XM (exists i : nat, forall j : nat, exists k : nat, j < k /\ tilde_w_equiv f i k)) as [D|D].
+ now left.
+ right. intros i.
apply not_all_not_ex. intros D'.
apply D. apply not_all_not_ex. intros D''.
specialize (D'' i). apply not_all_ex_not in D''.
destruct D'' as[j D''].
apply D''. apply not_all_not_ex. intros D'''.
specialize (D' j). apply D'.
intros k. specialize (D''' k). apply not_and_or in D'''.
destruct D''' as [H|H].
* left. omega.
* right. assumption.
Qed.
Definition Pairs := drop 1 (fun j => mkstring (fun i => (j, i)) (pred j)).
Lemma find_pos_begin i j : i < j -> exists n, concat_inf Pairs n = (j, i).
Proof.
intros L. destruct j.
- exfalso. omega.
- exists (i + begin_in Pairs j).
rewrite concat_inf_correct; cbn; oauto.
Qed.
Definition pair_to_nat : (nat * nat ) -> nat.
Proof.
intros [i j]. decide (i < j) as [D|D].
- apply find_pos_begin in D. apply cc_nat in D.
+ destruct D as [n _]. exact n.
+ auto.
- exact 0.
Defined.
Definition nat_to_pair : nat -> (nat*nat) := fun n => swap (concat_inf Pairs n).
Lemma nat_to_pair_halfspace n : fst (nat_to_pair n) < snd (nat_to_pair n).
Proof.
unfold nat_to_pair. unfold concat_inf.
destruct (concat_inf_indices Pairs n) as [i j] eqn:H.
apply concat_inf_index_to_begin in H. destruct H as [H1 H2].
cbn. rewrite H1 in H2. cbn in H2.
remember (begin_in (fun n : nat => mkstring (fun i : nat => (S n, i)) n) i) as K.
omega.
Qed.
Lemma inv_nat_to_pair i j : i < j -> nat_to_pair (pair_to_nat (i,j)) = (i,j).
Proof.
intros L. unfold pair_to_nat, nat_to_pair, swap.
destruct decision as [D|D].
- destruct cc_nat as[n P]. now rewrite P.
- exfalso. auto.
Qed.
Lemma pair_nat_choice (P : nat -> nat -> Prop ) (decP: forall i j, dec (P i j)):
(exists i j , i < j /\ P i j) -> Sigma i, {j |i < j /\ P i j}.
Proof.
intros E.
enough (exists k, P (fst (nat_to_pair k)) (snd (nat_to_pair k))) as H.
- apply cc_nat in H; auto. destruct H as [k Q].
exists (fst (nat_to_pair k)), (snd (nat_to_pair k)). split; auto.
apply nat_to_pair_halfspace.
- destruct E as [i [j Q]].
exists (pair_to_nat (i, j)). now rewrite inv_nat_to_pair by omega.
Qed.
End ConstructiveChoiceNcrossN.
Context (X:FiniteSemigroup).
Variable (f: nat -> X).
Implicit Types (x y : X)(n m : nat).
Notation F i j := (ADD (extract i j f)).
Notation "i '~~@' j 'at' m" :=((m > i /\ m > j) /\ F i m = F j m) (at level 58).
Instance dec_merge_at k1 k2 m : dec (k1 ~~@ k2 at m).
Proof. auto. Qed.
Definition tilde_w_equiv (k k' : nat) := exists m, k ~~@ k' at m.
Notation "k1 '~~#' k2" := (tilde_w_equiv k1 k2) (at level 60).
Variable (IPP_DM: forall (w: Seq X), (exists x, infinite x w) \/ (forall x, exists n, forall i, n < i -> w i <> x)).
Variable (INF_DM: (exists i, forall j, exists k, j < k /\ i ~~# k) \/ (forall i, exists j, forall k, j >= k \/ ~ i~~# k)).
Lemma tilde_w_extend k k' m: (k ~~@ k' at m) -> forall m', m' >= m -> k ~~@ k' at m'.
Proof.
intros [G W] m' L. destruct L; auto.
repeat split; oauto.
rewrite <-(concat_extract f (i_1 := k)(i_2 := m)(i_3:=S m0)); oauto.
rewrite <-(concat_extract f (i_1 := k')(i_2 := m)(i_3:=S m0)); oauto.
rewrite !ADD_split; auto.
rewrite W. f_equal.
Qed.
Lemma tilde_w_index_reflexive k n : k < n -> k ~~@ k at n.
Proof. split; oauto. Qed.
Lemma tilde_w_index_symmetric k1 k2 m: k1 ~~@ k2 at m -> k2 ~~@ k1 at m.
Proof. split. omega. now symmetry. Qed.
Lemma tilde_w_index_transitive i j k m n:
i ~~@ j at m -> j ~~@ k at n -> i ~~@ k at (max m n).
Proof.
intros P1 P2. split.
- split; [apply max_le_left | apply max_le_right]; omega.
- apply tilde_w_extend with (m':= max m n) in P1.
apply tilde_w_extend with (m':= max m n) in P2.
+ destruct P2 as [H H']. now rewrite <-H'.
+ now apply max_le_right.
+ now apply max_le_left.
Qed.
Instance tilde_w_equivalence: Equivalence tilde_w_equiv.
Proof.
repeat split.
- intros n. exists (S n). apply tilde_w_index_reflexive. omega.
- intros i j [m E]. exists m. now apply tilde_w_index_symmetric.
- intros i j k [m Em] [n En]. exists (max m n). now apply tilde_w_index_transitive with (j:=j).
Qed.
Definition finiteIndex (X:Type) (R: X -> X -> Prop) := (exists n, forall (L : String X), |L| > n -> exists i j, i < j < |L| /\ R (L[i]) (L[j])).
Fixpoint max_of_nat_string w l:= match l with
| 0 => w 0
| S l => max (w (S l)) (max_of_nat_string w l) end.
Lemma max_of_nat_string_correct v l: forall n , n<=l -> (v n) <= max_of_nat_string v l.
Proof.
induction l; intros n L.
- now rewrite_eq (n = 0).
- simpl. decide (n = S l) as[D|D].
+ apply max_le_left. rewrite D. omega.
+ apply max_le_right. apply IHl. omega.
Qed.
Lemma tilde_w_equiv_finite_index: finiteIndex tilde_w_equiv.
Proof.
exists (S(Cardinality X)). intros L O.
destruct (can_find_duplicate (S(Cardinality X)) (fun n => F (L[n]) (S(max_of_nat_string (seq L) (|L|) )))) as [[i [j [G E]]]|N].
- exists i , j. split.
+ omega.
+ exists (S (max_of_nat_string (seq L) (| L |))). repeat split.
* enough (L [i] <= max_of_nat_string (seq L) (| L |)) by omega. apply max_of_nat_string_correct. omega.
* enough (L [j] <= max_of_nat_string (seq L) (| L |)) by omega. apply max_of_nat_string_correct. omega.
* assumption.
- exfalso. omega.
Qed.
Lemma not_tilde_w_equiv_sym i j :~ i ~~# j -> ~ j ~~# i.
Proof.
intros N [n [[O1 O2] E]]. apply N. exists n. repeat split; auto.
Qed.
Lemma infinite_equiv_indices' :exists i, forall j, exists k, j < k /\ i ~~# k.
Proof.
destruct INF_DM as [D|D].
- exact D.
- exfalso.
enough (forall i, exists j, i < j /\ forall k, j < k -> ~ i~~# k) as H.
+ enough (forall n, exists (l: String nat) m,
| l| >= n /\
(forall i j, i < j < |l| -> ~ l[i] ~~# l[j]) /\
(forall j k, j < |l| -> m <= k -> ~ k ~~# l[j]) ) as H'.
* destruct tilde_w_equiv_finite_index as [m FinIn].
destruct (H' (S m)) as [l [m' [G [NEq _]]]].
specialize (FinIn l G). destruct FinIn as [i [j [O E]]].
apply (NEq i j); oauto.
* intros n. induction n.
-- exists (mkstring (fun n => 0) 0), 0. simpl; repeat split; auto; intros * I; exfalso; omega.
-- destruct IHn as [l [m [L [P N]]]].
specialize (H m). destruct H as [j [H1 H2]].
exists ( mkstring (prepend m l) (S(|l|))), (S j). repeat split.
++ cbn. omega.
++ simpl. intros i k R. destruct i.
** simpl. destruct k. {exfalso. omega. } simpl. apply N; omega.
** destruct k. {exfalso. omega. } simpl. apply P. omega.
++ simpl. intros i k L1 L2. destruct i.
** simpl. apply not_tilde_w_equiv_sym. apply H2. omega.
** simpl. apply N; omega.
+ intros i. destruct (D i) as [j P]. exists (i + S j). split; oauto.
intros k L. specialize (P k). destruct P as [P|P]; auto. exfalso. omega.
Qed.
Lemma tilde_w_equiv_cc_nat i n : (exists j, n < j /\ i ~~# j) -> Sigma j, {k | n < j < k /\ i ~~@ j at k}.
Proof.
intros E.
enough (exists j k, j < k /\ i < k /\ n < j /\ F i k = F j k) as H.
- apply pair_nat_choice in H; auto.
destruct H as [j [k [O1 [O2 [O3 P]]]]].
exists j. exists k. split; auto.
- destruct E as [j [O1 [k [[O2 O3] P]]]].
exists j,k. repeat split; oauto.
Qed.
Fixpoint equiv_merge_subseq i (P : forall j, exists k, j < k /\ i ~~# k) (n:nat) {struct n} : nat * nat :=
match n with
| 0 => (i, S i)
| S n => match (equiv_merge_subseq P n) with (j, k) =>
match (tilde_w_equiv_cc_nat (P k)) with (existT _ j' (exist _ k' _)) => (j', k') end
end
end.
Lemma equiv_merge_subseq_s_monotone i (P : forall j, exists k, j < k /\ i ~~# k) : s_monotone (seq_map fst (equiv_merge_subseq P)).
Proof.
unfold seq_map. intros n. destruct n; cbn.
- destruct tilde_w_equiv_cc_nat as [j [k Q]]. simpl. omega.
- destruct (equiv_merge_subseq P n) as [j k].
destruct tilde_w_equiv_cc_nat as [j' [k' Q]].
destruct tilde_w_equiv_cc_nat as [j'' [k'' Q']]. simpl. omega.
Qed.
Lemma equiv_merge_subseq_merge_at_next i (P : forall j, exists k, j < k /\ i ~~# k):
forall n, (seq_map fst (equiv_merge_subseq P)) 0 ~~@ (seq_map fst (equiv_merge_subseq P)) n at ((seq_map fst (equiv_merge_subseq P)) (S n)).
Proof.
intros n. unfold seq_map. destruct n.
- simpl. destruct tilde_w_equiv_cc_nat as [j [k Q]]. apply tilde_w_index_reflexive. comega.
- simpl. destruct equiv_merge_subseq as [j k].
destruct tilde_w_equiv_cc_nat as [j' [k' [O Q]]]. simpl.
destruct tilde_w_equiv_cc_nat as [j'' [k'' [O' Q']]]. simpl.
apply (tilde_w_extend Q). omega.
Qed.
Lemma infinite_merge_at_next : exists g, s_monotone g /\ forall n, forall m, m > n -> g 0 ~~@ g n at g m.
Proof.
destruct infinite_equiv_indices' as [i P].
exists (seq_map fst (equiv_merge_subseq P)). split.
- apply equiv_merge_subseq_s_monotone.
- intros n m L. apply tilde_w_extend with (m:= (seq_map fst (equiv_merge_subseq P)) (S n)).
+ apply equiv_merge_subseq_merge_at_next.
+ apply s_monotone_order_preserving.
* apply equiv_merge_subseq_s_monotone.
* omega.
Qed.
Lemma ipp : InfinitePigeonholePrinciple X.
Proof.
intros w.
destruct (IPP_DM w) as [D|D].
- assumption.
- exfalso.
enough (exists n, forall m, m > n -> forall x, x el (elem X) -> w m <> x) as H'''.
+ destruct H''' as [n H'''].
specialize (H''' (S n)). assert (S n > n) as G by omega.
now apply (H''' G (w (S n))).
+ induction (elem X).
* exists 0. intros m G x L. now exfalso.
* destruct IHl as [n IHl]; auto.
specialize (D a). destruct D as [m H].
exists (max n m). intros k G x [P | P].
-- subst x. apply H. pose (Nat.le_max_r n m). omega.
-- apply IHl; auto. pose (Nat.le_max_l n m). omega.
Qed.
Lemma infinite_merge_at_next_same_color: exists g, s_monotone g /\ (forall n, g 0 ~~@ g n at g (S n)) /\ (forall n, F(g 0) (g 1) = F (g 0) (g (S n))).
Proof.
destruct infinite_merge_at_next as [g [Mon Merge]].
destruct (ipp (fun n => F (g 0) (g ( n)))) as [x Inf].
exists (fun n => g (fix_first_zero (infinite_filter Inf) n)). split.
- apply compose_s_monotone.
+ apply fix_first_zero_s_monotone. apply infinite_filter_s_monotone.
+ apply Mon.
- split.
+ intros n. simpl fix_first_zero. apply Merge. destruct n.
* simpl. pose proof (next_position_exists_increasing (Inf (S (next_position_exists (Inf 0))))). omega.
* simpl. pose proof (next_position_exists_increasing (Inf (S (next_position_exists (Inf (S (infinite_filter Inf n))))))). omega.
+ intros n. unfold fix_first_zero.
now rewrite 2(infinite_filter_correct Inf).
Qed.
Lemma ramseyan_factorization : admits_ramseyan_factorization f.
Proof.
destruct infinite_merge_at_next_same_color as [g [Mon [Merge Same]]].
exists g. split.
- apply Mon.
- intros n. destruct (Merge n) as [M1 M2]. rewrite <-M2.
apply Same.
Qed.
End DeriveRamseyFac.
Corollary XM_implies_RamseyFac: (forall p, p \/ ~ p) -> (forall X, RamseyFac X).
Proof.
Require Import Classical.
intros XM X f.
apply ramseyan_factorization.
- intros w. destruct (XM (exists x, infinite x w)) as [D|D].
+ now left.
+ right. unfold infinite in D.
intros x. apply not_all_not_ex. intros D'.
apply D. exists x. intros n.
apply not_all_not_ex. intros D''.
specialize (D' n). apply D'. intros i L.
specialize (D'' i). apply not_and_or in D''.
destruct D'' as [H|H].
* exfalso. omega.
* assumption.
- destruct (XM (exists i : nat, forall j : nat, exists k : nat, j < k /\ tilde_w_equiv f i k)) as [D|D].
+ now left.
+ right. intros i.
apply not_all_not_ex. intros D'.
apply D. apply not_all_not_ex. intros D''.
specialize (D'' i). apply not_all_ex_not in D''.
destruct D'' as[j D''].
apply D''. apply not_all_not_ex. intros D'''.
specialize (D' j). apply D'.
intros k. specialize (D''' k). apply not_and_or in D'''.
destruct D''' as [H|H].
* left. omega.
* right. assumption.
Qed.
Section RamseyanFactorizationMarkov.
Definition Markov := forall (f:nat -> bool), ~(forall n, f n = true) -> exists n, f n = false.
Definition sgBoolAnd := mkSG Bool.andb_assoc.
Lemma big_and_true f i j: true = ADD (X:=sgBoolAnd) (extract i j f) ->i < j -> forall n, i <=n < j -> f n = true.
Proof.
intros T O n [L G].
remember (j - i) as k. assert (j = i + k) by omega. subst j.
clear Heqk.
induction k.
- exfalso. omega.
- decide (k = 0).
+ subst k. rewrite_eq (i + 1 = S i) in T. rewrite ADD_single_extract in T.
assert (n = i) by omega. now subst n.
+ rewrite_eq (i + S k = S (i + k)) in T. rewrite ADD_extract_last in T by omega.
decide (n < i + k).
* apply IHk; oauto.
destruct (ADD (extract i (i + k) f)); auto.
* assert (n = i +k ) by omega. subst n.
destruct (f(i + k)); auto.
destruct ((ADD (extract i (i + k) f))); cbn in T; auto.
Qed.
Lemma big_and_false f i j: false = ADD (X:=sgBoolAnd) (extract i j f) -> i < j -> exists n, i <=n < j /\ f n = false.
Proof.
intros F O .
remember (j - i) as k. assert (j = i + k) by omega. subst j.
clear Heqk.
induction k.
- exfalso. omega.
- decide ( k = 0).
+ subst k. exists i. split; oauto.
rewrite_eq (i + 1 = S i) in F.
now rewrite ADD_single_extract in F.
+ rewrite_eq (i + S k =S (i + k)) in F.
rewrite ADD_extract_last in F by omega.
destruct (ADD (extract i (i + k) f)).
* exists (i + k). split; oauto.
* destruct IHk as [j [L F']]; oauto.
exists j. split; oauto.
Qed.
Lemma slot_in_smonotone g k : s_monotone g -> g 0 <= k -> exists n, g n <= k < g (S n).
Proof.
intros Mon G.
destruct (s_monotone_unbouded_ge Mon k) as [m P].
assert (k < g m) as H by omega.
assert (0 <= m) as H2 by omega.
exists (pred (next_position H2 H)).
pose proof (next_position_correct H2 H).
pose proof (next_position_all (L:=H2) (F:=H)).
destruct ((next_position H2 H)).
- simpl. exfalso. omega.
- simpl. split; oauto.
specialize (H1 n). omega.
Qed.
Lemma RamseyFacImpliesMarkov : RamseyFac sgBoolAnd -> Markov.
Proof.
intros RF f.
destruct (RF f) as [g [Mon Hom]].
destruct (ADD (extract (X:=sgBoolAnd) (g 0) (g 1) f)) eqn:E.
- decide (exists n, n < g 0 /\ f n = false) as [D|D].
+ intros _. firstorder.
+ intros N. exfalso. apply N.
intros n. decide (n < g 0).
* decide (f n = true) as [D'|D']; auto.
exfalso. apply D. exists n. split; auto.
destruct (f n); congruence.
* assert (exists k, g k <= n < g (S k)) as H2. {apply slot_in_smonotone; oauto. }
destruct H2 as [k H2].
specialize (Hom k).
apply (big_and_true Hom); omega.
- intros _. specialize (Hom 0).
destruct (big_and_false Hom) as [n [O F]]; oauto.
now exists n.
Qed.
End RamseyanFactorizationMarkov.
Definition Markov := forall (f:nat -> bool), ~(forall n, f n = true) -> exists n, f n = false.
Definition sgBoolAnd := mkSG Bool.andb_assoc.
Lemma big_and_true f i j: true = ADD (X:=sgBoolAnd) (extract i j f) ->i < j -> forall n, i <=n < j -> f n = true.
Proof.
intros T O n [L G].
remember (j - i) as k. assert (j = i + k) by omega. subst j.
clear Heqk.
induction k.
- exfalso. omega.
- decide (k = 0).
+ subst k. rewrite_eq (i + 1 = S i) in T. rewrite ADD_single_extract in T.
assert (n = i) by omega. now subst n.
+ rewrite_eq (i + S k = S (i + k)) in T. rewrite ADD_extract_last in T by omega.
decide (n < i + k).
* apply IHk; oauto.
destruct (ADD (extract i (i + k) f)); auto.
* assert (n = i +k ) by omega. subst n.
destruct (f(i + k)); auto.
destruct ((ADD (extract i (i + k) f))); cbn in T; auto.
Qed.
Lemma big_and_false f i j: false = ADD (X:=sgBoolAnd) (extract i j f) -> i < j -> exists n, i <=n < j /\ f n = false.
Proof.
intros F O .
remember (j - i) as k. assert (j = i + k) by omega. subst j.
clear Heqk.
induction k.
- exfalso. omega.
- decide ( k = 0).
+ subst k. exists i. split; oauto.
rewrite_eq (i + 1 = S i) in F.
now rewrite ADD_single_extract in F.
+ rewrite_eq (i + S k =S (i + k)) in F.
rewrite ADD_extract_last in F by omega.
destruct (ADD (extract i (i + k) f)).
* exists (i + k). split; oauto.
* destruct IHk as [j [L F']]; oauto.
exists j. split; oauto.
Qed.
Lemma slot_in_smonotone g k : s_monotone g -> g 0 <= k -> exists n, g n <= k < g (S n).
Proof.
intros Mon G.
destruct (s_monotone_unbouded_ge Mon k) as [m P].
assert (k < g m) as H by omega.
assert (0 <= m) as H2 by omega.
exists (pred (next_position H2 H)).
pose proof (next_position_correct H2 H).
pose proof (next_position_all (L:=H2) (F:=H)).
destruct ((next_position H2 H)).
- simpl. exfalso. omega.
- simpl. split; oauto.
specialize (H1 n). omega.
Qed.
Lemma RamseyFacImpliesMarkov : RamseyFac sgBoolAnd -> Markov.
Proof.
intros RF f.
destruct (RF f) as [g [Mon Hom]].
destruct (ADD (extract (X:=sgBoolAnd) (g 0) (g 1) f)) eqn:E.
- decide (exists n, n < g 0 /\ f n = false) as [D|D].
+ intros _. firstorder.
+ intros N. exfalso. apply N.
intros n. decide (n < g 0).
* decide (f n = true) as [D'|D']; auto.
exfalso. apply D. exists n. split; auto.
destruct (f n); congruence.
* assert (exists k, g k <= n < g (S k)) as H2. {apply slot_in_smonotone; oauto. }
destruct H2 as [k H2].
specialize (Hom k).
apply (big_and_true Hom); omega.
- intros _. specialize (Hom 0).
destruct (big_and_false Hom) as [n [O F]]; oauto.
now exists n.
Qed.
End RamseyanFactorizationMarkov.