proposition: Lemma xxx: forall {G : CFGV} {vc : VarSym G} (lswP : list (Swapping vc)) {mp : MixtureParam} (m : Mixture mp) (lln : list (list nat)), lBoundVars vc lln (mSwapTermPat m lswP (genTermSwapping lln lswP)) = map (fun p => swapLVar (snd p) (fst p) ) (combine (lBoundVars vc lln m) (genTermSwapping lln lswP)).
proof: Proof. intros. apply eq_maps2 with (defa:=[]) (defc:=([],[])); [unfold genTermSwapping, lBoundVars; rw combine_length; autorewrite with fast;rw min_eq; sp |]. introv Hlt. destruct lln; cpx. allsimpl. Lemma ndRenAlAxAlpha3 : forall {G : CFGV} {vc : VarSym G} (lswP : list (Swapping vc)) (n:nat) {mp : MixtureParam} (m : Mixture mp) (lln : list (list nat)), n< length mp -> let labs := (MakeAbstractionsTNodeAux vc lln m) in let labsR := (MakeAbstractionsTNodeAux vc lln (mSwapTermPat m lswP (genTermSwapping lln lswP))) in match (nth_error labs n, nth_error labsR n) with | (Some ab, Some abR) => AlphaEqAbs ab abR | _ => False end. Proof. induction n. - introv Hn. destruct m; cpx. unfold MakeAbstractionsTNodeAux. allsimpl. remember (genTermSwapping lln lswP) as swT. remember (mSwapTermPat (mtcons ph m) lswP swT) as RR. duplicate HeqRR. simpl in HeqRR. rw HeqRR0 in HeqRR. rewrite <- HeqRR. allsimpl. Abort. Lemma ndRenAlAxAlpha2 : forall {G : CFGV} {vc : VarSym G} (lswP : list (Swapping vc)) {mp : MixtureParam} (m : Mixture mp) (lln : list (list nat)), mAlphaEq vc m (mSwapTermPat m lswP (genTermSwapping lln lswP)) lln. Proof. unfold mAlphaEq. induction m; cpx. unfold MakeAbstractionsTNodeAux. - intros. allsimpl. constructor. + destruct lln as [|lnh lnt]; [allsimpl; autorewrite with fast; apply AlphaEqNilAbsT; eauto with Alpha; fail|]. induction lnh as [|n ntl]; allsimpl; cpx; autorewrite with fast; [apply AlphaEqNilAbsT; eauto with Alpha; fail|]. destruct a; cpx. Admitted. Lemma ndRenAlAxAlpha : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (m : Mixture mp) (lln : list (list nat)) (lvA : list (vType vc)), lAlphaEqAbs (MakeAbstractionsTNodeAux vc lln m) (MakeAbstractionsTNodeAux vc lln (nodeRenAlphaAux lln m lvA)). Proof. unfold MakeAbstractionsTNodeAux. induction m; cpx. - introv. allsimpl. constructor. + induction lln; allsimpl; cpx; autorewrite with fast; [apply AlphaEqNilAbsT; cpx|]. Admitted. Lemma RenAlphaAlpha : forall {G : CFGV} {vc : VarSym G}, ( (forall (s : GSym G) (ta : Term s) (lvA : list (vType vc)), tAlphaEq vc ta (tRenAlpha ta lvA)) * (forall (s : GSym G) (pta : Pattern s) (lvA : list (vType vc)), pAlphaEq vc pta (pRenAlpha pta lvA)) * (forall (l : MixtureParam) (ma: Mixture l) (llbv : list (list (vType vc))) (lvA : list (vType vc)), let maR := mRenAlpha ma lvA in lAlphaEqAbs (MakeAbstractions vc ma llbv) (MakeAbstractions vc maR llbv))). Proof. intros. GInduction; intros; cpx; try (econstructor; eauto; fail);[| |]. - Case "tnode". allsimpl. constructor. unfold MakeAbstractionsTNode. unfold nodeRenAlpha. eapply (alphaEqTransitive); [ |apply ndRenAlAxAlpha with (lvA0 := lvA); eauto]. unfold MakeAbstractionsTNodeAux. rw <- (@mRenlBinderShallowSame G vc). apply X; cpx. - Case "mtcons". subst maR. allunfold MakeAbstractionsTNodeAux. simpl. constructor; cpx. apply AlphaEqNilAbsT; cpx. - Case "mpcons". subst maR. allunfold MakeAbstractionsTNodeAux. simpl. constructor; cpx. apply AlphaEqNilAbsP; cpx. Qed.
imports: SubstAux AlphaEqProps