proposition: Lemma inv_unseen_newcost: forall (g: @DijkGG size inf) (dst src i u: V) dist prev popped newcost, (forall dst : Z, vvalid g dst -> inv_popped g src popped prev dist dst) -> (forall dst : Z, 0 <= dst < i -> inv_unseen g src popped prev dist dst) -> vvalid g i -> Zlength dist = size -> 0 <= dst < i + 1-> newcost < inf -> inv_unseen g src popped (upd_Znth i prev u) (upd_Znth i dist newcost) dst.
proof: Proof. intros ? ? ? ? ? ? ? ? ? H_inv_popped H_inv_unseen H_i_valid. intros. unfold inv_unseen; intros. destruct (H_inv_popped _ H4 H5) as [[? ?] | [optp2m [? [? ?]]]]. - destruct H6 as [? [? _]]. specialize (H9 p2m H10). contradiction. - destruct H6 as [? [? _]]. specialize (H10 p2m H6 H11). assert (0 <= dst < i). { assert (dst <> i). { intro. subst dst. rewrite (vvalid_meaning g i) in H_i_valid. rewrite upd_Znth_same in H3; ulia. } lia. } apply (vvalid_meaning g) in H_i_valid. rewrite upd_Znth_diff in H3; try ulia. red in H_inv_unseen. intro. apply (H_inv_unseen _ H12 H2 H3 m optp2m); trivial. destruct H8 as [? [? _]]. apply valid_path_split in H13. 2: { apply (path_ends_meet _ _ _ src m dst); trivial. red. simpl. rewrite (edge_dst_snd g); simpl; split; trivial. } destruct H13. apply valid_path_merge; trivial. apply (path_ends_meet _ _ _ src m dst); trivial. red. simpl. rewrite (edge_dst_snd g); simpl; split; trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure