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