proposition: Lemma roots_map_map_cons: forall a l (roots: roots_t), DoubleNoDup (a :: l) -> roots_map (a :: l) roots = roots_map [a] (roots_map l roots).
proof: Proof. intros. induction roots; simpl; auto. rewrite IHroots. f_equal. destruct a0; simpl; trivial. f_equal. clear IHroots. destruct (InEither_dec v (a :: l)). - destruct a as [a b]. rewrite DoubleNoDup_cons_iff in H. destruct H as [? [? [? ?]]]. rewrite InEither_cons_iff in i. destruct i. + red in H3. simpl in H3. destruct H3. * subst v. rewrite (list_bi_map_not_In l a); auto. unfold list_bi_map. simpl. now rewrite if_true; [rewrite if_true|]. * subst v. rewrite (list_bi_map_not_In l b); auto. unfold list_bi_map. simpl. rewrite if_false; [rewrite if_true|]; [rewrite if_false| | ]; try easy. rewrite if_true; easy. + unfold list_bi_map at 1. simpl. rewrite if_false. 2: unfold equiv; intro; now subst. rewrite if_false. 2: unfold equiv; intro; now subst. fold (list_bi_map l v). remember (list_bi_map l v) as v'. assert (InEither v' l). { subst v'. apply list_bi_map_In in H3. destruct H3 as [k0 [v0 [? ?]]]. apply In_InEither in H3. destruct H3. destruct H4 as [[? ?] | [? ?]]; now rewrite H6. } unfold list_bi_map. simpl. rewrite if_false. 2: unfold equiv; intro; now subst. rewrite if_false. 2: unfold equiv; intro; now subst. easy. - rewrite list_bi_map_not_In; auto. assert (~ InEither v l). { intro. apply n. rewrite InEither_cons_iff. now right. } rewrite (list_bi_map_not_In _ _ H0). assert (~ InEither v [a]). { intro. apply n. rewrite InEither_cons_iff. left. unfold InEither in H1. unfold IsEither. destruct a as [a b]. simpl in *. intuition. } rewrite (list_bi_map_not_In _ _ H1). easy. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph