Skel.v

Require Termes.
Require Conv.
Require Types.
Require Class.
Require Export MyLogicType.

  Inductive skel: Type :=
     PROP: skel
   | PROD: skel->skel->skel.

  Definition predl: skel->skel :=
    [a:skel]Cases a of
        (PROD a1 _) => a1
      | _ => PROP
      end.

  Definition predr: skel->skel :=
    [a:skel]Cases a of
        (PROD _ a2) => a2
      | _ => PROP
      end.

  Lemma EQ_skel: (a,b:skel)(ORT (a===b) (notT (a===b))).
(Induction a; Destruct b; Intros).
(Left; Auto).

(Right; Red; Intros).
Inversion X.

(Right; Red; Intros).
Inversion X1.

(Elim X with s1; Intros).
Elim y.
(Elim X0 with s2; Intros).
Elim y0.
(Left; Auto).

(Right; Red; Intros; Apply y0).
(Injection X1; Auto).

(Right; Red; Intros; Apply y).
(Injection X1; Auto).
Save.

  Fixpoint cv_skel [K:term]: cls->skel :=
   [F:cls]Cases K of
       (Prod T U) => ([G:cls]Cases (cl_term U G) (cl_term T F) of
                             Ord Ord => (PROD (cv_skel T F) (cv_skel U G))
                           | Ord Typ => (cv_skel U G)
                           | _ _ => PROP
                           end
                      (cons ? (cl_term T F) F))
     | _ => PROP
     end.

  Fixpoint typ_skel [T:term]: env->skel :=
   [e:env]Cases T of
      (Srt _) => PROP
    | (Ref k) => (Fix nthk {nthk/1: env->nat->skel :=
                      [e:env][n:nat]Cases e n of
                           (cons _ f) (S m) => (nthk f m)
                         | (cons h f) O => (cv_skel h (class_env f))
                         | _ _ => PROP
                         end} e k)
    | (Abs A t) => Cases (cl_judge (cons ? A e) t) (cl_judge e A) of
                     Typ Ord => (PROD (cv_skel A (class_env e))
                                               (typ_skel t (cons ? A e)))
                   | Typ Typ => (typ_skel t (cons ? A e))
                   | _ _ => PROP
                   end
    | (App u v) => Cases (cl_judge e u) (cl_judge e v) of
                     Typ Typ => (predr (typ_skel u e))
                   | Typ Trm => (typ_skel u e)
                   | _ _ => PROP
                   end
    | (Prod _ _) => PROP
    end.

  Lemma skel_not_ord: (T,K:term)(e:env)(lift_cls (cl_judge e T) (cl_judge e K))
                        ->(cv_skel T (class_env e))==PROP.
Destruct T;Simpl;Auto.
Unfold 1 cl_judge .
Simpl.
Destruct 1;Auto.
Save.

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

(Elim cl_term_lift with x t0 k f g ;Auto).
(Elim cl_term_lift with x t1 (S k) (cons ? (cl_term t0 f) f)
                        (cons ? (cl_term t0 f) g) ;Auto).
Elim H with f g k ;Auto.
Elim H0 with (cons ? (cl_term t0 f) f) (cons ? (cl_term t0 f) g)(S k) ;Auto.
Save.

  Lemma cv_skel_subst:
     (g:env)(v,V:term)(lift_cls (cl_judge g v) (cl_judge g V))
      ->(t:term)(k:nat)(e,f:env)(sub_in_env v V k e f)
       ->(trunc ? k f g)
     ->(cv_skel t (class_env e))==(cv_skel (subst_rec v t k) (class_env f)).
(Induction t;Simpl;Intros;Auto).
(Elim (lt_eq_lt_dec k n);Simpl;Intros;Auto).
(Elim y;Simpl;Intros;Auto).
Generalize H1 .
Elim H0;Intros.
Rewrite -> lift0.
Symmetry.
(Apply skel_not_ord with V ;Auto).
Inversion_clear H2;Auto.

Inversion_clear H4.
Rewrite -> simpl_lift.
Unfold 1 lift .
Rewrite -> H3;Auto.
Simpl.
(Apply cv_skel_lift with (cl_term (subst_rec v u n0) (class_env f0)) ;Auto).

Replace (cons ? (cl_term t0 (class_env e)) (class_env e)) with (
           class_env (cons ? t0 e));Auto.
Replace (cons ? (cl_term (subst_rec v t0 k) (class_env f))
          (class_env f)) with (class_env (cons ? (subst_rec v t0 k) f));Auto.
Replace (cl_term t1 (class_env (cons ? t0 e))) with (cl_judge
                                                       (cons ? t0 e) t1);Auto.
Replace (cl_term (subst_rec v t1 (S k)) (class_env (cons ?
        (subst_rec v t0 k) f))) with (cl_judge (cons ? ( subst_rec v t0 k) f)
         (subst_rec v t1 ( S k)));Auto.
(Replace (cl_term (subst_rec v t0 k) (class_env f)) with (cl_judge f
                                                (subst_rec v t0 k));Auto).
Elim cl_judge_subst with g v V (S k) (cons ? t0 e) (cons ?
                                              (subst_rec v t0 k) f) t1 ;Auto.
Elim cl_judge_subst with g v V k e f t0 ;Auto.
(Elim H0 with k e f ;Auto).
(Elim H1 with (S k) (cons ? t0 e) (cons ? (subst_rec v t0 k) f) ;Auto).
Save.

  Lemma typ_skel_lift: (t:term)(k:nat)(f,g:env)(x:term)(ins_in_env x k f g)
                   ->(typ_skel t f)==(typ_skel (lift_rec (S O) t k) g).
(Induction t;Simpl;Auto).
Induction n.
(Destruct 1;Intros).
(Elim (le_gt_dec O O);Intros;Auto).
Simpl.
Auto.

Inversion_clear y.

(Elim (le_gt_dec (S n0) O);Intros).
Inversion_clear y.

Simpl.
(Apply cv_skel_lift with (cl_judge e (lift n0 x)) ;Auto).
(Apply class_env_lift;Auto).

(Destruct 2;Simpl;Intros).
(Elim (le_gt_dec O (S n0));Simpl;Auto;Intros).
Inversion_clear y.

(Rewrite -> (H n1 e f0 x);Auto).
Elim (le_gt_dec n1 n0);Elim (le_gt_dec (S n1) (S n0));Intros;Auto.
Absurd (le n1 n0);Auto.

Absurd (le (S n1) (S n0));Auto.

Intros.
Elim cl_judge_lift with f g k x t0 ;Auto.
Elim cl_judge_lift with (cons ? t0 f) (cons ? (lift_rec (S O) t0 k) g) (
S k) x t1 ;Auto.
Elim H0 with (S k) (cons ? t0 f) (cons ? (lift_rec (S O) t0 k) g) x ;Auto.
(Elim cv_skel_lift with (cl_judge f (lift k x)) t0 (class_env f) (
class_env g) k ;Auto).
Apply class_env_lift;Auto.

Intros.
(Elim H with k f g x ;Auto).
(Elim cl_judge_lift with f g k x t0 ;Auto).
Elim cl_judge_lift with f g k x t1 ;Auto.
Save.

  Lemma typ_skel_subst: (g:env)(v,V:term)
      (lift_cls (cl_judge g v) (cl_judge g V))
       ->(typ_skel v g)==(cv_skel V (class_env g))
        ->(t:term)(k:nat)(e,f:env)(sub_in_env v V k e f)
         ->(trunc ? k f g)
          ->(typ_skel t e)==(typ_skel (subst_rec v t k) f).
Induction t;Simpl;Auto.
Induction n.
Intros.
Elim (lt_eq_lt_dec k O);Intros.
Elim y;Intros.
Inversion_clear y0.

Generalize H1 H2 .
Rewrite -> y0;Intros.
Rewrite -> lift0.
Inversion_clear H3.
Inversion_clear H4;Auto.

Generalize y H1 H2 .
(Case k;Intros).
Inversion_clear y0.

Generalize H4 .
Inversion_clear H3;Intros.
Inversion_clear H3.
Simpl.
(Apply cv_skel_subst with g V ;Auto).

Destruct 2;Intros.
Inversion_clear H3.
Elim (lt_eq_lt_dec O (S n0));Intros.
Elim y;Intros.
Simpl.
Auto.

Discriminate y0.

Inversion_clear y.

Inversion_clear H4.
Rewrite -> (H1 n1 e0 f0);Auto;Intros.
Elim (lt_eq_lt_dec n1 n0);Intros.
Elim (lt_eq_lt_dec (S n1) (S n0));Intros.
Elim y;Elim y0;Auto.
Case n0;Intros;Auto.
Inversion_clear y2.

Intro.
Inversion_clear y1;Intros.
Elim lt_n_n with n0 ;Auto.

Intros.
Inversion_clear y2 in y1.
Elim lt_n_n with (S n0) ;Auto.

Intros.
Rewrite -> simpl_lift.
Unfold 2 lift .
Apply typ_skel_lift with (subst_rec v u n1) ;Auto.

Elim y;Intros.
Absurd (le (S n1) n0);Auto.

Inversion_clear y1 in y0.
Elim lt_n_n with (S n0) ;Auto.

Elim (lt_eq_lt_dec (S n1) (S n0));Intros.
Elim y0;Intros.
Absurd (le (S n0) n1);Auto.

Inversion_clear y1 in y.
Elim lt_n_n with n0 ;Auto.

Simpl;Auto.

Intros.
Elim cl_judge_subst with g v V k e f t0 ;Auto.
Elim cl_judge_subst with g v V (S k) (cons ? t0 e) (cons ?
                                                     (subst_rec v t0 k)
                                                     f) t1 ;Auto.
Elim cv_skel_subst with g v V t0 k e f ;Auto.
Elim H2 with (S k) (cons ? t0 e) (cons ? (subst_rec v t0 k) f) ;Auto.

Intros.
Elim cl_judge_subst with g v V k e f t0 ;Auto.
Elim cl_judge_subst with g v V k e f t1 ;Auto.
Elim H1 with k e f ;Auto.
Save.

  Lemma skel_red1: (e:env)(A,T:term)(typ e A T)->(B:term)(red1 A B)
        ->(cv_skel A (class_env e))==(cv_skel B (class_env e)).
(Induction 1;Intros;Auto).
Inversion_clear H1.

Inversion_clear H2.

Simpl.
(Inversion_clear H6;Simpl;Auto).

Generalize H2 .
(Inversion_clear H4;Simpl;Auto;Intros).
(Apply inv_typ_abs with e0 T0 M (Prod V Ur) ;Auto;Intros).
Symmetry.
Apply skel_not_ord with (subst v T1) .
Apply corr_lift with (Srt s2) ;Auto.
Apply substitution with T0 ;Auto.
(Apply type_conv with V s1 ;Auto).
(Apply inv_conv_prod_l with Ur T1 ;Auto).

(Replace (Srt s2) with (subst v (Srt s2));Auto).
Apply substitution with T0 ;Auto.
(Apply type_conv with V s1 ;Auto).
(Apply inv_conv_prod_l with Ur T1 ;Auto).

(Inversion_clear H4;Simpl).
Replace (cl_term N1 (class_env e0)) with (cl_judge e0 T0).
(Elim H1 with N1 ;Auto).

Change (eq ? (cl_judge e0 T0) (cl_judge e0 N1)).
Apply cl_judge_red with (Srt s1) ;Auto.

(Replace (cons ? (cl_term T0 (class_env e0)) (class_env e0)) with (
class_env (cons ? T0 e0));Auto).
Elim H3 with N2 ;Auto.
(Replace (cl_term N2 (class_env (cons ? T0 e0))) with (cl_term U
                                                      (class_env
                                                        (cons ? T0 e0)));Auto).
Change (eq ? (cl_judge (cons ? T0 e0) U) (cl_judge (cons ? T0 e0) N2)).
(Apply cl_judge_red with (Srt s2) ;Auto).
Save.

  Lemma skel_red: (A,B:term)(red A B)->(e:env)(T:term)(typ e A T)
        ->(cv_skel A (class_env e))==(cv_skel B (class_env e)).
Induction 1;Intros;Auto.
Rewrite -> (H1 e T);Auto.
(Apply skel_red1 with T ;Auto).
(Apply subject_reduction with A ;Auto).
Save.

  Lemma skel_conv: (e:env)(A,T:term)(typ e A T)->(B,U:term)(typ e B U)
          ->(conv A B)->(cv_skel A (class_env e))==(cv_skel B (class_env e)).
Intros.
(Elim church_rosser with A B ;Intros;Auto).
(Rewrite -> (skel_red A x H2 e T);Auto).
(Elim skel_red with B x e U ;Auto).
Save.

  Lemma skel_sound: (e:env)(t,T:term)(typ e t T)
                ->(cv_skel T (class_env e))==(typ_skel t e).
Induction 1;Auto.
Do 3 Intro.
Generalize e0 .
Elim v.
Destruct e0;Intros.
(Elim H1;Intros).
Inversion_clear H3.

(Elim H1;Intros).
Rewrite -> H2.
Inversion_clear H3.
(Simpl;Unfold lift ).
Symmetry.
Apply cv_skel_lift with (cl_term t0 (class_env l)) ;Auto.

(Destruct 2;Intros).
Rewrite -> H3.
(Inversion_clear H4;Simpl).
Rewrite -> simpl_lift.
Unfold 1 lift .
(Elim cv_skel_lift with (cl_term y (class_env l)) (lift (S n) x) (
class_env l) (cons ? (cl_term y (class_env l)) (class_env l)) O ;Auto).
Simpl in H1.
Apply H1.
(Exists x ;Auto).

Simpl;Intros.
Rewrite -> H5.
Replace (cl_term U (cons ? (cl_term T0 (class_env e0)) (class_env e0))) with (
cl_judge (cons ? T0 e0) U);Auto.
(Elim corr_lift with (cons ? T0 e0) M U (Srt s2) ;Auto).

(Simpl;Intros).
Elim H3;Clear H3.
(Elim type_case with e0 u (Prod V Ur) ;Intros;Auto).
Elim H3;Intros.
Apply inv_typ_prod with e0 V Ur (Srt x) ;Auto;Intros.
Unfold subst .
Elim cv_skel_subst with e0 v V Ur O (cons ? V e0) e0 ;Auto.
Replace (cons ? (cl_term V (class_env e0)) (class_env e0)) with (
class_env (cons ? V e0));Auto.
(Replace (cl_term V (class_env e0)) with (cl_judge e0 V);Auto).
Replace (cl_term Ur (class_env (cons ? V e0))) with (cl_judge e0
                                                      (Prod V Ur));Auto.
Generalize (inv_class e0 (Prod V Ur) (Srt x) H4) .
(Elim corr_lift with e0 u (Prod V Ur) (Srt x) ;Auto).
Intro.
Apply skel_not_ord with (Srt x) .
Change (lift_cls (cl_judge e0 (Prod V Ur)) Ord).
(Rewrite -> (class_typ e0 (Prod V Ur) (Srt x));Auto).

Intro.
(Elim corr_lift with e0 v V (Srt s1) ;Auto).

(Apply corr_lift with (Srt s1) ;Auto).

Discriminate H3.

Intros.
(Elim type_case with e0 t0 U ;Intros;Auto).
(Elim H5;Intros).
Elim H1.
(Apply skel_conv with (Srt s) (Srt x) ;Auto).

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

  Lemma typ_skel_red1: (e:env)(T,U,K:term)(typ e T K)->(red1 T U)
          ->(typ_skel T e)==(typ_skel U e).Intros.
(Elim skel_sound with e T K ;Auto).
(Apply skel_sound;Auto).
(Apply subject_reduction with T ;Auto).
Save.

  Lemma typ_skel_red_env: (e:env)(t,s:term)(typ e t s)
              ->(f:env)(red1_in_env e f)
                        ->(typ_skel t e)==(typ_skel t f).
Induction 1;Simpl;Intros;Auto.
Generalize e0 f H2 H0 .
(Elim v;Simpl;Auto).
(Destruct 1;Intros).
Inversion_clear H5.
Apply skel_red1 with (Srt s0) ;Auto.

Elim class_env_red1 with e2 f1 ;Auto.
Inversion_clear H5.
(Apply typ_wf with t1 (Srt s0) ;Auto).

(Destruct 2;Simpl;Intros;Auto).
(Apply H3;Auto).
Inversion_clear H6.
(Apply typ_wf with t1 (Srt s0) ;Auto).

Unfold cl_judge .
Elim class_env_red1 with (cons ? T e0) (cons ? T f) ;Auto.
Elim class_env_red1 with e0 f ;Auto.
(Elim H5 with (cons ? T f) ;Auto).

(Apply typ_wf with T (Srt s1) ;Auto).

(Apply wf_var with s1 ;Auto).

Unfold cl_judge .
Elim class_env_red1 with e0 f ;Auto.
(Elim H3 with f ;Auto).

Apply typ_wf with v V ;Auto.
Save.

06/11/96, 12:34