(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                Lexicographic_Exponentiation.v                            *)
(****************************************************************************)
(*                            Cristina Cornes                               *)
(*                                                                          *)
(*  From : Constructing Recursion Operators in Type Theory                  *)
(*         L. Paulson  JSC (1986) 2, 325-355                                *)
(****************************************************************************)

Require Eqdep.
Require PolyList.
Require PolyListSyntax.
Require Relation_Operators.
Require Transitive_Closure.

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

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

Syntactic Definition List := (list A).
Syntactic Definition Nil := (nil A).
(* useless but symmetric *)
Syntactic Definition Cons := (cons 1!A).

Syntax constr
  level 1:
    List [<<(list A)>>] -> ["List"]
  | Nil  [<<(nil A)>>] -> ["Nil"]
  | Cons [<<(cons 1!A)>>] -> ["Cons"]
  ;
  level 10:
    Cons2 [<<(cons 1!A $e $l)>>] -> ["Cons " $e:L " " $l:L ].

Hints Resolve d_one d_nil  t_step.

Syntax constr level 1:
  pair_sig [<<(exist (list A) Desc $e $d)>>] -> ["<<" $e:L "," $d:L ">>"].


Lemma left_prefix : (x,y,z:List)(ltl x^y z)-> (ltl x z).
Proof.
 Induction x.
 Induction z.
 (Simpl;Intros H).
 Inversion_clear H. 
 (Simpl;Intros;Apply (Lt_nil A leA)).
 Intros a l HInd.
 Simpl.
 Intros.
 Inversion_clear H.
 (Apply (Lt_hd A leA);Auto with sets).
 Apply (Lt_tl A leA).
 (Apply (HInd y y0);Auto with sets).
Qed.


