proposition: Lemma PermOK {T : Type} {n : nat} : forall (cp1 cp2 : cartesianPower T (S (S n))) (appPred : (cartesianPower T (S (S n))) -> Prop), (forall (A : T) (X : cartesianPower T (S n)), appPred (consHeadCP A X) -> appPred (consTailCP X A)) -> (forall (A B : T) (X : cartesianPower T n), appPred (consHeadCP A (consHeadCP B X)) -> appPred (consHeadCP B (consHeadCP A X))) -> appPred cp1 -> Permutation.Permutation (CPToList cp1) (CPToList cp2) -> appPred cp2.
proof: Proof. induction n; intros cp1 cp2 appPred pred_perm_1 pred_perm_2 Hpred HPerm. assert (Hcp1 := CPPair cp1); rewrite Hcp1 in *; clear Hcp1. assert (Hcp2 := CPPair cp2); rewrite Hcp2 in *; clear Hcp2. simpl in *. apply Permutation.Permutation_length_2 in HPerm. elim HPerm; clear HPerm; intro HPerm; destruct HPerm as [HEq1 HEq2]; rewrite <- HEq1; rewrite <- HEq2. assumption. apply pred_perm_1; assumption. rewrite consTailCPOK. assert (H' := lastCPIn cp2). assert (H : InCP (lastCP cp2) cp1) by (unfold InCP;apply Permutation.Permutation_in with (CPToList cp2); try apply Permutation.Permutation_sym; assumption); clear H'. assert (H' := InNth cp1 (lastCP cp2) (headCP cp2) H); clear H. destruct H' as [id [Hge [Hle Hnth]]]. assert (H : exists cp, appPred cp /\ Permutation.Permutation (CPToList cp2) (CPToList cp) /\ lastCP cp = lastCP cp2). induction id; try (unfold ge in Hge; assert (H := Le.le_Sn_0 0); contradiction); clear IHid. revert Hnth; revert HPerm; revert Hpred; revert cp1; induction id; intros. exists (consTailCP (tailCP cp1) (headCP cp1)). split. apply pred_perm_1. rewrite <- consHeadCPOK. assumption. split. apply Permutation.perm_trans with (CPToList cp1); try (apply consTailPerm). apply Permutation.Permutation_sym; assumption. apply nthCircPerm1 in Hnth. rewrite Hnth. assert (H := nthLast (consTailCP (tailCP cp1) (headCP cp1)) (headCP cp2)); rewrite H; reflexivity. assert (H := Hle). do 2 (apply Le.le_S_n in H). apply nthCircPerm2 in Hnth; try assumption; clear H. apply Le.le_Sn_le in Hle. assert (H : S id >= 1) by intuition; clear Hge; rename H into Hge. assert (H : appPred (consTailCP (tailCP cp1) (headCP cp1))) by (apply pred_perm_1; rewrite <- consHeadCPOK; assumption) ; clear Hpred; rename H into Hpred. assert (H := consTailPerm cp1); apply Permutation.Permutation_sym in H. assert (H' : Permutation.Permutation (CPToList (consTailCP (tailCP cp1) (headCP cp1))) (CPToList cp2)) by (apply Permutation.perm_trans with (CPToList cp1); assumption); clear HPerm; rename H' into HPerm. assert (H' := IHid Hge Hle (consTailCP (tailCP cp1) (headCP cp1)) Hpred HPerm Hnth). destruct H' as [cp [Hpredcp [HPermcp Hlastcp]]]; exists cp. do 2 (split; try assumption). clear Hnth; clear Hle; clear Hge; clear id; clear HPerm; clear Hpred; clear cp1. destruct H as [cp [Hpred [HPerm Hlast]]]; rewrite <- Hlast. assert (H := consTailCPOK cp); rewrite H in HPerm; clear H. assert (H := consTailCPOK cp2); rewrite H in HPerm; clear H. do 2 (rewrite consTailOK in HPerm). rewrite Hlast in HPerm. apply Permutation.Permutation_app_inv_r in HPerm. assert (ablcp := allButLastCP cp). assert (ablcp2 := allButLastCP cp2). assert (pred_perm_3 := PermOKAux appPred (S n) pred_perm_1). assert (HPerm1 : (forall (A : T) (X : cartesianPower T (S n)), (fixLastCP appPred (lastCP cp)) (consHeadCP A X) -> (fixLastCP appPred (lastCP cp)) (consTailCP X A))). unfold fixLastCP; intros A X HappPred. induction n. simpl in HappPred. apply pred_perm_2. simpl. assumption. clear IHn0. induction n. simpl. simpl in HappPred. simpl in pred_perm_1. simpl in pred_perm_2. apply pred_perm_2 in HappPred. apply pred_perm_1 in HappPred; simpl in HappPred. apply pred_perm_2 in HappPred. apply pred_perm_1 in HappPred; simpl in HappPred. apply pred_perm_3 in HappPred; simpl in HappPred. assumption. clear IHn0. induction n. simpl. simpl in HappPred. simpl in pred_perm_1. simpl in pred_perm_2. apply pred_perm_2 in HappPred. apply pred_perm_1 in HappPred; simpl in HappPred. apply pred_perm_2 in HappPred. apply pred_perm_1 in HappPred; simpl in HappPred. apply pred_perm_2 in HappPred. apply pred_perm_1 in HappPred; simpl in HappPred. apply pred_perm_1 in HappPred; simpl in HappPred. apply pred_perm_1 in HappPred; simpl in HappPred. assumption. clear IHn0. assert (H := consHeadCPOK X); rewrite H in *; clear H. assert (H := consTailCPOK (tailCP X)); rewrite H in *; clear H. set (B := headCP X) in *. set (CP := allButLastCP (allButLastCP (tailCP X))) in *. set (C := tailCP (allButLastCP (tailCP X))) in *. set (D := lastCP (tailCP X)) in *. set (E := lastCP cp) in *. apply pred_perm_3 in HappPred; rewrite consTlHdHdTl in HappPred; rewrite circPermNConsOK in HappPred. apply pred_perm_1 in HappPred; do 2 (rewrite <- consHdTlTlHd in HappPred). apply pred_perm_2 in HappPred. apply pred_perm_1; rewrite <- consHdTlTlHd; rewrite <- circPermNConsOK. apply pred_perm_3. do 2 (apply pred_perm_1; rewrite consHdTlTlHd); rewrite consHdTlTlHd. apply pred_perm_1. assumption. assert (HPerm2 : (forall (A B : T) (X : cartesianPower T n), (fixLastCP appPred (lastCP cp)) (consHeadCP A (consHeadCP B X)) -> (fixLastCP appPred (lastCP cp)) (consHeadCP B (consHeadCP A X)))) by (unfold fixLastCP; intros A B X HappPred; rewrite <- consTlHdHdTl; apply pred_perm_2; rewrite consTlHdHdTl; assumption). apply Permutation.Permutation_sym in HPerm. assert (H := IHn (allButLastCP cp) (allButLastCP cp2) (fixLastCP appPred (lastCP cp)) HPerm1 HPerm2). apply H; try assumption. rewrite <- fixLastCPOK. rewrite <- consTailCPOK. assumption. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality