Intuitionistic Ramsey Theorem

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