Friday 4 December 2015, 10:30, LSV: An axiom free Coq proof of Kruskal's tree theorem, Dominique Larchey.

We present a Coq implementation of a purely inductive proof of Kruskal's tree theorem: "If R is a well quasi-order (WQO) on X then homeomorphic_embedding(R) is a WQO on the finite trees decorated by values in X."

Contrary to classical proofs, there are a few instances of intuitionistic proofs for the Kruskal tree theorem. Some of these proofs requires the further assumption that the ground relation R is decidable (eg. Monika Seisenberger's proof or Jean Goubault-Larrecq's proof). Wim Veldman's proof is the only published proof that does not require that assumption of decidability, but it requires "Brouwer's thesis". Moreover, none of these proofs had been mechanized before.

We implement a typed variant of Wim Veldman's intuitionistic proof and we show that the use of the axiom called "Brouwer's thesis" is not necessary in that setting which makes our proof an axiom free one (w.r.t. the CIC on which Coq is based).

We use Thierry Coquand et al. inductive definition of Almost Full (AF) relations as an alternative to Wim Veldman's. We present the architecture of Wim Veldman's proof and its fundamental constituents: Ramsey's theorem, the Fan theorem, combinatorial principles and Evaluation maps. We show how to replace Wim Veldman "stump" based induction by lexicographic products of relations well-founded upto a projection.