proposition: Lemma uf_under_bound_make_set_graph: forall (default_dv: DV) (default_de: DE) (default_dg: DG) (v: addr) (g: UFGraph) (Hn: v <> null) (Hi: ~ vvalid g v) (extract: DV -> nat), extract default_dv = O -> uf_under_bound extract g -> uf_under_bound extract (make_set_Graph default_dv default_de default_dg v g Hn Hi).
proof: Proof. intros. hnf in H0 |-* . simpl. intro x; intros. unfold addValidFunc in H1. destruct (SGBA_VE x v). - hnf in e. subst v. destruct H1; [exfalso; auto |]. clear H1. hnf. intros. rewrite H. destruct p as [p l]. destruct l; simpl; auto. exfalso. apply pfoot_in_cons in H2. destruct H2 as [e [? ?]]. simpl in H3. unfold updateEdgeFunc in H3. pose proof (valid_path_strong_evalid _ _ _ _ H1 H2). hnf in H4. simpl in H4. unfold addValidFunc, updateEdgeFunc in H4. destruct H4 as [? [? ?]]. destruct (equiv_dec (x, tt) e). 1: exfalso; auto. compute in c. destruct H4; auto. destruct (@valid_graph _ _ _ _ g _ (maGraph g) _ H4) as [_ ?]. rewrite H3 in H7. destruct H7; auto. - compute in c. destruct H1; [|exfalso; auto]. hnf. intros. assert (pfoot g p = x /\ valid_path g p) by (apply (make_set_valid_path_pfoot v); auto; exact (maGraph g)). destruct H4. unfold uf_bound in H0. apply H0; auto. Qed.
imports: Coq.Logic.Classical Coq.Lists.List Coq.Sets.Ensembles CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.Relation_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.weak_mark_lemmas CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_computable CertiGraph.graph.FiniteGraph CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.UnionFind CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph