proposition: Lemma labeledgraph_add_edge_ecopy1_left: forall (g g1 g2: Graph) (g1' g2': LGraph) (x l r x0 l0: addr), vvalid g x -> vgamma g x = (null, l, r) -> vcopy1 x g g1 g1' -> extended_copy l (g1: LGraph, g1') (g2: LGraph, g2') -> x0 = LocalGraphCopy.vmap g1 x -> l = null /\ l0 = null \/ l0 = LocalGraphCopy.vmap g2 l -> is_guarded_BinMaFin' (fun v => x0 <> v) (fun e => ~ In e nil) g2' -> x0 <> null -> let g3 := Graph_egen g2 (x, L) (x0, L): Graph in let g3' := labeledgraph_add_edge g2' (x0, L) x0 l0 (null, L): LGraph in ecopy1 (x, L) (g2: LGraph, g2') (g3: LGraph, g3') /\ is_guarded_BinMaFin' (fun v => x0 <> v) (fun e => ~ In e ((x0, L) :: nil)) g3' /\ (x0, L) = LocalGraphCopy.emap g3 (x, L) /\ dst g3' (x0, L) = l0.
proof: Proof. intros. unfold ecopy1. assert (~ evalid g2' (x0, L)) as HH. 1: { eapply is_BinMaFin_not_evalid; eauto; [| intros ? []]. eapply extended_copy_vvalid_mono in H2; [exact H2 |]. eapply vcopy1_copied_root_valid in H1; auto. subst x0; auto. } split; [split; [| split] | split; [| split]]. + reflexivity. + apply WeakMarkGraph.labeledgraph_egen_do_nothing. + assert (g ~=~ g2) as HH0. 1: { destruct H1 as [? _], H2 as [? _]. rewrite <- H2, <- H1; reflexivity. } assert (x0 = LocalGraphCopy.vmap g2 (src g2 (x, L))) as HH1. 1: { rewrite left_right_sound by (rewrite <- (proj1 HH0); auto). destruct H1 as [_ [? _]], H2 as [_ [_ ?]]. subst x0. destruct H2 as [_ [? _]]. rewrite guarded_pointwise_relation_spec in H2. apply H2. unfold Complement, Ensembles.In; intro. apply reachable_by_foot_prop in H3. apply H3. destruct H1 as [_ [? _]]; auto. } destruct H4. - pose proof LocalGraphCopy.labeledgraph_egen_ecopy1_not_vvalid g2 g2' (x, L) (x0, L) x0 l0. apply H7; clear H7; auto. * destruct H4. subst l0. destruct H5 as [[? ? ?] _]. pose proof @valid_not_null' _ _ _ _ (gpredicate_sub_labeledgraph (fun v : addr => x0 <> v) (fun e : addr * LR => ~ In e nil) g2') _ ma' null. intro. apply H5; [| reflexivity]. simpl. rewrite Intersection_spec; split; auto. * inversion H0. rewrite <- (si_dst1 _ _ _ HH0); [| apply (@left_valid _ _ _ _ _ _ g (binGraph _)); auto]. destruct H4; rewrite H9; subst l. intro. apply (@valid_not_null _ _ _ _ g2 _ (maGraph _) null); auto; reflexivity. - pose proof LocalGraphCopy.labeledgraph_egen_ecopy1 g2 g2' (x, L) (x0, L) x0 l0. apply H7; clear H7; auto. subst l0. f_equal. inversion H0. destruct H1 as [? _], H2 as [? _]. rewrite <- H1 in H2. rewrite (si_dst1 _ _ _ H2); auto. apply (@left_valid _ _ _ _ _ _ g (binGraph _)); auto. + eapply is_guarded_BinMaFin'_labeledgraph_add_edge; [auto | | exact H5]. rewrite Same_set_spec; intro e; simpl. rewrite Intersection_spec. assert (e = (x0, L) <-> (x0, L) = e) by (split; intros; congruence). tauto. + simpl. unfold update_elabel; simpl. destruct_eq_dec (x, L) (x, L); auto; congruence. + subst g3'. simpl. unfold updateEdgeFunc. rewrite if_true; reflexivity. Qed.
imports: CertiGraph.lib.Ensembles_ext Coq.Lists.List VST.msl.seplog VST.msl.log_normalize VST.msl.ramification_lemmas VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon 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 CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.graph.graph_morphism CertiGraph.graph.local_graph_copy CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.Graph_Copy Coq.Logic.Classical