Library TypeJudge


Require Import Types.

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)
    | 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,
        eq_typ e T T' (Srt s1) ->
        eq_typ (T :: e) U U' (Srt s2) ->
        eq_typ (T :: e) M M' U ->
        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,
        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) ->
        eq_typ e (App (Prod u Ur) v) (App (Prod u' Ur') v') (subst v Ur)
    | type_prod :
        forall e T T' U U' s1 s2,
        eq_typ e T T' (Srt s1) ->
        eq_typ (T :: e) U U' (Srt s2) ->
        eq_typ e (Prod T U) (Prod T' U') (Srt s2)
    | type_beta : forall e T T' M M' N N' U U' s1 s2,
        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) ->
        eq_typ e (App (Prod (Abs T M) U) 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.

  Definition eq_red e M M' T:=
    clos_refl_trans _ (fun x y => eq_typ e x y T) M M'.
  Definition eq_conv e M M' T:=
    clos_refl_sym_trans _ (fun x y => eq_typ e x y T) M M'.

  Lemma eq_conv_refl : forall e t T, eq_conv e t t T.
  Hint Resolve eq_conv_refl : coc.

  Lemma eq_conv_sym :
    forall e t u T, eq_conv e t u T -> eq_conv e u t T.

  Lemma eq_conv_trans : forall e M M' M'' T,
    eq_conv e M M' T ->
    eq_conv e M' M'' T ->
    eq_conv e M M'' T.

  Lemma eq_red_conv : forall e M M' T, eq_red e M M' T -> eq_conv e M M' T.

  Lemma eq_conv_red : forall e T T' U,
    eq_typ e T T' U -> eq_conv e T T' U.

  Lemma eq_conv_exp : forall e T T' U,
    eq_typ e T T' U -> eq_conv e T' T U.
  Hint Resolve eq_conv_red eq_conv_exp : coc.

  Lemma type_eq_conv_gen : forall e M M' T T' s,
    eq_conv e T T' (Srt s) ->
    (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_eq_conv : forall e M M' T T' s,
    eq_typ e M M' T -> eq_conv e T T' (Srt s) -> eq_typ e M M' T'.

  Lemma eq_conv_conv : forall (e : env) (M M' T T' : term) s,
    eq_conv e M M' T -> eq_conv e T T' (Srt s) -> eq_conv e M M' T'.


  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 eq_conv_lift : forall e T U A x,
    eq_conv e T U A ->
    wf (x::e) ->
    eq_conv (x::e) (lift 1 T) (lift 1 U) (lift 1 A).

  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).

Lemma eq_conv_subst_ty_l : forall e M M' T U s,
  eq_conv e M M' T ->
  eq_typ (T::e) U U (Srt s) ->
  eq_conv e (subst M U) (subst M' U) (Srt s).

Lemma eq_conv_subst_r : forall e M T U U' A,
  eq_typ e M M T ->
  eq_conv (T::e) U U' A ->
  eq_conv e (subst M U) (subst M U') (subst M A).

  Inductive red1_in_env : env -> env -> Prop :=
    | red1_env_hd : forall e t u s, eq_conv 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_conv f t u (Srt s) & item_lift u f n).

  Lemma typ_red_env_raw :
   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 eq_conv_inv : forall e T T' U,
    eq_conv e T T' U ->
    T = T' \/ eq_typ e T T U /\ eq_typ e T' T' U.

  Lemma eq_conv_inv2 : forall e T T' U,
    eq_conv e T T' U ->
    eq_typ e T T U -> eq_typ e T' T' U.

  Lemma eq_red_inv : forall e T T' U,
    eq_red e T T' U ->
    T = T' \/ eq_typ e T T U /\ eq_typ e T' T' U.

  Lemma eq_red_inv2 : forall e T T' U,
    eq_red e T T' U ->
    eq_typ e T T U -> eq_typ e T' T' U.

  Lemma wf_red_env_trans :
    forall e f,
    clos_refl_trans _ red1_in_env e f ->
    wf e ->
    wf f.

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

  Lemma typ_red_env_trans :
    forall e f M M' T,
    clos_refl_trans _ red1_in_env e f ->
    eq_typ e M M' T ->
    eq_typ f M M' T.

  Lemma eq_conv_red_env : forall e f x y T,
    red1_in_env e f ->
    eq_conv e x y T ->
    f x y T.


  Lemma eq_conv_prod_r : forall e T U U' s1 s2,
    eq_typ e T T (Srt s1) ->
    eq_conv (T::e) U U' (Srt s2) ->
    eq_conv e (Prod T U) (Prod T U') (Srt s2).

  Lemma eq_conv_prod_l : forall e T T' U s1 s2,
    eq_conv e T T' (Srt s1) ->
    eq_typ (T::e) U U (Srt s2) ->
    eq_conv e (Prod T U) (Prod T' U) (Srt s2).

Lemma eq_conv_prod : forall e T T' U U' s1 s2,
  eq_typ e T T (Srt s1) ->
  eq_typ (T::e) U U (Srt s2) ->
  eq_conv e T T' (Srt s1) ->
  eq_conv (T :: e) U U' (Srt s2) ->
  eq_conv e (Prod T U) (Prod T' U') (Srt s2).

  Lemma eq_conv_abs_r : forall e T M M' U s1 s2,
    eq_typ e T T (Srt s1) ->
    eq_typ (T::e) U U (Srt s2) ->
    eq_conv (T::e) M M' U ->
    eq_conv e (Abs T M) (Abs T M') (Prod T U).

  Lemma eq_conv_abs_l : forall e T T' M U s1 s2,
    eq_conv e T T' (Srt s1) ->
    eq_typ (T::e) U U (Srt s2) ->
    eq_typ (T::e) M M U ->
    eq_conv e (Abs T M) (Abs T' M) (Prod T U).

  Lemma eq_conv_abs : forall e T T' M M' U s1 s2,
    eq_typ e T T (Srt s1) ->
    eq_typ (T::e) U U (Srt s2) ->
    eq_typ (T::e) M M U ->
    eq_conv e T T' (Srt s1) ->
    eq_conv (T::e) M M' U ->
    eq_conv e (Abs T M) (Abs T' M') (Prod T U).

Lemma eq_conv_app_r : forall e u v v' Ur V s1 s2,
  eq_typ e V V (Srt s1) ->
  eq_typ e u u (Prod V Ur) ->
  eq_typ (V::e) Ur Ur (Srt s2) ->
  eq_conv e v v' V ->
  eq_typ e v v V ->
  eq_conv e (App (Prod u Ur) v) (App (Prod u Ur) v') (subst v Ur).

Lemma eq_conv_app_m : forall e u v T Ur Ur' s1 s2,
  eq_typ e v v T ->
  eq_typ e T T (Srt s1) ->
  eq_conv (T::e) Ur Ur' (Srt s2) ->
  eq_typ e u u (Prod T Ur) ->
  eq_typ (T::e) Ur Ur (Srt s2) ->
  eq_conv e (App (Prod u Ur) v) (App (Prod u Ur') v) (subst v Ur).

Lemma eq_conv_app_l : forall e u u' v T Ur s1 s2,
  eq_typ e v v T ->
  eq_typ e T T (Srt s1) ->
  eq_typ (T::e) Ur Ur (Srt s2) ->
  eq_conv e u u' (Prod T Ur) ->
  eq_conv e (App (Prod u Ur) v) (App (Prod u' Ur) v) (subst v Ur).

Lemma eq_conv_app : forall e u u' v v' Ur Ur' V s1 s2,
  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) ->
  eq_conv e u u' (Prod V Ur) ->
  eq_conv e v v' V ->
  eq_conv (V :: e) Ur Ur' (Srt s2) ->
  eq_conv e (App (Prod u Ur) v) (App (Prod u' Ur') v') (subst v Ur).

Section Equivalence1.

  Fixpoint unmark_app (t:term) : term :=
    match t with
    | App (Prod u _) v => App (unmark_app u) (unmark_app v)
    | Abs T M => Abs (unmark_app T) (unmark_app M)
    | Prod T U => Prod (unmark_app T) (unmark_app U)
    | _ => t
    end.

  Definition unmark_env (e:env) : env := map unmark_app e.

  Lemma unmark_env_cons_inv : forall e1 T e,
    unmark_env e1 = T :: e ->
    exists2 T', unmark_app T' = T &
    exists2 e', unmark_env e' = e & e1 = T' :: e'.

  Lemma unmark_sort_inv : forall T s, unmark_app T = Srt s -> T = Srt s.

  Lemma unmark_prod_inv : forall T A B,
    unmark_app T = Prod A B ->
    exists2 A', unmark_app A' = A &
    exists2 B', unmark_app B' = B & T = Prod A' B'.

  Lemma unmark_lift : forall n t k,
    unmark_app (lift_rec n t k) = lift_rec n (unmark_app t) k.

  Lemma unmark_item_lift : forall t e n,
    item_lift t e n -> item_lift (unmark_app t) (unmark_env e) n.

  Lemma unmark_env_item : forall e e' n t,
    unmark_env e' = e ->
    item_lift t e n ->
    exists2 t', unmark_app t' = t & item_lift t' e' n.

  Lemma unmark_subst : forall N e M M' T,
    eq_typ e M M' T ->
    forall k,
    unmark_app (subst_rec N M k) = subst_rec (unmark_app N) (unmark_app M) k.
  Lemma unmark_subst0 : forall N e M M' T,
    eq_typ e M M' T ->
    unmark_app (subst N M) = subst (unmark_app N) (unmark_app M).
  Lemma unmark_subst2 : forall N e M M' T,
    eq_typ e M M' T ->
    forall k,
    unmark_app (subst_rec N M' k) = subst_rec (unmark_app N) (unmark_app M') k.

  Lemma eq_typ_par_red0 : forall e M M' T,
    eq_typ e M M' T -> par_red1 (unmark_app M) (unmark_app M').

  Lemma eq_typ_typ : forall e M M' T,
    eq_typ e M M' T ->
    typ (unmark_env e) (unmark_app M) (unmark_app T).

End Equivalence1.

Section CC_Is_Functional.

  Lemma sort_uniqueness : forall e M M1 M2 s1 s2,
    eq_typ e M M1 (Srt s1) ->
    eq_typ e M M2 (Srt s2) ->
    s1 = s2.

  Lemma eq_conv_sort_trans : forall e T U V s1 s2,
    eq_conv e T U (Srt s1) ->
    eq_conv e U V (Srt s2) ->
    eq_typ e T T (Srt s1) ->
    eq_conv e T V (Srt s1).

  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, T = Srt s \/ eq_typ e T T (Srt s).

  Definition inv_type (P : Prop) e t t' T :=
    match t with
    | Srt s1 => forall s,
        s1 = prop -> eq_conv e (Srt kind) T (Srt s) -> t' = (Srt s1) -> P
    | Ref n =>
        forall x s, item_lift x e n -> eq_conv e x T (Srt s) -> t' = Ref n -> P
    | Abs A M =>
        forall A' M' U U' s1 s2,
        eq_typ 8sPan class="id" type="variable">e A A' (Srt s1) ->
        eq_typ (A :: e) M M' U ->
        eq_typ (A :: e) U U' (Srt s2) ->
        eq_conv e (Prod A U) T (Srt s2) -> t' = Abs A' M' -> P
    | App (Prod u Ur) v =>
        forall u' v' Ur' V V' M M' U s1 s2,
        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) ->
        eq_typ (V::e) M M' U ->
        t' = App (Prod u' Ur') v' \/
        u=Abs V M /\ U = Ur /\ t' = subst v' M' ->
        eq_conv e (subst v Ur) T (Srt s2) -> P
    | Prod A B =>
        forall A' B' s1 s2 s,
        eq_typ e A A' (Srt s1) ->
        eq_typ (A :: e) B B' (Srt s2) ->
        eq_conv e (Srt s2) T (Srt s) -> t' = Prod A' B' -> P
    | _ => True
    end.

  Lemma inv_type_conv :
   forall P e t t' U V s, eq_conv e U V (Srt s) ->
   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.

  Lemma eq_typ_not_kind : forall e M M' T,
    eq_typ e M M' T ->
    M <> Srt kind.

  Lemma red_prod_prod_eq : forall e T U K,
    eq_red e T U K ->
    forall A B, T = Prod A B ->
    forall (P:Prop),
    (forall A' B' s1 s2, U = Prod A' B' ->
     eq_conv e A A' (Srt s1) -> eq_conv (A::e) B B' (Srt s2) -> P) -> P.

  Lemma red_prod_prod : forall e A B U K,
    eq_red e (Prod A B) U K ->
    forall (P:Prop),
    (forall A' B' s1 s2, U = Prod A' B' -> eq_conv e A A' (Srt s1) ->
     eq_conv (A::e) B B' (Srt s2) -> P) -> P.

  Lemma eq_typ_uniqueness :
    forall e M M' T',
    eq_typ e M M' T' ->
    forall M'' T'',
    eq_typ e M M'' T'' ->
    exists s, eq_conv e T' T'' (Srt s).

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

Lemma str_confl : forall e A B T,
   eq_typ e A B T ->
   forall e' A' B' T',
   eq_typ e' A' B' T' ->
   e = e' -> A = A' ->
   exists2 C, eq_typ e B C T & eq_typ e B' C T'.

  Lemma strip_lemma : forall e A B T,
   eq_red e A B T ->
   forall B',
   eq_typ e A B' T ->
   exists2 C, eq_red e B' C T & eq_typ e B C T.

  Lemma confluence : forall e A B T,
   eq_red e A B T=/spßn>8/a> ->
   forall B',
   
eq_red e A B' T ->
   exists2 C, eq_red e B' C T & eq_red e B C T.

  Lemma church_rosser : forall e M M' T,
    eq_conv e M M' T ->
    exists2 N, eq_red e M N T & eq_red e M' N T.

  Lemma inv_prod_l : forall e A B A' B' s3,
    eq_conv e (Prod A B) (Prod A' B') (Srt s3) ->
    exists s1, eq_conv e A A' (Srt s1).

  Lemma inv_prod_r : forall e A B A' B' s3,
    eq_conv e (Prod A B) (Prod A' B') (Srt s3) ->
    exists s2, eq_conv (A::e) B B' (Srt s2).


Inductive mpar_red1 : term -> term -> Prop :=
    par_beta : forall M M' N N' T U : term,
               mpar_red1 M M' ->
               mpar_red1 N N' ->
               mpar_red1 (App (Prod (Abs T M) U) N) (subst N' M')
  | sort_par_red : forall s, mpar_red1 (Srt s) (Srt s)
  | ref_par_red : forall n : nat, mpar_red1 (Ref n) (Ref n)
  | abs_par_red : forall M M' T T' : term,
                  mpar_red1 M M' ->
                  mpar_red1 T T' -> mpar_red1 (Abs T M) (Abs T' M')
  | app_par_red : forall M M' N N' U U' : term,
                  mpar_red1 M M' ->
                  mpar_red1 N N' ->
                  mpar_red1 U U' ->
                  mpar_red1 (App (Prod M U) N) (App (Prod M' U') N')
  | prod_par_red : forall M M' N N' : term,
                   mpar_red1 M M' ->
                   mpar_red1 N N' -> mpar_red1 (Prod M N) (Prod M' N').

Lemma mpar_red1_refl : forall e t t' u, eq_typ e t t' u -> mpar_red1 t t.

 Lemma subject_reduction :
    forall t u, mpar_red1 t u ->
    forall e t' T,
    eq_typ e t t' T ->
    eq_typ e t u T.

Lemma red1_mpar_red1 : forall e x x' T,
  eq_typ e x x' T ->
  forall y,
  par_red1 (unmark_app x) y ->
  exists2 y', mpar_red1 x y' & unmark_app y' = y.

  Lemma unmark_sr :
    forall e U U' T M',
    eq_typ e U U' T ->
    red (unmark_app U) M' ->
    exists2 M, unmark_app M = M' & eq_red e U M T.

  Lemma unmark_eq_conv : forall U V e U' V' T T',
    eq_typ e U U' T ->
    eq_typ e V V' T' ->
    unmark_app U = unmark_app V ->
    eq_conv e U V T.

  Lemma red_env_unmark_conv : forall e f,
    unmark_env e = unmark_env f ->
    wf e ->
    wf f ->
    clos_refl_trans _ red1_in_env e f.

  Lemma eq_typ_red_env_unmark : forall e f M M' T,
    unmark_env e = unmark_env f ->
    wf f ->
    eq_typ e M M' T ->
    eq_typ f M M' T.

  Lemma unmark_conv_sort : forall e U U' V V' s1 s2,
    eq_typ e U U' (Srt s1) ->
    eq_typ e V V' (Srt s2) ->
    conv (unmark_app U) (unmark_app V) ->
    eq_conv e U V (Srt s1).

  Lemma typ_eq_typ : forall e M T,
    typ e M T ->
    exists2 e', unmark_env e' = e &
    exists2 M', unmark_app M' = M &
    exists2 T', unmark_app T' = T &
    eq_typ e' M' M' T'.

End CC_Is_Functional.

End Typage.