proposition: Lemma Permutation_InA_cons {Value} : forall l (l' : list (key * Value)), NoDupA (@eq_key _) l -> NoDupA (@eq_key _) l' -> (forall k v, InA (@eq_key_elt _) (k, v) l' <-> (InA (@eq_key_elt _) (k, v) l)) -> Permutation (List.map snd l') (List.map snd l).
proof: Proof. induction l; intros. destruct l'. constructor. assert (InA (eq_key_elt (elt:=Value)) (fst p, snd p) []) as H2 by (eapply H1; left; split; reflexivity); inversion H2. destruct a as [k v]. assert (InA (eq_key_elt (elt:=Value)) (k, v) l') as H2 by (eapply H1; econstructor; split; reflexivity). destruct (InA_split H2) as [l'1 [kv [l'2 [eq_kv eq_l]]]]; subst. repeat rewrite List.map_app; simpl. etransitivity. symmetry. apply Permutation_middle. destruct eq_kv; simpl in *; subst; constructor. rewrite <- List.map_app. eapply NoDupA_swap in H0; eauto using eqk_equiv. inversion H0; inversion H; subst; apply IHl; eauto. assert (forall (k0 : key) (v : Value), InA (eq_key_elt (elt:=Value)) (k0, v) (kv :: (l'1 ++ l'2)) <-> InA (eq_key_elt (elt:=Value)) (k0, v) ((k, snd kv) :: l)) by (split; intros; [ eapply H1; eapply InA_app_cons_swap | eapply H1 in H4; eapply InA_app_cons_swap in H4 ]; eauto using eqke_equiv). split; intros. + generalize (proj1 (H4 k0 v) (InA_cons_tl _ H5)); intros. inversion H8; subst; eauto. destruct H12; simpl in *. exfalso; apply H6. revert H5 H9 H3; clear; induction (l'1 ++ l'2); intros; inversion H5; subst; [ constructor; destruct H0; simpl in *; unfold eq_key; rewrite <- H3, <- H9; eauto | constructor 2; eauto ]. + generalize (proj2 (H1 k0 v) (InA_cons_tl _ H5)); intros. eapply InA_app_cons_swap in H8; eauto using eqke_equiv. inversion H8; subst; eauto. destruct H12; simpl in *. exfalso; apply H10. revert H5 H9 H3; clear; induction l; intros; inversion H5; subst; [ constructor; destruct H0; simpl in *; unfold eq_key; simpl; rewrite <- H, H9; eauto | constructor 2; eauto ]. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances