proposition: Lemma path_cost_path_glue: forall (g: LabeledGraph V E DV Z DG) p1 p2, path_cost g (path_glue p1 p2) = path_cost g p1 + path_cost g p2.
proof: Proof. intros. unfold path_cost at 1, path_glue at 1. simpl. rewrite map_app. rewrite fold_left_app. assert ((fold_left Z.add (map (elabel g) (snd p1)) 0) = (path_cost g p1)) by now unfold path_cost. rewrite H. unfold path_cost at 3. remember (map (elabel g) (snd p2)) as l2. remember (path_cost g p1) as c1. replace c1 with (c1 + 0) at 1 by lia. rewrite path_cost_init; trivial. Qed.
imports: VST.floyd.proofauto Coq.Classes.EquivDec CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas