proposition: Lemma path_in_popped_Zlengths: forall (g: @DijkGG size inf) links s popped, valid_path g (s, links) -> acyclic_path g (s, links) -> path_in_popped g popped (s, links) -> Zlength links <= Zlength popped - 1.
proof: Proof. intros g. induction links; intros; destruct popped. + exfalso. apply (H1 s). left; trivial. + rewrite Zlength_nil. rewrite Zlength_cons_sub_1. apply Zlength_nonneg. + exfalso. apply (H1 s). left; trivial. + rewrite Zlength_cons_sub_1, Zlength_cons. replace s with (src g a) in * by (destruct H; lia). clear s. assert (In (src g a) (v :: popped)). { apply H1. left. trivial. } apply In_split in H2. destruct H2 as [l1 [l2 ?]]. specialize (IHlinks (dst g a) (l1 ++ l2)). spec IHlinks. 1: apply @valid_path_cons with (v := (src g a)); trivial. spec IHlinks. 1: apply (acyclic_path_cons _ _ _ _ H); trivial. spec IHlinks. 2: { assert (Zlength (v :: popped) = Zlength (l1 ++ src g a :: l2)) by congruence. repeat rewrite Zlength_app in *. repeat rewrite Zlength_cons in *. lia. } clear IHlinks. red in H0. rewrite H2 in *. clear H2 popped v. rewrite epath_to_vpath_cons_eq in H0; trivial. rewrite NoDup_cons_iff in H0. destruct H0. do 2 intro. specialize (H1 step). spec H1. 1: { destruct H3 as [? | [e' [? ?]]]. - simpl in H3. right. exists a. split; auto. left. trivial. - right. exists e'. simpl in *; auto. } apply in_app_or in H1. apply in_or_app. destruct H1; auto. destruct H1; auto. exfalso. apply H0. subst step. apply in_path_eq_epath_to_vpath; auto. apply valid_path_tail in H. apply H. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure