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
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.