Library TypeJudgeECC


Require Import TypeECC.

Section Typage.

  Inductive eq_typ : env -> term -> term -> term -> Prop :=
    | type_prop : forall e,
        wf e ->
        eq_typ e (Srt prop) (Srt prop) (Srt (kind 0))
    | type_kind : forall e n,
        wf e ->
        eq_typ e (Srt (kind n)) (Srt (kind n)) (Srt (kind(S n)))
    | type_var :
        forall e v t,
        wf e ->
        item_lift t e v ->
        eq_typ e (Ref v) (Ref v) t
    | type_abs :
        forall e T T' M M' U U' s1 s2 s3,
        eq_typ e T T' (Srt s1) ->
        eq_typ (T :: e) U U' (Srt s2) ->
        eq_typ (T :: e) M M' U ->
        ecc_prod s1 s2 s3 = true ->
        eq_typ e (Abs T M) (Abs T' M') (Prod T U)
    | type_app :
        forall e u u' v v' V V' Ur Ur' s1 s2 s3,
        eq_typ e v v' V ->
        eq_typ e V V' (Srt s1) ->
        eq_typ e u u' (Prod V Ur) ->
        eq_typ (V::e) Ur Ur' (Srt s2) ->
        ecc_prod s1 s2 s3 = true ->
        eq_typ e (App u v) (App u' v') (subst v Ur)
    | type_prod :
        forall e T T' U U' s1 s2 s3,
        eq_typ e T T' (Srt s1) ->
        eq_typ (T :: e) U U' (Srt s2) ->
        ecc_prod s1 s2 s3 = true ->
        eq_typ e (Prod T U) (Prod T' U') (Srt s3)
    | type_beta : forall e T T' M M' N N' U U' s1 s2 s3,
        eq_typ e N N' T ->
        eq_typ e T T' (Srt s1) ->
        eq_typ (T::e) M M' U ->
        eq_typ (T::e) U U' (Srt s2) ->
        ecc_prod s1 s2 s3 = true ->
        eq_typ e (App (Abs T M) N) (subst N' M') (subst N U)
    | type_red : forall e M M' T T' s,
        eq_typ e M M' T ->
        eq_typ e T T' (Srt s) ->
        eq_typ e M M' T'
    | type_exp : forall e M M' T T' s,
        eq_typ e M M' T' ->
        eq_typ e T T' (Srt s) ->
        eq_typ e M M' T
  with wf : env -> Prop :=
      wf_nil : wf nil
    | wf_var : forall e T T' s,
        eq_typ e T T' (Srt s) ->
        wf (T::e).

Scheme eq_typ_mind := Minimality for eq_typ Sort Prop
  with wf_mind := Minimality for wf Sort Prop.

  Lemma typ_wf : forall e t t' T, eq_typ e t t' T -> wf e.

  Lemma typ_refl : forall e t t' T, eq_typ e t t' T -> eq_typ e t t T.

  Lemma typ_thin :
   forall g A e t t' T,
   wf (A::g) ->
   eq_typ e t t' T ->
   forall n f,
   ins_in_env A n e f ->
   trunc n e g ->
   eq_typ f (lift_rec 1 t n) (lift_rec 1 t' n) (lift_rec 1 T n).

  Lemma typ_thinning :
   forall A e t t' T,
   wf (A::e) ->
   eq_typ e t t' T ->
   eq_typ (A::e) (lift 1 t) (lift 1 t') (lift 1 T).

  Lemma typ_thinning_n :
   forall f t t' T n e,
   wf e ->
   eq_typ f t t' T ->
   trunc n e f ->
   eq_typ e (lift n t) (lift n t') (lift n T).

  Lemma typ_sub :
   forall g d t e u u' U,
   eq_typ e u u' U ->
   forall d' n f,
   eq_typ g d d' t ->
   sub_in_env d t n e f ->
   trunc n f g ->
   wf f ->
   eq_typ f (subst_rec d u n) (subst_rec d' u' n) (subst_rec d U n).

  Theorem substitution :
   forall e t u u' U d d',
   eq_typ (t :: (e:env)) u u' U ->
   eq_typ e d d' t ->
   eq_typ e (subst d u) (subst d' u') (subst d U).

  Inductive red1_in_env : env -> env -> Prop :=
    | red1_env_hd : forall e t u s, eq_typ e t u (Srt s) ->
        red1_in_env (t :: e) (u :: e)
    | red1_env_tl :
        forall e f t, red1_in_env e f -> red1_in_env (t :: e) (t :: f).

  Hint Constructors red1_in_env: coc.

  Lemma red_item :
   forall n t e f,
   item_lift t e n ->
   red1_in_env e f ->
   wf f ->
   item_lift t f n \/
   (forall g, trunc (S n) e g -> trunc (S n) f g) /\
   (exists2 u, exists s, eq_typ f t u (Srt s) & item_lift u f n).

  Lemma typ_red_env :
   forall e t t' T, eq_typ e t t' T -> forall f, red1_in_env e f -> wf f ->
   eq_typ f t t' T.

  Lemma typ_refl2 : forall e M M' T, eq_typ e M M' T -> eq_typ e M' M' T.

  Lemma wf_sort_lift :
   forall n e t, wf e -> item_lift t e n ->
   exists s, eq_typ e t t (Srt s).

  Theorem type_case :
   forall e t t' T, eq_typ e t t' T ->
   exists s, eq_typ e T T (Srt s).

Require Import Relation_Operators.

  Definition eq_typ_eq e :=
    clos_refl_sym_trans _ (fun x y => exists s, eq_typ e x y (Srt s)).
  Hint Unfold eq_typ_eq : coc.

  Lemma eq_typ_eq_red : forall e T T' s,
    eq_typ e T T' (Srt s) -> eq_typ_eq e T T'.

  Lemma eq_typ_eq_exp : forall e T T' s,
    eq_typ e T T' (Srt s) -> eq_typ_eq e T' T.

  Lemma type_conv_gen : forall e M M' T T',
    eq_typ_eq e T T' ->
    (eq_typ e M M' T -> eq_typ e M M' T') /\
    (eq_typ e M M' T' -> eq_typ e M M' T).
  Lemma type_conv : forall e M M' T T',
    eq_typ e M M' T -> eq_typ_eq e T T' -> eq_typ e M M' T'.

  Definition inv_type (P : Prop) e t t' T :=
    match t with
    | Srt prop => eq_typ_eq e (Srt (kind 0)) T -> t' = Srt prop -> P
    | Srt (kind n) => eq_typ_eq e (Srt (kind (S n))) T -> t' = Srt (kind n) -> P
    | Ref n =>
        forall x, item_lift x e n -> eq_typ_eq e x T -> t' = Ref n -> P
    | Abs A M =>
        forall s1 s2 s3 A' M' U U',
        eq_typ e A A' (Srt s1) ->
        eq_typ (A :: e) M M' U ->
        eq_typ (A :: e) U U' (Srt s2) ->
        ecc_prod s1 s2 s3 = true ->
        eq_typ_eq e (Prod A U) T -> t' = Abs A' M' -> P
    | App u v =>
        forall u' v' Ur Ur' V V' s1 s2 s3,
        eq_typ e v v' V ->
        eq_typ e V V' (Srt s1) ->
        eq_typ e u u' (Prod V Ur) ->
        eq_typ (V::e) Ur Ur' (Srt s2) ->
        ecc_prod s1 s2 s3 = true ->
        t' = App u' v' \/
        (exists2 M, u=Abs V M &
         exists2 M', eq_typ (V::e) M M' Ur & t' = subst v' M') ->
        eq_typ_eq e (subst v Ur) T -> P
    | Prod A B =>
        forall A' B' s1 s2 s3,
        eq_typ e A A' (Srt s1) ->
        eq_typ (A :: e) B B' (Srt s2) ->
        ecc_prod s1 s2 s3 = true ->
        eq_typ_eq e (Srt s3) T -> t' = Prod A' B' -> P
    end.

  Lemma inv_type_conv :
   forall P e t t' U V, eq_typ_eq e U V ->
   inv_type P e t t' V -> inv_type P e t t' U.

  Theorem typ_inversion :
    forall P e t t' T, eq_typ e t t' T -> inv_type P e t t' T -> P.

End Typage.