proposition: Lemma mark_list_get_marked: forall m1 l m2 (R_DEC: forall x, In x l -> ReachDecidable g x (negateP m1)) (V_DEC: forall x, In x l -> Decidable (vvalid g x)), mark_list m1 l m2 -> forall z n, In z l -> g |= z ~o~> n satisfying (negateP m1) -> m2 n.
proof: Proof. apply (ind_RV_DEC (fun m1 l m2 => forall z n : V, In z l -> g |= z ~o~> n satisfying (negateP m1) -> m2 n)). + intros. inversion H0. + intros. destruct H2. - subst z. apply (mark_list_marked m' l m''); auto. * intros. apply (mark_preserved_reach_decidable m v m'); auto. 1: apply reachable_by_head_valid in H3; auto. 1: apply R_DEC; right; auto. 1: apply R_DEC; left; auto. * intros; apply V_DEC; right; auto. * destruct H0 as [? _]; auto. - destruct (V_DEC v (or_introl eq_refl)). 1: { apply (mark_unmarked m v m') in H3; auto; [| apply R_DEC; left; auto]. destruct H3. + apply (H z); auto. + apply (mark_list_marked m' l); auto. - intros. apply (mark_preserved_reach_decidable m v m'); auto. * apply R_DEC; right; auto. * apply R_DEC; left; auto. - intros; apply V_DEC; right; auto. } 1: { pose proof (mark_invalid m v m' n0 H0). apply (H z); auto. erewrite si_reachable_by in H3; [exact H3 | reflexivity |]. hnf in H4 |- *; clear - H4. intros. specialize (H4 x). rewrite !negateP_spec. tauto. } Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2