(**************************************************************) (* Copyright Dominique Larchey-Wendling [*] *) (* *) (* [*] Affiliation LORIA -- CNRS *) (**************************************************************) (* This file is distributed under the terms of the *) (* Mozilla Public License Version 2.0, MPL-2.0 *) (**************************************************************)

What is this library?

This sub-project is part of the larger project Coq-Kruskal described here: https://github.com/DmxLarchey/Coq-Kruskal.

This library formalizes in Coq 8.14+ the notion of rose tree via purely inductive characterizations and provides implementations of proper (nested) induction principles and tools to manipulate those trees.

It is was extracted from a complete rework of the proof of Kruskal's tree theorem based on dependent vectors instead of lists, but can be used independently under the Mozilla Public License MPL-2.0, as initially requested by eg @jjhugues.

This README file provides a simple introduction to the main definitions.

Overview of the definitions

Some remarks about notations below:

• implicit parameters are denoted between {...} as in Coq (eg {X : Type}) and we do not specify them afterwards except when terms are preceded with an @ which locally disables implicit parameters. Eg we can write @In X x l or In x l or x ∊ l -- they are the same, -- provided the type of x is guessably X, or the type of l is guessably list X;
• we write _ for arguments that Coq can guess by unification from other arguments, eg @In _ x l is the same as In x l, and vec _ n gives the length of vectors without giving the base type.

Data structures for lists, indices idx n and vectors vec X n:

Let us continue with the usual data-structures:

• type of natural numbers nat;
• type of lists list X over base type X : Type;
• type of indices idx n from [0,n[ (identical to Fin.t);
• dependent (uniform) vectors vec X n with X : Type and n : nat (identical to Vector.t);
• access to components of vectors via v⦃i⦄ with v : vec _ n and i : idx n.

``` Inductive nat : Type := | O : nat | S : nat → nat. (* Decimal notations 0, 1, 2, ... are accepted *)

Inductive list (X : Type) : Type := | nil : list X | cons : X → list X → list X where "[]" := (@nil _) and "x :: l" := (@cons _ x l).

Fixpoint In {X} (x : X) (l : list X) : Prop := match l with | [] ⇒ False | y::l ⇒ y = x ⋁ x ∊ l end where "x ∊ l" := (@In _ x l).

Inductive idx n : Type := | idxfst : idx (S n) | idxnxt : idx n → idx (S n) where "𝕆" := idxfst and "𝕊" := idxnxt.

Inductive vec X : nat → Type := | vecnil : vec X 0 | veccons : ∀n, X → vec X n → vec X (S n). where "∅" := vecnil. and "x ## v" := (@veccons _ x v).

Fixpoint vecprj X n (v : vec X n) : idx n → X := match v with ... (* a bit complicated but critical piece of code *) end where "v⦃i⦄" := (@vecprj _ _ v i).

(* Verifies the below fixpoint equations by reduction) Goal (x##)⦃𝕆⦄ = x. Goal (##v)⦃𝕊 p⦄ = v⦃p⦄. ```

Data structure for trees

Now we come to variations arround rose trees (finitely branching finite trees), ie direct sub-trees are collected in list or vec _ n:

• uniform trees ltree X as lists of trees with nodes of type X : Type;
• dependent trees dtree X where each arity n as nodes of type X n : Type;
• dependent uniform trees vtree X as vectors of trees with nodes of type X : Type;
• undecorated trees btree k with branching bounded by k : nat;
• undecorated finitely branching trees rtree as lists of trees.

``` Inductive ltree (X : Type) : Type := | inltree : X → list (ltree X) → ltree X where "⟨x|l⟩ₗ" := (@inltree _ x l).

Inductive dtree (X : nat → Type) : Type := | indtree k : X k → vec (dtree X) k → dtree X where "⟨x|v⟩" := (@indtree _ _ x v).

Notation "vtree X" := (dtree (λ _, X)).

Inductive btree k := btree_cons n : vec btree n → n < k → btree.

Inductive rtree := rt : list rtree -> rtree. ```

The critical tools and inductions principles, ie ltree_rect, dtree_rect, vtree_rect, btree_rect and rtree_rect.

Notice that the arity/breadth can be bounded at k : nat in dtree X by forcing X n to be an void type for n ≥ k, ie a type without inhabitants; this is a requirement in eg Higman's theorem.