proposition: Lemma comp_abs_ind : forall (P: CompTerm * CompTerm) W (Wapp: isApp W) (WLabs: isAbs (appBodyL Wapp)), (forall G (cs: correct_subst (absBody WLabs) G) T, isSingletonSubst T G -> Computable T -> Computable (subst cs)) -> algebraic W -> absBody WLabs = proj1_sig (fst P) -> appBodyR Wapp = proj1_sig (snd P) -> Computable W.
proof: Proof. intro P. apply well_founded_ind with (R := TermsPairLex) (P := fun (P: CompTerm * CompTerm) => forall W (Wapp: isApp W) (WLabs: isAbs (appBodyL Wapp)), (forall G (cs: correct_subst (absBody WLabs) G) T, isSingletonSubst T G -> Computable T -> Computable (subst cs) ) -> algebraic W -> absBody WLabs = proj1_sig (fst P) -> appBodyR Wapp = proj1_sig (snd P) -> Computable W ). unfold TermsPairLex. eapply lexprod_wf; try solve [ eexact SetTheory_Comp | unfold R_Comp; intros x x' y y' xx' yy' xy; inversion xx'; inversion yy'; trivial | apply well_founded_R_comp ]; try apply R_Comp_morph. clear P; intros P IH W Wapp WLabs WL_Hyp Wnorm PL PR. assert (WLnorm: algebraic (appBodyL Wapp)). apply algebraic_appBodyL; trivial. unfold isFunApp; intro WFapp. rewrite (appHead_app W Wapp), (appHead_notApp (appBodyL Wapp) (abs_isnot_app (appBodyL Wapp) WLabs)) in WFapp. term_inv (appBodyL Wapp). assert (WRnorm: algebraic (appBodyR Wapp)). apply algebraic_appBodyR; trivial. rewrite_rl (neutral_comp_step Wnorm (app_neutral W Wapp)). intros W' WW'. destruct P as [[PLT PLC] [PRT PRC]]; simpl in * . destruct (R_app_reduct (N:=W') Wapp) as [[W'abs W'beta] | [W'app [[W'L_eq W'R_red] | [[W'L_red W'R_eq] | [W'L_red W'R_red]]]]]; trivial. left; apply funAbs_notFunApp. rewrite (appHead_app W Wapp), appHead_notApp; trivial. term_inv (appBodyL Wapp). rewrite W'beta, <- (Computable_morph (terms_lower_conv (subst (beta_subst W Wapp W'abs)) (beta_lowering W Wapp W'abs))), (abs_proof_irr (appBodyL Wapp) W'abs WLabs). apply WL_Hyp with (lift (appBodyR Wapp) 1). apply singletonSubst_cond. apply comp_lift_comp. rewrite PR; trivial. assert (W'Labs: isAbs (appBodyL W'app)). rewrite <- W'L_eq; trivial. set (WL_W'L := absBody_eq WLabs W'Labs W'L_eq). assert (W'Lcomp: Computable (absBody W'Labs)). rewrite <- WL_W'L, PL; trivial. assert (W'Rcomp: Computable (appBodyR W'app)). apply comp_step_comp with (appBodyR Wapp); trivial. rewrite PR; trivial. set (P'L := exist W'Lcomp). set (P'R := exist W'Rcomp). apply (IH (P'L, P'R)) with W'app W'Labs; trivial. constructor 2. unfold CompTerm_eq; simpl. rewrite <- PL; trivial. unfold R_Comp; simpl; rewrite <- PR; trivial. intros G cs T GT Tcomp. assert (cs': correct_subst (absBody WLabs) G). destruct cs; constructor; try solve [ trivial | rewrite (absBody_eq WLabs W'Labs); trivial ]. replace (subst cs) with (subst cs'). apply WL_Hyp with T; trivial. apply term_eq. rewrite !subst_env, (absBody_eq WLabs W'Labs); trivial. rewrite !subst_term, (absBody_eq WLabs W'Labs); trivial. apply algebraic_app with W'app. rewrite <- W'L_eq; trivial. apply R_algebraic_preserving with (appBodyR Wapp); trivial. destruct (R_abs_reduct WLabs W'L_red) as [W'Labs W'Lbody_red]. assert (W'Lcomp: Computable (absBody W'Labs)). apply comp_step_comp with (absBody WLabs); trivial. rewrite PL; trivial. assert (W'Rcomp: Computable (appBodyR W'app)). rewrite <- W'R_eq, PR; trivial. set (P'L := exist W'Lcomp). set (P'R := exist W'Rcomp). apply (IH (P'L, P'R)) with W'app W'Labs; trivial. constructor 1. unfold R_Comp; simpl; rewrite <- PL; trivial. intros G cs T TG Tcomp. assert (CS: correct_subst (absBody WLabs) G). destruct cs; constructor; trivial. rewrite (R_env_preserving W'Lbody_red); trivial. rewrite (R_env_preserving W'Lbody_red); trivial. apply comp_step_comp with (subst CS). apply WL_Hyp with T; trivial. apply R_subst_stable; trivial. apply singletonSubst_algebraic with T; trivial. apply comp_algebraic; trivial. apply algebraic_app with W'app. apply R_algebraic_preserving with (appBodyL Wapp); trivial. rewrite <- W'R_eq; trivial. destruct (R_abs_reduct WLabs W'L_red) as [W'Labs W'Lbody_red]. assert (W'Lcomp: Computable (absBody W'Labs)). apply comp_step_comp with (absBody WLabs); trivial. rewrite PL; trivial. assert (W'Rcomp: Computable (appBodyR W'app)). apply comp_step_comp with (appBodyR Wapp); trivial. rewrite PR; trivial. set (P'L := exist W'Lcomp). set (P'R := exist W'Rcomp). apply (IH (P'L, P'R)) with W'app W'Labs; trivial. constructor 1. unfold R_Comp; simpl; rewrite <- PL; trivial. intros G cs T GT Tcomp. assert (CS: correct_subst (absBody WLabs) G). destruct cs; constructor; trivial. rewrite (R_env_preserving W'Lbody_red); trivial. rewrite (R_env_preserving W'Lbody_red); trivial. apply comp_step_comp with (subst CS). apply WL_Hyp with T; trivial. apply R_subst_stable; trivial. apply singletonSubst_algebraic with T; trivial. apply comp_algebraic; trivial. apply algebraic_app with W'app. apply R_algebraic_preserving with (appBodyL Wapp); trivial. apply R_algebraic_preserving with (appBodyR Wapp); trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)