proposition: Lemma graphs_graphs': forall S (g: Graph) {rfg: ReachableFiniteGraph g} (V_DEC: forall x : V, In x S -> Decidable (vvalid g x)), graphs S g = reachable_through_vertices_at S g.
proof: Proof. induction S; intros until g; intros rfg V_DEC. + unfold graphs. unfold reachable_through_vertices_at, vertices_at, pred_sepcon. apply pred_ext. - apply (exp_right nil). simpl. apply andp_right; auto. apply andp_right; [| apply prop_right; constructor]. apply prop_right. intro x. split; intros. * inversion H. * unfold reachable_through_set in H. destruct H as [s [? _]]. inversion H. - normalize. intro l; intros. normalize. destruct l; simpl; auto. specialize (H v). assert (In v (v :: l)) by apply in_eq. rewrite H in H1. unfold reachable_through_set in H1. destruct H1 as [s [? _]]. inversion H1. + unfold graphs. fold graphs. rewrite IHS; [| auto | intros; apply V_DEC; right; auto]. unfold reachable_through_vertices_at, reachable_vertices_at, vertices_at, pred_sepcon. clear IHS. apply pred_ext. - normalize_overlap. intros. rename x into la. normalize_overlap. rename x into lS. normalize_overlap. rewrite (add_andp _ _ (iter_sepcon_unique_nodup la (sepcon_unique_graph_cell (Graph_PointwiseGraph g)))). rewrite (add_andp _ _ (iter_sepcon_unique_nodup lS (sepcon_unique_graph_cell (Graph_PointwiseGraph g)))). normalize_overlap. rewrite (iter_sepcon_ocon equiv_dec); auto. apply (exp_right (nodup equiv_dec (la ++ lS))). apply andp_right; [apply andp_right |]. * apply prop_right. unfold reachable_set_list in *. unfold reachable_list in *. intros. rewrite nodup_In. rewrite reachable_through_set_eq. specialize (H1 x). specialize (H x). split; intro; [apply in_app_or in H3 | apply in_or_app]; destruct H3; [left | right | left | right]; tauto. * apply prop_right. apply NoDup_nodup. * auto. * apply precise_graph_cell. * apply joinable_graph_cell. - normalize. intro l; intros. assert (In a (a :: S)) by apply in_eq. destruct (construct_reachable_list g a) as [la [? ?]]; [apply V_DEC; left; auto |]. normalize_overlap. apply (exp_right la). destruct (construct_reachable_set_list g S) as [lS [? ?]]; [intros; apply V_DEC; right; auto |]. normalize_overlap. apply (exp_right lS). normalize_overlap. rewrite (add_andp _ _ (iter_sepcon_unique_nodup l (sepcon_unique_graph_cell (Graph_PointwiseGraph g)))). normalize. rewrite (iter_sepcon_ocon equiv_dec); auto. 2: apply precise_graph_cell. 2: apply joinable_graph_cell. rewrite iter_sepcon_permutation with (l2 := nodup equiv_dec (la ++ lS)); auto. apply NoDup_Permutation; auto. apply NoDup_nodup. intros. rewrite nodup_In. clear -H H2 H5. specialize (H x). specialize (H2 x). specialize (H5 x). rewrite H. rewrite reachable_through_set_eq. rewrite in_app_iff. tauto. Qed.
imports: Coq.Logic.Classical VST.msl.seplog VST.msl.log_normalize VST.msl.ramification_lemmas CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.Morphisms_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.ramification_lemmas CertiGraph.msl_ext.abs_addr CertiGraph.msl_ext.seplog CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.dag CertiGraph.graph.FiniteGraph