proposition: Lemma path_correct_path_glue_one: forall (g: @DijkGG size inf) src u mom p2mom prev dist, path_correct g prev dist src mom p2mom -> Znth u dist = Znth mom dist + elabel g (mom, u) -> Znth mom dist + elabel g (mom, u) <= (size-1) * (Int.max_signed / size) -> strong_evalid g (mom, u) -> Znth u prev = mom -> ~ In_path g u p2mom -> path_correct g prev dist src u (path_glue p2mom (mom, [(mom, u)])).
proof: Proof. intros. rename H4 into Hb. destruct H as [? [? [? [? [? Ha]]]]]. assert (path_cost g p2mom + elabel g (mom, u) <= (size-1) * (Int.max_signed / size)) by ulia. split3; [| | split3; [| |split]]; trivial. - destruct H4; apply (valid_path_app_cons g); trivial; try rewrite <- surjective_pairing; trivial. - destruct H4; apply (path_ends_app_cons g); trivial. split; trivial. rewrite <- (surjective_pairing p2mom); trivial. - rewrite (path_cost_glue_one_step g); ulia. - rewrite (path_cost_glue_one_step g). rewrite <- H6. ulia. - rewrite Forall_forall. intros. rewrite Forall_forall in H7. apply in_app_or in H9. destruct H9. + apply H7; trivial. + simpl in H9. destruct H9; [| lia]. rewrite (surjective_pairing x) in *. inversion H9. simpl. rewrite <- H11, <- H12. ulia. - red in Ha |- *. pose proof (epath_to_vpath_path_glue_one_step g src mom u p2mom H H4). symmetry in H9. apply (Permutation_NoDup H9). apply NoDup_cons; trivial. intro. apply in_path_eq_epath_to_vpath in H10; trivial. contradiction. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure