A mechanized inductive proof of Kruskal's tree theorem

This repository is about a formal intuitionistic Coq proof of the Kruskal tree theorem. For busy Coq developers, a brief description of the results with the minimal definitions to state them can be found in the readme.v file. The Kruskal_2.0.tar.gz archive contains the whole project. And developers interested in contributing further to the project can contact me directly to get an access to the living Mercurial SCM repository on BitBucket.

The Kruskal tree theorem states that well quasi orders (WQO) are stable under the tree homeomorphic embedding:

Kruskal tree theorem: if a relation R is a WQO then so is embed_tree_homeo(R)
The order-theory part of the theorem is really trivial stuff. What is highly non-trivial is the Well part. In fact, the concepts of quasi-order and well are orthogonal in the case of Kruskal's tree theorem. A binary relation R on X is Well if any infinite sequence s : nat -> X contains a good pair, i.e. i < j such that R (s i,s j). But there are numerous classically equivalent characterization of that property.

The proof we have developed shows that a suitable intuitionistic formulation of Well is the notion of Almost Full relations as defined by Thierry Coquand (there is an intutionistically equivalent formulation in terms of Bar predicates, as e.g. in Daniel Fridlender's thesis). Hence, we prove the following inductive Kruskal tree theorem:

Inductive Kruskal tree theorem: if a relation R is almost full then so is embed_tree_homeo(R)

It is easy to show (intuitionistically) that an almost full quasi-order is also a WQO. The converse is classically provable, but intuitionistically, it depends on how you define WQOs: the many classically equivalent definitions of WQO are generally not intuitionistically equivalent to each other.

The inductive proof of Kruskal's tree theorem we have developed does not suffer any of the restrictions that occur in other existing intuitionistic proofs of Kruskal's theorem such as:

Our proof is purely based on intuitionistic reasoning with inductive predicates and thus, cannot really be compared to shorter (and easier) classical proofs such as those based on the Crispin Nash-William's minimal bad-sequence argument, like in e.g.

Certified Kruskal's Tree Theorem in Christian Sternagel paper (with a mechanized proof in Isabelle/HOL)
Those proofs assume the excluded middle as well as some form of the axiom of choice.

In a way, the proof we have obtained can be seen as a mix and extension of the following contributions:

The code is distributed under the CeCILL v2 Free Software Licence Agreement and can be accessed in form the a Kruskal_2.0.tar.gz archive containing a Makefile and the readme.v. It borrows a bit of an apparently unlicensed Coq source code that comes as a companion to the excellent paper (a Must Read):

Stop when you are Almost-Full: Adventures in constructive termination by Dimitrios Vytiniotis, Thierry Coquand and David Wahlstedt
The proof of the Fan theorem implements the ideas developed in:
An Interpretation of the Fan Theorem in Type Theory by Daniel Fridlender
and of course, the general concept of the proof is strongly based on the reference paper
An intuitionistic proof of Kruskal's Theorem by Wim Veldman
It includes no code borrowed from any other project but uses and extends the Coq Standard Library.

This project was developed by Dominique Larchey-Wendling over a period starting from May 2015 until October 2015. Many thanks to Wim Veldman (in helping me understanding the inner workings of his proof), and to Thierry Coquand and Jean Goubault-Larrecq for fruitfull interactions on alternative approaches to the Kruskal tree theorem.