proposition: Lemma inv_unpopped_weak_add_unpopped: forall (g: @DijkGG size inf) prev dist popped src u dst, dijkstra_correct g src popped prev dist -> ~ In u popped -> vvalid g dst -> inv_unpopped_weak g src (u :: popped) prev dist dst u.
proof: Proof. intros. unfold inv_unpopped_weak. intros. apply not_in_cons in H2; destruct H2 as [_ ?]. destruct (H dst H1) as [_ [? _]]. specialize (H4 H2 H3) as [? | [? [? [? [? [? [? ?]]]]]]]; [left | right]; trivial. remember (Znth dst prev) as mom. assert (evalid g (mom, dst)). { rewrite (evalid_meaning g). split. apply (edge_representable). intro. replace (elabel g (mom, dst)) with inf in H7. apply Zlt_not_le in H7; apply H7; reflexivity. } assert (Znth mom dist < inf) by (pose proof (valid_edge_bounds g _ H11); ulia). destruct (popped_noninf_has_path _ _ _ _ _ _ H H6 H12) as [p2mom [? [? ?]]]; trivial. assert (mom <> u). { intro contra. rewrite contra in *. apply H0; trivial. } split3; [|split3; [| |split3; [| |split]]|]; trivial. 1: simpl; right; trivial. intros. apply H10; trivial. simpl in H19; destruct H19; ulia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure