proposition: Lemma inv_unpopped_newcost: forall (g: @DijkGG size inf) src dst (u i: V) dist prev popped newcost, (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) -> (forall dst : Z, i <= dst < size -> inv_unseen_weak g src popped prev dist dst u) -> newcost = Znth u dist + elabel g (u, i) -> vvalid g u -> vvalid g i -> u <> i -> In u popped -> inrange_dist dist -> Zlength prev = size -> Zlength dist = size -> 0 <= Znth u dist <= inf -> 0 <= elabel g (u, i) <= Int.max_signed / size -> 0 <= Znth i dist <= inf -> newcost < Znth i dist -> ~ In i popped -> Znth i dist = inf \/ Znth i dist < inf -> 0 <= dst < i + 1 -> inv_unpopped g src popped (upd_Znth i prev u) (upd_Znth i dist newcost) dst.
proof: Proof. intros ? ? ? ? ? ? ? ? ? H_inv_popped H_inv_unpopped H_inv_unpopped_weak H_inv_unseen_weak Heqnewcost. intros. destruct (Z.eq_dec dst i). 2: apply inv_unpopped_newcost_dst_neq_i; trivial. subst dst; clear H12. unfold inv_unpopped; intros. destruct (Z.eq_dec i src); [left | right; split]; trivial. destruct (H_inv_popped _ H H2). 1: ulia. assert (0 <= i < size) by now apply (vvalid_meaning g). assert (0 <= u < size) by now apply (vvalid_meaning g). rewrite upd_Znth_same by lia. split3; [| |split3; [| |split]]; trivial. 1: ulia. 1: rewrite upd_Znth_diff; ulia. 1: rewrite upd_Znth_same; [rewrite upd_Znth_diff|]; ulia. intros. rewrite upd_Znth_same; [|ulia]. assert (mom' <> i). { intro. subst mom'. apply H10; trivial. } rewrite upd_Znth_diff; trivial. 2: apply (vvalid_meaning g) in H17; ulia. 2: lia. destruct (Znth_dist_cases mom' dist); trivial. 1: apply (vvalid_meaning g) in H17; ulia. 1: { rewrite H20. pose proof (edge_cost_pos g (mom', i)). ulia. } destruct (H_inv_popped _ H17 H18) as [[? ?] | [p2mom' [? [? ?]]]]. 1: pose proof (edge_cost_pos g (mom', i)); ulia. assert (Hrem:= H21). destruct H21 as [? [? [? ?]]]. pose proof (path_ends_In_path_dst _ _ _ _ H24). destruct (zlt ((Znth mom' dist) + elabel g (mom', i)) inf). 2: { destruct (zlt (elabel g (mom', i)) inf); lia. } destruct (in_dec zeq u (epath_to_vpath g p2mom')). - apply in_path_eq_epath_to_vpath in i0. 2: trivial. destruct (Z.eq_dec mom' u). 1: { subst mom'. unfold path_globally_optimal in H13. ulia. } destruct H11. 1: { assert (i <= i < size) by lia. exfalso. apply (H_inv_unseen_weak _ H28 H10 H11 mom' p2mom' H17 H18 n0 Hrem H22). apply valid_path_merge; trivial. 2: { simpl. rewrite (edge_src_fst g); split; trivial. apply strong_evalid_dijk; ulia. } apply (path_ends_meet _ _ _ src mom' i); trivial. red. simpl. rewrite (edge_dst_snd g). simpl. split; trivial. } assert (Znth i dist <= Znth mom' dist + elabel g (mom', i)). { assert (i <= i < size) by lia. assert (0 <= mom' < size). { apply (vvalid_meaning g); ulia. } destruct (H_inv_unpopped_weak _ H28 H10 H11). 1: lia. destruct H30 as [_ [_ ?]]. apply H30; trivial. } ulia. - assert (mom' <> u). { intro. subst mom'. apply n0. apply in_path_eq_epath_to_vpath; trivial. } destruct H11. 1: { assert (i <= i < size) by lia. pose proof (H_inv_unseen_weak _ H29 H10 H11 mom' p2mom' H17 H18 H28 Hrem H22). exfalso. apply H30. apply valid_path_merge; trivial. 2: { simpl. rewrite (edge_src_fst g); split; trivial. apply strong_evalid_dijk; ulia. } apply (path_ends_meet _ _ _ src mom' i); trivial. red. simpl. rewrite (edge_dst_snd g). simpl. split; trivial. } assert (i <= i < size) by lia. destruct (H_inv_unpopped_weak i H29 H10 H11). 1: subst i; exfalso; lia. apply Z.lt_le_incl. apply Z.lt_le_trans with (m:=Znth i dist). 1: lia. destruct H30 as [_ [_ ?]]. apply H30; trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure