Library Coq.Wellfounded.Lexicographic_Exponentiation

Require Import List.
Require Import Relation_Operators.
Require Import Transitive_Closure.

Section Wf_Lexicographic_Exponentiation.
  Variable A : Set.
  Variable leA : A -> A -> Prop.

  Notation Power := (Pow A leA).
  Notation Lex_Exp := (lex_exp A leA).
  Notation ltl := (Ltl A leA).
  Notation Descl := (Desc A leA).

  Notation List := (list A).
  Notation Nil := (nil (A:=A)).
  Notation Cons := (cons (A:=A)).
  Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).


  Lemma left_prefix : forall x y z:List, ltl (x ++ y) z -> ltl x z.

  Lemma right_prefix :
    forall x y z:List,
      ltl x (y ++ z) -> ltl x y \/ (exists y´ : List, x = y ++ y´ /\ ltl y´ z).

  Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x.

  Lemma desc_tail :
    forall (x:List) (a b:A),
      Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b.

  Lemma dist_aux :
    forall z:List, Descl z -> forall x y:List, z = x ++ y -> Descl x /\ Descl y.

  Lemma dist_Desc_concat :
    forall x y:List, Descl (x ++ y) -> Descl x /\ Descl y.

  Lemma desc_end :
    forall (a b:A) (x:List),
      Descl (x ++ Cons a Nil) /\ ltl (x ++ Cons a Nil) (Cons b Nil) ->
      clos_trans A leA a b.

  Lemma ltl_unit :
    forall (x:List) (a b:A),
      Descl (x ++ Cons a Nil) ->
      ltl (x ++ Cons a Nil) (Cons b Nil) -> ltl x (Cons b Nil).

  Lemma acc_app :
    forall (x1 x2:List) (y1:Descl (x1 ++ x2)),
      Acc Lex_Exp << x1 ++ x2, y1 >> ->
      forall (x:List) (y:Descl x), ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>.

  Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.

End Wf_Lexicographic_Exponentiation.