proposition: Lemma predicate_partial_finitegraph: forall (g: PreGraph V E) (p: NodePred V), FiniteGraph g -> FiniteGraph (predicate_partialgraph g p).
proof: Proof. intros. destruct X as [X Y]. constructor. + destruct X as [l ?]. exists (filter (fun v => if node_pred_dec p v then true else false) l); split. - apply NoDup_filter; tauto. - intros. unfold predicate_subgraph, predicate_vvalid, predicate_evalid; simpl; intros. rewrite filter_In. unfold Ensembles.In in *. assert (false <> true) by congruence. destruct (node_pred_dec p x); firstorder. + destruct Y as [l ?]. exists (filter (fun e => if (node_pred_dec p (src g e)) then true else false) l); split. - apply NoDup_filter; tauto. - intros e. unfold predicate_subgraph, predicate_vvalid, predicate_evalid; simpl; intros. rewrite filter_In. unfold Ensembles.In in *. assert (false <> true) by congruence. destruct (node_pred_dec p (src g e)); firstorder. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas