proposition: Lemma triple2_mark: forall (g g1 g2: Graph) root l l_done son l_later, vvalid g root -> (unmarked g) root -> let marked' := Union _ (marked g) (eq root) in step_list g root l -> l = l_done ++ son :: l_later -> let PV1 := reachable_by_through_set g l_done (Complement _ marked') in (predicate_partialgraph g (Complement _ (Union _ PV1 (eq root)))) ~=~ (predicate_partialgraph g1 (Complement _ (Union _ PV1 (eq root)))) /\ Same_set (marked g1) (Union _ marked' PV1) -> mark son g1 g2 -> let PV2 := reachable_by_through_set g (l_done ++ son :: nil) (Complement _ marked') in Same_set (marked g2) (Union _ marked' PV2).
proof: Proof. intros. destruct H3 as [PRE_psi PRE_unm]. apply mark_marked' in H4. rewrite H4, PRE_unm. rewrite Union_assoc. apply Union_proper; [reflexivity |]. unfold unmarked. rewrite negateP_spec'. rewrite PRE_unm. unfold PV2. rewrite reachable_by_eq_partialgraph_reachable'. rewrite (Union_comm _ marked' PV1). rewrite (triple_mark_aux1' g PV1 root marked') by auto. rewrite <- Intersection_Complement. rewrite <- partial_partialgraph, <- PRE_psi. rewrite partial_partialgraph. rewrite Intersection_Complement. rewrite <- (triple_mark_aux1' g PV1 root marked') by auto. rewrite <- Intersection_Complement. rewrite <- partial_partialgraph, <- reachable_by_eq_partialgraph_reachable'. unfold PV2. fold PV1. rewrite reachable_by_through_app_strong', reachable_by_through_singleton'. + rewrite !reachable_by_eq_partialgraph_reachable'. rewrite partial_partialgraph. rewrite Intersection_comm. reflexivity. + rewrite Same_set_spec in PRE_unm |- *. intro v; specialize (PRE_unm v). rewrite Union_spec in PRE_unm |- *. unfold PV1 in PRE_unm. unfold Complement at 2; unfold Ensembles.In. pose proof reachable_by_through_set_foot_prop g l_done v (Complement V marked'). unfold Complement at 2 in H3; unfold Ensembles.In in H3. assert ((marked g1) v \/ ~ (marked g1) v) by (destruct (node_pred_dec (marked g1) v); auto). assert (marked' v \/ ~ marked' v). 1: { unfold marked'. rewrite Union_spec. destruct (node_pred_dec (marked g) v); destruct_eq_dec root v; auto. tauto. } pose proof Full_intro _ v. unfold Ensembles.In in H. tauto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Classes.Morphisms VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.Relation_ext CertiGraph.lib.relation_list CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.subgraph2 CertiGraph.graph.dual_graph