proposition: Lemma inv_unpopped_newcost_dst_neq_i: forall (g: @DijkGG size inf) src (dst u i: V) newcost prev dist popped, (forall dst : Z, 0 <= dst < i -> inv_unpopped g src popped prev dist dst) -> vvalid g i -> Zlength prev = size -> Zlength dist = size -> ~ In i popped -> 0 <= dst < i + 1 -> dst <> i -> inv_unpopped g src popped (upd_Znth i prev u) (upd_Znth i dist newcost) dst.
proof: Proof. intros. assert (0 <= dst < i) by lia. assert (0 <= i < size) by now apply (vvalid_meaning g). unfold inv_unpopped. intros. rewrite upd_Znth_diff in H9 by ulia. rewrite upd_Znth_diff by ulia. destruct (H _ H6 H8) as [? | [? [? [? [? [? [? ?]]]]]]]; trivial; [left | right]; trivial. remember (Znth dst prev) as mom. split; trivial. assert (Znth mom dist < inf). { pose proof (edge_cost_pos g (mom, dst)). ulia. } assert (vvalid g dst). { apply (vvalid_meaning g); ulia. } assert (mom <> i). { intro. subst i. apply H3; trivial. } assert (0 <= mom < Zlength dist). { apply (vvalid_meaning g) in H11; ulia. } split3; [| |split3; [| |split]]; trivial. - rewrite upd_Znth_diff; lia. - repeat rewrite upd_Znth_diff; trivial; ulia. - intros. assert (mom' <> i). { intro contra. subst mom'. apply H3; trivial. } repeat rewrite upd_Znth_diff; trivial. apply H16; trivial. 1: apply (vvalid_meaning g) in H21; ulia. all: lia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure