proposition: Lemma inv_popped_add_src: forall (g: @DijkGG size inf) src popped prev dist, dijkstra_correct g src popped prev dist -> vvalid g src -> Znth src dist = 0 -> inv_popped g src (src :: popped) prev dist src.
proof: Proof. intros. right. exists (src, []); split3; trivial. - split3; [| | split3; [| |split]]; trivial. + split; trivial. + unfold path_cost. simpl fold_left. pose proof (size_representable g). apply Z.mul_nonneg_nonneg; [|apply Z.div_pos]; try ulia. + apply acyclic_nil_path. - unfold path_in_popped. intros. destruct H3 as [? | [? [? _]]]. + simpl in H3. simpl. left; lia. + simpl in H3; lia. - unfold path_globally_optimal; intros. unfold path_cost at 1; simpl. apply path_cost_pos; trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure