proposition: Lemma singleton_subst_activeEnv_subst_aux : forall M T i A (MG: correct_subst M (copy i None ++ Some T :: nil)), (activeEnv M |= i := A) -> activeEnv (subst MG) [=] (initialSeg (activeEnv M) i ++ None :: finalSeg (activeEnv M) (S i)) [+] activeEnv T.
proof: Proof. destruct M as [E Pt T M]; induction M; intros. simpl in H. destruct (lt_eq_lt_dec x i) as [[x_i | xi] | i_x]. exfalso; apply varD_UD_absurd with (copy x None ++ A[#]EmptyEnv) i A0; trivial. constructor; apply nth_beyond. autorewrite with datatypes using simpl; try lia. rewrite (@activeEnv_var (buildT (TVar v)) x); trivial. rewrite (equiv_term_activeEnv (subst MG) T). simpl. assert (ES: envSubset (initialSeg (copy x None ++ A[#]EmptyEnv) i ++ None :: finalSeg (copy x None ++ A[#]EmptyEnv) (S i)) (activeEnv T)). rewrite xi. apply env_eq_empty_subset. rewrite (@initialSeg_app (option SimpleType) (copy i None) (A[#]EmptyEnv) i). rewrite finalSeg_app_right; autorewrite with datatypes using auto. replace (S i - i) with 1; [idtac | lia]. unfold finalSeg; simpl. rewrite initialSeg_full. change ((None (A:=SimpleType)) :: nil) with (copy 1 (None (A:=SimpleType))). rewrite <- copy_split. apply env_eq_empty. intro w. destruct (le_gt_dec (i + 1) w). left; apply nth_beyond; autorewrite with datatypes using trivial. right; apply nth_copy_in; trivial. autorewrite with datatypes using auto. autorewrite with datatypes using auto. rewrite <- (env_eq_subset_sum_l ES); auto with terms. autorewrite with terms. unfold presubst; simpl. rewrite xi. rewrite nth_app_right; autorewrite with datatypes; auto. replace (i - i) with 0; [idtac | lia]. simpl; rewrite lift_0; trivial. apply subst_env_compat with i. unfold varSubstTo; apply nth_after_copy. exfalso; apply varD_UD_absurd with (copy x None ++ A[#]EmptyEnv) i A0; trivial. unfold VarUD; rewrite nth_app_left; autorewrite with datatypes using auto. rewrite activeEnv_funS in H; simpl; trivial. destruct i; try_solve. rewrite (activeEnv_abs (buildT (TAbs M)) I). rewrite (activeEnv_abs (subst MG) (abs_subst_abs (M:=buildT (TAbs M))I MG)). destruct (abs_subst (M:=buildT (TAbs M)) I MG). rewrite H1. set (IHyp := IHM (lift T 1) (S i) A0). replace (copy (S i) None ++ {x/lift T 1}) with (None :: lift_subst (copy i None ++ {x/T}) 1) in IHyp. simpl. set (w := IHyp (subst_abs_c (M:=buildT (TAbs M)) I MG)). apply env_eq_trans with (tail ((initialSeg (activeEnv (buildT M)) (S i) ++ None :: finalSeg (activeEnv (buildT M)) (S (S i))) [+] activeEnv (lift T 1))). apply env_eq_tail. apply IHyp. apply varD_tail_rev; trivial. apply env_eq_trans with (tail ((initialSeg (activeEnv (buildT M)) (S i) ++ None :: finalSeg (activeEnv (buildT M)) (S (S i))) [+] liftedEnv 1 (activeEnv T) 0)). apply env_eq_tail. rewrite (activeEnv_lift T 1); apply env_eq_refl. set (envM := activeEnv (buildT M)). set (envT := activeEnv T). rewrite tail_distr_sum. simpl; autorewrite with datatypes using simpl. destruct envM; simpl. destruct envT; destruct i; simpl; autorewrite with datatypes; unfold finalSeg; simpl. apply env_eq_empty_none_empty. apply env_eq_empty_none_empty. destruct o; destruct envT; auto with terms. destruct o; destruct envT; auto with terms. auto with terms. rewrite lift_subst_app. rewrite lift_empty_subst; trivial. rewrite (activeEnv_app (buildT (TApp M1 M2)) I). rewrite (activeEnv_app (subst MG) (app_subst_app (M:=buildT (TApp M1 M2)) I MG)). destruct (app_subst (M := buildT (TApp M1 M2)) I MG). simpl; rewrite (@activeEnv_app (buildT (TApp M1 M2)) I) in H. unfold appBodyL, appBodyR in H; cbv beta in H. set (AE1 := activeEnv (buildT M1)) in * . set (AE2 := activeEnv (buildT M2)) in * . assert (forall j, j <> i -> env_comp_on (env T) E j). clear H0; clear H1; destruct MG. rewrite subst_ran_single_after_empty in ran_c0. simpl in ran_c0. intros; intros C D Tj Ej. apply (ran_c0 j); trivial. apply env_sub_ly_rn; trivial. apply subst_dom_singleton_after_none_nodecl; lia. assert (forall j, j <> i -> env_comp_on (activeEnv T) AE1 j). intros. apply env_comp_on_subset with (env T) E. apply H2; trivial. apply activeEnv_subset. unfold AE1; change E with (env (appBodyL (M:=buildT (TApp M1 M2)) I)). apply activeEnv_subset. assert (forall j, j <> i -> env_comp_on (activeEnv T) AE2 j). intros. apply env_comp_on_subset with (env T) E. apply H2; trivial. apply activeEnv_subset. unfold AE2; change E with (env (appBodyR (M:=buildT (TApp M1 M2)) I)). apply activeEnv_subset. assert (activeEnv T [<->] initialSeg AE1 i ++ None :: finalSeg AE1 (S i)). intro p. destruct (eq_nat_dec p i). intros C D _ F. exfalso; apply varD_UD_absurd with (initialSeg AE1 i ++ None :: finalSeg AE1 (S i)) p D; trivial. rewrite e; apply varUD_hole. apply env_comp_on_subset with (activeEnv T) AE1. apply H3; trivial. apply env_subset_refl. apply env_hole_subset. assert (activeEnv T [<->] initialSeg AE2 i ++ None :: finalSeg AE2 (S i)). intro p. destruct (eq_nat_dec p i). intros C D _ F. exfalso; apply varD_UD_absurd with (initialSeg AE2 i ++ None :: finalSeg AE2 (S i)) p D; trivial. rewrite e; apply varUD_hole. apply env_comp_on_subset with (activeEnv T) AE2. apply H4; trivial. apply env_subset_refl. apply env_hole_subset. assert (AE1 [<->] AE2). unfold AE1, AE2. change (buildT M1) with (appBodyL (M:=buildT (TApp M1 M2)) I). change (buildT M2) with (appBodyR (M:=buildT (TApp M1 M2)) I). apply activeEnv_app_comp. assert (forall (j : nat) (A : SimpleType), j <> i -> ((initialSeg AE1 i ++ None :: finalSeg AE1 (S i)) |= j := A <-> AE1 |= j := A)). intros; split; intro. apply varD_hole_rev with i; [lia | trivial]. apply varD_hole; [lia | trivial]. assert (forall (j : nat) (A : SimpleType), j <> i -> ((initialSeg AE2 i ++ None :: finalSeg AE2 (S i)) |= j := A <-> AE2 |= j := A)). intros; split; intro. apply varD_hole_rev with i; [lia | trivial]. apply varD_hole; [lia | trivial]. destruct (env_sum_varDecl AE1 AE2 H) as [[MLi MRi] | MRi]. rewrite H0. simpl; rewrite (IHM1 T i A0 (subst_appL_c (M:=buildT (TApp M1 M2)) I MG) MLi). rewrite H1. rewrite <- (singleton_subst_activeEnv_noSubst_aux T (subst_appR_c (M:=buildT (TApp M1 M2)) I MG) MRi). apply singleton_subst_active_aux; trivial. simpl; unfold AE2; split; auto. apply varUD_hole. rewrite H1. simpl; rewrite (IHM2 T i A0 (subst_appR_c (M:=buildT (TApp M1 M2)) I MG) MRi). rewrite H0. destruct (isVarDecl_dec AE1 i) as [[A1 MLi] | MLn]. assert (A01: A1 = A0). apply (@activeEnv_app_comp (buildT (TApp M1 M2)) I i); trivial. rewrite A01 in MLi. simpl; rewrite (IHM1 T i A0 (subst_appL_c (M:=buildT (TApp M1 M2)) I MG) MLi). rewrite env_comp_sum_comm with (initialSeg AE2 i ++ None :: finalSeg AE2 (S i)) (activeEnv T). rewrite env_sum_assoc. rewrite <- env_sum_assoc with (activeEnv T) (activeEnv T) (initialSeg AE2 i ++ None :: finalSeg AE2 (S i)). rewrite env_sum_double. rewrite <- env_sum_assoc. apply singleton_subst_active_aux; trivial. apply varUD_hole. apply varUD_hole. apply env_comp_sym; trivial. rewrite <- (singleton_subst_activeEnv_noSubst_aux T (subst_appL_c (M:=buildT (TApp M1 M2)) I MG) MLn). rewrite env_comp_sum_comm with (initialSeg AE2 i ++ None :: finalSeg AE2 (S i)) (activeEnv T). rewrite <- env_sum_assoc. apply singleton_subst_active_aux; trivial. simpl; unfold AE1; split; auto. apply varUD_hole. apply env_comp_sym; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)