[Agda] Ramsey theorem

[Sergei Meshveliani]

My aim is to 
find and investigate a possibly simplest problem such that  
1) it has a short and nice classical proof,
2) any its known constructive proof is considerably more difficult and 
   larger.

And I keep in mind its possible implementation in Agda.  
I need both, to see and understand a classical proof and to see/compose
a constructive proof.

People have advised me these candidates:  

(1) Higman's lemma about an infinite sequence of words in the alphabet 
    {a, b}, 
(2) Ramsey's theorem about about sub-graphs (is occurs now that there 
    are different versions).
(3) Dickson's lemma.

They say, there is a nice classical proof due to Nash-Williams for  (1)
for any finite alphabet.
I cannot directly access to the Nash-Williams paper.
A certain other paper retells this proof, with writing in the middle
"Using Ramsey's theorem and the fact that our alphabet A is well quasi
ordered, we know that there exists an infinite subsequence ...
". 

I decide, that probably, Ramsey's theorem is more basic, and it needs to
be investigated earlier.
Right?

I find a formulation of some Ramsey's theorem on

  https://proofwiki.org/wiki/Ramsey's_Theorem

It is about the Ramsey's numbers R(r,s), a bound on them, it does not
involve infinite sequences, and the proof there looks simple and
constructive.  

And   http://www.ling.gu.se/~davidw/IRT/ramsey1-4.pdf

writes about the  infinite version of Ramsey’s Theorem.

Also I see the slides by Josef Berger on

http://www.google.com/url?q=http://www.math-inf.uni-greifswald.de/mathe/images/Gassner/Arbeitstreffen/JosefBergerSlides2013&sa=U&ei=YKK2U-DEDuKAywOErIGgCA&ved=0CBYQFjAA&sig2=DQ-YqNoYyGXiaHi5-HVCqA&usg=AFQjCNE1M2-987YOmQ-6Y3gMPYl4_i4O2w

where the Higman's lemma is derived from the Dickson's lemma. 
And the Dickson's lemma looks to me as the simplest one.

Now, I have the following questions.

(a) Which version of Ramsey’s Theorem is used in the Nash-Williams' 
    proof for the Higman's lemma?
(b) May it occur that the infinite version of the Ramsey's theorem 
    can be constructively derived in a simpler way from the Dickson's 
    lemma?
(c) Which of the above problems is more simple for a classical proof?
    For constructive proof?  

Thanks,

------
Sergei




On Fri, 2014-07-04 at 13:48 +0200, Josef Svenningsson wrote:
> If you're interested in Ramsey's theorem for the purpose of
> termination I suggest you read the paper "Stop When You Are
> Almost-Full", by Dimitrios Vytiniotis, Thierry Coquand and David
> Wahlstedt. They develop an intuitionistic Ramsey theorem to be used
> for proving termination. The paper uses Coq but there is an Agda
> formalization here:
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.IntuitionisticRamseyTheorem
> 
> 
> Josef
> 
> 
> 
> 
> On Fri, Jul 4, 2014 at 1:29 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         People,
>         
>         is there publicly available a proof  in Agda  of the  Ramsey's
>         theorem
>         (about the size of a monochromatic sub-graph in a complete
>         graph)
>         ?
>         
>         Thanks,
>         
>         ------
>         Sergei
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
> 
>