(**************************************************************)
(* Copyright Dominique Larchey-Wendling [*] *)
(* *)
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
(*
This file contains the basic definitions needed to state the
Higman lemma, the Higman theorem, the Vazsonyi's conjecture
and the Kruskal tree theorem.
To stay short, nearly no proof is provided in here but the
source code in the other *.v files contains all the proofs
required for those theorems.
To compile them, you need Coq 8.4 or newer (the code was
developed with Coq 8.4pl3)
type "make kruskal_thm.vo"
other targets of interest:
- higman_lemma.vo
- higman_thm.vo
- higman_abt.vo
- vazsonyi.vo
*)
Require Import Arith.
Require Import List.
Require Import Wf.
Set Implicit Arguments.
Notation "A 'inc1' B" := (forall x, A x -> B x) (at level 75, no associativity).
Notation "A 'inc2' B" := (forall x y, A x y -> B x y) (at level 75, no associativity).
Notation full := ((fun X (R : X -> X -> Prop) => forall x y, R x y) _).
Definition rel_restr X (R : X -> X -> Prop) (P : X -> Prop) (x y : { a | P a }) := R (proj1_sig x) (proj1_sig y).
Implicit Arguments rel_restr [ X ].
Notation "R '<#' P '#>'" := (rel_restr R P) (at level 70, no associativity).
Section words_as_lists.
Variables (X Y : Type) (R : X -> Y -> Prop).
Infix "<<" := R (at level 70).
Reserved Notation "x '<*' y" (at level 70).
Inductive subword : list X -> list Y -> Prop :=
| in_sw_0 : nil <* nil
| in_sw_1 : forall ll mm b, ll <* mm -> ll <* b::mm
| in_sw_2 : forall ll mm a b, a << b -> ll <* mm -> a::ll <* b::mm
where "x <* y" := (subword x y).
End words_as_lists.
Section trees.
Variable (X : Type).
(* because of nested induction tree X ~ X * list (tree X),
the following definition DOES NOT automatically generate a powerfull
enough elimination scheme/induction principle ... we have to build
it by hand (see source code)
*)
Inductive tree : Type := in_tree : X -> list tree -> tree.
Definition tree_fall : (X -> list tree -> Prop) -> tree -> Prop.
Admitted.
Fact tree_fall_fix P x ll : tree_fall P (in_tree x ll)
<-> P x ll
/\ forall t, In t ll -> tree_fall P t.
Admitted.
(* btrees are tree of breadth strictly bounded by k, ie each node has
strictly less than k sons *)
Definition btree k := tree_fall (fun _ ll => length ll < k).
Variable (R : X -> X -> Prop).
(* the two following definitions DO NOT generate powerfull enough elimination
schemes/induction principle ... we have to build them by hand
*)
Reserved Notation "x ' tree -> Prop :=
| in_emb_tree_product_0 : forall s t x ll, In t ll -> s s Forall2 emb_tree_product ll mm -> in_tree x ll tree -> Prop :=
| in_emb_tree_homeo_0 : forall s t x ll, In t ll -> s s subword emb_tree_homeo ll mm -> in_tree x ll X -> Prop) a := fun x y => R x y \/ R a x.
Infix "rlift" := (@lift_rel _) (at level 71, left associativity).
Section af_type.
Variable (X : Type).
Implicit Types R S : X -> X -> Prop.
(* this is the informative (or type-bounded) definition of Almost Full relations
given by Thierry Coquand *)
Inductive af_type : (X -> X -> Prop) -> Type :=
| in_af_t0 : forall R, full R -> af_type R
| in_af_t1 : forall R, (forall a, af_type (R rlift a)) -> af_type R.
(* this is the non-informative (or logical or prop-bounded) definition of Almost Full relations
given by Thierry Coquand *)
Inductive af : (X -> X -> Prop) -> Prop :=
| in_af_0 : forall R, full R -> af R
| in_af_1 : forall R, (forall a, af (R rlift a)) -> af R.
(* the computational content of af_type contains a way to compute a bound
on the search space for "good" pairs, and that for any sequence f of
elements of X *)
Fact af_type_inc R S : R inc2 S -> af_type R -> af_type S.
Proof.
intros H1 H2; revert H2 S H1.
induction 1 as [ | R HR IH ]; intros S H1.
constructor 1; auto.
constructor 2; intros x.
apply (IH x).
intros ? ? [|];
[ left | right ]; auto.
Qed.
Fact af_type_inf_chain R : af_type R -> forall f : nat -> X, { n | exists i j, i < j <= n /\ R (f i) (f j) }.
Admitted.
Fact af_inf_chain R : af R -> forall f : nat -> X, exists n i j, i < j <= n /\ R (f i) (f j).
Admitted.
End af_type.
(* the natural order on nat is almost full, a straightforward proof *)
Fact le_af_type : af_type le.
Proof.
constructor 2.
intros n; induction n as [ n IHn ]
using (well_founded_induction_type lt_wf).
constructor 2; intros x.
destruct (le_lt_dec n x) as [ | H ].
constructor 1; do 2 right; assumption.
generalize (IHn _ H).
apply af_type_inc.
intros ? ?; cbv; tauto.
Qed.
(*
And for really non trivial proofs, as of Wed Sep. 23, 2015, I have
finished the purelly intuitionistic proofs of all the following
three theorems, transposing the proof of Wim Veldman in Coq type theory
Notice that Brouwer's thesis is not used in those proofs. In fact,
those proofs require no additional axiom.
Moreover, no hypothesis is made regarding the ground relation.
In particular, it is NOT required that this relation is decidable.
*)
Section Higman_and_Kruskal_results.
(* the following are the informative version's of Higman theorem
and Kruskal's theorem. I have completed the proofs of
higman_btree_af_type, higman_list_af_type, vazsonyi_af_type
and kruskal_tree_af_type *)
Variables (X : Type).
Implicit Types (R : X -> X -> Prop).
(* Higman Theorem is easily proved equivalent to a restriction of the Kruskal
tree theorem to trees of bounded breadth *)
Theorem higman_btree_af_type k R : af_type R -> af_type (emb_tree_product R <# btree k #>).
Admitted.
(* Higman Lemma is the restriction of Higman theorem to trees of breadth 0 or 1
ie lists
However, a direct proof is much shorter than going through Higman Theorem
*)
Corollary higman_list_af_type R : af_type R -> af_type (subword R).
Admitted.
(* Vazsonyi's conjecture is the restriction of the Kruskal tree theorem to
undecorated trees *)
Theorem vazsonyi_af_type : af_type (emb_tree_homeo (fun _ _ : unit => True)).
Admitted.
(* and this is the full Kruskal tree theorem *)
Theorem kruskal_tree_af_type R : af_type R -> af_type (emb_tree_homeo R).
Admitted.
End Higman_and_Kruskal_results.
Section Higman_and_Kruskal_results_prop_bounded.
(* the following are the non-informative version's of Higman theorem
and Kruskal's theorem. I have completed the proofs of
higman_btree_af and higman_list_af and kruskal_tree_af.
vazsonyi_af is a trivial consequence of vazsonyi_af_type
The proof of kruskal_tree_af is now finished as well. I did
find a replacement for the "more-facile" induction principle
using the interesting notion of "being well-founded upto a
projection".
*)
Variables (X : Type).
Implicit Types (R : X -> X -> Prop).
Theorem higman_btree_af k R : af R -> af (emb_tree_product R <# btree k #>).
(* the proof of the non-informative (or logical, or prop-bounded) version
of Higman's theorem is more difficult that the informative version.
But I found a replacement for the lexicographic induction principle
on finite sequences stumps that was used by Wim Veldman.
The replacement concept is "well-founded upto".
*)
Admitted.
Corollary higman_list_af R : af R -> af (subword R).
Admitted.
(* and this is the full Kruskal tree theorem *)
Theorem kruskal_tree_af R : af R -> af (emb_tree_homeo R).
(* the proof of the non-informative (or logical, or prop-bounded) version Kruskal
theorem is now finished as well. Like for Higman's theorem, it is actually more
difficult to prove than the informative version because the outermost induction principle
used in Wim Veldman's proof : more facile well-founded induction on non-trivial
finitary stumps.
The replacement concept is "well-founded upto".
*)
Admitted.
End Higman_and_Kruskal_results_prop_bounded.