proposition: Lemma inv_unpopped_new_dst: forall (g: @DijkGG size inf) (src dst u i: V) dist prev popped, vvalid g i -> (forall dst : Z, vvalid g dst -> inv_popped g src popped prev dist dst) -> (forall dst : Z, 0 <= dst < i -> inv_unpopped g src popped prev dist dst) -> (forall dst : Z, i <= dst < size -> inv_unpopped_weak g src popped prev dist dst u) -> inrange_dist dist -> Zlength dist = size -> Znth u dist + elabel g (u, i) >= Znth i dist -> 0 <= dst < i + 1 -> inv_unpopped g src popped prev dist dst.
proof: Proof. intros ? ? ? ? ? ? ? ? ? H_inv_popped H_inv_unpopped H_inv_unpopped_weak. intros. destruct (Z.eq_dec dst i). 2: apply H_inv_unpopped; lia. subst dst. unfold inv_unpopped; intros. apply (vvalid_meaning g) in H. assert (i <= i < size) by lia. destruct (H_inv_unpopped_weak i H6 H4 H5) as [? | [? [[? [? [? [? [? ?]]]]] ?]]]; [left | right]; trivial. remember (Znth i prev) as mom. split3; [| |split3; [| |split3]]; trivial. intros. pose proof (Znth_dist_cases mom' dist). rename H17 into e. destruct e as [e | e]; trivial. 1: apply (vvalid_meaning g) in H15; ulia. 1: { rewrite e. pose proof (edge_cost_pos g (mom', i)). ulia. } destruct (H_inv_popped _ H15 H16) as [[? ?] | ?]. 1: pose proof (edge_cost_pos g (mom', i)); ulia. destruct H17 as [p2mom' [? [? ?]]]. assert (Hrem := H17). destruct (in_dec zeq u (epath_to_vpath g p2mom')). - destruct H17 as [? [? [? [? ?]]]]. apply in_path_eq_epath_to_vpath in i0; trivial. destruct (Z.eq_dec mom' u). + subst mom'. specialize (H18 _ i0). rename p2mom' into p2u. unfold path_globally_optimal in H19. apply Z.ge_le in H2. destruct (zlt (Znth u dist + elabel g (u, i)) inf); ulia. + destruct Hrem as [? [? [? [? ?]]]]. assert (In_path g mom' p2mom'). { destruct H25. apply pfoot_in in H29. trivial. } destruct (zlt (Znth mom' dist + elabel g (mom', i)) inf). 2: { destruct (zlt (elabel g (mom', i)) inf); lia. } assert (0 <= mom' < size). { apply (vvalid_meaning g) in H15; ulia. } destruct (H_inv_unpopped_weak _ H6 H4 H5) as [? | [? [[? [? [? [? [? ?]]]]]]]]. 1: lia. apply H38; trivial. - apply H14; trivial. intro. apply n. destruct H17 as [? [? [? [? ?]]]]. rewrite in_path_eq_epath_to_vpath; trivial. destruct H21. apply pfoot_in in H25. rewrite H20 in *. trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure