proposition: Lemma alphaEqSwapNonFree : forall {G : CFGV} {vc : VarSym G}, ( (forall (s : GSym G) (t : Term s) (sw : Swapping vc), leavesLVarUnchanged sw (tfreevars vc t) -> tAlphaEq vc t (tSwap t sw)) * (forall (s : GSym G) (pt : Pattern s) (sw : Swapping vc), leavesLVarUnchanged sw (pfreevars vc pt) -> pAlphaEq vc pt (pSwap pt sw)) * (forall (l : MixtureParam) (m : Mixture l) (sw : Swapping vc) (lbv : list (list (vType vc))), leavesLVarUnchanged sw (mfreevars vc m lbv) -> lAlphaEqAbs (MakeAbstractions vc m lbv) (MakeAbstractions vc (mSwap m sw) (swapLLVar sw lbv)))).
proof: Proof. intros. GInduction; introns Hyp; intros; cpx; allsimpl; try dlist_len lbv; try (econstructor; eauto with slow; fail). - Case "vleaf". rewrite DeqSym. ddeq; sp;[| eauto with Alpha; fail]. destruct e. allsimpl. repeat (disjoint_reasoning). rewrite Hyp; cpx. eauto 1 with Alpha. - Case "tnode". constructor. allunfold mAlphaEq. unfold MakeAbstractionsTNode. unfold MakeAbstractionsTNodeAux. unfold allBndngVars. rewrite <- lBoundVars_equivariant. cpx. - Case "pnode". constructor. allunfold mAlphaEq. unfold MakeAbstractionsPNode. specialize (Hyp sw nil). simpl in Hyp. cpx. - Case "mtcons". destruct lbv; cpx; apply lforallApp in Hyp1; repnd; [ allsimpl; specialize (Hyp0 sw []); simpl in Hyp0; constructor; cpx ; apply AlphaEqNilAbsT; apply Hyp; cpx|]. constructor; cpx. allsimpl. pose proof (GFreshDistRenWSpec vc l (tAllVars ph++tAllVars (tSwap ph sw)++ (swapLVar sw l)++ l ++ (tfreevars vc ph)++ ALDom sw ++ ALRange sw ++ l)) as Hfr. exrepnd. apply alAbT with (lbnew:=lvn); try (unfold swapLVar ; autorewrite with fast; congruence; fail); [unfolds_base; simpl; dands | | ]; cpx; try (autorewrite with fast; repeat (disjoint_reasoning); fail);[]. autorewrite with SwapAppR. assert (lvn = swapLVar sw lvn ) as XX by (symmetry; apply swapLVarNoChange; repeat (disjoint_reasoning)). remember (combine l lvn) as swt. rewrite XX. unfold swapLVar. rewrite <- map_combine. fold (swapSwap sw (combine l lvn)). rewrite <- (tcase swap_prop_e1Stronger). subst swt. apply tAlphaEqEquivariantRev with (sw0:=rev (combine l lvn)). autorewrite with SwapAppR. autorewrite with fast. apply Hyp. intros v Hin. unfolds_base. autorewrite with SwapAppL. assert (disjoint l lvn) as Xd by repeat(disjoint_reasoning). destruct (in_deq _ (DeqVtype vc) v l) as [Xin | Xnot]. + dimp (@swapVar_in G vc l lvn v); cpx. remember (swapVar (combine l lvn) v) as vs. assert (leavesLVarUnchanged sw lvn) as Xun by (apply leavesLVarUnchanged1;repeat (disjoint_reasoning)). apply Xun in hyp. repnud hyp. rw hyp. subst vs. autorewrite with SwapAppR. autorewrite with fast. refl. + assert (disjoint (tfreevars vc ph) lvn) as Hdiss by repeat (disjoint_reasoning). assert (LIn v (tfreevars vc ph -- l)) as Hins by (apply in_diff; dands; cpx). apply Hdiss in Hin. pattern ((swapVar (combine l lvn) v)). rewrite swapVarNoChange; cpx; autorewrite with fast; try congruence. apply Hyp2 in Hins. rewrite Hins. apply swapVarNonChangeRev. rewrite swapVarNoChange; cpx; autorewrite with fast; try congruence. - Case "mpcons". destruct lbv; cpx; apply lforallApp in Hyp1; repnd; [ allsimpl; specialize (Hyp0 sw []); simpl in Hyp0; constructor; cpx ; apply AlphaEqNilAbsP; apply Hyp; cpx|]. constructor; cpx. allsimpl. pose proof (GFreshDistRenWSpec vc l (pAllVars ph++pAllVars (pSwap ph sw)++ (swapLVar sw l)++ l ++ (pfreevars vc ph)++ ALDom sw ++ ALRange sw ++ l)) as Hfr. exrepnd. apply alAbP with (lbnew:=lvn); try (unfold swapLVar ; autorewrite with fast; congruence; fail); [unfolds_base; simpl; dands | | ]; cpx; try (autorewrite with fast; repeat (disjoint_reasoning); fail);[]. autorewrite with SwapAppR. assert (lvn = swapLVar sw lvn ) as XX by (symmetry; apply swapLVarNoChange; repeat (disjoint_reasoning)). remember (combine l lvn) as swt. rewrite XX. unfold swapLVar. rewrite <- map_combine. fold (swapSwap sw (combine l lvn)). rewrite <- (pcase swap_prop_e1Stronger). subst swt. apply pAlphaEqEquivariantRev with (sw0:=rev (combine l lvn)). autorewrite with SwapAppR. autorewrite with fast. apply Hyp. intros v Hin. unfolds_base. autorewrite with SwapAppL. assert (disjoint l lvn) as Xd by repeat(disjoint_reasoning). destruct (in_deq _ (DeqVtype vc) v l) as [Xin | Xnot]. + dimp (@swapVar_in G vc l lvn v); cpx. remember (swapVar (combine l lvn) v) as vs. assert (leavesLVarUnchanged sw lvn) as Xun by (apply leavesLVarUnchanged1;repeat (disjoint_reasoning)). apply Xun in hyp. repnud hyp. rw hyp. subst vs. autorewrite with SwapAppR. autorewrite with fast. refl. + assert (disjoint (pfreevars vc ph) lvn) as Hdiss by repeat (disjoint_reasoning). assert (LIn v (pfreevars vc ph -- l)) as Hins by (apply in_diff; dands; cpx). apply Hdiss in Hin. pattern ((swapVar (combine l lvn) v)). rewrite swapVarNoChange; cpx; autorewrite with fast; try congruence. apply Hyp2 in Hins. rewrite Hins. apply swapVarNonChangeRev. rewrite swapVarNoChange; cpx; autorewrite with fast; try congruence. Qed.
imports: AlphaEquality SwapProps Eqdep_dec