proposition: Lemma no_edge_gen_dst_equiv: forall e p (g: Graph) pa x y, ~ In e (snd p) -> (pregraph_gen_dst g e pa) |= p is x ~o~> y satisfying (fun _ => True) <-> g |= p is x ~o~> y satisfying (fun _ => True).
proof: Proof. intros. destruct p as [p l]. simpl in H. split; intro; destruct H0 as [[? ?] [? ?]]; split; split; auto; clear H0 H3. - clear H2. revert p H H1. induction l; intros. 1: simpl in *; auto. rewrite pfoot_cons in H1. remember (dst (pregraph_gen_dst g e pa) a) as w. simpl in Heqw. unfold updateEdgeFunc in Heqw. destruct (equiv_dec e a). + unfold Equivalence.equiv in e0; exfalso; apply H; left; auto. + rewrite pfoot_cons. apply IHl. * intro. apply H; right; auto. * subst w. auto. - clear H1. revert p H H2. induction l; intros. 1: simpl in *; auto. rewrite valid_path_cons_iff in H2 |-* . destruct H2 as [? [? ?]]. split; [|split]. + simpl in H0. auto. + hnf in H1. simpl in H1. unfold updateEdgeFunc in H1. destruct (equiv_dec e a). 1: unfold Equivalence.equiv in e0; exfalso; apply H; left; auto. apply H1. + remember (dst (pregraph_gen_dst g e pa) a) as w. simpl in Heqw. unfold updateEdgeFunc in Heqw. destruct (equiv_dec e a). 1: exfalso; apply H; left; auto. subst w. apply IHl; auto. intro; apply H; right; auto. - clear H2. revert p H H1. induction l; intros. 1: simpl; auto. rewrite pfoot_cons. remember (dst (pregraph_gen_dst g e pa) a) as w. simpl in Heqw. unfold updateEdgeFunc in Heqw. destruct (equiv_dec e a). 1: exfalso; apply H; left; auto. subst w. apply IHl. + intro; apply H; right; auto. + rewrite pfoot_cons in H1. auto. - clear H1. revert p H H2. induction l; intros. 1: simpl in *; auto. rewrite valid_path_cons_iff in H2 |-* . destruct H2 as [? [? ?]]. split; [|split]. + simpl; auto. + hnf. simpl. unfold updateEdgeFunc. destruct (equiv_dec e a). 1: unfold Equivalence.equiv in e0; exfalso; apply H; left; auto. apply H1. + remember (dst (pregraph_gen_dst g e pa) a) as w. simpl in Heqw. unfold updateEdgeFunc in Heqw. destruct (equiv_dec e a). 1: exfalso; apply H; left; auto. subst w. apply IHl; auto. intro; apply H; right; auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.relation_list CertiGraph.lib.List_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 Coq.Lists.List CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind