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
subterm: term->term->Prop :=
sbtrm_abs_l: (A,B:term)(subterm A (Abs A B))
| sbtrm_abs_r: (A,B:term)(subterm B (Abs A B))
| sbtrm_app_l: (A,B:term)(subterm A (App A B))
| sbtrm_app_r: (A,B:term)(subterm B (App A B))
| sbtrm_prod_l: (A,B:term)(subterm A (Prod A B))
| sbtrm_prod_r: (A,B:term)(subterm B (Prod A B)).
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 sbtrm_abs_l sbtrm_abs_r sbtrm_app_l sbtrm_app_r
sbtrm_prod_l sbtrm_prod_r.
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
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
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).
(Exists (Abs z B); Auto).
(Exists (Abs A z); Auto).
(Exists (App z B); Auto).
(Exists (App A z); Auto).
(Exists (Prod z B); Auto).
(Exists (Prod A z); 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.
06/11/96, 12:31