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:

TheKruskal tree theorem: if a relation R is a WQO then so is embed_tree_homeo(R)

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.

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

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*):

The proof of the Fan theorem implements the ideas developed in:Stop when you are Almost-Full: Adventures in constructive terminationby Dimitrios Vytiniotis, Thierry Coquand and David Wahlstedt

and of course, the general concept of the proof is strongly based on the reference paperAn Interpretation of the Fan Theorem in Type Theoryby Daniel Fridlender

It includes no code borrowed from any other project but uses and extends the Coq Standard Library.An intuitionistic proof of Kruskal's Theoremby Wim Veldman

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.