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