IntuitionisticRamseyTheorem

A proof by Thierry Coquand, of an intuitionistic interpretation of Ramsey's Theorem. This is part of the paper Stop when you are Almost-Full, Adventures in constructive termination, by Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt, submitted for ITP 2012.

• A direct proof of Ramsey’s Theorem (pdf), Thierry Coquand, Oct 24, 2011.
• Agda formalisation in html, by David Wahlstedt,
• or the two above, and Agda source code, in a zip-file.

A revised version of David Wahlstedt's Agda formalization (by Sergei Romanenko) can be found here. The purpose of this refactoring is twofold:

• To reuse the stuff provided by the standard library. This can be useful in cases where the proof has to be embedded into another Agda project based on the standard library.
• To make the form of the proof more "human-friendly". In particular, by the extensive use of Relation.Binary.PreorderReasoning.

In addition, an Agda version of (a subset of the) Coq code, accompanying the paper Stop when you are Almost-Full, Adventures in constructive termination can be found here.