Lemma  right_prefix : 
  (x,y,z:List)(ltl x y^z)-> (ltl x y) \/ (EX y':List | x=(y^y') /\ (ltl y' z)).
Proof.
 (Intros x y;Generalize x ).
 (Elim y;Simpl).
 Right.
 (Exists x0 ;Auto with sets).
 Intros.
 Inversion H0.
 (Left;Apply (Lt_nil A leA)).
 (Left;Apply (Lt_hd A leA);Auto with sets).
 Generalize (H x1 z H3) .
 Induction 1.
 (Left;Apply (Lt_tl A leA);Auto with sets).
 Induction 1.
 (Induction 1;Intros).
 Rewrite -> H8.
 (Right;Exists x2 ;Auto with sets).
Qed.



Lemma desc_prefix: (x:List)(a:A)(Descl x^(Cons a Nil))->(Descl x).
Proof.
 Intros.
 Inversion H.
 Generalize (app_cons_not_nil H1); Induction 1. 
 Cut (x^(Cons a Nil))=(Cons x0 Nil); Auto with sets.
 Intro.
 Generalize (app_eq_unit H0) .
 Induction 1; Induction 1; Intros.
 Rewrite -> H4; Auto with sets.
 Discriminate H5.
 Generalize (app_inj_tail H0) .
 Induction 1; Intros.
 Rewrite <- H4; Auto with sets.
Qed.

Lemma desc_tail: (x:List)(a,b:A)
          (Descl (Cons b (x^(Cons a Nil))))-> (clos_trans A leA a b).
Proof.
 Intro.
 Apply rev_ind with  A:=A
             P:=[x:List](a,b:A)
          (Descl (Cons b (x^(Cons a Nil))))-> (clos_trans A leA a b).
 Intros.

 Inversion  H.
 Cut (Cons b (Cons a Nil))= ((Nil^(Cons b Nil))^ (Cons a Nil)); Auto with sets; Intro.
 Generalize H0.
 Intro.
 Generalize (app_inj_tail 2!(l^(Cons y Nil)) 3!(Nil^(Cons b Nil)) H4);
 Induction 1.
 Intros.

 Generalize (app_inj_tail H6); Induction 1; Intros.
 Generalize H1.
 Rewrite <- H10; Rewrite <- H7; Intro.
 Apply (t_step A leA); Auto with sets.



 Intros.
 Inversion H0.
 Generalize  (app_cons_not_nil H3); Intro.
 Elim H1.

 Generalize H0.
 Generalize (app_comm_cons (l^(Cons x0 Nil)) (Cons a Nil) b); Induction 1.
 Intro.
 Generalize (desc_prefix (Cons b (l^(Cons x0 Nil))) a H5); Intro.
 Generalize (H x0 b H6).
 Intro.
 Apply t_trans with A:=A  y:=x0; Auto with sets.

 Apply  t_step.
 Generalize H1.
 Rewrite -> H4; Intro.

 Generalize (app_inj_tail H8); Induction 1.
 Intros.
 Generalize H2; Generalize (app_comm_cons l (Cons x0 Nil) b).
 Intro.
 Generalize H10.
 Rewrite ->H12; Intro.
 Generalize (app_inj_tail H13); Induction 1.
 Intros.
 Rewrite <- H11; Rewrite <- H16; Auto with sets.
Qed.


Lemma dist_aux : (z:List)(Descl z)->(x,y:List)z=(x^y)->(Descl x)/\ (Descl y).
Proof.
 Intros z D.
 Elim D.
 Intros.
 Cut (x^y)=Nil;Auto with sets; Intro.
 Generalize (app_eq_nil H0) ; Induction 1.
 Intros.
 Rewrite -> H2;Rewrite -> H3; Split;Apply d_nil.

 Intros.
 Cut (x0^y)=(Cons x Nil); Auto with sets.
 Intros E.
 Generalize (app_eq_unit E); Induction 1.
 Induction 1;Intros.
 Rewrite -> H2;Rewrite -> H3; Split.
 Apply d_nil.

 Apply d_one.

 Induction 1; Intros.
 Rewrite -> H2;Rewrite -> H3; Split.
 Apply d_one.

 Apply d_nil.

 Do 5 Intro.
 Intros Hind.
 Do 2 Intro.
 Generalize x0 .
 Apply rev_ind with A:=A 
      P:=[y0:List]
          (x0:List)
          ((l^(Cons y Nil))^(Cons x Nil))=(x0^y0)->(Descl x0)/\(Descl y0).

 Intro.
 Generalize (app_nil_end x1) ; Induction 1; Induction 1.
 Split. Apply d_conc; Auto with sets.

 Apply d_nil.

 Do 3 Intro.
 Generalize x1 .
 Apply rev_ind with 
  A:=A 
  P:=[l0:List]
     (x1:A)
      (x0:List)
       ((l^(Cons y Nil))^(Cons x Nil))=(x0^(l0^(Cons x1 Nil)))
         ->(Descl x0)/\(Descl (l0^(Cons x1 Nil))).


 Simpl.
 Split.
 (Generalize (app_inj_tail H2) ;Induction 1).
 (Induction 1;Auto with sets).

 Apply d_one.
 Do 5 Intro.
 Generalize (app_ass x4 (l1^(Cons x2 Nil)) (Cons x3 Nil)) .
 Induction 1.
 (Generalize (app_ass x4 l1 (Cons x2 Nil)) ;Induction 1).
 Intro E.
 Generalize (app_inj_tail E) .
 (Induction 1;Intros).
 (Generalize (app_inj_tail H6) ;Induction 1;Intros).
 (Rewrite <- H7;  Rewrite <- H10; Generalize H6) .
 (Generalize (app_ass x4 l1 (Cons x2 Nil)) ;Intro E1).
 Rewrite -> E1.
 Intro.
 Generalize (Hind x4 (l1^(Cons x2 Nil))  H11) .
 (Induction 1;Split).
 Auto with sets.

 Generalize H14.
 (Rewrite <- H10; Intro).
 (Apply d_conc;Auto with sets).
Qed.



Lemma dist_Desc_concat : (x,y:List)(Descl x^y)->(Descl x)/\(Descl y).
Proof.
  Intros.
  Apply (dist_aux (x^y) H x y); Auto with sets.
Qed.


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

Proof.
 Intros a b x.
 Case x.
 Simpl.
 Induction 1.
 Intros.
 (Inversion H1;Auto with sets).
 Inversion H3.

 Induction 1.
 Generalize (app_comm_cons l (Cons a Nil) a0).
 (Intros E; Rewrite <- E; Intros).
 Generalize (desc_tail l a a0 H0); Intro.
 Inversion H1.
 (Apply t_trans with y:=a0 ;Auto with sets).

 Inversion H4.
Qed.




Lemma  ltl_unit: (x:List)(a,b:A)
 (Descl (x^(Cons a Nil))) -> (ltl x^(Cons a Nil) (Cons b Nil))
               -> (ltl x (Cons b Nil)).
Proof.
 Intro.
 Case x.
 (Intros;Apply (Lt_nil A leA)).

 (Simpl;Intros).
 Inversion_clear H0.
 (Apply (Lt_hd A leA  a b);Auto with sets).
 
 Inversion_clear H1.
Qed.


Lemma acc_app: 
    (x1,x2:List)(y1:(Descl x1^x2))
     (Acc Power Lex_Exp (exist List Descl (x1^x2)  y1))
     ->(x:List)
        (y:(Descl x))
         (ltl x (x1^x2))->(Acc Power Lex_Exp (exist List Descl x y)).
Proof.
 Intros.
 Apply (Acc_inv Power Lex_Exp (exist List Descl (x1^x2) y1)).
 Auto with sets.

 (Unfold lex_exp ;Simpl;Auto with sets).
Qed.


Theorem wf_lex_exp :
  (well_founded A leA)->(well_founded Power Lex_Exp).
Proof.
 Unfold 2 well_founded .
 (Induction a;Intros).
 Apply Acc_intro.
 Induction y0.
 (Unfold 1 lex_exp ;Simpl).
 Apply rev_ind with A:=A P:=[x:List]
                            (x0:List)
                             (y:(Descl x0))
                              (ltl x0 x)
                               ->(Acc Power Lex_Exp (exist List Descl x0 y)) .
 Intros.
 Inversion_clear H0.

 Intro.
 Generalize (well_founded_ind A (clos_trans A leA) (wf_clos_trans A leA H)).
 Intros GR.
 Apply GR with P:=[x0:A]
                  (l:List)
                   ((x1:List)
                     (y:(Descl x1))
                      (ltl x1 l)
                       ->(Acc Power Lex_Exp (exist List Descl x1 y)))
                    ->(x1:List)
                       (y:(Descl x1))
                        (ltl x1 (l^(Cons x0 Nil)))
                         ->(Acc Power Lex_Exp (exist List Descl x1 y)) .
 (Intro;Intros HInd; Intros).
 Generalize (right_prefix x2 l (Cons x1 Nil) H1) .
 Induction 1.
 Intro; Apply (H0 x2 y1 H3).

 Induction 1.
 (Intro;Induction 1).
 (Clear  H4  H2).
 (Intro;Generalize y1 ;Clear  y1).
 Rewrite -> H2.
 Apply rev_ind with A:=A P:=[x3:List]
                            (y1:(Descl (l^x3)))
                             (ltl x3 (Cons x1 Nil))
                              ->(Acc Power Lex_Exp
                                  (exist List Descl (l^x3) y1)) .
 Intros.
 (Generalize (app_nil_end l) ;Intros Heq).
 Generalize y1 .
 Clear  y1.
 Rewrite <- Heq.
 Intro.
 Apply Acc_intro.
 Induction y2.
 Unfold 1 lex_exp .
 (Simpl;Intros).
 (Apply (H0 x4 y3);Auto with sets).

 Intros. 
 Generalize (dist_Desc_concat l (l0^(Cons x4 Nil)) y1) .
 Induction 1.
 Intros.
 (Generalize (desc_end x4 x1 l0  (conj ? ? H8 H5)) ; Intros).
 Generalize y1 .
 (Rewrite <- (app_ass l l0 (Cons x4 Nil)); Intro).
 (Generalize (HInd x4 H9 (l^l0)) ; Intros HInd2).
 (Generalize (ltl_unit l0 x4 x1 H8 H5); Intro).
 Generalize (dist_Desc_concat (l^l0) (Cons x4 Nil) y2) .
 (Induction 1;Intros).
 (Generalize (H4 H12 H10) ;Intro).
 Generalize (Acc_inv Power Lex_Exp (exist List Descl (l^l0) H12) H14) .
 Generalize (acc_app l l0 H12 H14).
 Intros f g.
 (Generalize (HInd2 f);Intro).
 Apply Acc_intro.
 Induction y3.
 (Unfold 1 lex_exp ;Simpl; Intros).
 (Apply H15;Auto with sets).
Qed.


End Wf_Lexicographic_Exponentiation.


(* $Id: Lexicographic_Exponentiation.v,v 1.13 1999/06/29 07:48:56 loiseleu Exp $ *)
