Termes.v
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]Cases t of
(Srt s) => (Srt s)
| (Ref i) => (Ref Cases (le_gt_dec k i) of
(left _) => (plus n i)
| (right _) => i
end)
| (Abs a m) => (Abs (lift_rec n a 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][N:term](lift_rec n N O).
Fixpoint
subst_rec [ts:term; t:term]: nat -> term :=
[k]Cases t of
(Srt s) => (Srt s)
| (Ref i) => Cases (lt_eq_lt_dec k i) of
(inleft (left _)) => (Ref (pred i))
| (inleft (right _)) => (lift k ts)
| (inright _) => (Ref i)
end
| (Abs a m) => (Abs (subst_rec ts a k) (subst_rec ts m (S k)))
| (App u v) => (App (subst_rec ts u k) (subst_rec ts v k))
| (Prod a b) => (Prod (subst_rec ts a k) (subst_rec ts b (S k)))
end.
Definition
subst:=[N,M:term](subst_rec N M O).
Theorem
lift_naif: (n:nat)(t:term){ u:term | u=(lift n t) }.
Realizer lift.
Program_all.
Save.
Theorem
subst_naif: (u,v:term){ t:term | t=(subst u v) }.
Realizer subst.
Program_all.
Save.
Lemma
lift_ref_ge: (k,n,p:nat)(le p n)
->(lift_rec k (Ref n) p)=(Ref (plus k n)).
Proof.
(Intros;Simpl).
(Elim (le_gt_dec p n);Auto with arith).
(Intro;Absurd (le p n);Auto with arith).
Save.
Lemma
lift_ref_lt: (k,n,p:nat)(gt p n)
->(lift_rec k (Ref n) p)=(Ref n).
Proof.
(Intros;Simpl).
(Elim (le_gt_dec p n);Auto with arith).
(Intro;Absurd (le p n);Auto with arith).
Save.
Lemma
subst_ref_lt: (u:term)(n,k:nat)(gt k n)
->(subst_rec u (Ref n) k)=(Ref n).
Proof.
Simpl;Intros.
(Elim (lt_eq_lt_dec k n);Intros;Auto with arith).
(Elim y;Intros).
(Absurd (le k n);Auto with arith).
Inversion_clear y0 in H.
(Elim gt_antirefl with n ;Auto with arith).
Save.
Lemma
subst_ref_gt: (u:term)(n,k:nat)(gt n k)
->(subst_rec u (Ref n) k)=(Ref (pred n)).
Proof.
(Simpl;Intros).
(Elim (lt_eq_lt_dec k n);Intros).
(Elim y;Intros;Auto with arith).
Inversion_clear y0 in H.
Elim gt_antirefl with n ;Auto with arith.
Absurd (le k n);Auto with arith.
Save.
Lemma
subst_ref_eq: (u:term)(n:nat)(subst_rec u (Ref n) n)=(lift n u).
Proof.
(Intros;Simpl).
(Elim (lt_eq_lt_dec n n);Intros).
(Elim y;Intros;Auto with arith).
(Elim lt_n_n with n ;Auto with arith).
(Elim gt_antirefl with n ;Auto with arith).
Save.
Lemma
lift_rec0: (M:term)(k:nat)(lift_rec O M k)=M.
Proof.
(Induction M;Simpl;Intros;Auto with arith).
(Elim (le_gt_dec k n);Auto with arith).
(Rewrite -> H;Rewrite -> H0;Auto with arith).
(Rewrite -> H;Rewrite -> H0;Auto with arith).
(Rewrite -> H;Rewrite -> H0;Auto with arith).
Save.
Lemma
lift0: (M:term)(lift O M)=M.
Proof [M:term](lift_rec0 M O).
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).
Proof.
(Induction M; Simpl; Intros; Auto with arith).
(Elim (le_gt_dec k n); Intros).
(Elim (le_gt_dec i (plus n0 n)); Intros).
(Rewrite -> plus_assoc_l; Auto with arith).
(Absurd (le i (plus n0 n)); Auto with arith).
Rewrite -> plus_sym.
(Apply le_trans with (plus k n0); Auto with arith).
(Elim (le_gt_dec i n); Intros; Auto with arith).
(Absurd (le k n); Auto with arith).
(Apply le_trans with i; Auto with arith).
(Rewrite -> H; Auto with arith; Rewrite -> H0; Simpl; Auto with arith).
(Rewrite -> H; Auto with arith; Rewrite -> H0; Simpl; Auto with arith).
(Rewrite -> H; Auto with arith; Rewrite -> H0; Simpl; Auto with arith).
Save.
Lemma
simpl_lift: (M:term)(n:nat)(lift (S n) M)=(lift (S O) (lift n M)).
Proof.
Intros;Unfold lift .
(Rewrite -> simpl_lift_rec;Auto with arith).
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)).
Proof.
Induction M;Intros;Auto with arith.
Unfold 2 4 lift_rec .
Elim (le_gt_dec k n);Elim (le_gt_dec i n);Intros.
(Rewrite -> lift_ref_ge;Auto with arith).
(Rewrite -> lift_ref_ge;Auto with arith).
Elim plus_assoc_r with p n0 n .
Elim plus_assoc_r with n0 p n .
Elim plus_sym with p n0 ;Auto with arith.
Apply le_trans with n ;Auto with arith.
Absurd (le i n);Auto with arith.
Apply le_trans with k ;Auto with arith.
(Rewrite -> lift_ref_ge;Auto with arith).
(Rewrite -> lift_ref_lt;Auto with arith).
(Rewrite -> lift_ref_lt;Auto with arith).
(Rewrite -> lift_ref_lt;Auto with arith).
Apply le_gt_trans with k ;Auto with arith.
Simpl.
(Rewrite -> H;Auto with arith;Rewrite -> H0;Auto with arith).
(Rewrite -> plus_n_Sm;Auto with arith).
Simpl.
Rewrite -> H;Auto with arith;Rewrite -> H0;Auto with arith.
Simpl.
(Rewrite -> H;Auto with arith;Rewrite -> H0;Auto with arith).
(Rewrite -> plus_n_Sm;Auto with arith).
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)).
Proof [M:term][k:nat](permute_lift_rec M (S O) k (S O) O (le_O_n k)).
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).
Proof.
(Induction M; Intros; Auto with arith).
Unfold lift_rec .
(Elim (le_gt_dec k n); Intros).
(Rewrite -> subst_ref_gt; Auto with arith).
(Red; Red).
(Apply le_trans with (S (plus n0 k)); Simpl; Auto with arith).
(Rewrite -> subst_ref_lt; Auto with arith).
(Apply le_gt_trans with k; Auto with arith).
Simpl.
(Rewrite -> H; Auto with arith; Rewrite -> H0; Auto with arith).
(Elim plus_n_Sm with n k; Auto with arith).
Simpl.
(Rewrite -> H; Auto with arith; Rewrite -> H0; Auto with arith).
Simpl.
(Rewrite -> H; Auto with arith; Rewrite -> H0; Auto with arith).
(Elim plus_n_Sm with n k; Auto with arith).
Save.
Lemma
simpl_subst: (N,M:term)(n,p:nat)(le p n)
->(subst_rec N (lift (S n) M) p)=(lift n M).
Proof.
(Intros;Unfold lift ).
(Apply simpl_subst_rec;Auto with arith).
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)).
Proof.
(Induction M;Intros;Auto with arith).
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 with arith).
(Rewrite -> subst_ref_gt;Auto with arith).
Elim plus_n_Sm with n0 n1 ;Auto with arith.
Apply le_trans with p ;Auto with arith.
Induction 1.
Rewrite -> subst_ref_eq.
Unfold lift .
(Rewrite -> simpl_lift_rec;Auto with arith).
(Absurd (le k n);Auto with arith).
(Apply le_trans with p ;Auto with arith).
(Elim y0;Auto with arith).
(Induction 1;Auto with arith).
(Rewrite -> lift_ref_ge;Auto with arith).
(Rewrite -> subst_ref_lt;Auto with arith).
(Rewrite -> lift_ref_lt;Auto with arith).
(Rewrite -> subst_ref_lt;Auto with arith).
Apply le_gt_trans with p ;Auto with arith.
Simpl.
Rewrite -> plus_n_Sm.
(Rewrite -> H;Auto with arith;Rewrite -> H0;Auto with arith).
(Simpl;Rewrite -> H;Auto with arith;Rewrite -> H0;Auto with arith).
(Simpl;Rewrite -> plus_n_Sm).
(Rewrite -> H;Auto with arith;Rewrite -> H0;Auto with arith).
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)).
Proof.
Intros;Unfold lift .
(Rewrite -> commut_lift_subst_rec;Auto with arith).
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).
Proof.
(Induction M;Intros;Auto with arith).
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 with arith).
Elim plus_n_Sm with n0 n1 .
Rewrite -> subst_ref_gt;Auto with arith.
(Red;Red;Apply le_n_S).
Apply le_trans with (plus n0 (plus p k)) ;Auto with arith.
Apply le_trans with (plus p k) ;Auto with arith.
(Rewrite -> lift_ref_lt;Auto with arith).
(Rewrite -> subst_ref_gt;Auto with arith).
Induction 1.
Unfold lift .
(Rewrite <- permute_lift_rec;Auto with arith).
Rewrite -> lift_ref_lt;Auto with arith.
(Rewrite -> subst_ref_eq;Auto with arith).
(Rewrite -> lift_ref_lt;Auto with arith).
(Rewrite -> lift_ref_lt;Auto with arith).
(Rewrite -> subst_ref_lt;Auto with arith).
(Simpl;Replace (S (plus p k)) with (plus (S p) k);Auto with arith).
(Rewrite -> H;Rewrite -> H0;Auto with arith).
(Simpl;Rewrite -> H;Rewrite -> H0;Auto with arith).
Simpl;Replace (S (plus p k)) with (plus (S p) k);Auto with arith.
(Rewrite -> H;Rewrite -> H0;Auto with arith).
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))).
Proof [M,N:term][n:nat](distr_lift_subst_rec M N n O).
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).
Proof.
(Induction M;Auto with arith;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 with arith).
(Rewrite -> subst_ref_gt;Auto with arith).
Apply gt_le_trans with (plus p n0) ;Auto with arith.
Induction 1.
(Rewrite -> subst_ref_eq;Auto with arith).
(Rewrite -> simpl_subst;Auto with arith).
(Rewrite -> subst_ref_lt;Auto with arith).
(Rewrite -> subst_ref_gt;Auto with arith).
Induction 1.
(Rewrite -> subst_ref_lt;Auto with arith).
Rewrite -> subst_ref_eq.
Unfold lift .
(Rewrite -> commut_lift_subst_rec;Auto with arith).
Do 3 (Rewrite -> subst_ref_lt;Auto with arith).
(Simpl;Replace (S (plus p n)) with (plus (S p) n);Auto with arith).
(Rewrite -> H;Auto with arith;Rewrite -> H0;Auto with arith).
(Simpl;Rewrite -> H;Rewrite -> H0;Auto with arith).
Simpl;Replace (S (plus p n)) with (plus (S p) n);Auto with arith.
Rewrite -> H;Rewrite -> H0;Auto with arith.
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))).
Proof [P,N,M:term][k:nat](distr_subst_rec M N P k O).
23/12/98, 14:36