proposition: Lemma inv_popped_add_u: forall (g: @DijkGG size inf) src dst u popped prev (dist: list Z), dijkstra_correct g src popped prev dist -> Znth src dist = 0 -> inrange_dist dist -> Zlength dist = size -> ~ In u popped -> vvalid g u -> Znth u dist < inf -> vvalid g dst -> In src popped -> (forall i, vvalid g i -> ~ In i popped -> Znth u dist <= Znth i dist) -> inv_popped g src (u :: popped) prev dist dst.
proof: Proof. intros. rename H8 into H_u_best. destruct (Z.eq_dec dst u). 2: { intro. simpl in H8; destruct H8; [lia|]. destruct (H _ H6) as [? _]. specialize (H9 H8); destruct H9 as [[? ?]|[? [? [? ?]]]]; [left | right]. - split; trivial. - exists x; split3; trivial. unfold path_in_popped. intros. specialize (H10 _ H12). simpl; right; trivial. } subst dst. clear H6. destruct (H _ H4) as [_ [? _]]. specialize (H6 H3 H5). destruct H6 as [? | [_ [? [? [? [? [? ?]]]]]]]. 1: subst src; apply inv_popped_add_src; trivial. remember (Znth u prev) as mom. destruct (popped_noninf_has_path _ _ _ _ _ _ H H8) as [p2mom [? [? ?]]]; trivial. 1: pose proof (edge_cost_pos g (mom, u)); ulia. right. clear H16. exists (fst p2mom, snd p2mom +:: (mom, u)). assert (Hg: evalid g (mom, u)). { rewrite (evalid_meaning g); split. apply edge_representable. trivial. intro. replace (elabel g (mom, u)) with inf in H9. apply Zlt_not_le in H9; apply H9; reflexivity. } assert (strong_evalid g (mom, u)). { split3; trivial. rewrite (edge_src_fst g); simpl; trivial. rewrite (edge_dst_snd g); simpl; trivial. } split3. - apply (path_correct_path_glue_one); trivial. + replace (Znth mom dist + elabel g (mom, u)) with (Znth u dist). apply (sublist.Forall_Znth _ _ u) in H1. destruct H1; try ulia. apply (vvalid_meaning g) in H4; lia. + lia. + intro. apply H3, H14; trivial. - unfold path_in_popped. intros. destruct H13 as [? [? _]]. apply (in_path_app_cons g _ _ src) in H17; trivial. destruct H17. + specialize (H14 _ H17). simpl. right; trivial. + subst step. simpl; left; trivial. - unfold path_globally_optimal in H15. destruct H13 as [? [? [? [? ?]]]]. unfold path_globally_optimal; intros. rewrite (path_cost_app_cons g); trivial. destruct (Z_le_gt_dec (path_cost g p2mom + elabel g (mom, u)) (path_cost g p')); auto. apply Z.gt_lt in g0. destruct (zlt (path_cost g p') inf); [|ulia]. exfalso. apply Zlt_not_le in g0. apply g0. rewrite (surjective_pairing p') in *. remember (snd p') as links. replace (fst p') with src in *. 2: destruct H22; simpl in H22; lia. assert (Htemp: In src popped). { destruct H22. apply H14; trivial. left. rewrite (surjective_pairing p2mom) in *. simpl. destruct H17. simpl in H17. lia. } destruct (path_leaving_popped_stronger g links src u popped) as [p1 [mom' [child' [p2 [? [? [? [? [? [? [? [? [? [? [? Ha]]]]]]]]]]]]]]]; trivial. clear Htemp. replace (path_cost g (src, links)) with (path_cost g p1 + elabel g (mom', child') + path_cost g p2). 2: { rewrite <- H23. do 2 rewrite (path_cost_path_glue g). rewrite (one_step_path_Znth g). symmetry. apply Z.add_assoc. } assert (vvalid g mom'). { destruct H30 as [_ [? _]]. rewrite (edge_src_fst g) in H30. simpl in H30; trivial. } assert (vvalid g child'). { destruct H30 as [_ [_ ?]]. rewrite (edge_dst_snd g) in H30; simpl in H30; trivial. } destruct (H mom' H34) as [? _]. destruct (H36 H28) as [[? ?] | [optp2mom' [? [? ?]]]]. 1: specialize (H38 p1 H26); contradiction. pose proof (H39 p1 H24 H26). apply Z.le_trans with (m := path_cost g optp2mom' + elabel g (mom', child')). 2: pose proof (path_cost_pos _ _ H25); lia. assert (Znth mom' dist + elabel g (mom', child') < inf). { destruct H37 as [_ [_ [_ [? _]]]]. rewrite H37. apply Z.le_lt_trans with (m := path_cost g p1 + elabel g (mom', child')); [lia|]. rewrite <- H23 in l. replace (path_glue p1 (path_glue (mom', [(mom', child')]) p2)) with (path_glue (path_glue p1 (mom', [(mom', child')])) p2) in l. 2: { apply (path_glue_assoc g). apply (path_ends_meet _ _ _ src mom' child'); trivial. apply (path_ends_one_step g). apply (path_ends_meet _ _ _ mom' child' u); trivial. apply (path_ends_one_step g). } apply path_cost_path_glue_lt in l; trivial. 2: { apply valid_path_merge; trivial. apply (path_ends_meet _ _ _ src mom' child'); trivial. apply (path_ends_one_step g). simpl; split; trivial. rewrite (edge_src_fst g); trivial. } destruct l as [l _]. rewrite (path_cost_path_glue g) in l; trivial. } assert (0 <= Znth mom' dist). { rewrite (vvalid_meaning g) in H34. apply (sublist.Forall_Znth _ _ mom') in H1. destruct H1; ulia. ulia. } assert (Htemp: 0 <= child' < Zlength dist). { apply (vvalid_meaning g) in H35; trivial. ulia. } destruct (Znth_dist_cases child' dist) as [? | [_ ?]]; trivial; clear Htemp. + exfalso. destruct (H _ H35) as [_ [_ ?]]. specialize (H44 H29 H43 mom' optp2mom' H34 H28 H37 H38). exfalso. apply H44. destruct H37 as [? [? _]]. apply valid_path_merge; trivial. * apply (path_ends_meet _ _ _ src mom' child'); trivial. red. simpl. rewrite (edge_dst_snd g). simpl. split; trivial. * simpl. rewrite (edge_src_fst g). split; trivial. + destruct (H _ H35) as [_ [? _]]. red in H44. assert (Znth child' dist < inf). { pose proof (inf_bounded_above_dist g). lia. } specialize (H44 H29 H45). destruct H44 as [? | [_ [? [? [? [? [? ?]]]]]]]. * exfalso. subst child'. apply H29, H38. destruct H37 as [_ [[? _] _]]. left. rewrite (surjective_pairing optp2mom') in *; simpl. simpl in H37; lia. * specialize (H50 mom' H34 H28). apply Z.le_trans with (m := Znth child' dist); trivial. 2: destruct H37 as [_ [_ [_ [? _]]]]; ulia. rewrite <- H19, <- H11. apply H_u_best; trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure