Home

Awesome

(**************************************************************)
(*   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 library formalizes ground results about Almost Full relations (AF) in Coq 8.14+, up to Dickson's lemma, but excluding Higman's lemma or the more complex Kruskal's tree theorem which are to be provided in upcoming libraries. This library is a major and modular rewrite of a somewhat monolithic development concluding in a constructive/inductive proof of Kruskal's tree theorem. This library has some overlap with the Almost Full coq-community project (see below) but they have different objectives.

We define the notion of AF relation inductively as the constructive counterpart of the classical notion of Well Quasi Order (WQO). The results contained in here are:

This library is distributed under the terms of the MPL-2.0 license.

Dependencies and install

It can be installed via opam

opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install coq-kruskal-almostfull

and requires

but see also

It can then be accessed via From KruskalAfProp Require ... or From KruskalAfType Require ..., see section on the external interface below.

Comparisons with the Almost Full coq-community project

That project was initiated as the artifact of the paper of Coquand et al Stop When You Are Almost-Full. It has not really evolved beyond that goal. As with the current Kruskal-Almostfull, there is a Type-bounded and a Prop-bounded version of the almost-full library, but they have a disjoint code base. Comparing the contents of the libraries, there is some overlap in the results: eg Ramsey's theorem (of which of our own proof is a cleanup/rework a former version of theirs). But the two projects head in different directions.

The main differences with the Kruskal-Almostfull project are (IMHO):

Overview of the definitions

Following the work of , we characterize AF relations using an inductive predicate:

Inductive af {X : Type} (R : X → X → Prop) : Prop :=
  | af_full : (∀ x y, R x y) → af R
  | af_lift : (∀ a, af (R↑a)) → af R
where "R↑a" := (λ x y, R x y ∨ R a x).

From this definition, we recover the property characterising WQOs classically:

af_recursion : af R → ∀f : nat → X, ∃ i j, i < j ∧ R fᵢ fⱼ

where the type X is not explicit: this means that any (infinite) sequence f : nat → X contains a good pair (ie increasing: both i < j and R fᵢ fⱼ hold). Notice that the af R predicate is constructively stronger than its classical characterization, mainly because, as Coquand frames it, it works also for sequences that are not given by a law (hence living outside of type nat → X).

A variant definition can be implemented at Type level (informative) instead of the Prop level (non-informative) with the nearly identical definition (except of the output type):

Inductive af {X : Type} (R : X → X → Prop) : Type :=
  | af_full : (∀ x y, R x y) → af R
  | af_lift : (∀ a, af (R↑a)) → af R.

In that case, the af_recursion we derive is more informative:

af_recursion : af R → ∀f : nat → X, { n | ∃ i j, i < j < n ∧ R fᵢ fⱼ }

and read as follows: for any sequence f : nat → X, one can compute a bound (from information contained in both af R and f) such that below that bound n, we know for sure that there is a good pair in the initial segment f₀,...,fₙ₋₁. Notice that we do not necessarily have enough information to compute where precisely this good pair resides inside that initial segment (eg when R is not decidable).

In the Type case, the af predicate is more informative (and indeed stronger) than in the Prop case: it contains a computational contents. See below for a section discussing this question specifically.

Dealing with Prop vs Type

The library deals with both versions af R : Prop or af R : Type in a generic way, using the same code base. Indeed, in Ltac language, identical proof scripts can accommodate with the two variants Prop vs Type in a uniform way. The actual Coq lambda-terms produced by these scripts differ however but these terms are here computer generated exclusively by Ltac proof scripts.

To deal with the Prop vs Type choice, we define a notation Base which is either Base := Prop or Base := Type and, consistently with this choice, notations for first order like connectives described below:

+------+-----------+---------+----------+--------------+
| Base |   ⊥ₜ      |   ∨ₜ    |   ∧ₜ     |   ∃ₜ         |
+------+-----------+---------+----------+--------------+
| Prop | False     | ∨ / or  | ∧ / and  | ∃ / ex       |
| Type | Empty_set | + / sum | * / prod | { & } / sigT |
+------+-----------+---------+----------+--------------+

The if and only if connective is also defined as ⇄ₜ but it is not primitive, ie it is a combination of ∧ₜ and the arrow . Notice that universal quantification (and its restriction, the arrow ) are naturally parametric in the Prop vs Type choice (they are not inductive) whereas the other above (eg. or and ex) are not parametric (and they are inductivelly defined).

In that setting grounded on the Base choice/notation, the parametric definition of af becomes

Inductive af {X} (R : X → X → Prop) : Base :=
  | af_full : (∀ x y, R x y) → af R
  | af_lift : (∀ a, af (R↑a)) → af R.

To be complete, with af_recursion, we get a refinement of the property classically characterizing WQOs, stated (and proved) as

Fact af_recursion X (R : X → X → Prop) : af R → ∀f : nat → X, ∃ₜ n, ∃ i j, i < j < n ∧ R fᵢ fⱼ

using the generic first order syntax depending on the choice of Base:

The existential quantifiers binding i and j are non-informative in either case. As hinted above, the af R predicate itself does not contain enough information to compute the exact position of a good pair. Only a bound under which one such pair must exist can be extracted. Provided that we are given a decision procedure for the relation R, this bound can then be used to compute a good pair using exhaustive finitary search.

See the discussion below for more details on the proof of af_recursion and the computational contents of the af predicate.

Some results contained in Kruskal-AlmostFull

We give a non-exhaustive summary of the main results contained in this library:

Theorem af_le_nat : af ≤. 
Theorem af_eq_fin X : (∃ₜ l : list X, ∀x, x ∊ l) → af (@eq X).
Theorem af_inter X (R T : X → X → Prop) : af R → af T → af (R ∩₂ T).
Theorem af_product X (R T : X → X → Prop) : af R → af T → af (R ⨯ T).
Theorem af_vec_fall2 k X (R : X → X → Prop) : af R → af (vec_fall2 R k).

Combining af_le_nat, af_vec_fall2 and af_recursion, we get Dickson_lemma:

Theorem Dickson_lemma k : ∀f : nat → vec nat k, ∃ₜ n ∃ i j, i < j < n ∧ ∀p, fᵢ⦃p⦄ ≤ fⱼ⦃p⦄.

and, because the relation _ ≤ _ over nat is decidable, we can derive the stronger form

Theorem Dickson_lemma_strong k : ∀f : nat → vec nat k, ∃ₜ i j, i < j ∧ ∀p, fᵢ⦃p⦄ ≤ fⱼ⦃p⦄.

hence a computation of a good pair (not just a bound) (using the Base := Type variant).

The external interface

The installation procedure compiles the code base twice:

Then both KruskalAfProp and KruskalAfType can be imported from at the same time but there name spaces coincide and it is strongly advised not to load both. The intent is to write code that works with either choice.

From the point of view of the external interface of the library, if one wants the Base := Prop choice, then the import command would be:

From KruskalAfProp Require Export base almost_full.

and on the other hand, for the Base := Type choice, the import command would be:

From KruskalAfType Require Export base almost_full.

It is recommended to perform this import in a single file using the Export directive so that Base would be properly defined uniformly in every single file importing the library.

The computational contents of the af predicate

We elaborate on the computational contents (CC) of the af predicate in case the choice Base := Type was made. The CC is also meaningful when Base := Prop however, as is conventional in Coq, that CC is sandboxed in the Prop realm, and it cannot leak in the Type realm.

A way to look at the CC is to study the proof term for af_recursion which would be the following

Fixpoint af_recursion {R} (a : af R) f {struct a} : { n | ∃ i j, i < j < n ∧ R fᵢ fⱼ } :=
  match a with
  | af_full h => exist _ 2 [PO₁]
  | af_lift h => let (n,hn) := af_recursion (h f₀) (λ x, f (S x)) in
                 exist _ (S n) [PO₂]
  end.

in programming style where proofs are just Coq lambda-terms. It is easier to analyse the CC in this form of proofs rather than Ltac style proofs.

We see that it proceeds as a fixpoint by structural recursion on the proof of the af R predicate:

Hence, we can view the computational contents of a : af R as containing well founded tree and use f to traverse a branch of that tree, selecting the upper node with f₀, f₁, f₂ successively until the relation R↑f₀...↑fₙ₋₁ becomes full. The number n of nodes crossed until the af tree tells us this relation is full gives the bound 2+n. The well founded tree contained in a : af R collects, along its branches, bounds on the position of good pairs for every possible sequence of values.

Relational surjective morphisms

Transporting the AF property from R : X → X → Prop to T : Y → Y → Prop can be performed using a morphism f : X → Y which is a relation preserving map, moreover supposed to be surjective. Hence, proving a statement like eg af R → af T only involves providing f : X → Y, and proving:

which is very convenient indeed: the notion of AF is absent from those two requirements. Unfortunately this does not work very well with Σ-types. For instance consider the natural statement that AF is closed under restriction:

af_af_sub_rel X (P : X → Prop) (R : X → X → Prop): af R → af R⇓P

where R⇓P : {x | P x} → {x | P x} → Prop is the restriction of R : X → X → Prop to the Σ-type {x | P x}. There is an "obvious" surjective morphism from X to {x | P x} except that it is not so obvious:

To avoid these strong impairments, we can instead view the morphism as a relation of type f : X → Y → Prop instead of type f : X → Y. Then:

In the case of the projection on the Σ-type {x | P x}, the morphism f is simply defined as f := λ x y, x = π₁ y and we are (almost) done!! Using relational morphisms it becomes trivial to establish results like eg:

Fact af_lift_af_sub_rel X R (x₀ : X) : af R↑x₀ → af R⇓(λ x, ¬ R x₀ x).
Proof.
  af rel morph (λ x y, x = π₁ y).
  + intros []; simpl; eauto.
  + intros ? ? [] [] -> ->; simpl; tauto.
Qed.

Beware the converse implication af R⇓(λ x, ¬ R x₀ x) → af R↑x₀ is an involved question related to the decidability of R x₀.