proposition: Lemma list_map_idempotent: forall l, DoubleNoDup l -> idempotent (list_map l).
proof: Proof. destruct l; intros; red; intros. - unfold list_map. now simpl. - destruct p as [k v]. rewrite DoubleNoDup_cons_iff in H. destruct H as [? [? [? ?]]]. unfold list_map. simpl. destruct (equiv_dec k x); unfold equiv in *. + subst x. destruct (equiv_dec k v); auto. destruct (look_up l v) eqn:? ; auto. apply In_look_up in Heqo. exfalso. apply H2. rewrite InEither_map_iff. now left. + unfold complement in c. destruct (look_up l x) eqn:? . * apply In_look_up in Heqo. destruct Heqo. destruct (equiv_dec k a); unfold equiv in *. -- subst a. exfalso. apply H1. rewrite InEither_map_iff. now right. -- destruct (look_up l a) eqn:? ; auto. apply In_look_up in Heqo. destruct Heqo as [? _]. red in H. destruct (split l) eqn:? . rewrite map_fst_split, Heqp in H5. rewrite map_snd_split, Heqp in H4. simpl in H4, H5. rewrite NoDup_app_iff in H. destruct H as [_ [_ ?]]. exfalso. now apply (H a). * destruct (equiv_dec k x); unfold equiv in *; [easy | now rewrite Heqo]. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver