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.

Page last modified on October 05, 2014, at 08:03 PM

Powered by
PmWiki