proposition: Lemma subgraph_update: forall (g g': Graph) (S1 S1' S2: list addr), (forall x : addr, In x (S1 ++ S2) -> Decidable (vvalid g x)) -> (forall x : addr, In x (S1' ++ S2) -> Decidable (vvalid g' x)) -> (predicate_partial_labeledgraph g (Complement addr (reachable_through_set g S1))) ~=~ (predicate_partial_labeledgraph g' (Complement addr (reachable_through_set g' S1')))%LabeledGraph -> @derives pred _ (graphs S1 g ⊗ graphs S2 g) (graphs S1 g * (graphs S1' g' -* graphs S1' g' ⊗ graphs S2 g')).
proof: Proof. intros. apply subgraph_update; auto. + apply RGF. + apply RGF. + apply unreachable_partialgraph_si_vertices_identical; auto. + apply Included_trans with (vvalid g). - hnf; intros. apply reachable_through_set_foot_valid in H0. destruct H0; auto. - intro v; apply vvalid_vguard. + apply Included_trans with (vvalid g'). - hnf; intros. apply reachable_through_set_foot_valid in H0. destruct H0; auto. - intro v; apply vvalid_vguard. Qed.
imports: CertiGraph.lib.Ensembles_ext Coq.Lists.List VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.seplog CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.BinGraph CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.msl_application.Graph Coq.Logic.Classical