proposition: Lemma kruskal_minimal_induction: forall ldiff lsame (g t1 t2: @EdgeListGG size) {fg: FiniteGraph g} {ft1: FiniteGraph t1} {ft2: FiniteGraph t2}, labeled_spanning_uforest t1 g -> labeled_spanning_uforest t2 g -> Permutation (ldiff++lsame) (EList t1) -> incl lsame (EList t2) -> (forall e, In e ldiff -> ~ In e (EList t2)) -> (forall e, In e ldiff -> exists p l, connected_by_path t2 p (src t1 e) (dst t1 e) /\ NoDup p /\ fits_upath t2 l p /\ forall e', In e' l -> elabel g e' <= elabel g e) -> (forall i j, 0 <= i < j -> j < Zlength ldiff -> elabel g (Znth i ldiff) <= elabel g (Znth j ldiff)) -> exists lmsf, Zlength ldiff = Zlength lmsf /\ Permutation (lmsf++lsame) (EList t2) /\ (forall i, 0 <= i < Zlength lmsf -> elabel g (Znth i lmsf) <= elabel g (Znth i ldiff)) .
proof: Proof. induction ldiff; intros. rename H5 into Hsorted. + exists nil. split. auto. rewrite app_nil_l in H1; rewrite app_nil_l. assert (NoDup lsame). apply NoDup_Perm_EList in H1; auto. split. apply NoDup_Permutation. auto. apply NoDup_EList. intros; split; intros. apply H2; auto. apply EList_evalid in H6. destruct x as [u v]. destruct (in_dec E_EqDec (u,v) lsame). auto. assert (connected_by_path t2 (u::v::nil) u v). split. simpl. split. exists (u,v). split. apply evalid_strong_evalid; auto. left. rewrite (src_fst t2), (dst_snd t2) by auto. auto. apply evalid_uv_vvalid in H6. apply H6. simpl. split; auto. assert (connected t1 u v). apply H. apply H0. exists (u::v::nil). auto. destruct H8 as [p ?]. pose proof (connected_exists_list_edges t1 p u v H8). destruct H9 as [l ?]. assert (~ In (u,v) l). unfold not; intros. assert (evalid t1 (u,v)). apply (fits_upath_evalid t1 p l (u,v) H9 ). auto. rewrite <- EList_evalid in H11. apply (Permutation_in (l':=lsame)) in H11. contradiction. apply Permutation_sym. apply H1. apply (sound_fits_upath_transfer p l t1 t2) in H9; auto. 2: { intros. rewrite <- (spanning_preserves_vertices g t1). apply (spanning_preserves_vertices g t2). apply H0. apply H. } 2: { intros. assert (In e lsame). apply (Permutation_in (l:=(EList t1))). apply Permutation_sym. apply H1. apply EList_evalid. apply (fits_upath_evalid t1 p l); auto. rewrite <- EList_evalid. apply H2. auto. } apply (forest_edge' p l t2 (u,v)) in H9. contradiction. apply H0. apply H0. auto. rewrite (src_fst t2), (dst_snd t2) by auto. simpl. split. apply valid_upath_exists_list_edges'. exists l; auto. apply H8. intros. rewrite Zlength_nil in Hsorted. lia. + rename H5 into Hsorted. simpl in H2. destruct a as (u1,v1). assert (Ha: evalid t1 (u1,v1)). rewrite <- EList_evalid. apply (Permutation_in (l:=((u1, v1) :: ldiff ++ lsame))). apply H1. left; auto. assert (Ht2_u1v1: ~ evalid t2 (u1,v1)). rewrite <- EList_evalid. apply H3. left; auto. assert (H_NoDup_ldiff: NoDup ((u1,v1)::ldiff++lsame)). apply NoDup_Perm_EList in H1; auto. assert (connected t2 u1 v1). apply H0. apply H. exists (u1::v1::nil). assert (connected_by_path t1 (src t1 (u1, v1) :: dst t1 (u1, v1) :: nil) (src t1 (u1, v1)) (dst t1 (u1, v1))). apply (trivial_path1 t1 (u1,v1)). apply evalid_strong_evalid; auto. rewrite (src_fst t1), (dst_snd t1) in H5 by auto. auto. destruct H5 as [p2' ?]. assert (exists p', connected_by_path t2 p' u1 v1 /\ simple_upath t2 p'). apply (connected_by_upath_exists_simple_upath t2 p2' u1 v1). auto. clear p2' H5. destruct H6 as [p2 [? ?]]. assert (exists l2, fits_upath t2 l2 p2). apply (connected_exists_list_edges t2 p2 u1 v1). auto. destruct H7 as [l2 ?]. assert (H_l2_weight: forall e, In e l2 -> elabel g e <= elabel g (u1,v1)). { intros. specialize H4 with ((u1,v1)). assert (exists (p : upath) (l : list EType), connected_by_path t2 p (src t1 (u1, v1)) (dst t1 (u1, v1)) /\ NoDup p /\ fits_upath t2 l p /\ (forall e' : EType, In e' l -> elabel g e' <= elabel g (u1, v1))). apply H4. left; auto. destruct H9 as [p' [l' [? [? [? ?]]]]]. rewrite (src_fst t1), (dst_snd t1) in H9 by auto. simpl in H9. assert (l' = l2). assert (unique_simple_upath t2). apply H0. assert (p' = p2). apply (H13 u1 v1 p' p2); auto. split. apply H9. apply H10. apply (uforest'_unique_lpath p2 l' l2 t2); auto. apply H0. rewrite <- H14; auto. apply H12. rewrite H13. auto. } assert (exists b, In b (EList t2) /\ ~ In b (EList t1) /\ bridge t2 b u1 v1). { assert (exists b : EType, In b l2 /\ ~ In b (EList t1)). apply list_not_forall_exists. unfold not; intros. subst l2. destruct p2. destruct H5. destruct H8. inversion H8. destruct p2. destruct H5. destruct H8. inversion H8. inversion H9. subst u1; subst v1. destruct H. destruct H. destruct H11. destruct H11. assert (src t1 (v, v) <> dst t1 (v, v)). auto. rewrite (src_fst t1), (dst_snd t1) in H14 by auto. contradiction. simpl in H7; auto. apply EList_In_dec. unfold not; intros. assert (fits_upath t1 l2 p2). apply (sound_fits_upath_transfer p2 l2 t2 t1); auto. intros; split; intros. apply (spanning_preserves_vertices g). apply H. apply (spanning_preserves_vertices g t2). apply H0. auto. apply (spanning_preserves_vertices g). apply H0. apply (spanning_preserves_vertices g t1). apply H. auto. intros. rewrite <- EList_evalid. apply H8. auto. assert (connected_by_path t1 p2 u1 v1). split. apply valid_upath_exists_list_edges'. exists l2. auto. apply H5. assert (In (u1,v1) l2). apply (forest_edge' p2 l2 t1 (u1,v1)); auto. apply H. apply evalid_strong_evalid; auto. rewrite (src_fst t1), (dst_snd t1) by auto. auto. apply Ht2_u1v1. apply (fits_upath_evalid t2 p2 l2); auto. destruct H8 as [b [? ?]]. exists b. split. apply EList_evalid. apply (fits_upath_evalid t2 p2 l2); auto. split. auto. apply (forest_simple_bridge p2 l2); auto. apply H0. } destruct H8 as [b [? [? ?]]]. assert (elabel g b <= elabel g (u1,v1)). { assert (exists (p : upath) (l : list EType), connected_by_path t2 p (src t1 (u1, v1)) (dst t1 (u1, v1)) /\ NoDup p /\ fits_upath t2 l p /\ (forall e' : EType, In e' l -> elabel g e' <= elabel g (u1, v1))). apply H4. left; auto. destruct H11 as [p [l ?]]. apply H11. unfold bridge in H10. apply (H10 p l). rewrite (src_fst t1), (dst_snd t1) in H11 by auto. apply H11. apply H11. } pose proof (bridge_splittable p2 t2 u1 v1 b H5 H10). destruct H12 as [p2a [p2b [? ?]]]. assert (Hevalid_b: evalid t2 b). apply EList_evalid in H8; auto. rewrite (src_fst t2), (dst_snd t2) in H13 by auto. assert (exists l2a l2x l2b : list EType, fits_upath t2 l2a p2a /\ fits_upath t2 l2b p2b /\ l2 = l2a ++ l2x ++ l2b). apply (fits_upath_split t2 p2a p2b l2). rewrite <- H12. auto. destruct H14 as [l2a [l2x [l2b [? [? ?]]]]]. destruct b as (u2,v2). simpl in H13. pose proof (size_bound g) as size_bound. assert (Hu1: 0 <= u1 < size). rewrite <- (vertex_valid t1). apply evalid_uv_vvalid in Ha; apply Ha. assert (Hv1: 0 <= v1 < size). rewrite <- (vertex_valid t1). apply evalid_uv_vvalid in Ha; apply Ha. assert (Hw1: Int.min_signed <= (elabel t1 (u1, v1)) <= Int.max_signed). apply weight_valid; auto. set (remove:=(@EdgeListGG_eremove size size_bound t2 (u2,v2))). set (swap:=(@EdgeListGG_adde size size_bound remove u1 v1 (elabel t1 (u1, v1))) Hu1 Hv1 Hw1). assert (Hevalid_swap_u1v1: evalid swap (u1,v1)). simpl. unfold addValidFunc, removeValidFunc. right; auto. set (fswap:=finite swap). assert (Hnew: exists p l, connected_by_path swap p u2 v2 /\ fits_upath swap l p /\ In (u1,v1) l /\ forall e', In e' l -> elabel g e' <= elabel g (u1,v1)). { destruct H13; destruct H13. + exists ((rev p2a)++(rev p2b)). exists (rev l2a ++ (u1,v1)::nil ++ rev l2b). assert (fits_upath swap (rev l2a ++ (u1, v1) :: nil ++ rev l2b) (rev p2a ++ rev p2b)). { apply (fits_upath_app swap (rev p2a) (rev p2b) (rev l2a) (rev l2b) (u1,v1) u1 v1). apply fits_upath_rev. apply (sound_fits_upath_transfer _ _ t2 swap); auto. simpl. intros; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p2a l2a); auto. unfold not; intros. subst e. apply (fits_upath_vertex_in_path t2 p2a (u2,v2) l2a) in H18. rewrite (src_fst t2), (dst_snd t2) in H18 by auto. simpl in H18; destruct H18. assert (NoDup p2). apply H6. rewrite H12 in H20. pose proof (NoDup_app_not_in VType p2a p2b H20). apply (H21 v2). auto. apply hd_error_In. apply H17. auto. apply fits_upath_rev. apply (sound_fits_upath_transfer _ _ t2 swap); auto. simpl. intros; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p2b l2b); auto. unfold not; intros. subst e. apply (fits_upath_vertex_in_path t2 p2b (u2,v2) l2b) in H18. rewrite (src_fst t2), (dst_snd t2) in H18 by auto. simpl in H18; destruct H18. assert (NoDup p2). apply H6. rewrite H12 in H20. pose proof (NoDup_app_not_in VType p2a p2b H20). apply (H21 u2). auto. apply last_error_In. apply H13. auto. auto. rewrite <- rev_hd_last. apply H13. rewrite rev_hd_last, rev_involutive. apply H17. split. apply add_edge_strong_evalid. simpl. apply (connected_vvalid t2 u1 v1). exists p2; apply H5. simpl. apply (connected_vvalid t2 u1 v1). exists p2; apply H5. left. rewrite (src_fst swap), (dst_snd swap); auto. } split. split. apply valid_upath_exists_list_edges'. exists (rev l2a ++ (u1, v1) :: nil ++ rev l2b); auto. split. apply (hd_error_app (rev p2b) (rev p2a) u2). rewrite rev_hd_last, rev_involutive. apply H13. apply (last_err_app (rev p2a) (rev p2b) v2). rewrite <- rev_hd_last. apply H17. split. auto. split. simpl. apply in_or_app. right; left; auto. intros. apply in_app_or in H19. destruct H19. apply in_rev in H19. apply H_l2_weight. rewrite H16. apply in_or_app. left; auto. simpl in H19. destruct H19. subst e'. lia. apply in_rev in H19. apply H_l2_weight. rewrite H16. apply in_or_app. right; apply in_or_app. auto. + exists (p2b++p2a). exists (l2b ++ (u1,v1)::nil ++ l2a). assert (fits_upath swap (l2b ++ (u1, v1) :: nil ++ l2a) (p2b ++ p2a)). { apply (fits_upath_app swap (p2b) (p2a) l2b (l2a) (u1,v1) v1 u1). apply (sound_fits_upath_transfer _ _ t2 swap); auto. simpl. intros; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p2b l2b); auto. unfold not; intros. subst e. apply (fits_upath_vertex_in_path t2 p2b (u2,v2) l2b) in H18. rewrite (src_fst t2), (dst_snd t2) in H18 by auto. simpl in H18. destruct H18. assert (NoDup p2). apply H6. rewrite H12 in H20. pose proof (NoDup_app_not_in VType p2a p2b H20). apply (H21 v2). auto. apply last_error_In. apply H13. auto. auto. apply (sound_fits_upath_transfer _ _ t2 swap); auto. simpl. intros; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p2a l2a); auto. unfold not; intros. subst e. apply (fits_upath_vertex_in_path t2 p2a (u2,v2) l2a) in H18. rewrite (src_fst t2), (dst_snd t2) in H18 by auto. simpl in H18. destruct H18. assert (NoDup p2). apply H6. rewrite H12 in H20. pose proof (NoDup_app_not_in VType p2a p2b H20). apply (H21 u2). auto. apply hd_error_In. apply H17. auto. apply H17. apply H13. split. apply add_edge_strong_evalid. simpl. apply (connected_vvalid t2 u1 v1). exists p2; apply H5. simpl. apply (connected_vvalid t2 u1 v1). exists p2; apply H5. right. rewrite (src_fst swap), (dst_snd swap); auto. } split. split. apply valid_upath_exists_list_edges'. exists (l2b ++ (u1, v1) :: nil ++ l2a); auto. split. apply hd_error_app. apply H17. apply last_err_app. apply H13. split. auto. split. simpl. apply in_or_app. right; left; auto. intros. apply in_app_or in H19. destruct H19. apply H_l2_weight. rewrite H16. apply in_or_app. right. apply in_or_app. auto. simpl in H19. destruct H19. subst e'. lia. apply H_l2_weight. rewrite H16. apply in_or_app. left; auto. } destruct Hnew as [p' [l' Hnew]]. set (b:=(u2,v2)). specialize IHldiff with ((u1,v1)::lsame) g t1 swap ft1 fswap. assert (exists lmsf : list EType, Zlength ldiff = Zlength lmsf /\ Permutation (lmsf ++ (u1, v1) :: lsame) (EList swap) /\ (forall i : Z, 0 <= i < Zlength lmsf -> elabel g (Znth i lmsf) <= elabel g (Znth i ldiff))). apply IHldiff; clear IHldiff. auto. auto. auto. { split. split. { split. intros. simpl in H17. apply (spanning_preserves_vertices g t2). apply H0. auto. split. intros. simpl in H17. unfold addValidFunc, removeValidFunc in H17. destruct H17. destruct H17. apply H0. auto. apply H. rewrite H17. auto. split. simpl. unfold addValidFunc, removeValidFunc, updateEdgeFunc, EquivDec.equiv_dec. intros. destruct (E_EqDec (u1, v1) e). unfold Equivalence.equiv in e0. subst e. rewrite (src_fst g). auto. apply H. auto. unfold RelationClasses.complement, Equivalence.equiv in c. destruct H17. destruct H17. apply H0. auto. auto. symmetry in H17; contradiction. simpl. unfold addValidFunc, removeValidFunc, updateEdgeFunc, EquivDec.equiv_dec. intros. destruct (E_EqDec (u1, v1) e). unfold Equivalence.equiv in e0. subst e. rewrite (dst_snd g); auto. apply H. auto. unfold RelationClasses.complement, Equivalence.equiv in c. destruct H17. destruct H17. apply H0. auto. auto. symmetry in H17; contradiction. } split. { assert (uforest' remove /\ ~ connected remove (src t2 b) (dst t2 b)). apply (remove_edge_uforest' t2 b). auto. apply H0. apply EList_evalid in H8. auto. destruct H17. apply add_edge_uforest'. auto. simpl. apply (spanning_preserves_vertices g t2). apply H0. apply (spanning_preserves_vertices g t1). apply H. apply evalid_uv_vvalid in Ha; apply Ha. simpl. apply (spanning_preserves_vertices g t2). apply H0. apply (spanning_preserves_vertices g t1). apply H. apply evalid_uv_vvalid in Ha; apply Ha. unfold not, connected; intros. destruct H19 as [p ?]. pose proof (connected_exists_list_edges remove p u1 v1 H19). destruct H20 as [l ?]. assert (fits_upath t2 l p). apply (sound_fits_upath_transfer p l _ t2) in H20. auto. simpl; intros; split; auto. intros. apply (fits_upath_evalid _ p l e H20) in H21. simpl in H21. unfold removeValidFunc in H21. apply H21. assert (connected_by_path t2 p u1 v1). split. apply valid_upath_exists_list_edges'. exists l. auto. apply H19. assert (In b l). apply (H10 p l). auto. auto. assert (evalid remove b). apply (fits_upath_evalid _ p l). auto. auto. pose proof (eremove_evalid1 H24). auto. } { unfold spanning; intros. assert (spanning t2 g). apply H0. unfold spanning in H17. rewrite H17. clear H17. split; intros; destruct H17 as [p ?]. pose proof (connected_by_upath_exists_simple_upath t2 p u v H17). clear p H17. destruct H18 as [p [? ?]]. assert (exists l, fits_upath t2 l p). apply (connected_exists_list_edges t2 p u v); auto. destruct H19 as [l ?]. destruct (in_dec E_EqDec (u2,v2) l). unfold b; fold swap. assert (HNoDup_l: NoDup l). apply (simple_upath_list_edges_NoDup t2 p l); auto. pose proof (fits_upath_split' t2 p l (u2,v2) H19 i). destruct H20 as [pb1 [pb2 [lb1 [lb2 ?]]]]. { destruct H20 as [? [? [? [? ?]]]]. rewrite (src_fst t2), (dst_snd t2) in H21 by auto. destruct H21; simpl in H21. assert (Hc1: connected swap u u2). exists pb1. split. apply valid_upath_exists_list_edges'. exists lb1. apply (sound_fits_upath_transfer pb1 lb1 t2 swap); auto. intros; simpl; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p l). auto. rewrite H24. apply in_or_app. left; auto. unfold not; intros. rewrite H24 in HNoDup_l. simpl in HNoDup_l. subst e. apply (NoDup_app_not_in _ _ _ HNoDup_l) in H25. apply H25. left; auto. destruct H21. destruct pb1. inversion H21. destruct H17. rewrite H20 in H26. destruct H26; inversion H26. subst v0. simpl; auto. assert (Hc2: connected swap u2 v2). exists p'; apply Hnew. assert (Hc3: connected swap v2 v). exists pb2. split. apply valid_upath_exists_list_edges'. exists lb2. apply (sound_fits_upath_transfer pb2 lb2 t2 swap); auto. intros; simpl; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p l). auto. rewrite H24. apply in_or_app. right. apply in_or_app. right; auto. unfold not; intros. rewrite H24 in HNoDup_l. simpl in HNoDup_l. subst e. apply NoDup_app_r in HNoDup_l. apply NoDup_cons_2 in HNoDup_l. contradiction. split. apply H21. destruct pb2. destruct H21. inversion H25. rewrite <- (last_err_split2 pb1 pb2 v0). rewrite <- H20. apply H17. apply (connected_trans swap u v2 v); auto. apply (connected_trans swap u u2 v2); auto. assert (Hc1: connected swap u v2). exists pb1. split. apply valid_upath_exists_list_edges'. exists lb1. apply (sound_fits_upath_transfer pb1 lb1 t2 swap); auto. intros; simpl; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p l). auto. rewrite H24. apply in_or_app. left; auto. unfold not; intros. rewrite H24 in HNoDup_l. simpl in HNoDup_l. subst e. apply (NoDup_app_not_in _ _ _ HNoDup_l) in H25. apply H25. left; auto. destruct H21. destruct pb1. inversion H21. destruct H17. rewrite H20 in H26. destruct H26; inversion H26. subst v0. simpl; auto. assert (Hc3: connected swap u2 v). exists pb2. split. apply valid_upath_exists_list_edges'. exists lb2. apply (sound_fits_upath_transfer pb2 lb2 t2 swap); auto. intros; simpl; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p l). auto. rewrite H24. apply in_or_app. right. apply in_or_app. right; auto. unfold not; intros. rewrite H24 in HNoDup_l. simpl in HNoDup_l. subst e. apply NoDup_app_r in HNoDup_l. apply NoDup_cons_2 in HNoDup_l. contradiction. split. apply H21. destruct pb2. destruct H21. inversion H25. rewrite <- (last_err_split2 pb1 pb2 v0). rewrite <- H20. apply H17. apply (connected_trans swap u u2 v); auto. apply (connected_trans swap u v2 u2); auto. apply connected_symm. exists p'. apply Hnew. } exists p. split. apply add_edge_valid_upath. unfold not; simpl; unfold removeValidFunc; intros. destruct H20; contradiction. apply (remove_edge_valid_upath _ _ p l); auto. apply H17. apply H17. pose proof (connected_by_upath_exists_simple_upath swap p u v H17). clear p H17. destruct H18 as [p [? ?]]. assert (exists l, fits_upath swap l p). apply (connected_exists_list_edges swap p u v); auto. destruct H19 as [l ?]. destruct (in_dec E_EqDec (u1,v1) l). assert (HNoDup_l: NoDup l). apply (simple_upath_list_edges_NoDup swap p l); auto. pose proof (fits_upath_split' swap p l (u1,v1) H19 i). destruct H20 as [pa1 [pa2 [la1 [la2 ?]]]]. { destruct H20 as [? [? [? [? ?]]]]. rewrite (src_fst swap), (dst_snd swap) in H21 by auto. destruct H21; simpl in H21. assert (Hc1: connected t2 u u1). exists pa1. split. apply valid_upath_exists_list_edges'. exists la1. apply (sound_fits_upath_transfer pa1 la1 swap t2); auto. intros; simpl; split; auto. intros. assert (evalid swap e). apply (fits_upath_evalid swap p l); auto. rewrite H24. apply in_or_app. left; auto. simpl in H26. unfold addValidFunc, removeValidFunc in H26. destruct H26. apply H26. rewrite H24 in HNoDup_l. simpl in HNoDup_l. subst e. apply (NoDup_app_not_in _ _ _ HNoDup_l) in H25. exfalso. apply H25. left; auto. destruct H21. destruct pa1. inversion H21. destruct H17. rewrite H20 in H26. destruct H26; inversion H26. subst v0. simpl; auto. assert (Hc3: connected t2 v1 v). exists pa2. split. apply valid_upath_exists_list_edges'. exists la2. apply (sound_fits_upath_transfer pa2 la2 swap t2); auto. intros; simpl; split; auto. intros. assert (evalid swap e). apply (fits_upath_evalid swap p l). auto. rewrite H24. apply in_or_app. right. apply in_or_app. right; auto. simpl in H26. unfold addValidFunc, removeValidFunc in H26. destruct H26. apply H26. rewrite H24 in HNoDup_l. simpl in HNoDup_l. subst e. apply NoDup_app_r in HNoDup_l. apply NoDup_cons_2 in HNoDup_l. contradiction. split. apply H21. destruct pa2. destruct H21. inversion H25. rewrite <- (last_err_split2 pa1 pa2 v0). rewrite <- H20. apply H17. apply (connected_trans t2 u v1 v); auto. apply (connected_trans t2 u u1 v1); auto. exists p2. auto. assert (Hc1: connected t2 u v1). exists pa1. split. apply valid_upath_exists_list_edges'. exists la1. apply (sound_fits_upath_transfer pa1 la1 swap t2); auto. intros; simpl; split; auto. intros. assert (evalid swap e). apply (fits_upath_evalid swap p l). auto. rewrite H24. apply in_or_app. left; auto. simpl in H26. unfold addValidFunc, removeValidFunc in H26. destruct H26. apply H26. rewrite H24 in HNoDup_l. simpl in HNoDup_l. subst e. apply (NoDup_app_not_in _ _ _ HNoDup_l) in H25. exfalso. apply H25. left; auto. destruct H21. destruct pa1. inversion H21. destruct H17. rewrite H20 in H26. destruct H26; inversion H26. subst v0. simpl; auto. assert (Hc2: connected t2 v1 u1). apply connected_symm. exists p2; auto. assert (Hc3: connected t2 u1 v). exists pa2. split. apply valid_upath_exists_list_edges'. exists la2. apply (sound_fits_upath_transfer pa2 la2 swap t2); auto. intros; simpl; split; auto. intros. assert (evalid swap e). apply (fits_upath_evalid swap p l). auto. rewrite H24. apply in_or_app. right. apply in_or_app. right; auto. simpl in H26. unfold addValidFunc, removeValidFunc in H26. destruct H26. apply H26. rewrite H24 in HNoDup_l. simpl in HNoDup_l. subst e. apply NoDup_app_r in HNoDup_l. apply NoDup_cons_2 in HNoDup_l. contradiction. split. apply H21. destruct pa2. destruct H21. inversion H25. rewrite <- (last_err_split2 pa1 pa2 v0). rewrite <- H20. apply H17. apply (connected_trans t2 u u1 v); auto. apply (connected_trans t2 u v1 u1); auto. } exists p. split. apply (add_edge_unaffected _ (u1,v1) u1 v1 p l) in H19. apply (remove_edge_unaffected t2 (u2,v2)) in H19. auto. apply valid_upath_exists_list_edges'. exists l; auto. auto. apply H17. } split. unfold preserve_vlabel; intros. destruct vlabel. destruct vlabel. auto. unfold preserve_elabel; intros. simpl in H17. unfold addValidFunc, removeValidFunc in H17. simpl. unfold update_elabel. unfold EquivDec.equiv_dec. destruct E_EqDec. unfold Equivalence.equiv in e0. subst e. apply H. auto. unfold RelationClasses.complement, Equivalence.equiv in c. destruct H17. apply H0. apply H17. symmetry in H17. contradiction. } apply (Permutation_trans (l':=((u1, v1) :: ldiff ++ lsame))). 2: auto. apply (Permutation_trans (l':=((u1, v1) :: lsame ++ ldiff))). apply Permutation_app_comm. apply perm_skip. apply Permutation_app_comm. unfold incl; intros. apply EList_evalid. simpl. unfold addValidFunc, removeValidFunc. destruct H17. right; auto. left; split. apply H2 in H17. apply EList_evalid in H17. auto. unfold not; intros. subst a. apply H9. apply (Permutation_in (l:=((u1, v1) :: ldiff ++ lsame))). auto. right. apply in_or_app. right; auto. intros. rewrite EList_evalid. simpl. unfold addValidFunc, removeValidFunc, not; intros. destruct H18. destruct H18. rewrite <- EList_evalid in H18. apply H3 in H18. auto. right; auto. subst e. apply NoDup_cons_2 in H_NoDup_ldiff. apply H_NoDup_ldiff. apply in_or_app. left; auto. { intros. unfold b; fold swap. assert (exists (p : upath) (l : list EType), connected_by_path t2 p (src t1 e) (dst t1 e) /\ NoDup p /\ fits_upath t2 l p /\ (forall e' : EType, In e' l -> elabel g e' <= elabel g e)). apply H4. right; auto. destruct H18 as [p [l [? [? [? ?]]]]]. destruct (in_dec E_EqDec (u2,v2) l). + pose proof (fits_upath_split' t2 p l (u2,v2) H20 i). destruct H22 as [pb1 [pb2 [lb1 [lb2 ?]]]]. destruct H22 as [? [? [? [? ?]]]]. assert (Hl: NoDup l). apply (simple_upath_list_edges_NoDup t2 p). split. apply H18. auto. auto. rewrite (src_fst t2), (dst_snd t2) in H23 by auto. simpl in H23. set (u:=src t1 e). set (v:=dst t1 e). destruct H23; destruct H23. ++ set (pnew:=(pb1 ++ (tail p') ++ (tail pb2))). set (lnew:=(lb1++l'++lb2)). assert (Hpb1: last_error pb1 = hd_error p'). { rewrite H23. symmetry. apply Hnew. } assert (Hpb2: last_error p' = hd_error pb2). { rewrite H27. apply Hnew. } assert (fits_upath swap lnew pnew). { unfold pnew, lnew. destruct l'. destruct Hnew as [? [? [? ?]]]. contradiction. destruct p'. destruct Hnew as [? [? [? ?]]]. contradiction. destruct p'. destruct Hnew as [? [? [? ?]]]. simpl in H25; contradiction. replace (lb1 ++ (e0 :: l') ++ lb2) with (lb1 ++ (e0 :: nil) ++ (l'++lb2)). 2: simpl; auto. apply (fits_upath_app _ _ _ _ _ e0 u2 v3). - apply (sound_fits_upath_transfer pb1 lb1 t2 swap); auto. simpl. intros; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 pb1 lb1); auto. unfold not; intros. subst e1. rewrite H26 in Hl. apply (NoDup_app_not_in _ _ _ Hl) in H28. apply H28. simpl; left; auto. - destruct pb2. inversion H27. destruct pb2. destruct lb2. simpl. do 2 rewrite app_nil_r. simpl in H27; inversion H27. subst v4. apply Hnew. destruct Hnew as [? [? [? ?]]]. simpl in H25. contradiction. destruct lb2. destruct Hnew as [? [? [? ?]]]. simpl in H25. contradiction. apply (fits_upath_app _ _ _ _ _ e1 v2 v5). apply Hnew. apply (sound_fits_upath_transfer _ _ t2 swap); auto. simpl; intros; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left; split. apply (fits_upath_evalid t2 (v4::v5::pb2) (e1::lb2)); auto. right; auto. unfold not; intros. subst e2. rewrite H26 in Hl. apply NoDup_app_r in Hl. apply (NoDup_app_not_in EType ((u2,v2)::nil) (e1::lb2) Hl (u2,v2)). left; auto. right; auto. apply H25. simpl. apply Hnew. simpl; auto. simpl in H27; inversion H27. subst v4. destruct H25. assert (evalid t2 e1). apply (fits_upath_evalid t2 p l); auto. rewrite H26. apply in_or_app. right. apply in_or_app. right. left; auto. split. split. simpl. unfold addValidFunc, removeValidFunc. left. split. apply H25. unfold not; intros. subst e1. rewrite H26 in Hl. apply NoDup_app_r in Hl. apply (NoDup_app_not_in EType ((u2,v2)::nil) ((u2,v2)::lb2) Hl (u2,v2)). left; auto. left; auto. simpl. unfold updateEdgeFunc. unfold EquivDec.equiv_dec. destruct E_EqDec. unfold Equivalence.equiv in e2. subst e1. contradiction. apply evalid_strong_evalid in H29; auto. apply H29. simpl. unfold updateEdgeFunc. unfold EquivDec.equiv_dec. destruct E_EqDec. unfold Equivalence.equiv in e2. subst e1. contradiction. apply H25. - auto. - simpl. auto. - destruct Hnew as [? [? [? ?]]]. destruct H29. destruct H28. destruct H33. simpl in H33; inversion H33. subst v0. apply H29. } assert (connected_by_path swap pnew u v). split. apply valid_upath_exists_list_edges'. exists lnew; auto. unfold pnew; split. destruct H18. rewrite H22 in H29; destruct H29. destruct pb1. inversion H23. simpl in H29. simpl. auto. destruct pb2. inversion H27. destruct pb2. simpl in Hpb2. simpl in H27. inversion H27. subst v0. destruct H18. destruct H29. rewrite H22 in H30. rewrite last_err_appcons in H30. inversion H30. simpl. rewrite app_nil_r. unfold v; rewrite <- H32. subst v2. destruct Hnew as [? [? [? ?]]]. destruct p'. inversion Hpb2. destruct p'. destruct l'. contradiction. simpl in H32; contradiction. simpl. rewrite last_error_cons in Hpb2. apply last_err_app. auto. unfold not; intros. inversion H35. simpl. apply last_err_app. apply last_err_app. destruct H18. destruct H29. rewrite H22 in H30. rewrite last_err_split2 in H30. rewrite last_error_cons in H30. auto. unfold not; intros. inversion H31. assert (forall e' : EType, In e' lnew -> elabel g e' <= elabel g e). unfold lnew; intros. apply in_app_or in H30. destruct H30. apply H21. rewrite H26. apply in_or_app. left; auto. apply in_app_or in H30; destruct H30. apply (Z.le_trans _ (elabel g (u1,v1)) _). apply Hnew. auto. assert (In e ((u1, v1) :: ldiff)). right; auto. apply In_Znth_iff in H31. destruct H31 as [i' [? ?]]. rewrite <- H32. replace (u1,v1) with (Znth 0 ((u1,v1)::ldiff)). 2: apply Znth_0_cons. destruct (Z.lt_trichotomy 0 i'). apply Hsorted. lia. apply H31. destruct H33. subst i'. do 2 rewrite Znth_0_cons. lia. lia. apply H21. rewrite H26. apply in_or_app. right; right; auto. pose proof (upath_simplifiable_edges swap pnew lnew u v H29 H28). destruct H31 as [psim [lsim [? [? [? [? ?]]]]]]. exists psim; exists lsim. split. auto. split. apply H32. split. apply H34. intros. apply H30. apply H35. apply H36. ++ set (pnew:=(pb1 ++ (tail (rev p')) ++ (tail pb2))). set (lnew:=(lb1++(rev l')++lb2)). assert (Hpb1: last_error pb1 = hd_error (rev p')). { rewrite H23. symmetry. rewrite rev_hd_last, rev_involutive. apply Hnew. } assert (Hpb2: last_error (rev p') = hd_error pb2). { rewrite H27. rewrite <- rev_hd_last. apply Hnew. } assert (fits_upath swap lnew pnew). { unfold pnew, lnew. destruct Hnew as [? [? [? ?]]]. assert (connected_by_path swap (rev p') v2 u2). split. apply valid_upath_rev. apply H28. split. rewrite rev_hd_last, rev_involutive. apply H28. rewrite <- rev_hd_last; apply H28. assert (fits_upath swap (rev l') (rev p')). apply fits_upath_rev. auto. assert (In (u1,v1) (rev l')). apply in_rev. rewrite rev_involutive. auto. destruct (rev l'). contradiction. destruct (rev p'). simpl in H33; contradiction. destruct l1. simpl in H33; contradiction. replace (lb1 ++ (e0 :: l0) ++ lb2) with (lb1 ++ (e0::nil) ++ (l0++lb2)). 2: simpl; auto. apply (fits_upath_app _ _ _ _ _ e0 v2 v3). - apply (sound_fits_upath_transfer _ _ t2 swap); auto. simpl; intros; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p l). auto. rewrite H26. apply in_or_app. left; auto. unfold not; intros. subst e1. assert (~ In (u2,v2) ((u2, v2) :: nil ++ lb2)). apply (NoDup_app_not_in EType lb1 (((u2,v2)::nil)++lb2)). simpl. rewrite H26 in Hl. simpl in Hl. auto. auto. apply H36. left; auto. - destruct pb2. inversion H27. destruct pb2. destruct lb2. simpl. do 2 rewrite app_nil_r. simpl in H27; inversion H27. subst v4. apply H33. simpl in H25. contradiction. rename l1 into revp'. destruct lb2. simpl in H25. contradiction. apply (fits_upath_app _ _ _ _ _ e1 u2 v5). simpl. apply H33. apply (sound_fits_upath_transfer _ _ t2 swap); auto. simpl; intros; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p l). auto. rewrite H26. apply in_or_app. right. apply in_or_app. right. right; auto. unfold not; intros. subst e2. rewrite H26 in Hl; simpl in Hl. apply NoDup_app_r in Hl. apply NoDup_cons_2 in Hl. apply Hl. right; auto. apply H25. rewrite H27 in Hpb2. apply Hpb2. simpl; auto. assert (evalid swap e1). simpl. unfold addValidFunc, removeValidFunc. left. split. apply H25. unfold not; intros. subst e1. rewrite H26 in Hl. simpl in Hl. apply NoDup_app_r in Hl. apply NoDup_cons_2 in Hl. apply Hl. left; auto. destruct H25. simpl in H27. inversion H27. subst v4. destruct H25. split. apply evalid_strong_evalid; auto. rewrite (src_fst swap), (dst_snd swap); auto. simpl in H35. unfold addValidFunc, removeValidFunc in H35. destruct H35. destruct H35. rewrite (src_fst t2), (dst_snd t2) in H37; auto. exfalso. subst e1. destruct H25. contradiction. - auto. - simpl. auto. - destruct H33. rewrite H23 in Hpb1. simpl in Hpb1. inversion Hpb1. auto. } assert (connected_by_path swap pnew u v). split. apply valid_upath_exists_list_edges'. exists lnew; auto. unfold pnew; split. destruct H18. rewrite H22 in H29; destruct H29. destruct pb1. inversion H23. simpl in H29. simpl. auto. destruct pb2. inversion H27. destruct pb2. simpl in Hpb2. simpl in H27. inversion H27. subst v0. destruct H18. destruct H29. rewrite H22 in H30. rewrite last_err_appcons in H30. inversion H30. simpl. rewrite app_nil_r. unfold v; rewrite <- H32. subst u2. destruct Hnew as [? [? [? ?]]]. destruct (rev p') eqn:revp. inversion Hpb2. destruct l0. destruct l'. contradiction. assert (p' = v0::nil). symmetry. rewrite <- rev_involutive. rewrite revp. simpl; auto. rewrite H35 in H32. contradiction. simpl. rewrite last_err_split2. apply Hpb2. simpl. rewrite app_assoc. rewrite last_err_split2. destruct H18. destruct H29. rewrite H22 in H30. rewrite last_err_split2 in H30. apply H30. assert (forall e' : EType, In e' lnew -> elabel g e' <= elabel g e). unfold lnew; intros. apply in_app_or in H30. destruct H30. apply H21. rewrite H26. apply in_or_app. left; auto. apply in_app_or in H30; destruct H30. apply (Z.le_trans _ (elabel g (u1,v1)) _). apply Hnew. apply in_rev. auto. assert (In e ((u1, v1) :: ldiff)). right; auto. apply In_Znth_iff in H31. destruct H31 as [i' [? ?]]. rewrite <- H32. replace (u1,v1) with (Znth 0 ((u1,v1)::ldiff)). 2: apply Znth_0_cons. destruct (Z.lt_trichotomy 0 i'). apply Hsorted. lia. apply H31. destruct H33. subst i'. do 2 rewrite Znth_0_cons. lia. lia. apply H21. rewrite H26. apply in_or_app. right; right; auto. pose proof (upath_simplifiable_edges swap pnew lnew u v H29 H28). destruct H31 as [psim [lsim [? [? [? [? ?]]]]]]. exists psim; exists lsim. split. auto. split. apply H32. split. apply H34. intros. apply H30. apply H35. apply H36. + exists p. exists l. assert (fits_upath swap l p). apply (sound_fits_upath_transfer _ _ t2 swap); auto. simpl. intros; split; auto. intros. simpl. unfold addValidFunc, removeValidFunc. left. split. apply (fits_upath_evalid t2 p l); auto. unfold not; intros. subst e0. contradiction. split. split. apply valid_upath_exists_list_edges'. exists l; auto. apply H18. split. auto. split. auto. auto. } intros. specialize Hsorted with (i+1) (j+1). replace (Znth i ldiff) with (Znth (i+1) ((u1,v1)::ldiff)). replace (Znth j ldiff) with (Znth (j+1) ((u1,v1)::ldiff)). apply Hsorted. lia. rewrite Zlength_cons. lia. rewrite Znth_pos_cons. rewrite Z.add_simpl_r. auto. lia. rewrite Znth_pos_cons. rewrite Z.add_simpl_r. auto. lia. destruct H17 as [lmsf [? [? ?]]]. exists (b::lmsf). split. do 2 rewrite Zlength_cons. rewrite H17. auto. split. assert (Permutation ((u1,v1)::lmsf++lsame) (EList swap)). apply (Permutation_trans (l':=(lmsf ++ (u1, v1) :: lsame))). apply Permutation_middle. auto. pose proof (finite remove) as fremove. apply adde_EList_rev in H20. apply (@eremove_EList_rev size size_bound t2 (u2,v2) Hevalid_b) in H20. unfold b; simpl. apply (Permutation_trans H20). apply NoDup_Permutation. apply NoDup_EList. apply NoDup_EList. intros; rewrite EList_evalid; rewrite EList_evalid; split; auto. unfold not; intros. destruct H21. assert (~ In (u1,v1) (EList t2)). apply H3. left; auto. rewrite EList_evalid in H23. contradiction. intros. rewrite Zlength_cons in H20. destruct (Z.lt_trichotomy i 0). lia. destruct H21. subst i. do 2 rewrite Znth_0_cons. unfold b; auto. do 2 rewrite Znth_pos_cons by lia. apply H19. split. lia. destruct H20. apply (Z.sub_lt_mono_r i (Z.succ (Zlength lmsf)) 1) in H22. replace (Z.succ (Zlength lmsf) - 1) with (Zlength lmsf) in H22. auto. lia. Qed.
imports: VST.floyd.proofauto VST.floyd.library CertiGraph.floyd_ext.share CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.graph_relation CertiGraph.msl_application.ArrayGraph CertiGraph.unionfind.env_unionfind_arr CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.kruskal.spatial_wedgearray_graph CertiGraph.kruskal.kruskal_specs CertiGraph.graph.undirected_uf_lemmas