proposition: Lemma inv_unseen_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_unseen_weak g src (u :: popped) prev dist dst u.
proof: Proof. repeat intro. apply not_in_cons in H2; destruct H2. destruct (H dst H1) as [_ [_ ?]]. destruct H5; [ulia|]. apply (H11 H10 H3 m p2m); trivial. red in H8 |- *. intros. specialize (H8 _ H12). destruct H8; auto. subst step. exfalso. pose proof (in_path_split g p2m u H12). apply valid_path_split in H9. 2: { exists m. destruct H7 as [_ [[? ?] _]]. split; auto. } destruct H9. destruct H13 as [_ ?]. simpl in H13. specialize (H8 H9). destruct H8 as [p1 [p2 [? ?]]]. destruct (H _ H4) as [? _]. destruct (H15 H5). * destruct H16. specialize (H17 p2m). destruct H7 as [? ?]. tauto. * destruct H16 as [p2u' [? ?]]. pose proof (path_correct_unique_path _ _ _ _ _ _ _ H7 H16). subst p2u'. destruct H17. clear -H17 H12 H0. specialize (H17 _ H12). contradiction. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure