Class.v

Require Termes.
Require Conv.
Require Types.

  Inductive Set class:= Trm:class | Typ: class | Ord: class.

  Definition cls:= (list class).

  Syntactic Definition nthf:= (nth_def class Trm).

  Inductive lift_cls: class->class->Prop :=
     lift_t: (lift_cls Trm Typ)
   | lift_T: (lift_cls Typ Ord).

  Hint lift_t lift_T.

  Fixpoint cl_term [t:term]: cls->class :=
    [i:cls]Cases t of
        (Srt _) => Ord
      | (Ref n) => Cases (nthf i n) of
                     Ord => Typ
                   | _ => Trm
                   end
      | (Abs A B) => (cl_term B (cons ? (cl_term A i) i))
      | (App u v) => (cl_term u i)
      | (Prod T U) => (cl_term U (cons ? (cl_term T i) i))
      end.

  Fixpoint class_env [e:env]: cls :=
    Cases e of
      nil => (nil ?)
    | (cons t f) => (cons ? (cl_term t (class_env f)) (class_env f))
    end.

  Definition cl_judge:= [e:env][t:term](cl_term t (class_env e)).

  Lemma cl_term_lift: (x:class)(t:term)(k:nat)(f,g:cls)(insert ? x k f g)
                     ->(cl_term t f)=(cl_term (lift_rec (S O) t k) g).
Induction t;Simpl;Intros;Auto.
(Elim (le_gt_dec k n);Simpl;Intros).
(Elim ins_le with class k f g Trm x n ;Auto).

(Elim ins_gt with class k f g Trm x n ;Auto).

(Elim H with k f g ;Auto).

(Elim H with k f g ;Auto).
Save.

  Lemma class_env_lift: (e,f:env)(k:nat)(x:term)(ins_in_env x k e f)
         ->(insert ? (cl_judge e (lift k x)) k (class_env e) (class_env f)).
(Induction 1;Intros).
Rewrite -> lift0.
Simpl;Auto.

Rewrite -> simpl_lift.
Simpl.
Unfold cl_judge 1 lift ;Simpl.
Elim cl_term_lift with (cl_term t (class_env e0)) (lift n x) O (
class_env e0) (cons ? (cl_term t (class_env e0)) (class_env e0)) ;Auto.
Elim cl_term_lift with (cl_judge e0 (lift n x)) t n (class_env e0) (
class_env f0) ;Auto.
Save.

  Lemma cl_judge_lift: (e,f:env)(k:nat)(x,t:term)(ins_in_env x k e f)
           ->(cl_judge e t)=(cl_judge f (lift_rec (S O) t k)).
Unfold cl_judge .
Intros.
Apply cl_term_lift with (cl_judge e (lift k x)) .
(Apply class_env_lift;Auto).
Save.

  Lemma cl_term_subst: (a:class)(G:cls)(x:term)(lift_cls (cl_term x G) a)
                 ->(t:term)(k:nat)(E,F:cls)(insert ? a k E F)
                  ->(trunc ? k E G)
           ->(cl_term t F)=(cl_term (subst_rec x t k) E).
(Induction t;Simpl;Intros;Auto).
(Elim (lt_eq_lt_dec k n);Simpl;Intros).
Elim y.
(Case n;Simpl;Intros).
Inversion_clear y0.

(Elim ins_le with class k E F Trm a n0 ;Auto).

Induction 1.
(Rewrite -> (ins_eq class k E F Trm a);Auto).
Replace (cl_term (lift k x) E) with (cl_term x G).
Inversion_clear H;Auto.

Elim H1;Intros.
Rewrite -> lift0;Auto.

Rewrite -> H3.
Rewrite -> simpl_lift.
Unfold 2 lift .
(Apply cl_term_lift with x0 ;Auto).

(Elim ins_gt with class k E F Trm a n ;Auto).

(Elim H0 with k E F ;Auto).

(Elim H0 with k E F ;Auto).
Save.

  Lemma sub_env_ins:
    (g:env)(v,V:term)(lift_cls (cl_judge g v) (cl_judge g V))
         ->(k:nat)(e,f:env)(sub_in_env v V k e f)
          ->(trunc ? k f g)
        ->(insert ? (cl_judge g V) k (class_env f) (class_env e)).
Induction 2;Simpl;Intros.
Inversion_clear H1.
(Unfold cl_judge ;Auto).

Inversion_clear H3.
Elim cl_term_subst with (cl_judge g V) (class_env g) v u n (class_env f0) (
class_env e0) ;Auto.
Elim H4;Simpl;Auto.
Save.

  Lemma cl_judge_subst:
      (g:env)(v,V:term)(lift_cls (cl_judge g v) (cl_judge g V))
       ->(k:nat)(e,f:env)(sub_in_env v V k e f)
        ->(trunc ? k f g)
      ->(t:term)(cl_judge e t)=(cl_judge f (subst_rec v t k)).
Unfold cl_judge .
Intros.
Cut (trunc ? k (class_env f) (class_env g));Intros.
Apply cl_term_subst with (cl_judge g V) (class_env g) ;Auto.
Apply sub_env_ins with v ;Auto.

(Elim H1;Simpl;Auto).
Save.

  Lemma class_sound_w: (e:env)(t,T:term)(typ e t T)->
               ((n:nat)(x:term)(item ? x e n)->(f:env)(trunc ? (S n) e f)->
                   (((typ f x (Srt prop))->(nthf (class_env e) n)=Typ)
                /\ ((typ f x (Srt kind))->(nthf (class_env e) n)=Ord)))
                   -> ((typ e T (Srt prop))->(cl_judge e t)=Trm)
                    /\ ((typ e T (Srt kind))->(cl_judge e t)=Typ)
                    /\ ((T=(Srt kind))->(cl_judge e t)=Ord).
(Induction 1; Simpl; Intros).
(Split; Intros).
(Elim inv_typ_kind with e0 (Srt prop); Auto).

(Split; Intros).
(Elim inv_typ_kind with e0 (Srt kind); Auto).

(Simpl; Auto).

(Elim H1; Intros).
Rewrite -> H3.
(Elim item_trunc with term v e0 x; Intros; Auto).
(Elim H2 with v x x0; Intros; Auto).
(Elim wf_sort with v e0 x0 x; Auto).
(Unfold cl_judge ; Simpl).
Intros.
Cut (typ e0 (lift (S v) x) (Srt x1)).
Intro.
(Split; Intros).
(Rewrite -> H6; Auto).
(Elim conv_sort with x1 prop; Auto).
(Apply typ_unique with e0 (lift (S v) x); Auto).

(Split; Intros).
(Rewrite -> H7; Auto).
(Elim conv_sort with x1 kind; Auto).
(Apply typ_unique with e0 (lift (S v) x); Auto).

Elim inv_typ_kind with e0 (Srt x1).
(Elim H10; Auto).

(Replace (Srt x1) with (lift (S v) (Srt x1)); Auto).
(Apply thinning_n with x0; Auto).

(Elim H5; Auto).
Clear H1 H3 H5 H6.
Intros.
(Elim H3; Intros).
Clear H3.
(Split; Intros).
Apply H1.
(Apply inv_typ_prod with e0 T0 U (Srt prop); Auto; Intros).
(Elim conv_sort with s3 prop; Auto).

(Split; Intros).
Apply H5.
(Apply inv_typ_prod with e0 T0 U (Srt kind); Auto; Intros).
(Elim conv_sort with s3 kind; Auto).

Discriminate H3.

Clear H3 H5.
(Destruct n; Simpl; Intros).
(Elim H1; Auto; Intros).
(Elim H8; Intros).
Clear H1 H6 H8.
Inversion_clear H3.
Inversion_clear H5.
Inversion H1.
Elim H6.
(Split; Intros).
Apply H9.
(Elim conv_sort with prop s1; Auto).
Apply type_prop.
(Apply typ_wf with T0 (Srt s1); Auto).

(Apply typ_unique with e0 T0; Auto).

Apply H10.
(Elim conv_sort with s1 kind; Auto).
(Apply typ_unique with e0 T0; Auto).

Inversion_clear H3.
Inversion_clear H5.
(Apply H6; Auto).

(Elim H3; Auto; Induction 2; Intros).
Clear H1 H3 H4 H6 H8.
(Elim type_case with e0 u (Prod V Ur); Intros; Auto).
(Elim H1; Intros).
Clear H1.
(Cut (typ e0 (subst v Ur) (Srt x)); Intros).
(Split; Intros).
Apply H5.
(Elim conv_sort with x prop; Auto).
(Apply typ_unique with e0 (subst v Ur); Auto).

(Split; Intros).
Apply H7.
(Elim conv_sort with x kind; Auto).
(Apply typ_unique with e0 (subst v Ur); Auto).

Elim inv_typ_kind with e0 (Srt x).
(Elim H4; Auto).

(Apply inv_typ_prod with e0 V Ur (Srt x); Auto; Intros).
Replace (Srt x) with (subst v (Srt s2)).
(Apply substitution with V; Auto).

(Elim conv_sort with s2 x; Auto).

Discriminate H1.

Elim H3.
(Induction 2; Intros).
Clear H1 H3 H4 H6.
(Split; Intros).
Apply H5.
(Replace (Srt s2) with (lift (S O) (Srt s2)); Auto).
(Replace (Srt prop) with (lift (S O) (Srt prop)); Auto).
(Apply thinning; Auto).
(Apply wf_var with s1; Auto).

(Split; Intros; Auto).
Apply H7.
(Replace (Srt s2) with (lift (S O) (Srt s2)); Auto).
(Replace (Srt kind) with (lift (S O) (Srt kind)); Auto).
(Apply thinning; Auto).
(Apply wf_var with s1; Auto).

(Destruct n; Simpl; Intros).
(Elim H1; Auto; Intros).
(Elim H8; Intros).
Clear H1 H3 H4 H8.
Inversion_clear H5.
Inversion_clear H6.
Inversion H1.
Elim H5.
(Split; Intros).
Apply H9.
(Elim conv_sort with prop s1; Auto).
Apply type_prop.
(Apply typ_wf with T0 (Srt s1); Auto).

(Apply typ_unique with e0 T0; Auto).

Apply H10.
(Elim conv_sort with kind s1; Auto).
(Apply typ_unique with e0 T0; Auto).

Clear H1 H3.
Inversion_clear H5.
Inversion_clear H6.
Auto.

(Elim H1; Auto; Induction 2; Intros).
Clear H1 H4 H5 H7.
(Cut (typ e0 U (Srt s)); Intros).
(Split; Intros).
Apply H6.
(Elim conv_sort with s prop; Auto).
(Apply typ_unique with e0 V; Auto).

(Split; Intros).
Apply H8.
(Elim conv_sort with s kind; Auto).
(Apply typ_unique with e0 V; Auto).

(Elim inv_typ_kind with e0 (Srt s); Auto).
(Elim H4; Auto).

(Elim type_case with e0 t0 U; Auto; Intros).
(Elim H1; Intros).
(Elim conv_sort with x s; Auto).
(Apply typ_conv_conv with e0 U V; Auto).

(Elim inv_typ_conv_kind with e0 V (Srt s); Auto).
(Elim H1; Auto).
Save.

  Lemma corr_class_env: (e:env)(wf e)->(n:nat)(x:term)(item ? x e n)->
            (f:env)(trunc ? (S n) e f)->
                   (((typ f x (Srt prop))->(nthf (class_env e) n)=Typ)
                /\ ((typ f x (Srt kind))->(nthf (class_env e) n)=Ord)).
(Induction e; Simpl).
Intros.
Inversion_clear H0.

(Destruct n; Simpl; Intros).
Inversion_clear H1.
Inversion_clear H2.
Inversion H1.
Elim H4.
Inversion_clear H0.
(Elim class_sound_w with l a (Srt s); Intros; Auto).
(Elim H6; Intros).
Clear H6.
(Split; Intros).
Apply H7.
(Elim conv_sort with prop s; Auto).
(Apply type_prop; Apply typ_wf with a (Srt s); Auto).

(Apply typ_unique with l a; Auto).

Apply H8.
(Elim conv_sort with s kind; Auto).
(Apply typ_unique with l a; Auto).

(Apply H; Auto).
(Apply typ_wf with a (Srt s); Auto).

Inversion_clear H1.
Inversion_clear H2.
(Apply H; Auto).
Inversion_clear H0.
(Apply typ_wf with a (Srt s); Auto).
Save.

  Lemma class_trm: (e:env)(t,T:term)(typ e t T)->(typ e T (Srt prop))
                  ->(cl_judge e t)=Trm.
Intros.
Elim class_sound_w with e t T ;Auto.
Intros.
(Apply corr_class_env;Auto).
(Apply typ_wf with t T ;Auto).
Save.

  Lemma class_typ: (e:env)(t,T:term)(typ e t T)->(typ e T (Srt kind))
                  ->(cl_judge e t)=Typ.
Intros.
(Elim class_sound_w with e t T ;Auto).
Intros.
(Elim H2;Auto).

Intros.
Apply corr_class_env;Auto.
Apply typ_wf with t T ;Auto.
Save.

  Lemma class_ord: (e:env)(t:term)(typ e t (Srt kind))->(cl_judge e t)=Ord.
Intros.
Elim class_sound_w with e t (Srt kind) ;Auto.
Intros.
Elim H1;Auto.

Intros.
(Apply corr_class_env;Auto).
(Apply typ_wf with t (Srt kind) ;Auto).
Save.

  Lemma inv_class: (e:env)(t,T:term)(typ e t T)
                     -> Cases (cl_judge e t) of
                          Trm => (typ e T (Srt prop))
                        | Typ => (typ e T (Srt kind))
                        | Ord => T=(Srt kind)
                        end.
Intros.
Elim type_case with e t T ;Intros;Auto.
Elim H0.
(Induction x;Intros).
Rewrite -> (class_typ e t T);Auto.

Rewrite -> (class_trm e t T);Auto.

Rewrite -> (class_ord e t);Auto.
(Elim H0;Auto).
Save.

  Lemma corr_lift: (e:env)(t,T,s:term)(typ e t T)->(typ e T s)
              ->(lift_cls (cl_judge e t) (cl_judge e T)).
Intros.
Generalize (inv_class e t T H) .
Elim (cl_judge e t);Intros.
Rewrite -> (class_typ e T (Srt prop));Auto.
Apply type_prop;Apply typ_wf with t T ;Auto.

Rewrite -> (class_ord e T);Auto.

Elim inv_typ_kind with e s ;Auto.
Elim H1;Auto.
Save.

  Lemma class_subst: (e:env)(t,v,V,s:term)(typ e v V)->(typ e V s)
                   ->(cl_judge (cons ? V e) t)=(cl_judge e (subst v t)).
Intros.
Unfold subst .
(Apply cl_judge_subst with e V ;Auto).
(Apply corr_lift with s ;Auto).
Save.

  Lemma cl_judge_red: (e:env)(T,K:term)(typ e T K)->(U:term)(red T U)
                ->(cl_judge e T)=(cl_judge e U).
Intros.
Cut (typ e U K);Intros.
Elim type_case with e T K ;Intros;Auto.
Elim H2.
(Induction x;Intros).
Rewrite -> (class_typ e T K);Auto.
Rewrite -> (class_typ e U K);Auto.

Rewrite -> (class_trm e T K);Auto.
Rewrite -> (class_trm e U K);Auto.

Rewrite -> (class_ord e T).
Rewrite -> (class_ord e U);Auto.
Elim H2;Auto.

Elim H2;Auto.

Apply subject_reduction with T ;Auto.
Save.

  Lemma class_env_red1: (e,f:env)(red1_in_env e f)->(wf e)
                  ->(class_env e)=(class_env f).
Induction 1;Simpl;Auto;Intros.
Change (eq ? (cons ? (cl_judge e0 t) (class_env e0))
         (cons ? (cl_judge e0 u) (class_env e0))).
Inversion_clear H1.
Elim cl_judge_red with e0 t (Srt s) u ;Auto.

Inversion_clear H2.
Elim H1;Auto.
Apply typ_wf with t (Srt s) ;Auto.
Save.

20/01/97, 14:42