proposition: Lemma comp_abs : forall M (Mabs: isAbs M), algebraic M -> (forall G (cs: correct_subst (absBody Mabs) G) T, isSingletonSubst T G -> Computable T -> Computable (subst cs)) -> Computable M.
proof: Proof. intros M Mabs Mnorm H. apply CompArrow; trivial. term_inv M. intros W Wapp WL WRnorm WR. assert (WLabs: isAbs (appBodyL Wapp)). rewrite WL; trivial. set (TL := absBody WLabs). set (TR := appBodyR Wapp). assert (M0: env (absBody Mabs) |= 0 := absType Mabs). term_inv M. assert (TLC: Computable (absBody WLabs)). set (idS1 := idSubst_correct (absBody Mabs)). simpl; setoid_replace (absBody WLabs) with (subst (idS1)) using relation terms_conv. set (S1eqS2 := idSubst_decl0 (absBody Mabs) M0). assert (idS2 : correct_subst (absBody Mabs) {x/buildT (TVar M0)}). rewrite <- S1eqS2; trivial. replace (subst idS1) with (subst (idS2)). apply H with (buildT (TVar M0)). apply singletonSubst_cond. apply var_comp; simpl; trivial. apply term_eq. rewrite !subst_env, S1eqS2; trivial. rewrite !subst_term, S1eqS2; trivial. unfold idS1; rewrite (idSubst_neutral (absBody (M:=M) Mabs)). apply abs_conv_absBody; trivial. set (PL := exist TLC). set (PR := exist WR). apply comp_abs_ind with (Wapp := Wapp) (WLabs := WLabs) (P := (PL, PR)); trivial. intros. destruct WL. set (WLM := abs_conv_absBody_aux WLabs Mabs H2). destruct (isVarDecl_dec (activeEnv (absBody WLabs)) 0) as [[B DB] | ND]. destruct (envSub_min_ex WLM) as [Q [Qconv [Qmin Qext]]]. assert (Q00: envSub Q 0 0). destruct (terms_conv_activeEnv Qconv DB). assert (x0 = 0). apply envSub_Lok with (envSubst_lift1 x) 0. apply (Qext 0 x0); trivial. destruct x; simpl; trivial. rewrite H4 in H3; trivial. destruct (conv_subst_singleton_build Q00 Qconv Qmin H0 cs) as [Q' [G' [T' [MG' [T'G' [Q'Q GG']]]]]]. set (Conv := conv_subst_conv cs MG' (terms_conv_extend_subst Qconv Q'Q) GG'). assert (Conv' : terms_conv (subst cs) (subst MG')) by (exists Q'; trivial). rewrite Conv'. apply H with T'; trivial. setoid_replace T' with T using relation terms_conv; trivial. apply terms_conv_sym; exists Q'; trivial. apply singletonSubst_conv with G G'; trivial. rewrite <- (uneffective_singleton_subst_conv cs H0 ND); trivial. apply algebraic_app with Wapp; trivial. rewrite WL; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)