Env.v

  Inductive decl: Set :=
    Ax: term -> decl
  | Def: term -> term -> decl.

  Definition typ_of_decl: decl -> term :=
    [d]Cases d of
         (Ax t) => t
       | (Def m t) => t
       end.

  Definition lift_decl := [n:nat][d:decl][k:nat]
    Cases d of
      (Ax t) => (Ax (lift_rec n t k))
    | (Def m t) => (Def (lift_rec n m k) (lift_rec n t k))
    end.

  Definition subst_decl := [a:term][d:decl][k:nat]
    Cases d of
      (Ax t) => (Ax (subst_rec a t k))
    | (Def m t) => (Def (subst_rec a m k) (subst_rec a t k))
    end.

  Definition val_ok: decl -> term ->Prop :=
    [d; t]Cases d of
            (Def t' _) => t=t'
          | _ => True
          end.

  Hints Unfold val_ok : pts.

  Definition env:= (list decl).

(* acces a un terme de l'environnement *)

  Definition item_lift := [t:term][e:env][n:nat]
      (EX u | t=(lift (S n) (typ_of_decl u)) & (item u e n)).

(* insertion dans un environnement *)

  Inductive ins_in_env [g:env; d1:decl]: nat->env->env->Prop :=
     ins_O: (ins_in_env g d1 O g (cons d1 g))
   | ins_S: (n:nat)(e,f:env)(d:decl)(ins_in_env g d1 n e f)
    ->(ins_in_env g d1 (S n) (cons d e) (cons (lift_decl (S O) d n) f)).

  Hints Resolve ins_O ins_S : pts.

  Lemma ins_item_ge: (d':decl)(n:nat)(g,e,f:env)(ins_in_env g d' n e f)
           ->(v:nat)(le n v)->(d:decl)(item d e v)->(item d f (S v)).
Induction 1;Auto with arith pts.
Destruct v;Intros.
Inversion_clear H2.

(Inversion_clear H3;Auto with arith pts).
Save.

  Lemma ins_item_lt: (d':decl)(n:nat)(g,e,f:env)(ins_in_env g d' n e f)
           ->(v:nat)(gt n v) ->(d:decl)(item d e v)
                   ->(item (lift_decl (S O) d (minus n (S v))) f v).
(Induction 1; Auto with arith pts).
Intros.
Inversion_clear H0.

(Destruct v; Simpl; Intros).
(Replace (minus n0 O) with n0; Auto with arith pts).
(Inversion_clear H3; Auto with arith pts).

Inversion_clear H3;Auto with arith pts.
Save.

  Lemma ins_item_lift_lt: (d':decl)(n:nat)(g,e,f:env)(ins_in_env g d' n e f)
           ->(v:nat)(gt n v) ->(t:term)(item_lift t e v)
                      ->(item_lift (lift_rec (S O) t n) f v).
(Destruct 3; Intros).
Exists (lift_decl (S O) x (minus n (S v))).
Rewrite -> H2.
Unfold lift .
Pattern 1 n .
(Replace n with (plus (S v) (minus n (S v))); Auto with arith pts).
(Rewrite <- permute_lift_rec; Auto with arith pts).
(Case x; Simpl; Auto with arith pts).

(Apply ins_item_lt with d' g e; Auto with arith pts).
Save.

(* substitution dans un environnement *)

  Inductive sub_in_env [g:env; d1:decl; t:term]: nat->env->env->Prop :=
     sub_O: (val_ok d1 t)->(sub_in_env g d1 t O (cons d1 g) g)
   | sub_S: (e,f:env)(n:nat)(d:decl)(sub_in_env g d1 t n e f)
         ->(sub_in_env g d1 t (S n) (cons d e) (cons (subst_decl t d n) f)).

  Hints Resolve sub_O sub_S : pts.

  Lemma nth_sub_sup: (t:term)(n:nat)(g,e,f:env)(d':decl)
    (sub_in_env g d' t n e f)
           ->(v:nat)(le n v)->(d:decl)(item d e (S v))->(item d f v).
Induction 1.
Intros.
(Inversion_clear H2; Trivial with arith pts).

(Destruct v; Intros).
Inversion_clear H2.

(Inversion_clear H3; Auto with arith pts).
Save.

  Lemma sub_decl_eq_def: (m,t,T:term)(n:nat)(g,e,f:env)
      (sub_in_env g (Def m T) t n e f)-> t=m.
(Induction 1; Auto with arith pts).
Save.

  Lemma nth_sub_eq: (t:term)(d1:decl)(n:nat)(g,e,f:env)
      (sub_in_env g d1 t n e f)
               ->(d:decl)(item d e n) -> d1=d.
(Induction 1; Intros; Auto with arith pts).
(Inversion_clear H1; Auto with arith pts).

(Inversion_clear H2; Auto with arith pts).
Save.

  Lemma nth_sub_inf: (t:term)(d1:decl)(n:nat)(g,e,f:env)
      (sub_in_env g d1 t n e f)
           ->(v:nat)(gt n v) ->(d:decl)(item d e v)
                   ->(item (subst_decl t d (minus n (S v))) f v).
(Induction 1; Auto with arith pts).
Intros.
Inversion H1.

(Destruct v; Simpl; Intros).
(Replace (minus n0 O) with n0; Auto with arith pts).
(Inversion_clear H3; Auto with arith pts).

(Inversion_clear H3; Auto with arith pts).
Save.

  Lemma nth_sub_item_inf: (t:term)(d1:decl)(n:nat)(g,e,f:env)
         (sub_in_env g d1 t n e f)
           ->(v:nat)(gt n v)
            ->(u:term)(item_lift u e v)->(item_lift (subst_rec t u n) f v).
(Destruct 3; Intros).
Exists (subst_decl t x (minus n (S v))).
Rewrite -> H2.
Unfold lift .
Pattern 1 n .
(Replace n with (plus (S v) (minus n (S v))); Auto with arith pts).
(Elim commut_lift_subst_rec with (typ_of_decl x) t (S v) (minus n (S v)) O;
Auto with arith pts).
(Case x; Simpl; Auto with arith pts).

(Apply nth_sub_inf with 1:=H; Auto with arith pts).
Save.

23/12/98, 14:29