proposition: Lemma algebraic_swap_funApp : forall T (pos: Pos T) (Mpos: PlaceHolder pos) (Npos: PlaceHolder pos) (M := proj1_sig2 Mpos) (N := proj1_sig2 Npos), ~isFunApp (T // pos) -> isFunApp T -> exists l t (tp: Pos t) (ph: PlaceHolder tp * PlaceHolder tp), isArg t T /\ ~isFunApp (t // tp) /\ proj1_sig2 (fst ph) = M /\ proj1_sig2 (snd ph) = N /\ appHead (swap Mpos) = appHead (swap Npos) /\ appArgs (swap Mpos) = fst l ++ (swap (fst ph)) :: snd l /\ appArgs (swap Npos) = fst l ++ (swap (snd ph)) :: snd l.
proof: Proof. induction pos; intros; try_solve. set (Lapp := swap_left_app Mpos). set (Rapp := swap_left_app Npos). destruct (placeHolder_appL Mpos) as [MLpos ML]. destruct (placeHolder_appL Npos) as [NLpos NL]. destruct (IHpos MLpos NLpos) as [[l r] [T [TP [[PHL PHR] [Targ [Tnfa [TM [TN [MNhead [Margs Nargs]]]]]]]]]]; trivial. change (buildT AppL) with (appBodyL (M:=buildT (TApp AppL AppR)) I). apply isFunApp_left; trivial. set (SL := swap_in_appL MLpos Mpos Lapp ML). set (SR := swap_in_appL NLpos Npos Rapp NL). exists (l, r ++ appBodyR Lapp::nil); simpl in * . exists T; exists TP; exists (PHL, PHR). repeat split; simpl; trivial. apply appArg_left with I; trivial. rewrite TM; trivial. rewrite TN; trivial. rewrite appHead_app with (swap Mpos) Lapp. rewrite appHead_app with (swap Npos) Rapp. rewrite <- SL; rewrite <- SR; trivial. rewrite appArgs_app with (swap Mpos) Lapp. rewrite <- SL; rewrite Margs. rewrite app_ass; auto with datatypes. rewrite appArgs_app with (swap Npos) Rapp. rewrite <- SR; rewrite Nargs. rewrite (appBodyR_swap_in_appL MLpos Mpos); trivial. rewrite (appBodyR_swap_in_appL NLpos Npos); trivial. rewrite app_ass; auto with datatypes. set (Lapp := swap_right_app Mpos). set (Rapp := swap_right_app Npos). destruct (placeHolder_appR Mpos) as [MLpos ML]. destruct (placeHolder_appR Npos) as [NLpos NL]. set (SL := swap_in_appR MLpos Mpos Lapp ML). set (SR := swap_in_appR NLpos Npos Rapp NL). exists (appArgs (appBodyL Lapp), nil (A:=Term)). exists (buildT AppR); exists pos; exists (MLpos, NLpos). repeat split; simpl; trivial. apply appArg_right with I; trivial. rewrite appHead_app with (swap Mpos) Lapp. rewrite appHead_app with (swap Npos) Rapp. rewrite (appBodyL_swap_in_appR MLpos Mpos); trivial. rewrite (appBodyL_swap_in_appR NLpos Npos); trivial. rewrite appArgs_app with (swap Mpos) Lapp. rewrite <- SL; trivial. rewrite appArgs_app with (swap Npos) Rapp. rewrite (appBodyL_swap_in_appR NLpos Npos); trivial. rewrite (appBodyL_swap_in_appR MLpos Mpos); trivial. rewrite <- SR; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)