Set Implicit Arguments.
Require Import Metatheory CoC_Definitions CoC_Infrastructure CoC_Conversion.
Lemma less_type_any_inv : forall T1 T2,
less T1 T2 -> forall i1, conv T1 (trm_type i1) ->
exists i2, i1 <= i2 /\ conv T2 (trm_type i2).
Proof.
induction 1; intros i1 C1.
exists* i1.
puts (conv_type_type_inv C1). subst. exists* j.
contradictions. apply (conv_type_prod_inv (equiv_sym C1)).
exists* i1.
destruct (IHless1 _ C1) as [i2 [Le2 C2]].
destruct (IHless2 _ C2) as [i3 [Le3 C3]].
exists i3. use (Le.le_trans i1 i2 i3).
Qed.
Lemma less_type_type_inv : forall i j,
less (trm_type i) (trm_type j) -> i <= j.
Proof.
introv Le.
destruct (@less_type_any_inv _ _ Le i) as [i' [Lei C]]. auto.
puts (conv_type_type_inv C). subst*.
Qed.
Lemma less_prod_any_inv : forall P1 P2,
less P1 P2 -> forall U1 T1, conv P1 (trm_prod U1 T1) ->
exists U2, exists T2, conv P2 (trm_prod U2 T2)
/\ conv U1 U2
/\ exists L, forall x, x \notin L -> less (T1 ^ x) (T2 ^ x).
Proof.
induction 1; intros U1 T1 C1.
exists U1 T1.
asserts* K (term (trm_prod U1 T1)). inversions K.
splits.
apply* (@equiv_trans beta t1).
auto.
exists_fresh. auto.
contradictions. apply (conv_type_prod_inv C1).
exists U' T'. asserts* K (less (trm_prod U T) (trm_prod U' T')).
destruct (conv_prod_prod_inv C1) as [C11 [L1 C12]].
splits.
auto.
apply* (@equiv_trans beta U).
exists_fresh. intros. apply (@less_trans (T ^ x)).
forward* (C12 x). auto.
exists U1 T1. asserts* K (term (trm_prod U1 T1)). inversions* K.
destruct (IHless1 _ _ C1) as [U2 [T2 [C2 [C21 [L2 C22]]]]].
destruct (IHless2 _ _ C2) as [U3 [T3 [C3 [C31 [L3 C32]]]]].
exists U3 T3. splits.
auto.
apply* (@equiv_trans beta U2).
exists_fresh. intros. apply* (@less_trans (T2 ^ x)).
Qed.
Lemma less_prod_prod_inv : forall U1 T1 U2 T2,
less (trm_prod U1 T1) (trm_prod U2 T2) ->
conv U1 U2
/\ exists L, forall x, x \notin L -> less (T1 ^ x) (T2 ^ x).
Proof.
introv Le.
destruct (@less_prod_any_inv _ _ Le U1 T1)
as [U2' [T2' [C [C1' [L' C2']]]]]; auto.
destruct (conv_prod_prod_inv C) as [C1 [L C2]].
splits.
apply* (@equiv_trans beta U2').
exists_fresh. intros. apply (@less_trans (T2' ^ x)).
auto.
forward* (C2 x).
Qed.
Lemma typing_prod_inv : forall E U T P,
typing E (trm_prod U T) P -> exists i, exists k,
less (trm_type i) P
/\ typing E U (trm_type k)
/\ (i = k \/ i = 0)
/\ exists L, forall x, x \notin L -> typing (E & x ~ U) (T ^ x) (trm_type i).
Proof.
introv Typ. gen_eq (trm_prod U T) as P1.
induction Typ; intros; subst; try solve [contradictions].
inversions H2. exists* i k.
destructi~ IHTyp1 as [i' [k' [EQi [TypU [Univ [L TypT]]]]]].
exists i' k'. use (@less_trans T0).
Qed.
Lemma typing_abs_inv : forall E V t P,
typing E (trm_abs V t) P -> exists T, exists i,
typing E (trm_prod V T) (trm_type i)
/\ less (trm_prod V T) P
/\ exists L, forall x, x \notin L -> typing (E & x ~ V) (t ^ x) (T ^ x).
Proof.
introv Typ. gen_eq (trm_abs V t) as u.
induction Typ; intros; subst; try solve [contradictions].
inversions H1. exists* T i.
destructi~ IHTyp1 as [T' [i' [TypP [LeP [L TypB]]]]].
exists T' i'. use (@less_trans T).
Qed.
Lemma typing_prod_type_inv : forall E U T i,
typing E (trm_prod U T) (trm_type i) ->
exists L, forall x, x \notin L ->
typing (E & x ~ U) (T ^ x) (trm_type i).
Proof.
introv Typ.
destruct (typing_prod_inv Typ) as [i' [k' [Le [TypU [Uni [L TypT]]]]]].
exists (L \u dom E). intros.
inversion Le; apply* (@typing_sub (trm_type i') (i+1)).
Qed.
Lemma typing_weaken : forall G E F t T,
typing (E & G) t T ->
wf (E & F & G) ->
typing (E & F & G) t T.
Proof.
introv Typ. gen_eq (E & G) as Env. gen G.
induction Typ; introv EQ W; subst; eauto.
apply* typing_var. apply* binds_weaken.
apply_fresh* (@typing_prod k) as y. apply_ih_bind* H0.
apply_fresh* (@typing_abs i) as y.
destructi (IHTyp G) as TypP; auto.
destruct (typing_prod_inv TypP) as [i' [k' [_ [TypU _]]]].
apply_ih_bind* H0.
Qed.
Lemma less_red_out : red_out less.
Proof.
introz. puts conv_red_out; induction H0; simpl; auto.
apply_fresh* less_prod as y. cross*.
apply* (@less_trans ([x ~> u]U)).
Qed.
Lemma typing_substitution : forall V F v E x t T,
typing E v V ->
typing (E & x ~ V & F) t T ->
typing (E & (map (subst x v) F)) (subst x v t) (subst x v T).
Proof.
introv Typv Typt.
gen_eq (E & x ~ V & F) as G. gen F.
apply typing_induct with
(P := fun G t T (Typt : typing G t T) =>
forall F, G = E & x ~ V & F ->
typing (E & map (subst x v) F) ([x ~> v]t) ([x ~> v]T))
(P0 := fun G (W:wf G) =>
forall F, G = E & x ~ V & F ->
wf (E & (map (subst x v) F)));
intros; subst; simpls subst.
auto*.
case_var.
binds_get b.
rewrite* subst_fresh. apply_empty* typing_weaken.
binds_cases b.
rewrite* subst_fresh.
auto*.
apply_fresh* (@typing_prod k) as y.
cross; auto. apply_ih_map_bind* H0.
apply_fresh* (@typing_abs i) as y.
cross; auto. apply_ih_map_bind* H0.
rewrite* subst_open.
apply* (@typing_sub ([x ~> v]T0)). apply* less_red_out.
contradictions. apply (eq_empty_inv H).
destruct F as [|(y,a)]; simpls; env_fix.
auto.
destruct (eq_push_inv H0) as [e1 [e2 e3]].
subst. apply* (@wf_cons i).
auto.
Qed.
Lemma typing_wf_from_context : forall x U E,
binds x U E ->
wf E ->
exists i, typing E U (trm_type i).
Proof.
introv B W. induction E as [|(y,a)]; env_fix.
inversion B.
inversions B. inversions W. case_var.
inversions H0. exists i. apply_empty* typing_weaken.
destructi~ IHE as [k P]. exists k. apply_empty* typing_weaken.
Qed.
Lemma typing_wf_from_typing : forall E t T,
typing E t T ->
exists i, typing E T (trm_type i).
Proof.
induction 1.
exists* ((i+1)+1).
destruct* (typing_wf_from_context H0).
exists* (i+1).
exists* i.
destruct IHtyping1 as [i Typ].
destruct (typing_prod_inv Typ) as [i' [k' [Le [TypU [Uni [L TypT]]]]]].
exists i'.
pick_fresh x. rewrite~ (@subst_intro x).
unsimpl ([x ~> u](trm_type i')).
apply_empty* (@typing_substitution U).
exists* i.
Qed.
Inductive env_less : env -> env -> Prop :=
| env_less_head : forall E U U' x,
less U U' ->
env_less (E & x ~ U) (E & x ~ U')
| env_less_tail : forall E E' x U,
term U -> env_less E E' -> env_less (E & x ~ U) (E' & x ~ U).
Hint Constructors env_less.
Lemma env_less_binds : forall x U E E',
env_less E' E -> wf E -> wf E' -> binds x U E ->
binds x U E'
\/ exists U', exists i,
binds x U' E' /\ less U' U /\ typing E' U (trm_type i).
Proof.
induction 1; intros WfE WfE' Has;
unfolds binds; simpls; case_var; env_fix.
right. inversions Has. inversions WfE. exists U0 i.
splits. auto. apply_empty* typing_weaken.
left*.
left*.
inversions WfE. inversions WfE'.
destruct~ IHenv_less as [|[U' [i' [P1 [P2 P3]]]]].
right. exists U' i'. splits; auto. apply_empty* typing_weaken.
Qed.
Lemma typing_sub_env : forall E E' t T,
typing E t T ->
env_less E' E ->
wf E' ->
typing E' t T.
Proof.
introv Typ. gen E'. induction Typ; intros E' C W; eauto.
destruct (env_less_binds C H W H0) as [B |[U' [i [B [Le Typ]]]]].
apply* typing_var.
apply* (@typing_sub U' i).
apply_fresh (@typing_prod k) as y; auto. apply* (H0 y).
destructi~ (IHTyp E') as TypP.
destruct (typing_prod_inv TypP) as [i' [k [_ [Typt1 _]]]].
apply_fresh (@typing_abs i) as y; auto. apply* (H0 y).
Qed.
Lemma subject_reduction_ind : forall E t t' T,
typing E t T -> beta t t' -> typing E t' T.
Proof.
introv Typ. gen t'.
induction Typ; introv Red;
try solve [ apply* typing_sub ]; inversions Red.
apply_fresh* (@typing_prod k) as y.
apply (@typing_sub_env (E & y ~ U)); eauto 7.
apply_fresh* (@typing_prod k) as y.
destructi~ (IHTyp (trm_prod t1' T)) as Typt1'T.
destruct (typing_prod_type_inv Typt1'T) as [L2 TypT].
apply* (@typing_sub (trm_prod t1' T) i).
apply_fresh less_prod as y.
auto.
forward* (H y).
apply_fresh* (@typing_abs i) as y.
forward~ (TypT y) as K.
apply (@typing_sub_env (E & y ~ U)); eauto 7.
apply_fresh* (@typing_abs i) as y.
destruct (typing_abs_inv Typ1) as [T' [i [TypP [LeP [L1 Typt2]]]]].
destruct (typing_prod_inv TypP) as [i' [k [EQi [Typt1 [Uni [L2 TypT']]]]]].
destruct (less_prod_prod_inv LeP) as [C [L3 LeT]].
destruct (typing_wf_from_typing Typ1) as [j TypUT].
destruct (typing_prod_type_inv TypUT) as [L4 TypT].
pick_fresh x.
rewrite* (@subst_intro x t2).
rewrite* (@subst_intro x T).
apply_empty (@typing_substitution t1).
apply* (@typing_sub U k).
apply (@typing_sub (T' ^ x) j); auto.
apply* (@typing_sub_env (E & x ~ U)).
auto*.
destruct (typing_wf_from_typing Typ1) as [i TypUT].
destruct (typing_prod_type_inv TypUT) as [L TypT].
apply* (@typing_sub (T ^^ t2') i).
apply less_conv. apply* conv_from_open_beta.
pick_fresh x. rewrite* (@subst_intro x T).
unsimpl (subst x u (trm_type i)).
apply_empty* (@typing_substitution U).
Qed.
Lemma subject_reduction_result : subject_reduction beta.
Proof.
introv Red Typ. apply* subject_reduction_ind.
Qed.
Lemma subject_reduction_star_result :
subject_reduction (beta star).
Proof.
introv H. induction* H. apply* subject_reduction_result.
Qed.