Termes.v

Require Export Arith.
Require Export Compare_dec.
Require Export Relations.

Section Termes.

  Inductive Set sort:=
     kind: sort
   | prop: sort.

  Inductive Set term:=
      Srt: sort->term
    | Ref: nat->term
    | Abs: term->term->term
    | App: term->term->term
    | Prod: term->term->term.

  Fixpoint lift_rec [n:nat;t:term]: nat->term :=
     [k:nat]Cases t of
         (Srt s) => (Srt s)
       | (Ref i) => Case (le_gt_dec k i) of
                      [_:(le k i)](Ref (plus n i))
                      [_:(gt k i)](Ref i)
                    end
       | (Abs T M) => (Abs (lift_rec n T k) (lift_rec n M (S k)))
       | (App u v) => (App (lift_rec n u k) (lift_rec n v k))
       | (Prod A B) => (Prod (lift_rec n A k) (lift_rec n B (S k)))
       end.

  Definition lift:=[n:nat][t:term](lift_rec n t O).

  Fixpoint subst_rec [N,M:term]: nat->term :=
    [k:nat]Cases M of
         (Srt s) => (Srt s)
       | (Ref i) => Case (lt_eq_lt_dec k i) of
                      [C:{(lt k i)}+{k=i}]
                        Case C of
                          [_:(gt i k)](Ref (pred i))
                          [_:k=i](lift k N)
                        end
                      [_:(lt i k)](Ref i)
                    end
       | (Abs A B) => (Abs (subst_rec N A k) (subst_rec N B (S k)))
       | (App u v) => (App (subst_rec N u k) (subst_rec N v k))
       | (Prod T U) => (Prod (subst_rec N T k) (subst_rec N U (S k)))
       end.

  Definition subst:=[N,M:term](subst_rec N M O).

  Inductive free_db: nat->term->Prop :=
    db_srt: (n:nat)(s:sort)(free_db n (Srt s))
  | db_ref: (k,n:nat)(gt k n) -> (free_db k (Ref n))
  | db_abs: (k:nat)(A,M:term)(free_db k A) -> (free_db (S k) M)
                 -> (free_db k (Abs A M))
  | db_app: (k:nat)(u,v:term)(free_db k u) -> (free_db k v)
                 -> (free_db k (App u v))
  | db_prod: (k:nat)(A,B:term)(free_db k A) -> (free_db (S k) B)
                 -> (free_db k (Prod A B)).

  Inductive subt_bind [T,M:term]: term -> Prop :=
    Bsbt_abs: (subt_bind T M (Abs T M))
  | Bsbt_prod: (subt_bind T M (Prod T M)).

  Inductive subt_nobind [m:term]: term -> Prop :=
    Nbsbt_abs: (n:term)(subt_nobind m (Abs m n))
  | Nbsbt_app_l: (v:term)(subt_nobind m (App m v))
  | Nbsbt_app_r: (u:term)(subt_nobind m (App u m))
  | Nbsbt_prod: (n:term)(subt_nobind m (Prod m n)).

  Inductive subterm [m,n:term]: Prop :=
    Sbtrm_bind: (t:term)(subt_bind t m n)->(subterm m n)
  | Sbtrm_nobind: (subt_nobind m n)->(subterm m n).

(*   Definition mem_sort := [s:sort][t:term](clos_refl_trans ? subterm (Srt s) t). *)

  Inductive mem_sort [s:sort]: term->Prop :=
     mem_eq: (mem_sort s (Srt s))
   | mem_prod_l: (u,v:term)(mem_sort s u)->(mem_sort s (Prod u v))
   | mem_prod_r: (u,v:term)(mem_sort s v)->(mem_sort s (Prod u v))
   | mem_abs_l: (u,v:term)(mem_sort s u)->(mem_sort s (Abs u v))
   | mem_abs_r: (u,v:term)(mem_sort s v)->(mem_sort s (Abs u v))
   | mem_app_l: (u,v:term)(mem_sort s u)->(mem_sort s (App u v))
   | mem_app_r: (u,v:term)(mem_sort s v)->(mem_sort s (App u v)).

End Termes.

  Hint db_srt db_ref db_abs db_app db_prod.
  Hint Bsbt_abs Bsbt_prod Nbsbt_abs Nbsbt_app_l Nbsbt_app_r Nbsbt_prod.
  Hint Sbtrm_nobind.

(*   Hint Unfold mem_sort. *)
  Hint mem_eq mem_prod_l mem_prod_r mem_abs_l mem_abs_r mem_app_l mem_app_r.

Section Beta_Reduction.

  Inductive red1: term->term->Prop :=
    beta: (M,N,T:term)(red1 (App (Abs T M) N) (subst N M))
  | abs_red_l: (M,M':term)(red1 M M') -> (N:term)(red1 (Abs M N) (Abs M' N))
  | abs_red_r: (M,M':term)(red1 M M') -> (N:term)(red1 (Abs N M) (Abs N M'))
  | app_red_l:(M1,N1:term)(red1 M1 N1)
                 ->(M2:term)(red1 (App M1 M2)(App N1 M2))
  | app_red_r:(M2,N2:term)(red1 M2 N2)
                 ->(M1:term)(red1 (App M1 M2)(App M1 N2))
  | prod_red_l:(M1,N1:term)(red1 M1 N1)
                 ->(M2:term)(red1 (Prod M1 M2)(Prod N1 M2))
  | prod_red_r:(M2,N2:term)(red1 M2 N2)
                 ->(M1:term)(red1 (Prod M1 M2)(Prod M1 N2)).

  Inductive red [M:term]: term->Prop :=
    refl_red: (red M M)
  | trans_red: (P,N:term)(red M P)->(red1 P N)->(red M N).

  Inductive conv [M:term]: term->Prop :=
    refl_conv: (conv M M)
  | trans_conv_red: (P,N:term)(conv M P)->(red1 P N)->(conv M N)
  | trans_conv_exp: (P,N:term)(conv M P)->(red1 N P)->(conv M N).

  Inductive par_red1 : term -> term -> Prop :=
    par_beta : (M,M':term)(par_red1 M M') -> (N,N':term)(par_red1 N N')
                      ->(T:term)(par_red1 (App (Abs T M) N) (subst N' M'))
  | sort_par_red: (s:sort)(par_red1 (Srt s) (Srt s))
  | ref_par_red : (n:nat)(par_red1 (Ref n) (Ref n))
  | abs_par_red : (M,M':term)(par_red1 M M') ->(T,T':term)(par_red1 T T')
                  -> (par_red1 (Abs T M) (Abs T' M'))
  | app_par_red : (M,M':term)(par_red1 M M') -> (N,N':term)(par_red1 N N') ->
                              (par_red1 (App M N) (App M' N'))
  | prod_par_red : (M,M':term)(par_red1 M M') -> (N,N':term)(par_red1 N N') ->
                              (par_red1 (Prod M N) (Prod M' N')).

  Definition par_red := (clos_trans term par_red1).

End Beta_Reduction.

  Hint beta abs_red_l abs_red_r app_red_l app_red_r prod_red_l prod_red_r.
  Hint refl_red refl_conv.
  Hint par_beta sort_par_red ref_par_red abs_par_red app_par_red prod_par_red.

  Hint Unfold par_red.

Section Normalisation_Forte.

  Definition normal: term->Prop :=
    [t:term](u:term)~(red1 t u).

  Definition sn: term->Prop := (Acc ? (transp ? red1)).

End Normalisation_Forte.

  Hint Unfold sn.

  Lemma lift_ref_ge: (k,n,p:nat)(le p n)
            ->(lift_rec k (Ref n) p)=(Ref (plus k n)).
(Intros;Simpl).
(Elim (le_gt_dec p n);Auto).
(Intro;Absurd (le p n);Auto).
Save.

  Lemma lift_ref_lt: (k,n,p:nat)(gt p n)
            ->(lift_rec k (Ref n) p)=(Ref n).
(Intros;Simpl).
(Elim (le_gt_dec p n);Auto).
(Intro;Absurd (le p n);Auto).
Save.

  Lemma subst_ref_lt: (u:term)(n,k:nat)(gt k n)
            ->(subst_rec u (Ref n) k)=(Ref n).
Simpl;Intros.
(Elim (lt_eq_lt_dec k n);Intros;Auto).
(Elim y;Intros).
(Absurd (le k n);Auto).

Inversion_clear y0 in H.
(Elim gt_antirefl with n ;Auto).
Save.

  Lemma subst_ref_gt: (u:term)(n,k:nat)(gt n k)
            ->(subst_rec u (Ref n) k)=(Ref (pred n)).
(Simpl;Intros).
(Elim (lt_eq_lt_dec k n);Intros).
(Elim y;Intros;Auto).
Inversion_clear y0 in H.
Elim gt_antirefl with n ;Auto.

Absurd (le k n);Auto.
Save.

  Lemma subst_ref_eq: (u:term)(n:nat)(subst_rec u (Ref n) n)=(lift n u).
(Intros;Simpl).
(Elim (lt_eq_lt_dec n n);Intros).
(Elim y;Intros;Auto).
(Elim lt_n_n with n ;Auto).

(Elim gt_antirefl with n ;Auto).
Save.

  Lemma lift_rec0: (M:term)(k:nat)(lift_rec O M k)=M.
(Induction M;Simpl;Intros;Auto).
(Elim (le_gt_dec k n);Auto).

(Rewrite -> H;Rewrite -> H0;Auto).

(Rewrite -> H;Rewrite -> H0;Auto).

(Rewrite -> H;Rewrite -> H0;Auto).
Save.

  Lemma lift0: (M:term)(lift O M)=M.
(Intros;Unfold lift ).
(Apply lift_rec0;Auto).
Save.

  Lemma simpl_lift_rec: (M:term)(n,k,p,i:nat)(le i (plus k n))->(le k i)
          ->(lift_rec p (lift_rec n M k) i)
              =(lift_rec (plus p n) M k).
(Induction M;Simpl;Intros;Auto).
(Elim (le_gt_dec k n);Intros).
(Rewrite -> lift_ref_ge;Auto).
(Rewrite -> plus_assoc_l;Auto).

Rewrite -> plus_sym.
(Apply le_trans with (plus k n0) ;Auto).

(Rewrite -> lift_ref_lt;Auto).
(Apply le_gt_trans with k ;Auto).

Rewrite -> H;Auto;Rewrite -> H0;Simpl;Auto.

Rewrite -> H;Auto;Rewrite -> H0;Simpl;Auto.

Rewrite -> H;Auto;Rewrite -> H0;Simpl;Auto.
Save.

  Lemma simpl_lift: (M:term)(n:nat)(lift (S n) M)=(lift (S O) (lift n M)).
Intros;Unfold lift .
(Rewrite -> simpl_lift_rec;Auto).
Save.

  Lemma permute_lift_rec: (M:term)(n,k,p,i:nat)(le i k)
       ->(lift_rec p (lift_rec n M k) i)
           =(lift_rec n (lift_rec p M i) (plus p k)).
Induction M;Simpl;Intros;Auto.
Elim (le_gt_dec k n);Elim (le_gt_dec i n);Intros.
(Rewrite -> lift_ref_ge;Auto).
(Rewrite -> lift_ref_ge;Auto).
Elim plus_assoc_r with p n0 n .
Elim plus_assoc_r with n0 p n .
Elim plus_sym with p n0 ;Auto.

Apply le_trans with n ;Auto.

Absurd (le i n);Auto.
Apply le_trans with k ;Auto.

(Rewrite -> lift_ref_ge;Auto).
(Rewrite -> lift_ref_lt;Auto).

(Rewrite -> lift_ref_lt;Auto).
(Rewrite -> lift_ref_lt;Auto).
Apply le_gt_trans with k ;Auto.

(Rewrite -> H;Auto;Rewrite -> H0;Auto).
(Rewrite -> plus_n_Sm;Auto).

Rewrite -> H;Auto;Rewrite -> H0;Auto.

(Rewrite -> H;Auto;Rewrite -> H0;Auto).
(Rewrite -> plus_n_Sm;Auto).
Save.

  Lemma permute_lift: (M:term)(k:nat)
      (lift (S O) (lift_rec (S O) M k))=(lift_rec (S O) (lift (S O) M) (S k)).
Intros.
Change (eq ? (lift_rec (S O) (lift_rec (S O) M k) O)
         (lift_rec (S O) (lift_rec (S O) M O) (plus (S O) k))).
(Apply permute_lift_rec;Auto).
Save.

  Lemma simpl_subst_rec: (N,M:term)(n,p,k:nat)(le p (plus n k))->(le k p)
          ->(subst_rec N (lift_rec (S n) M k) p)=(lift_rec n M k).
(Induction M;Simpl;Intros;Auto).
(Elim (le_gt_dec k n);Intros).
Rewrite -> subst_ref_gt;Auto.
Red;Red.
(Apply le_trans with (S (plus n0 k)) ;Auto).

(Rewrite -> subst_ref_lt;Auto).
Apply le_gt_trans with k ;Auto.

(Rewrite -> H;Auto;Rewrite -> H0;Auto).
Elim plus_n_Sm with n k ;Auto.

Rewrite -> H;Auto;Rewrite -> H0;Auto.

Rewrite -> H;Auto;Rewrite -> H0;Auto.
(Elim plus_n_Sm with n k ;Auto).
Save.

  Lemma simpl_subst: (N,M:term)(n,p:nat)(le p n)
                 ->(subst_rec N (lift (S n) M) p)=(lift n M).
(Intros;Unfold lift ).
(Apply simpl_subst_rec;Auto).
Save.

  Lemma commut_lift_subst_rec: (M,N:term)(n,p,k:nat)(le k p)
            ->(lift_rec n (subst_rec N M p) k)
               =(subst_rec N (lift_rec n M k) (plus n p)).
(Induction M;Intros;Auto).
Unfold 1 subst_rec 2 lift_rec .
(Elim (lt_eq_lt_dec p n);Elim (le_gt_dec k n);Intros).
Elim y0.
(Case n;Intros).
Inversion_clear y1.

Unfold pred .
(Rewrite -> lift_ref_ge;Auto).
(Rewrite -> subst_ref_gt;Auto).
Elim plus_n_Sm with n0 n1 .
Auto.

Apply le_trans with p ;Auto.

Induction 1.
Rewrite -> subst_ref_eq.
Unfold lift .
(Rewrite -> simpl_lift_rec;Auto).

(Absurd (le k n);Auto).
(Apply le_trans with p ;Auto).
(Elim y0;Auto).
(Induction 1;Auto).

(Rewrite -> lift_ref_ge;Auto).
(Rewrite -> subst_ref_lt;Auto).

(Rewrite -> lift_ref_lt;Auto).
(Rewrite -> subst_ref_lt;Auto).
Apply le_gt_trans with p ;Auto.

Simpl.
Rewrite -> plus_n_Sm.
(Rewrite -> H;Auto;Rewrite -> H0;Auto).

(Simpl;Rewrite -> H;Auto;Rewrite -> H0;Auto).

(Simpl;Rewrite -> plus_n_Sm).
(Rewrite -> H;Auto;Rewrite -> H0;Auto).
Save.

  Lemma commut_lift_subst: (M,N:term)(k:nat)
    (subst_rec N (lift (S O) M) (S k))=(lift (S O) (subst_rec N M k)).
Intros;Unfold lift .
(Rewrite -> commut_lift_subst_rec;Auto).
Save.

  Lemma distr_lift_subst_rec: (M,N:term)(n,p,k:nat)
             (lift_rec n (subst_rec N M p) (plus p k))
                =(subst_rec (lift_rec n N k) (lift_rec n M (S (plus p k))) p).
(Induction M;Intros;Auto).
Unfold 1 subst_rec .
Elim (lt_eq_lt_dec p n);Intro.
Elim y.
(Case n;Intros).
Inversion_clear y0.

Unfold pred 1 lift_rec .
Elim (le_gt_dec (plus p k) n1);Intro.
(Rewrite -> lift_ref_ge;Auto).
Elim plus_n_Sm with n0 n1 .
Rewrite -> subst_ref_gt;Auto.
(Red;Red;Apply le_n_S).
Apply le_trans with (plus n0 (plus p k)) ;Auto.
Apply le_trans with (plus p k) ;Auto.

(Rewrite -> lift_ref_lt;Auto).
(Rewrite -> subst_ref_gt;Auto).

Induction 1.
Unfold lift .
(Rewrite <- permute_lift_rec;Auto).
Rewrite -> lift_ref_lt;Auto.
(Rewrite -> subst_ref_eq;Auto).

(Rewrite -> lift_ref_lt;Auto).
(Rewrite -> lift_ref_lt;Auto).
(Rewrite -> subst_ref_lt;Auto).

(Simpl;Replace (S (plus p k)) with (plus (S p) k);Auto).
(Rewrite -> H;Rewrite -> H0;Auto).

(Simpl;Rewrite -> H;Rewrite -> H0;Auto).

Simpl;Replace (S (plus p k)) with (plus (S p) k);Auto.
(Rewrite -> H;Rewrite -> H0;Auto).
Save.

  Lemma distr_lift_subst: (M,N:term)(n,k:nat)
             (lift_rec n (subst N M) k)
                =(subst (lift_rec n N k) (lift_rec n M (S k))).
(Intros;Unfold subst ).
Pattern 1 3 k .
(Replace k with (plus O k);Auto).
Apply distr_lift_subst_rec.
Save.

  Lemma distr_subst_rec: (M,N,P:term)(n,p:nat)
      (subst_rec P (subst_rec N M p) (plus p n))
      = (subst_rec (subst_rec P N n) (subst_rec P M (S (plus p n))) p).
(Induction M;Auto;Intros).
Unfold 2 subst_rec .
Elim (lt_eq_lt_dec p n);Intro.
Elim y.
Case n;Intros.
Inversion_clear y0.

Unfold pred 1 subst_rec .
Elim (lt_eq_lt_dec (plus p n0) n1);Intro.
Elim y1.
Case n1;Intros.
Inversion_clear y2.

(Rewrite -> subst_ref_gt;Auto).
(Rewrite -> subst_ref_gt;Auto).
Apply gt_le_trans with (plus p n0) ;Auto.

Induction 1.
(Rewrite -> subst_ref_eq;Auto).
(Rewrite -> simpl_subst;Auto).

(Rewrite -> subst_ref_lt;Auto).
(Rewrite -> subst_ref_gt;Auto).

Induction 1.
(Rewrite -> subst_ref_lt;Auto).
Rewrite -> subst_ref_eq.
Unfold lift .
(Rewrite -> commut_lift_subst_rec;Auto).

Do 3 (Rewrite -> subst_ref_lt;Auto).

(Simpl;Replace (S (plus p n)) with (plus (S p) n);Auto).
(Rewrite -> H;Auto;Rewrite -> H0;Auto).

(Simpl;Rewrite -> H;Rewrite -> H0;Auto).

Simpl;Replace (S (plus p n)) with (plus (S p) n);Auto.
Rewrite -> H;Rewrite -> H0;Auto.
Save.

  Lemma distr_subst: (P,N,M:term)(k:nat)
             (subst_rec P (subst N M) k)
                =(subst (subst_rec P N k) (subst_rec P M (S k))).
(Intros;Unfold subst ).
Pattern 1 3 k .
(Replace k with (plus O k);Auto).
Apply distr_subst_rec.
Save.

  Lemma one_step_red: (M,N:term)(red1 M N)->(red M N).
Intros.
(Apply trans_red with M ;Auto).
Save.

  Hint one_step_red.

  Lemma red1_red_ind: (N:term)(P:term->Prop)(P N)
                         ->((M,R:term)(red1 M R)->(red R N)->(P R)->(P M))
                          ->(M:term)(red M N)->(P M).
Cut (M,N:term)
     (red M N)
      ->(P:term->Prop)
         (P N)->((M,R:term)(red1 M R)->(red R N)->(P R)->(P M))->(P M).
Intros.
Apply (H M N);Auto.

Induction 1;Intros;Auto.
Apply H1;Auto.
Apply H4 with N0 ;Auto.

Intros.
Apply H4 with R ;Auto.
Apply trans_red with P ;Auto.
Save.

  Lemma trans_red_red: (M,N,P:term)(red M N)->(red N P)->(red M P).
Intros.
Generalize H0 M H .
(Induction 1;Auto).
Intros.
Apply trans_red with P0 ;Auto.
Save.

  Lemma red_red_app: (u,u0,v,v0:term)(red u u0)->(red v v0)
                   ->(red (App u v)(App u0 v0)).
Induction 1.
(Induction 1;Intros;Auto).
(Apply trans_red with (App u P) ;Auto).

Intros.
Apply trans_red with (App P v0) ;Auto.
Save.

  Lemma red_red_abs: (u,u0,v,v0:term)(red u u0)->(red v v0)
                   ->(red (Abs u v)(Abs u0 v0)).
Induction 1.
Induction 1;Intros;Auto.
Apply trans_red with (Abs u P) ;Auto.

Intros.
Apply trans_red with (Abs P v0) ;Auto.
Save.

  Lemma red_red_prod: (u,u0,v,v0:term)(red u u0)->(red v v0)
                    ->(red (Prod u v)(Prod u0 v0)).
Induction 1.
(Induction 1;Intros;Auto).
(Apply trans_red with (Prod u P) ;Auto).

Intros.
(Apply trans_red with (Prod P v0) ;Auto).
Save.

  Hint red_red_app red_red_abs red_red_prod.

  Lemma red1_lift: (u,v:term)(red1 u v)
               ->(n,k:nat)(red1 (lift_rec n u k) (lift_rec n v k)).
Induction 1;Simpl;Intros;Auto.
(Rewrite -> distr_lift_subst;Auto).
Save.

  Hint red1_lift.

  Lemma red1_subst_r: (t,u:term)(red1 t u)->(a:term)(k:nat)
                      (red1 (subst_rec a t k) (subst_rec a u k)).
Induction 1;Simpl;Intros;Auto.
Rewrite -> distr_subst;Auto.
Save.

  Lemma red1_subst_l: (a,t,u:term)(k:nat)(red1 t u)->
                        (red (subst_rec t a k) (subst_rec u a k)).
(Induction a;Simpl;Auto).
Intros.
(Elim (lt_eq_lt_dec k n);Intros;Auto).
(Elim y;Auto).
(Unfold lift ;Auto).
Save.

  Hint red1_subst_l red1_subst_r.

  Lemma red_prod_prod: (u,v,t:term)(red (Prod u v) t)
                 ->(P:Prop)((a,b:term)t=(Prod a b)->(red u a)->(red v b)->P)
                        ->P.
Induction 1;Intros.
Apply H0 with u v ;Auto.

Apply H1;Intros.
Inversion_clear H4 in H2.
Inversion H2.
(Apply H3 with N1 b ;Auto).
(Apply trans_red with a ;Auto).

(Apply H3 with a N2 ;Auto).
(Apply trans_red with b ;Auto).
Save.

  Lemma red_sort_sort: (s:sort)(t:term)(red (Srt s) t)->~t=(Srt s)->False.
(Induction 1; Intros; Auto).
Apply H1.
Generalize H2 .
(Case P; Intros; Try Discriminate).
Inversion_clear H4.
Save.

  Lemma one_step_conv_exp: (M,N:term)(red1 M N)->(conv N M).
Intros.
(Apply trans_conv_exp with N ;Auto).
Save.

  Lemma red_conv: (M,N:term)(red M N)->(conv M N).
(Induction 1;Auto).
Intros;Apply trans_conv_red with P ;Auto.
Save.

  Hint one_step_conv_exp red_conv.

  Lemma sym_conv: (M,N:term)(conv M N)->(conv N M).
(Induction 1;Auto).
Induction 2;Intros;Auto.
Apply trans_conv_red with P0 ;Auto.

Apply trans_conv_exp with P0 ;Auto.

Induction 2;Intros;Auto.
Apply trans_conv_red with P0 ;Auto.

Apply trans_conv_exp with P0 ;Auto.
Save.

  Immediate sym_conv.

  Lemma trans_conv_conv: (M,N,P:term)(conv M N)->(conv N P)->(conv M P).
Intros.
Generalize M H ;Elim H0;Intros;Auto.
(Apply trans_conv_red with P0 ;Auto).

(Apply trans_conv_exp with P0 ;Auto).
Save.

  Lemma conv_conv_prod: (a,b,c,d:term)(conv a b)->(conv c d)
                             ->(conv (Prod a c)(Prod b d)).
Intros.
Apply trans_conv_conv with (Prod a d) .
Elim H0;Intros;Auto.
(Apply trans_conv_red with (Prod a P) ;Auto).

(Apply trans_conv_exp with (Prod a P) ;Auto).

(Elim H;Intros;Auto).
(Apply trans_conv_red with (Prod P d) ;Auto).

(Apply trans_conv_exp with (Prod P d) ;Auto).
Save.

  Lemma conv_conv_lift: (a,b:term)(n,k:nat)(conv a b)
                           ->(conv (lift_rec n a k) (lift_rec n b k)).
Intros.
Elim H;Intros;Auto.
(Apply trans_conv_red with (lift_rec n P k) ;Auto).

(Apply trans_conv_exp with (lift_rec n P k) ;Auto).
Save.

  Lemma conv_conv_subst: (a,b,c,d:term)(k:nat)(conv a b)->(conv c d)
                           ->(conv (subst_rec a c k)(subst_rec b d k)).
Intros.
Apply trans_conv_conv with (subst_rec a d k) .
Elim H0;Intros;Auto.
(Apply trans_conv_red with (subst_rec a P k) ;Auto).

(Apply trans_conv_exp with (subst_rec a P k) ;Auto).

Elim H;Intros;Auto.
(Apply trans_conv_conv with (subst_rec P d k) ;Auto).

(Apply trans_conv_conv with (subst_rec P d k) ;Auto).
(Apply sym_conv;Auto).
Save.

  Hint conv_conv_prod conv_conv_lift conv_conv_subst.

  Lemma refl_par_red1 : (M:term)(par_red1 M M).
Induction M; Auto.
Save.

  Hint refl_par_red1.

  Lemma red1_par_red1 : (M,N:term)(red1 M N) -> (par_red1 M N).
(Induction 1;Auto;Intros).
Save.

  Hint red1_par_red1.

  Lemma red_par_red : (M,N:term)(red M N) -> (par_red M N).
Red;Induction 1;Intros;Auto.
Apply t_trans with P ;Auto.
Save.

  Lemma par_red_red : (M,N:term) (par_red M N) -> (red M N).
Induction 1.
Induction 1;Intros;Auto.
Apply trans_red with (App (Abs T M') N') ;Auto.

Intros.
(Apply trans_red_red with y ;Auto).
Save.

  Hint red_par_red par_red_red.

  Lemma par_red1_lift: (n:nat)(a,b:term)(par_red1 a b)
          ->(k:nat)(par_red1 (lift_rec n a k) (lift_rec n b k)).
Induction 1;Simpl;Auto.
Intros.
(Rewrite -> distr_lift_subst;Auto).
Save.

  Lemma par_red1_subst: (c,d:term)(par_red1 c d)
         ->(a,b:term)(par_red1 a b)
          ->(k:nat)(par_red1 (subst_rec a c k) (subst_rec b d k)).
Induction 1;Simpl;Auto;Intros.
(Rewrite distr_subst;Auto).

(Elim (lt_eq_lt_dec k n);Auto;Intros).
(Elim y;Intros;Auto).
Unfold lift .
(Apply par_red1_lift;Auto).
Save.

  Lemma inv_par_red_abs: (P:Prop)(T,U,x:term)(par_red1 (Abs T U) x)
          ->((T',U':term)(x=(Abs T' U'))->(par_red1 U U')->P)->P.
Do 5 Intro.
(Inversion_clear H;Intros).
(Apply H with T' M' ;Auto).
Save.

  Hint par_red1_lift par_red1_subst.

  Lemma subterm_abs: (t,m:term)(subterm m (Abs t m)).
Intros.
(Apply Sbtrm_bind with t; Auto).
Save.

  Lemma subterm_prod: (t,m:term)(subterm m (Prod t m)).
Intros.
(Apply Sbtrm_bind with t; Auto).
Save.

  Hint subterm_abs subterm_prod.

(*   Lemma mem_sort_ref: (s:sort)(n:nat)~(mem_sort s (Ref n)). (Red; Intros). Cut (b:term)(mem_sort s b)->b=(Ref n)->False. Intros. (Apply H0 with (Ref n); Auto). Do 2 Intro. (Elim H0 using clos_refl_trans_ind_left; Intros; Auto). Discriminate H1. Rewrite H4 in H3. (Inversion_clear H3; Inversion_clear H5). Save. *)

  Lemma mem_sort_lift: (t:term)(n,k:nat)(s:sort)
         (mem_sort s (lift_rec n t k))->(mem_sort s t).
(Induction t;Simpl;Intros;Auto).
(Generalize H ;Elim (le_gt_dec k n);Intros;Auto).
Inversion_clear H0.

Inversion_clear H1.
Apply mem_abs_l;Apply H with n k ;Auto.

Apply mem_abs_r;Apply H0 with n (S k) ;Auto.

Inversion_clear H1.
(Apply mem_app_l;Apply H with n k ;Auto).

(Apply mem_app_r;Apply H0 with n k ;Auto).

Inversion_clear H1.
Apply mem_prod_l;Apply H with n k ;Auto.

Apply mem_prod_r;Apply H0 with n (S k) ;Auto.
Save.

  Lemma mem_sort_subst: (b,a:term)(n:nat)(s:sort)(mem_sort s (subst_rec a b n))
                         ->(mem_sort s a)\/(mem_sort s b).
Induction b;Simpl;Intros;Auto.
(Generalize H ;Elim (lt_eq_lt_dec n0 n);Intro).
(Elim y;Intros).
Inversion_clear H0.

Left.
Apply mem_sort_lift with n0 O ;Auto.

Intros.
Inversion_clear H0.

Inversion_clear H1.
Elim H with a n s ;Auto.

Elim H0 with a (S n) s ;Auto.

Inversion_clear H1.
(Elim H with a n s ;Auto).

(Elim H0 with a n s ;Auto).

Inversion_clear H1.
Elim H with a n s ;Auto.

Elim H0 with a (S n) s ;Intros;Auto.
Save.

  Lemma red_sort_mem: (t:term)(s:sort)(red t (Srt s))->(mem_sort s t).
Intros.
Pattern t .
Apply red1_red_ind with (Srt s) ;Auto.
Do 4 Intro.
Elim H0;Intros.
(Elim mem_sort_subst with M0 N O s ;Intros;Auto).

(Inversion_clear H4;Auto).

(Inversion_clear H4;Auto).

(Inversion_clear H4;Auto).

(Inversion_clear H4;Auto).

(Inversion_clear H4;Auto).

(Inversion_clear H4;Auto).
Save.

  Lemma red_normal: (u,v:term)(red u v)->(normal u)->(u=v).
(Induction 1;Auto;Intros).
Absurd (red1 u N);Auto.
Absurd (red1 P N);Auto.
Elim (H1 H3).
Unfold not ;Intro;Apply (H3 N);Auto.
Save.

  Lemma sn_red_sn: (a,b:term)(sn a)->(red a b)->(sn b).
Unfold sn .
(Induction 2; Intros; Auto).
(Apply Acc_inv with P; Auto).
Save.

  Lemma commut_red1_subterm: (commut ? subterm (transp ? red1)).
Red.
(Induction 1; Intros).
Inversion_clear H0.
(Exists (Abs t z); Auto).

(Exists (Prod t z); Auto).

Inversion_clear H0.
(Exists (Abs z n); Auto).

(Exists (App z v); Auto).

(Exists (App u z); Auto).

(Exists (Prod z n); Auto).
Save.

  Lemma subterm_sn: (a:term)(sn a)->(b:term)(subterm b a)->(sn b).
Unfold sn .
(Induction 1; Intros).
(Apply Acc_intro; Intros).
(Elim commut_red1_subterm with x b y; Intros; Auto).
(Apply H1 with x0; Auto).
Save.

  Lemma sn_prod: (A:term)(sn A)->(B:term)(sn B)->(sn (Prod A B)).
Unfold sn.
Induction 1.
Induction 3;Intros.
Apply Acc_intro;Intros.
Inversion_clear H5;Auto.
(Apply H1;Auto).
(Apply Acc_intro;Auto).
Save.

  Lemma sn_subst: (T,M:term)(sn (subst T M))->(sn M).
Intros.
Cut (t:term)(sn t)->(m:term)t=(subst T m)->(sn m).
Intros.
(Apply H0 with (subst T M); Auto).

Unfold sn.
(Induction 1; Intros).
(Apply Acc_intro; Intros).
(Apply H2 with (subst T y); Auto).
Rewrite -> H3.
Unfold subst;Auto.
Save.

07/03/97, 14:35