proposition: Lemma algebraic_swap_notFunApp : forall M (pos: Pos M) (MP: PlaceHolder pos) (P := proj1_sig2 MP), (forall Min (pos: Pos Min) (MP: PlaceHolder pos) (P := proj1_sig2 MP), subterm Min M -> ~isFunApp (Min // pos) -> algebraic Min -> algebraic P -> algebraic (swap MP)) -> pos <> PThis M -> ~isFunApp M -> ~isFunApp (M // pos) -> (forall M', isAppUnit M' M -> algebraic M') -> algebraic P -> (forall M', isAppUnit M' (swap MP) -> algebraic M').
proof: Proof. induction pos; intros MP P IH Pthis Mnfa Mpnfa Mualg Palg M' M'unit; try_solve. assert (MPabs: isAbs (swap MP)). apply swap_abs. unfold isAppUnit in M'unit. rewrite appUnits_notApp in M'unit. inversion M'unit; try_solve. rewrite <- H. apply algebraic_swap_abs; try_solve. apply Mualg. unfold isAppUnit. rewrite appUnits_notApp; auto with datatypes. term_inv (swap MP). set (Lapp := swap_left_app MP). destruct (placeHolder_appL MP) as [MLP ML]. set (SL := swap_in_appL MLP MP Lapp ML). unfold isAppUnit in M'unit. rewrite (appUnits_app (swap MP) Lapp) in M'unit. destruct (in_app_or M'unit). destruct (posThis_dec pos). apply algebraic_appUnits with P; trivial. apply algebraic_arrowType; trivial. unfold P; destruct MP; simpl. rewrite <- e1; rewrite e; simpl; trivial. rewrite <- SL in H. replace (swap MLP) with P in H; trivial. apply term_eq. rewrite swap_env_eq. unfold P; destruct MP; simpl. rewrite <- e0; rewrite e; trivial. rewrite swap_term_is; rewrite ML. unfold P; destruct MP; simpl. rewrite e; trivial. apply IHpos with MLP; trivial. intros; apply IH; trivial. apply AppLsub with I; constructor; trivial. change (buildT AppL) with (@appBodyL (buildT (TApp AppL AppR)) I). apply notFunApp_left_inv; trivial. intros; apply Mualg. apply appUnit_left with I; trivial. rewrite ML; trivial. rewrite SL; trivial. inversion H; try_solve. apply Mualg. rewrite <- H0. rewrite (appBodyR_swap_in_appL MLP MP); trivial. change (buildT AppR) with (@appBodyR (buildT (TApp AppL AppR)) I). apply appUnit_right with I; trivial. set (Rapp := swap_right_app MP). destruct (placeHolder_appR MP) as [MRP MR]. set (SR := swap_in_appR MRP MP Rapp MR). unfold isAppUnit in M'unit. rewrite (appUnits_app (swap MP) Rapp) in M'unit. destruct (in_app_or M'unit). apply Mualg. apply appUnit_left with I; simpl. rewrite <- (appBodyL_swap_in_appR MRP MP Rapp MR); trivial. inversion H; try_solve. rewrite <- H0; rewrite <- SR. apply IH; trivial. change (buildT AppR) with (@appBodyR (buildT (TApp AppL AppR)) I). apply appBodyR_subterm. apply Mualg. apply appUnit_right with I; trivial. rewrite MR; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)