proposition: Lemma edge_spanning_tree_left_reachable: forall (g1 g2: Graph) x l r, vvalid g1 x -> vgamma g1 x = (true, l, r) -> edge_spanning_tree g1 (x, L) g2 -> Included (reachable g2 r) (reachable g1 x).
proof: Proof. intros. assert (Hv: vvalid g2 r -> vvalid g1 r). { intros. rewrite (edge_spanning_tree_left_vvalid g1 g2 x r); auto. } hnf in H1. assert (l = dst g1 (x, L)) by (simpl in H0; inversion H0; auto). change (lg_gg g1) with (g1: LGraph) in *. rewrite <- H2 in H1. destruct (node_pred_dec (marked g1) l). + destruct H1 as [[? [? [? [? ?]]]] ?]. intro v. unfold Ensembles.In . intros. apply edge_reachable_by with r; auto. - split; [|split]; auto. * apply Hv. apply reachable_head_valid in H8; auto. * rewrite (gamma_step g1 x true l r); auto. - change (g1 |= r ~o~> v satisfying (fun _ : addr => True)) with (reachable g1 r v). rewrite reachable_ind_reachable in H8. clear H0. induction H8. * rewrite reachable_ind_reachable. constructor. rewrite H1; auto. * destruct H0 as [? [? ?]]. apply edge_reachable with y. apply IHreachable. rewrite H1; auto. split; [|split]; [rewrite H1; auto .. |]. rewrite step_spec in H10 |- *. destruct H10 as [e [? [? ?]]]. exists e. assert (e <> (x, L)) by (intro; subst; destruct H6; [|destruct H2]; auto). specialize (H3 _ H13). specialize (H4 _ H13). specialize (H5 _ H13). subst x0. subst y. intuition. + apply (spanning_tree_left_reachable g1 g2 x l r); auto. Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext Coq.Lists.List CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind CertiGraph.graph.spanning_tree CertiGraph.graph.BinGraph CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.GraphBin_Mark