proposition: Lemma permutation_map_base : forall {A} {B} (f: B -> A) {shuffled: list A} {l1}, Permutation shuffled l1 -> forall l1', List.map f l1' = l1 -> exists l', List.map f l' = shuffled /\ Permutation l' l1'.
proof: Proof. induction shuffled; simpl; intros. { repeat match goal with | [ H : _ |- _ ] => apply Permutation_nil in H | _ => progress subst | [ H : _ |- _ ] => apply map_eq_nil in H end. exists (@nil B); simpl; intuition. } symmetry in H. pose proof (permutation_cons_in H) as in_l1. apply in_split in in_l1. destruct in_l1 as [ l2 [ l3 l1_split ] ]. rewrite l1_split in H, H0; clear l1_split l1. rewrite <- Permutation_middle in H. apply Permutation_cons_inv in H. symmetry in H. specialize (IHshuffled _ H). symmetry in H0. apply app_map_inv in H0. destruct H0 as [ l2' [ l3' (l1'_app & l2l2' & l3l3') ] ]. apply cons_map_inv in l3l3'. destruct l3l3' as [ a' [ l3'' ( ? & ? & ?) ] ]; subst. specialize (IHshuffled (l2' ++ l3'')); rewrite map_app in IHshuffled. specialize (IHshuffled eq_refl). destruct IHshuffled as [ l' (map_eq & perm) ]. exists (a' :: l'); subst; simpl. rewrite <- Permutation_middle; split; eauto. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts