proposition: Lemma not_in_popped: forall (g: @DijkGG size inf) src u i cost prev dist popped, vvalid g u -> vvalid g i -> (forall dst : Z, vvalid g dst -> inv_popped g src popped prev dist dst) -> In u popped -> cost = elabel g (u, i) -> 0 <= Znth i dist <= inf -> 0 <= Znth u dist + cost <= Int.max_signed -> Znth u dist + cost < Znth i dist -> 0 <= Znth u dist < inf -> ~ In i popped.
proof: Proof. intros ? ? ? ? ? ? ? ? H_u_valid H_i_valid H_inv_popped ? ? ? ? H_improvement ?. intro. destruct (H_inv_popped _ H_i_valid H4) as [[? ?]|?]. 1: { destruct (H_inv_popped _ H_u_valid H) as [[? _] | [p2u [? [? ?]]]]. 1: lia. assert (path_ends g (path_glue p2u (u, [(u,i)])) src i). { destruct H7 as [_ [? _]]. apply (path_ends_app_cons g _ _ _ src); trivial. 2: rewrite <- surjective_pairing; split. all: destruct H7; trivial. } assert (valid_path g (path_glue p2u (u, [(u,i)]))). { destruct H7 as [? [? _]]. apply valid_path_merge; trivial. - apply (path_ends_meet _ _ _ src u i); trivial. split; trivial. simpl. rewrite (edge_dst_snd g). trivial. - simpl. split. + rewrite (edge_src_fst g); trivial. + apply strong_evalid_dijk; ulia. } specialize (H6 _ H10). contradiction. } apply Zlt_not_le in H_improvement; apply H_improvement. destruct (H_inv_popped _ H_u_valid H) as [? | [p2u [? _]]]. 1: ulia. destruct H5 as [p2i [[_ [_ [_ [? _]]]] [_ ?]]]. destruct H6 as [? [? [_ [? _]]]]. rewrite H9, H5. specialize (H7 (fst p2u, snd p2u +:: (u,i))). rewrite (path_cost_app_cons g) in H7; trivial. rewrite H0. apply H7. - apply (valid_path_app_cons g). + rewrite <- surjective_pairing; trivial. + rewrite (surjective_pairing p2u) in H8. destruct H8; simpl in H8; ulia. + apply strong_evalid_dijk; ulia. - apply (path_ends_app_cons g) with (a' := src); trivial. 2: rewrite <- surjective_pairing; split. all: rewrite (surjective_pairing p2u) in *; destruct H8; simpl in H8; trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure