proposition: Lemma make_set_valid_path_pfoot: forall (v: addr) (g: PreGraph addr (addr * unit)) x p (Hn: v <> null) (Hi: ~ vvalid g v) (Hm: MathGraph g is_null_SGBA), x <> v -> pfoot (make_set_pregraph v g) p = x -> valid_path (make_set_pregraph v g) p -> pfoot g p = x /\ valid_path g p.
proof: Proof. intros. destruct p as [p l]. assert (forall e, List.In e l -> e <> (v, tt)). { intros. apply (valid_path_strong_evalid _ _ _ e) in H1; auto. hnf in H1. simpl in H1. unfold addValidFunc, updateEdgeFunc in H1. destruct H1 as [? [? ?]]. intro. destruct (equiv_dec (v, tt) e). 2: compute in c; auto. destruct H4; auto. destruct Hm. apply valid_not_null in H4; simpl; auto. } split. - clear H1. revert p H0. induction l; intros. 1: simpl in H0 |-* ; auto. assert (forall e : addr * unit, List.In e l -> e <> (v, tt)) by (intros; apply H2; right; auto). specialize (IHl H1). clear H1. rewrite pfoot_cons in H0 |-* . simpl dst in H0. unfold updateEdgeFunc in H0. destruct (equiv_dec (v, tt) a). + hnf in e. assert (a <> (v, tt)) by (apply H2; left; auto). exfalso; auto. + apply IHl; auto. - assert (p <> v). { intro. subst p. destruct l. 1: simpl in H0; auto. simpl in H1. destruct H1. assert (strong_evalid (make_set_pregraph v g) p) by (destruct l; [|destruct H3]; auto). clear H3. hnf in H4. simpl in H4. unfold addValidFunc, updateEdgeFunc in H1, H4. destruct H4 as [? _]. assert (p <> (v, tt)) by (apply H2; left; auto). destruct (equiv_dec (v, tt) p). 1: hnf in e; auto. destruct H3; auto. destruct Hm. apply valid_graph in H3. destruct H3 as [? _]. rewrite <- H1 in H3. auto. } clear H0. revert p H1 H3. induction l; intros. + simpl in H1. unfold addValidFunc in H1. simpl. destruct H1; [|exfalso]; auto. + assert (forall e : addr * unit, List.In e l -> e <> (v, tt)) by (intros; apply H2; right; auto). specialize (IHl H0). clear H0. assert (a <> (v, tt)) by (apply H2; left; auto). rewrite valid_path_cons_iff in H1 |-* . destruct H1 as [? [? ?]]. split; [|split]. * simpl in H1. unfold updateEdgeFunc in H1. destruct (equiv_dec (v, tt) a); [exfalso|]; auto. * hnf in H4. simpl in H4. unfold addValidFunc, updateEdgeFunc in H4. destruct H4 as [? [? ?]]. destruct (equiv_dec (v, tt) a); [hnf in e; exfalso|]; auto. destruct H4; [|exfalso]; auto. clear c. destruct H6. 2: destruct Hm; apply valid_graph in H4; destruct H4; rewrite H6 in H4; exfalso; auto. destruct H7. 2: destruct Hm; apply valid_graph in H4; destruct H4; hnf in H8; simpl in H8; rewrite H7 in H8; exfalso; destruct H8; auto. hnf. split; auto. * simpl dst in H5. unfold updateEdgeFunc in H5. destruct (equiv_dec (v, tt) a); [hnf in e; exfalso|]; auto. apply IHl; auto. destruct H4 as [? _]. simpl in H4. unfold addValidFunc in H4. destruct H4; [|exfalso]; auto. destruct Hm. apply valid_graph in H4. destruct H4 as [_ ?]. hnf in H4. simpl in H4. intro. rewrite H6 in H4. destruct H4; 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