proposition: Lemma inv_unpopped_weak_newcost: forall (g: @DijkGG size inf) src dst u i prev dist popped newcost, (forall dst : Z, i <= dst < size -> inv_unpopped_weak g src popped prev dist dst u) -> vvalid g i -> Zlength prev = size -> Zlength dist = size -> ~ In i popped -> i + 1 <= dst < size -> inv_unpopped_weak g src popped (upd_Znth i prev u) (upd_Znth i dist newcost) dst u.
proof: Proof. intros ? ? ? ? ? ? ? ? ? H_inv_unpopped_weak. intros. assert (0 <= i < size) by now apply (vvalid_meaning g). unfold inv_unpopped_weak. intros. assert (i <= dst < size) by lia. destruct (Z.eq_dec dst i). 1: subst dst; lia. rewrite upd_Znth_diff in H6 by lia. destruct (H_inv_unpopped_weak _ H7 H5 H6) as [? | [? [[? [? [? [? [? ?]]]]] ?]]]; [left | right]; trivial. rewrite upd_Znth_diff by ulia. remember (Znth dst prev) as mom. assert (mom <> i). { intro. subst i. apply H2; trivial. } assert (0 <= mom < size) by now apply (vvalid_meaning g). split3; [| split3; [| | split3; [| |split]]|]; trivial. 1,2: repeat rewrite upd_Znth_diff; ulia. intros. assert (mom' <> i). { intro contra. subst mom'. apply H2; trivial. } repeat rewrite upd_Znth_diff; trivial. apply H15; ulia. apply (vvalid_meaning g) in H19; ulia. all: ulia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure