proposition: Lemma inv_popped_newcost: forall (g: @DijkGG size inf) src dst u i newcost popped prev dist, vvalid g i -> vvalid g dst -> (forall dst : Z, vvalid g dst -> inv_popped g src popped prev dist dst) -> Zlength prev = size -> Zlength dist = size -> ~ In i popped -> inv_popped g src popped (upd_Znth i prev u) (upd_Znth i dist newcost) dst.
proof: Proof. intros. unfold inv_popped; intros. assert (n: dst <> i). { intro. subst dst. apply H4; trivial. } assert (0 <= dst < size). { apply (vvalid_meaning g) in H0; ulia. } assert (0 <= i < size). { apply (vvalid_meaning g) in H; ulia. } repeat rewrite upd_Znth_diff; try ulia. destruct (H1 dst H0 H5) as [? | [p2dst [? [? ?]]]]; [left | right]; trivial. exists p2dst. split3; trivial. - destruct H8 as [? [? [? [? [? Ha]]]]]. split3; [| | split3; [| |split]]; trivial. 1: rewrite upd_Znth_diff; ulia. rewrite Forall_forall; intros. pose proof (In_links_snd_In_path g _ _ H15). specialize (H9 _ H16). rewrite Forall_forall in H14. specialize (H14 _ H15). assert (snd x <> i). { intro contra. rewrite contra in *. apply H4; ulia. } rewrite upd_Znth_diff; try lia. rewrite H2, <- (vvalid_meaning g); trivial. apply (valid_path_valid _ p2dst); trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure