proposition: Lemma comp_step_comp : forall M N, Computable M -> M -R-> N -> Computable N.
proof: Proof. assert (forall A M N, type M = A -> Computable M -> M -R-> N -> Computable N). intro B. induction B. intros M N MT Mcomp MN. apply base_comp_step_comp with M; trivial. rewrite MT; auto with terms. intros M N Marr Mcomp MN. apply CompArrow. apply R_algebraic_preserving with M; trivial. apply comp_algebraic; trivial. rewrite <- (R_type_preserving MN), Marr; simpl; trivial. intros N'S N'S_app N'S_L N'S_Rnorm N'S_R. set (N' := appBodyL N'S_app) in * . set (S := appBodyR N'S_app) in * . destruct (terms_conv_sym N'S_L) as [Q NQN']. destruct (envSub_min_ex NQN') as [Q' [NQ'N' [Q'minN _]]]. destruct (term_build_conv_rel M (R_var_consistent MN) NQ'N') as [Q'' [Q''Q' [M' [MM' M'env]]]]; trivial. assert (N'S_M'_env: envSubset (env N'S) (env M')). rewrite <- (appBodyL_env N'S N'S_app); trivial. assert (N''S't: env M' |- term N'S := type N'S). apply typing_ext_env with (env N'S); trivial. exact (typing N'S). set (N''S' := buildT N''S't). assert (NS_conv: N'S ~ N''S'). apply terms_conv_criterion; trivial. simpl; apply env_subset_comp; trivial. set (N''S'_app := proj1 (isApp_morph NS_conv) N'S_app). set (SS' := app_conv_app_right N'S_app N''S'_app NS_conv); fold S in SS'. set (N'' := appBodyL N''S'_app) in * . set (S' := appBodyR N''S'_app) in * . set (typeMM' := terms_conv_eq_type (conv_by MM')). assert (M'S'_envOk: env M' = env S'). unfold S'; rewrite appBodyR_env; trivial. assert (M'S'_Marr: isArrowType (type M')). rewrite <- typeMM', Marr; simpl; trivial. assert (M'S'_typeOk: type_left (type M') = type S'). rewrite <- typeMM', (R_type_preserving MN), <- (terms_conv_eq_type N'S_L). set (w := app_conv_app_right N'S_app N''S'_app NS_conv). unfold S'; rewrite <- (terms_conv_eq_type w). term_inv N'S. set (M'S'_cond := Build_appCond M' S' M'S'_envOk M'S'_Marr M'S'_typeOk). set (M'S' := buildApp M'S'_cond). set (M'S'_app := buildApp_isApp M'S'_cond). set (M'S'_L := buildApp_Lok M'S'_cond). set (M'S'_R := buildApp_Rok M'S'_cond). assert (M'N': M' -R-> N''). apply R_conv_comp with M N Q''; trivial. apply terms_conv_diff_env with N'; trivial. apply terms_conv_extend_subst with Q'; trivial. unfold N', N''; apply term_appBodyL_eq; trivial. unfold N', N''. apply equiv_term_activeEnv. apply term_appBodyL_eq; trivial. rewrite !appBodyL_env. apply env_comp_sym; apply env_subset_comp; trivial. unfold N''; rewrite appBodyL_env; trivial. rewrite NS_conv. apply IHB2 with M'S'; unfold M'S'. rewrite buildApp_type; simpl. rewrite <- typeMM', Marr; trivial. apply CompCaseArrow with M' (buildApp_isApp M'S'_cond); trivial. assert (MeqM' : M ~ M') by (exists Q''; trivial). rewrite <- MeqM'; trivial. rewrite M'S'_R; simpl; trivial. rewrite <- (algebraic_morph SS'); trivial. rewrite M'S'_R; simpl; trivial. rewrite <- SS'; trivial. rewrite M'S'_L; apply terms_conv_refl. apply R_right_app_monotonous with M' N'' M'S'_app N''S'_app; trivial. rewrite <- (conv_by MM'). apply comp_algebraic; trivial. unfold M'S'_app; rewrite M'S'_R. simpl; rewrite <- SS'; trivial. intros. apply H with (type M) M; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)