proposition: Lemma is_list_edge: forall root v, G |= root ~> v -> is_list root -> is_list v.
proof: Proof. intros. unfold is_list in *. destruct H0 as [p [? ?]]. exists p. split; auto. intros. destruct H2 as [[v' pv] ?]. assert (v' = v) by (destruct H2 as [[? _] _]; simpl in H2; auto). subst v'. destruct H as [? [? ?]]. rewrite step_spec in H4. destruct H4 as [e [? [? ?]]]. assert (forall pp, G |= pp is v ~o~> y satisfying (fun _ => True) -> G |= (path_glue (root, e :: nil) pp) is root ~o~> y satisfying (fun _ => True)). { intros. apply reachable_by_path_merge with v; auto. split; split; simpl; auto. + unfold strong_evalid. rewrite H5, H6. split; auto. + hnf. rewrite Forall_forall. intros; auto. } pose proof (H7 _ H2). unfold path_glue, fst, snd in H8. rewrite <- app_comm_cons, app_nil_l in H8. pose proof (reachable_by_path_is_reachable _ _ _ _ _ H8). apply H1 in H9. clear H1. destruct H9 as [py [[? ?] ?]]. pose proof (H9 _ H8). exists (v, pv). split; split; auto. + intros. specialize (H7 _ H12). destruct x' as [x px]. assert (x = v) by (destruct H12 as [[? _] _]; simpl in H12; auto). subst x. unfold path_glue, fst, snd in H7. rewrite <- app_comm_cons, app_nil_l in H7. specialize (H9 _ H7). rewrite H9 in H11. inversion H11. auto. + simpl. destruct H10. subst py. simpl in *. clear -H10. unfold incl in *. intros. apply H10. right; auto. + simpl. destruct H10. subst py. simpl in *. unfold In_path. clear -H6 H10. right. exists e. split; intuition. Qed.
imports: Coq.Arith.Arith CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable Coq.Lists.List