proposition: Lemma comp_prop : forall A, ( forall M, type M = A -> Computable M -> AccR M ) /\ ( forall P, type P = A -> algebraic P -> isNeutral P -> (forall S, P -R-> S -> Computable S) -> Computable P).
proof: Proof. intro B. induction B. split. intros M MT Mcomp. apply CompCaseBasic; trivial. rewrite MT; auto with terms. intros P Pbase Pnorm Pneutral PScomp. assert (P_base: isBaseType (type P)). rewrite Pbase; auto with terms. apply CompBasic; trivial. constructor. intros S RS. apply CompCaseBasic. apply PScomp; trivial. apply base_step_base with P; trivial. destruct IHB1 as [IH_L1 IH_L2]. destruct IHB2 as [IH_R1 IH_R2]. split. intros M Marr Mcomp. destruct (apply_var_comp M Mcomp Marr) as [Mx [Mx_app [MxL [_ [_ Mxcomp]]]]]; trivial. rewrite <- MxL. apply acc_app_acc_L; trivial. rewrite MxL; apply comp_algebraic; trivial. apply algebraic_appBodyR. apply comp_algebraic; trivial. apply IH_R1; trivial. apply app_typeL_type with B1 Mx_app; trivial. rewrite <- terms_conv_eq_type with M (appBodyL Mx_app); trivial. apply terms_conv_sym; trivial. intros P Parr Palg Pneutral PScomp. apply CompArrow; trivial. rewrite Parr; simpl; trivial. intros N Napp NL NRnorm NR. assert (Hyp: forall W, Computable W -> type W = B1 -> forall N (Napp: isApp N), (appBodyL Napp) ~ P -> appBodyR Napp = W -> Computable N ). intros W Wcomp Wtyp. assert (Wacc: Acc (transp R) W). apply IH_L1; trivial. cut (type W = B1); trivial. cut (Computable W); trivial. cut (algebraic P); trivial. apply Acc_rect with (R := transp R)(P := fun W => algebraic P -> Computable W -> type W = B1 -> forall N (Napp: isApp N), (appBodyL Napp) ~ P -> appBodyR Napp = W -> Computable N ); trivial. clear N NRnorm Napp NL NR W Wcomp Wtyp Wacc. intros W _ IH Pnorm Wcomp Wtype N Napp NL NR. apply IH_R2; trivial. apply app_typeL_type with B1 Napp; trivial. rewrite (terms_conv_eq_type NL); trivial. apply algebraic_app with Napp. rewrite NL; trivial. rewrite NR; apply comp_algebraic; trivial. apply app_neutral; trivial. intros S NS. destruct (R_app_reduct (N:=S) Napp) as [NLabs_red | [Sapp [[Leq Rgt] | [[Lgt Req] | [Lgt Rgt]]]]]; trivial. left. apply algebraic_app_notFunApp with Napp. rewrite NL; trivial. rewrite NR; apply comp_algebraic; trivial. destruct NLabs_red. absurd (isAbs P); trivial. rewrite <- NL; trivial. apply IH with (appBodyR Sapp) Sapp; trivial. unfold transp; simpl. rewrite <- NR; trivial. apply comp_step_comp with (appBodyR Napp); trivial. rewrite NR; trivial. rewrite <- (R_type_preserving Rgt), NR; trivial. rewrite <- Leq; trivial. apply comp_app with Sapp. destruct (R_conv_to (M':=P) Lgt NL) as [S' [PS' SLS']]. rewrite SLS'. apply PScomp; trivial. rewrite <- Req, NR; trivial. apply comp_app with Sapp. destruct (R_conv_to (M':=P) Lgt NL) as [S' [PS' SLS']]. rewrite SLS'. apply PScomp; trivial. apply comp_step_comp with W; trivial. rewrite <- NR; trivial. apply Hyp with (appBodyR Napp) Napp; trivial. apply app_typeR with B2. rewrite (terms_conv_eq_type NL); trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)