(**************************************************************)
(*   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 '<et' y" (at level 70, no associativity).
  Reserved Notation "x '<eh' y" (at level 70, no associativity).

  (* this is the product embedding of Higman theorem, ie each son of
     the root of the lesser tree is less than the corresponding son of
     the root of the greater tree *)
  
  Inductive emb_tree_product : tree -> tree -> Prop :=
    | in_emb_tree_product_0 : forall s t x ll, In t ll -> s <et t -> s <et in_tree x ll
    | in_emb_tree_product_1 : forall x y ll mm, R x y -> Forall2 emb_tree_product ll mm -> in_tree x ll <et in_tree y mm
  where "x <et y" := (emb_tree_product x y).
  
  (* this is the homeomorphic embedding of Kruskal theorem, ie the word composed of
     the sons of the lesser tree is subword-lesser than the word of the sons greater tree *)

  Inductive emb_tree_homeo : tree -> tree -> Prop :=
    | in_emb_tree_homeo_0 : forall s t x ll, In t ll -> s <eh t -> s <eh in_tree x ll
    | in_emb_tree_homeo_1 : forall x y ll mm, R x y -> subword emb_tree_homeo ll mm -> in_tree x ll <eh in_tree y mm
  where "x <eh y" := (emb_tree_homeo x y).

  (* since the product order is included in the subword order, we get the obvious *)

  Fact emb_tree_product_emb_tree_homeo : emb_tree_product inc2 emb_tree_homeo.
  Admitted.
  
End trees.

Definition lift_rel X (R : X -> 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.