The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

After a long development effort, I am happy to announce the
availability of a mechanization in Coq (v8.4) of Higman's and
Kruskal's tree theorems. Higman's theorem is a restriction of
Kruskal's theorem to trees of arity bounded by a value k and
Higman's lemma is a restriction to lists (i.e. trees of
arity 0 or 1).

For a more complete description of the project achievements
and/or access to the source code, see

http://www.loria.fr/~larchey/Kruskal/

The code is distributed under the open source
CeCILL v2 Free Software Licence Agreement and
contains about 25k lines of definitions and proofs.

I would describe it as in beta stage, meaning that
it type-checks, it is soundly structured with
a Makefile, it contains comments, it is readable;
but some redundancies can still be removed and
better names could have been chosen, in particular
in the extension of the list library we propose.

The proof adapts the method of Wim Veldman to Inductive
Type Theory and replaces induction on finitary "stumps"
by inductive predicates.

Technically we show that:

 if R is an *Almost Full* relation, then
 so is the homeomorphic embedding emb_tree_homeo(R)

A brief Coq description of the results can be found
in the accompanying readme.v file.

The results are proved both in their informative (type-bounded) form
and their logical (prop-bounded) form. Notice that there is no easy
bridge from the informative version to the logical version and
that the proof of the logical version involved the use of
a weakened form of well-founded induction:
      "well-founded upto a projection".

The computational content of the informative version of the
theorems is the following:

a/ A "witness of almost-fullness" is a well-founded
  algorithm that computes for every infinite sequence of
  elements, a bound on the number of elements to consider
  to find a good pair;

b/ The proofs transforms a witness of almost-fullness for R
   into a witness of almost-fullness of emb_tree_homeo(R).

c/ But the proof do NOT compute a good pair (you cannot do
   this unless R is decidable), just a bound on the search
   space.

Both the informative and logical proofs requires no additional
axiom to Coq (like Brouwer's thesis in the paper of Wim Veldman).
They make no assumption on the relation R (like the decidability
of R in the work of Monika Seisenberger).

If you are interested in such a proof or in the development of
a extensive Coq library for Almost Full relations (which form
a solid basis for Open Induction), do not hesitate to contact
me to get a direct access to the development repository.

Dominique Larchey-Wendling
TYPES, LORIA, CNRS