proposition: Lemma Permutation_nth_error l l' : Permutation l l' <-> (length l = length l' /\ exists f:nat->nat, Injective f /\ forall n, nth_error l' n = nth_error l (f n)).
proof: Proof. split. { intros P. split; [now apply Permutation_length|]. induction P. - exists (fun n => n). split; try red; auto. - destruct IHP as (f & Hf & Hf'). exists (fun n => match n with O => O | S n => S (f n) end). split; try red. * intros [|y] [|z]; simpl; now auto. * intros [|n]; simpl; auto. - exists (fun n => match n with 0 => 1 | 1 => 0 | n => n end). split; try red. * intros [|[|z]] [|[|t]]; simpl; now auto. * intros [|[|n]]; simpl; auto. - destruct IHP1 as (f & Hf & Hf'). destruct IHP2 as (g & Hg & Hg'). exists (fun n => f (g n)). split; try red. * auto. * intros n. rewrite <- Hf'; auto. } { revert l. induction l'. - intros [|l] (E & _); now auto. - intros l (E & f & Hf & Hf'). simpl in E. assert (Ha : nth_error l (f 0) = Some a) by (symmetry; apply (Hf' 0)). destruct (nth_error_split l (f 0) Ha) as (l1 & l2 & L12 & L1). rewrite L12. rewrite <- Permutation_middle. constructor. apply IHl'; split; [|exists (adapt f); split]. * revert E. rewrite L12, !app_length. simpl. rewrite <- plus_n_Sm. now injection 1. * now apply adapt_injective. * intro n. rewrite <- (adapt_ok a), <- L12; auto. apply (Hf' (S n)). } Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat