proposition: Lemma bijective_list_bi_map: forall l, DoubleNoDup l -> bijective (list_bi_map l) (list_bi_map l).
proof: Proof. intros. constructor; intros. - destruct (InEither_dec x l). + apply list_bi_map_In in i. destruct i as [kx [vx [? ?]]]. destruct (InEither_dec y l). * apply list_bi_map_In in i. destruct i as [ky [vy [? ?]]]. destruct H2 as [[? ?] | [? ?]]; destruct H4 as [[? ?] | [? ?]]; rewrite H5, H6 in H0; subst. -- eapply DoubleNoDup_In_snd_eq; eauto. -- exfalso; eapply (DoubleNoDup_In_fst_snd_impsb _ kx); eauto. -- exfalso; eapply (DoubleNoDup_In_fst_snd_impsb _ ky); eauto. -- eapply DoubleNoDup_In_fst_eq; eauto. * pose proof n. apply list_bi_map_not_In in n. rewrite <- H0 in n. destruct H2 as [[? ?] | [? ?]]; rewrite H4 in n; rewrite n in H1; exfalso; apply H3; apply In_InEither in H1; destruct H1; assumption. + pose proof n. apply list_bi_map_not_In in n. rewrite H0 in n. destruct (InEither_dec y l). * apply list_bi_map_In in i. destruct i as [ky [vy [? ?]]]. destruct H3 as [[? ?] | [? ?]]; rewrite H4 in n; rewrite n in H2; exfalso; apply H1; apply In_InEither in H2; destruct H2; assumption. * apply list_bi_map_not_In in H1. apply list_bi_map_not_In in n0. rewrite H1, n0 in H0. assumption. - destruct (InEither_dec x l). + apply list_bi_map_In in i. destruct i as [k [v [? ?]]]. destruct (DoubleNoDup_bi_look_up _ _ _ H H0). destruct H1 as [[? ?] | [? ?]]; subst x; rewrite H4; unfold list_bi_map. * rewrite H3. reflexivity. * rewrite H2. reflexivity. + apply list_bi_map_not_In in n. rewrite n. assumption. 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