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:
- the
af R
predicate characterizing AF relations; - the classical characterization with good pairs (see
af_recursion
below); - the equivalence with Bar inductive predicates:
af R ↔ bar (good R) []
; - critically, closure properties for
af
/bar
:- under direct products and direct sums via Coquand's version Ramsey's theorem;
- under relational morphism;
af =
for finite types,af ≤
fornat
;- closure of
af
underk
-ary products
- as a consequence, we get Dickson's lemma.
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
Kruskal-Higman
if you need Higman's lemma (homeomorphic list embedding is AF);Kruskal-Veldman
for the critical/central/complicate proof, following Wim Veldman's account;Kruskal-Theorems
for Kruskal's and Higman's tree theorems.
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):
- the proofs scripts and notations are not really aimed at user readability;
- it is not designed as a toolkit for further developments:
- it is missing a nice tool like surjective relational morphisms;
- their
af_finite
is much less versatile than our own version which holds for identity over any listable type;
- it includes, as a sizable code base, examples of termination proofs for recursive programs, which was driving the motivation of their paper;
- the motivation for
Kruskal-Almostfull
is to study and provide basic but versatile tools for the closure properties of AF relations.
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
:
- when
Base := Prop
, the formula∃ₜ n, ∃ i j, i < j < n ∧ ...
expands to∃ n i j, i < j < n ∧ ...
which in turn is logically equivalent to∃ i j, i < j ∧ ...
; - when
Base := Type
, the∃ₜ n, ...
quantifier is informative, ie expands to{ n & ... }
.
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).
- in
af_le_nat
, the relation_ ≤ _ : nat → nat → Prop
is the less-than (or natural) ordering onnat
; af_eq_fin
means that if a typeX
is listable (finite), then equality on that type is AF;af_inter
is Coquand's et al constructive version of Ramsey's theorem andaf_product
an immediate consequence of it.- by
af_product
iterating overk
times, we lift the binary product tok
-ary products, ie vectors of typevec X k
and obtainaf_vec_fall2
wherevec_fall2 R k := λ v w : vec X k, ∀p : idx k, R u⦃p⦄ v⦃p⦄
.
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:
- once under the choice
Base := Prop
and it installs theKruskalAfProp
library; - and once under the choice
Base := Type
and it installs theKruskalAfType
library.
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:
- when
R
is full, witnessed byh : ∀ x y, R x y
, thenn := 2
satisfies both0 < 1 < n
andR f₀ f₁
, which is denoted as[PO₁]
above; - when all the lifts of
R
areaf
witnessed byh : ∀ a, af (R↑a)
, then a recursive call on the proofh f₀ : af (R↑f₀)
computes a boundn
forR↑f₀
and the tail of the sequencef
(ieλ x, f (S x)
), and we state thatS n
is a bound forf
itself, and then prove it as[PO₂]
above; - the proof obligations
[PO₁]
and[PO₂]
are omitted here because do not participate in the CC.
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:
- morphism as
∀ u v, R u v → T (f u) (f v)
; - and surjectivity
∀ y, ∃ₜ x, y = f x
;
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:
- it cannot be implemented as a Coq function of type
X → {x | P x}
because the morphism is in fact a partial function that is not supposed to map valuesx
for whichP x
does not hold; - it cannot be proved surjective because there is no reason for uniqueness of the proof of
P x
(unlessP
is turned into a Boolean predicate).
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:
- not only the partiality constraint fades away;
- but also, the morphism can have several output values (possibly even infinitely many).
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₀
.