proposition: Lemma path_leaving_popped_stronger: 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 -> path_cost g (s, links) < inf -> 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 /\ strong_evalid g (mom, child) /\ path_cost g p1 < inf /\ 0 <= elabel g (mom, child) < inf /\ path_cost g p2 + elabel g (mom, child) < inf /\ path_in_popped g popped p1.
proof: Proof. intros. destruct (path_leaving_popped g links s u popped H H0 H1 H2) as [p1 [mom' [child' [p2 [? [? [? [? [? [? [? [? Ha]]]]]]]]]]]]. exists p1, mom', child', p2. assert (valid_path g (path_glue (mom', [(mom', child')]) p2)). { apply valid_path_merge; trivial. apply (path_ends_meet _ _ _ mom' child' u); trivial. apply (path_ends_one_step g). simpl. rewrite (edge_src_fst g); split; trivial. split3; trivial. rewrite (edge_src_fst g); simpl; trivial. apply (path_ends_valid_dst _ s _ p1); trivial. rewrite (edge_dst_snd g); simpl; trivial. apply (path_ends_valid_src _ _ u p2); trivial. } assert (elabel g (mom', child') < inf). { apply (inf_gt_largest_edge g). trivial. } split3; [| |split3; [| |split3; [| |split3; [| |split3; [| |split]]]]]; trivial. - apply strong_evalid_dijk; trivial. + apply (path_ends_valid_dst _ s _ p1); trivial. + apply (path_ends_valid_src _ _ u p2); trivial. + intro. rewrite H14 in H13. apply Zlt_not_le in H13. apply H13; reflexivity. - rewrite <- H4 in H3. apply path_cost_path_glue_lt in H3; trivial. destruct H3; trivial. - split; trivial. apply edge_cost_pos. - rewrite <- H4 in H3. apply path_cost_path_glue_lt in H3; trivial. destruct H3 as [_ ?]. rewrite (path_cost_path_glue g) in H3; trivial. rewrite (one_step_path_Znth g) in H3. rewrite Z.add_comm. ulia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure