proposition: Lemma path_leaving_popped: forall (g: @DijkGG size inf) links s u popped, valid_path g (s, links) -> path_ends g (s, links) s u -> In s popped -> ~ In u popped -> exists (p1 : path) (mom child : V) (p2 : path), path_glue p1 (path_glue (mom, [(mom, child)]) p2) = (s, links) /\ valid_path g p1 /\ valid_path g p2 /\ path_ends g p1 s mom /\ path_ends g p2 child u /\ In mom popped /\ ~ In child popped /\ evalid g (mom, child) /\ path_in_popped g popped p1.
proof: Proof. intros. generalize dependent s. induction links. - intros. destruct H0. simpl in H0, H3. exfalso. apply H2. rewrite <- H3; trivial. - intros. assert (evalid g a). { apply (valid_path_evalid _ _ _ _ H). simpl; left; trivial. } assert (s = fst a). { simpl in H. destruct H as [? _]. rewrite (edge_src_fst g) in H; trivial. } remember (snd a) as t. assert (a = (s,t)). { rewrite (surjective_pairing a). subst; trivial. } destruct (in_dec zeq t popped). + assert (valid_path g (t, links)). { rewrite Heqt, <- (edge_dst_snd g); trivial. apply valid_path_cons with (v := s); trivial. } assert (path_ends g (t, links) t u). { split; trivial. destruct H0. rewrite Heqt, <- (edge_dst_snd g); trivial. rewrite <- H7. symmetry. apply pfoot_cons. } specialize (IHlinks _ H6 H7 i). destruct IHlinks as [p2m [m [c [p2u [? [? [? [? [? [? [? [? Ha]]]]]]]]]]]]. exists (path_glue (s, [(s,t)]) p2m), m, c, p2u. assert (evalid g (s,t)). { rewrite H5 in H3; trivial. } assert (paths_meet g (s, [(s, t)]) p2m). { apply (path_ends_meet _ _ _ s t m); trivial. split; simpl; trivial. rewrite (edge_dst_snd g); trivial. } assert (fst p2u = c). { destruct H12. rewrite (surjective_pairing p2u) in H12. simpl in H12. lia. } assert (fst p2m = t). { destruct H11. rewrite (surjective_pairing p2m) in H11. simpl in H11. lia. } split3; [| |split3; [| | split3; [| |split3]]]; trivial. * rewrite (path_glue_assoc g); trivial. -- fold E in *. rewrite H8. unfold path_glue; trivial. simpl. rewrite H5; trivial. -- apply (path_ends_meet _ _ _ t m u); trivial. split; trivial. unfold path_glue. simpl fst; simpl snd; simpl app. destruct H12. rewrite <- H20. rewrite (surjective_pairing p2u) at 2. assert (c = dst g (m, c)). { rewrite (edge_dst_snd g); trivial. } rewrite H18. rewrite H21 at 2. apply pfoot_cons. * apply valid_path_merge; trivial. simpl; unfold strong_evalid. rewrite (edge_dst_snd g), (edge_src_fst g); trivial; simpl; split3; trivial. split. -- apply (valid_path_valid _ _ _ H). rewrite in_path_or_cons; trivial. left; trivial. rewrite (edge_src_fst g); trivial. -- apply (valid_path_valid _ _ _ H6). unfold In_path. left; trivial. * split; trivial. unfold path_glue. simpl fst; simpl snd; simpl app. destruct H11. rewrite <- H20. rewrite (surjective_pairing p2m) at 2. rewrite H19. assert (t = dst g (s, t)). { rewrite (edge_dst_snd g); trivial. } rewrite H21 at 2. apply pfoot_cons. * red. intros. unfold path_glue in H20. simpl in H20. rewrite in_path_or_cons in H20. 2: rewrite (edge_src_fst g); trivial. red in Ha. destruct H20. 1: subst step; trivial. apply Ha. rewrite (edge_dst_snd g) in H20. simpl in H20. rewrite <- H19, <- surjective_pairing in H20. trivial. + clear IHlinks. exists (s, []), s, t, (t, links). assert (evalid g (s,t)). { rewrite H5 in H3; trivial. } split3; [| |split3; [| | split3; [| |split3]]]; trivial. * rewrite path_glue_nil_l. simpl. rewrite H5; trivial. * simpl. apply (valid_path_valid _ _ _ H). unfold In_path. left; trivial. * rewrite Heqt. rewrite <- (edge_dst_snd g); trivial. apply valid_path_cons with (v := s); trivial. * split; trivial. * destruct H0. split; trivial. rewrite <- H7. symmetry. rewrite Heqt, <- (edge_dst_snd g); trivial. apply pfoot_cons. * red. intros. red in H7. destruct H7. 1: simpl in H7; subst step; trivial. destruct H7 as [? [? ?]]. inversion H7. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure