proposition: Lemma dijkstra_correct_nothing_popped: forall (g: @DijkGG size inf) src, 0 <= src < size -> dijkstra_correct g src [] (upd_Znth src (repeat inf (Z.to_nat size)) src) (upd_Znth src (repeat inf (Z.to_nat size)) 0).
proof: Proof. intros. unfold dijkstra_correct, inv_popped, inv_unpopped, inv_unseen; split3; intros; [inversion H1 | left | inversion H4]. destruct (Z.eq_dec dst src); [trivial | exfalso]. apply (vvalid_meaning g) in H0. rewrite upd_Znth_diff in H2; trivial. rewrite Znth_repeat_inrange in H2; ulia. all: rewrite Zlength_repeat; lia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure