proposition: Lemma cc_comp : forall E v V, cc gt1 f ls E v V -> forall s, (forall x, XSet.In x (fvs ls) -> s x = s0 x) -> (forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) -> int I V (subs s v).
proof: Proof. induction 1; intros s hs1 hs2. rewrite <- Vnth_map with (f:=subs s). apply vint_elim_nth. assert (a : Vmap (subs s) ls = Vmap (subs s0) ls). apply Vmap_eq. apply Vforall_intro. intros lj hj. destruct (Vin_nth hj) as [j [j1 j2]]. subst lj. apply subs_seq. intros x hx. apply hs1. eapply In_fvs_Vnth. apply hx. rewrite a, hls. apply vint_sub_term_intro. hyp. apply hs2; hyp. simpl. apply IHcc1. hyp. hyp. apply IHcc2. hyp. hyp. gen (cp_int I_cp A). intros [A1 A2 A3 A4]. gen (cp_int I_cp B). intros [B1 B2 B3 B4]. simpl. apply cp_lam; class. intros a ha. rewrite subs_comp, single_update_var. eapply IHcc. intros y hy. unfold Def.update. eq_dec y x. subst. contr. apply hs1. hyp. intros z Z. simpl. rewrite add_mapsto_iff. intros [[h1 h2]|[h1 h2]] i; subst. rewrite update_eq. hyp. rewrite update_neq. apply hs2; hyp. hyp. rewrite <- Vnth_map with (f:=subs s). apply comp_acc. replace (Fun g) with (subs s (Fun g)). 2: refl. rewrite <- subs_apps. apply IHcc; hyp. rewrite subs_apps. simpl. assert (e : Vmap (subs s0) ls = Vmap (subs s) ls). apply Vmap_eq. apply Vforall_intro. intros y hy. destruct (Vin_nth hy) as [i [i1 i2]]. subst y. apply subs_seq. intros z hz. sym. apply hs1. eapply In_fvs_Vnth. apply hz. apply int_arrow with (n := arity (typ g) - p). rewrite arity_output. refl. intros vs hvs. rewrite output_output. assert (pg : p + (arity (typ g) - p) = arity (typ g)). lia. rewrite pg, apps_apps, <- apps_cast with (h:=pg). apply IH. rewrite (Veq_app ts h). assert (nf : n + (arity (typ f) - (0 + n)) = arity (typ f)). lia. eapply gt2_mcaeq with (x := mk_max_call f (Vcast (Vapp (Vmap (subs s) ls) (Vsub ts (Veq_app_aux2 h))) nf)). 2: refl. apply caeq_intro. rewrite Vforall2_cast. apply Vforall2_intro_nth. intros i hi. rewrite !Vnth_app. simpl. destruct (le_gt_dec n i). refl. apply Vforall2_elim_nth. rewrite <- e, (Vsub_pi h). hyp. eapply gt2_gt1; auto. apply H0. apply vint_app_intro with (h := Veq_app_aux2 h). rewrite <- e, hls. apply vint_sub_term_intro. hyp. apply vint_sub_intro. hyp. refl. hyp. rewrite vint_cast_term. clear pg. assert (pg : p + (arity (typ g) - p) <= arity (typ g)). lia. apply vint_app_intro with (h := pg). apply vint_intro_nth. lia. intros j jn jp. rewrite Vnth_map. apply H2; hyp. apply vint_eq. refl. intros j jn jp. rewrite Vnth_sub. assert (k : j < arity (output (typ g) p)). rewrite arity_output. hyp. assert (a : Vnth (inputs (typ g)) (Vnth_sub_aux p pg jn) = Vnth (inputs (output (typ g) p)) k). sym. simpl in H. rewrite inputs_output with (h:=H), Vnth_sub. apply Vnth_eq. refl. setoid_rewrite a. apply vint_elim_nth. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)