proposition: Lemma Permutation_inj l1 l2 : Permutation l1 l2 ↔ length l1 = length l2 ∧ ∃ f : nat → nat, Inj (=) (=) f ∧ ∀ i, l1 !! i = l2 !! f i.
proof: Proof. split. - intros Hl; split; [by apply Permutation_length|]. induction Hl as [|x l1 l2 _ [f [??]]|x y l|l1 l2 l3 _ [f [? Hf]] _ [g [? Hg]]]. + exists id; split; [apply _|done]. + exists (λ i, match i with 0 => 0 | S i => S (f i) end); split. * by intros [|i] [|j] ?; simplify_eq/=. * intros [|i]; simpl; auto. + exists (λ i, match i with 0 => 1 | 1 => 0 | _ => i end); split. * intros [|[|i]] [|[|j]]; congruence. * by intros [|[|i]]. + exists (g ∘ f); split; [apply _|]. intros i; simpl. by rewrite <-Hg, <-Hf. - intros (Hlen & f & Hf & Hl). revert l2 f Hlen Hf Hl. induction l1 as [|x l1 IH]; intros l2 f Hlen Hf Hl; [by destruct l2|]. rewrite (delete_Permutation l2 (f 0) x) by (by rewrite <-Hl). pose (g n := let m := f (S n) in if lt_eq_lt_dec m (f 0) then m else m - 1). apply Permutation_skip, (IH _ g). + rewrite length_delete by (rewrite <-Hl; eauto); simpl in *; lia. + unfold g. intros i j Hg. repeat destruct (lt_eq_lt_dec _ _) as [[?|?]|?]; simplify_eq/=; try lia. apply (inj S), (inj f); lia. + intros i. unfold g. destruct (lt_eq_lt_dec _ _) as [[?|?]|?]. * by rewrite lookup_delete_lt, <-Hl. * simplify_eq. * rewrite lookup_delete_ge, <-Nat.sub_succ_l by lia; simpl. by rewrite Nat.sub_0_r, <-Hl. Qed.
imports: stdpp(options)