(* A proof of infinite Ramsey's theorem *)



(* Unbounded sets *)
Let UB (I : nat -> Prop) : Prop := forall x, exists y, x <= y /\ I y.


(*
Theorem Ramsey :
forall f : nat -> nat -> nat, forall k : nat, (forall x y, f x y <= k) ->
exists U : nat -> Prop, UB U /\
  exists i, i <= k /\ forall x y : nat, U x -> U y -> x < y -> f x y = i.
*)




Section WF_Induction.

Theorem LtInd : forall P : nat -> Prop,
  (forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x.
Proof.
...
Qed.

End WF_Induction.

Section Minimum_Principle.
Hypothesis DNE : forall A, (~ ~ A) -> A.

Variable P : nat -> Prop.
Hypothesis ExP : exists x, P x.


Theorem MinP : exists x, P x /\ forall y, P y -> x <= y.
Proof.
...
Qed.
End Minimum_Principle.


(*************)
(*           *)
(*    IPP    *)
(*           *)
(*************)

Section IPP.
Hypothesis DNE : forall P, (~ ~ P) -> P.

Variable U : nat -> Prop.
Hypothesis UBU : UB U.

Variable I : nat -> nat -> Prop.
Variable k : nat.
Hypothesis I_bounded : forall x, U x -> exists i, i <= k /\ I i x.

(* To show : *)
(*
   IPP : exists i, i <= k /\ UB (fun t => U t /\ I i t)
*)

Theorem IPP : exists i, i <= k /\ UB (fun t => U t /\ I i t).
Proof.
...
Qed.

End IPP.





(****************)
(*              *)
(*    Ramsey    *)
(*              *)
(****************)

(* We show Ramsey's theorem, under the assumptions:
 * - The Minimum Principle
 * - IPP
 * - The predicate [Seq] the sequence is definable
 *)
Section Ramsey.
Hypothesis MinP : forall P : nat -> Prop, (exists x, P x) ->
  exists x, P x /\ forall y, P y -> x <= y.

Hypothesis IPP : forall U : nat -> Prop, UB U ->
  forall I : nat -> nat -> Prop, forall k : nat,
  (forall x, U x -> exists i, i <= k /\ I i x) ->
    exists i, i <= k /\ UB (fun t => U t /\ I i t).


Hypothesis EM : forall A, A \/ ~ A.


(* The coloring *)
Variable C : nat -> nat -> nat.
Variable k : nat.
Hypothesis C_bounded : forall x y, C x y <= k.

(* The [Seq] predicate *)
Variable Seq : nat -> Prop.

Hypothesis DefSeq : forall x, Seq x <->
  UB (fun t => forall y, y < x -> Seq y ->
        C y t = C y x
        /\ forall z, y < z -> z < x -> Seq z -> C y z = C y x).



(* The main goal is to show that [Seq] is unbounded *)
Section Seq_UB.

Let CumHom (n : nat) : nat -> Prop :=
  fun x =>
    UB (fun t => forall y, y < n -> Seq y ->
        C y t = C y x
        /\ forall z, y < z -> z < n -> Seq z -> C y z = C y x).


Section CumHom_UB.

Let Hom (n : nat) : nat -> Prop :=
  fun x => forall y, y < n -> Seq y ->
    forall z, y < z -> z < n -> Seq z -> C y z = C y x.

Lemma Hom_UB : forall n, UB (Hom n).
Proof.
...
Qed. 


Lemma CumHom_Hom : forall n, exists x, n <= x /\
    UB (fun t => Hom n t /\
     forall y, y < n -> Seq y -> C y t = C y x).
Proof. 
...
Qed.


Lemma CumHom_UB : forall n, exists x, n <= x /\ CumHom n x.
Proof.
...
Qed.
End CumHom_UB.


Lemma Seq_UB : UB Seq.
Proof.
...
Qed.

End Seq_UB.



Theorem Ramsey_MinP_IPP_EM : exists U : nat -> Prop, UB U /\
  exists i, i <= k /\
    forall x y : nat, U x -> U y -> x < y -> C x y = i.
Proof.
...
Qed.
End Ramsey.

Check Ramsey_MinP_IPP_EM.






(**************)
(*            *)
(*     Acc    *)
(*            *)
(**************)


(* Definition of the [Seq] predicate *)
Section Acc.

Lemma acc : forall x, Acc lt x.
Proof.
...
Qed.

Section Seq.
Variable C : nat -> nat -> nat.

Fixpoint seq (x : nat) (a : Acc lt x) {struct a} : Prop := ...

(* [seq] does not depend from the proof of [AccType lt x] *)
Lemma seq_invariant : forall x, forall (G K : Acc lt x),
  seq x G -> seq x K.
Proof.
...
Qed.


(* This justifies the following definition *)
Definition Seq x := seq x (acc x).

(* It remains to show that the predicate [Seq]
 * indeed satisfies [DefSeq] :
   Seq x <->
   UB (fun t => forall y, y < x -> A y ->
        C y t = C y x
        /\ forall z, y < z -> z < x -> A z -> C y z = C y x).
*)

Theorem Seq_Correct : forall x, Seq x <->
   UB (fun t => forall y, y < x -> Seq y ->
        C y t = C y x
        /\ forall z, y < z -> z < x -> Seq z -> C y z = C y x).
Proof.
...
Qed.

End Seq.
End Acc.


(* Putting everything together, we obtain Ramsey's theorem *)


Theorem Ramsey : (forall A, (~ ~ A) -> A) ->
  forall C : nat -> nat -> nat, forall k : nat,
  (forall x y, C x y <= k) ->
  exists U : nat -> Prop, UB U /\
    exists i, i <= k /\ forall x y : nat, U x -> U y -> x < y -> C x y = i.
Proof.
...
Qed.

Check Ramsey.