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:

the assumption of the decidability of the ground relation R as in Monika Seisenberger's work. Beware that M. Seisenberger's definition of Well (well-foundedness of the relation cons over R-bad sequences, where cons w w' iff w = a::w' for some a) is not intuitionistically equivalent to "R is almost full"; it is only equivalent when the relation R is decidable;
or any added axiom, like Brouwer's Thesis as in Wim Veldman's work. It is usually accepted by intuitionists but as we show, it is actually not needed for the proof of Kruskal's tree theorem;
the result is proved both in its informative (type-bounded) version and in its logical (prop-bounded) version (beware that the prop-bounded version is not a trivial consequence of the type-bounded version).

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:

it extends the work of Daniel Fridlender on Higman's Lemma but it is much more complicated. Two ingredients of Fridlender's proof are kept: bar induction and his formulation of the Fan theorem;
it follows the proof principles used by Wim Veldman but in the context of arbitrary types and relations. In particular, it uses generalizations of the Fan theorem, the Combinatorial Principle and the Evaluation maps;
it uses the definition of Almost Full relations proposed by Thierry Coquand as well his intuitionistic proof of Ramsey's Theorem;
to get the logical/prop-bounded version, it replaces Wim Veldman's induction on finitary stump's by a lexicographic induction principle based on the concept of being well-founded upto a projection (which might be a new concept, but I am not sure).

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.