```(*************************************************************************** * Calculus of Constructions - Subject Reduction * * Arthur Charguéraud, April 2007, Coq v8.1 * ***************************************************************************) Set Implicit Arguments. Require Import Metatheory CoC_Definitions CoC_Infrastructure CoC_Conversion. (* ********************************************************************** *) (** ** Inversion Lemmas for Subtyping *) 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. (* ********************************************************************** *) (** ** Inversion Lemmas for Typing *) 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. (* ********************************************************************** *) (** Typing preserved by Weakening *) 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. (* case: var *) apply* typing_var. apply* binds_weaken. (* case: trm_prod *) apply_fresh* (@typing_prod k) as y. apply_ih_bind* H0. (* case: trm_abs *) 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. (* ********************************************************************** *) (** ** Subtyping preserved by Substitution *) 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. (* ********************************************************************** *) (** Typing preserved by Substitution *) 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. (* case: trm_type *) auto*. (* case: var *) case_var. binds_get b. rewrite* subst_fresh. apply_empty* typing_weaken. binds_cases b. rewrite* subst_fresh. auto*. (* case: trm_prod *) apply_fresh* (@typing_prod k) as y. cross; auto. apply_ih_map_bind* H0. (* case: trm_abs *) apply_fresh* (@typing_abs i) as y. cross; auto. apply_ih_map_bind* H0. (* case: trm_app *) rewrite* subst_open. (* case: sub *) apply* (@typing_sub ([x ~> v]T0)). apply* less_red_out. (* case: wf nil *) contradictions. apply (eq_empty_inv H). (* case: wf cons *) destruct F as [|(y,a)]; simpls; env_fix. auto. destruct (eq_push_inv H0) as [e1 [e2 e3]]. subst. apply* (@wf_cons i). (* case: conclusion *) auto. Qed. (* ********************************************************************** *) (** Types are Themselves Well-typed *) 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. (* ********************************************************************** *) (** Typing preserved by Subtyping in Environment *) 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. (* ********************************************************************** *) (** Subject Reduction - Induction *) 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. (* case: trm_prod 1 *) apply_fresh* (@typing_prod k) as y. apply (@typing_sub_env (E & y ~ U)); eauto 7. (* case: trm_prod 2 *) apply_fresh* (@typing_prod k) as y. (* case: trm_abs 1 *) 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. (* case: trm_abs 2 *) apply_fresh* (@typing_abs i) as y. (* case: trm_app - beta reduction *) 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)). (* case: trm_app 1 *) auto*. (* case: trm_app 2 *) 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. (* ********************************************************************** *) (** Subject Reduction - Beta preserves typing *) Lemma subject_reduction_result : subject_reduction beta. Proof. introv Red Typ. apply* subject_reduction_ind. Qed. (* ********************************************************************** *) (** Subject Reduction - Beta Star preserves typing *) Lemma subject_reduction_star_result : subject_reduction (beta star). Proof. introv H. induction* H. apply* subject_reduction_result. Qed. ```