Library MetaRocq.Utils.wGraph

From Stdlib Require Import ZArith Zcompare Lia ssrbool.
From Stdlib Require Import MSetAVL MSetFacts MSetProperties.
From MetaRocq.Utils Require Import MRUtils.
From Stdlib Require Import ssreflect.
From Equations Require Import Equations.

Local Open Scope Z_scope.

Ltac Tauto.intuition_solver ::= auto with core arith zarith bool datatypes crelations relations.

Lemma fold_max_In n m l (H : fold_left Z.max l n = m)
  : n = m ∨ In m l.
Proof.
  revert n H; induction l; cbn; intros n H.
  intuition.
  apply IHl in H.
  apply or_assoc. destruct H; [left|now right]. lia.
Qed.

Lemma fold_max_le n m l (H : n ≤ m ∨ Exists (Z.le n) l)
  : n ≤ fold_left Z.max l m.
Proof.
  revert m H; induction l; cbn in *; intros m [H|H].
  assumption. inversion H.
  eapply IHl. left; lia.
  eapply IHl. inversion_clear H.
  left; lia. right; assumption.
Qed.

Lemma fold_max_le' n m l (H : In n (m :: l))
  : n ≤ fold_left Z.max l m.
Proof.
  apply fold_max_le. destruct H.
  left; lia. right. apply Exists_exists.
  eexists. split. eassumption. reflexivity.
Qed.

Definition eq_max n m k : max n m = k → n = k ∨ m = k.
  intro; lia.
Qed.

Module Nbar.
  (* None is -∞ *)
  Definition t := option Z.
  Definition max (n m : t) : t :=
    match n, m with
    | Some n, Some m ⇒ Some (Z.max n m)
    | Some n, None ⇒ Some n
    | None, Some m ⇒ Some m
    | _, _ ⇒ None
    end.
  Definition add (n m : t) : t :=
    match n, m with
    | Some n, Some m ⇒ Some (n + m)
    | _, _ ⇒ None
    end.

  Definition sub (n m : t) : t :=
    match n, m with
    | Some n, Some m ⇒ Some (n - m)
    | _, _ ⇒ None
    end.

  Definition S : t → t := option_map Z.succ.

  Definition le (n m : t) : Prop :=
    match n, m with
    | Some n, Some m ⇒ n ≤ m
    | Some _, None ⇒ False
    | None, _ ⇒ True
    end.

  Definition lt (n m : t) : Prop :=
    match n, m with
    | Some n, Some m ⇒ n < m
    | None, Some _ ⇒ True
    | _, None ⇒ False
    end.

  Arguments max _ _ : simpl nomatch.
  Arguments sub _ _ : simpl nomatch.
  Arguments add _ _ : simpl nomatch.
  Arguments le _ _ : simpl nomatch.
  Arguments lt _ _ : simpl nomatch.

  Declare Scope nbar_scope.
  Infix "+" := add : nbar_scope.
  Infix "-" := sub : nbar_scope.
  Infix "≤" := le : nbar_scope.
  Infix "<" := lt : nbar_scope.
  Delimit Scope nbar_scope with nbar.
  Bind Scope nbar_scope with t.

  Local Open Scope nbar_scope.

  #[global] Instance le_refl : Reflexive le.
  Proof.
    intro x; destruct x; cbn; reflexivity.
  Defined.

  #[global] Instance le_trans : Transitive le.
  Proof.
    intros [x|] [y|] [z|]; cbn; intuition.
  Defined.

  (* Definition is_finite (n : t) := is_Some n. *)
  (* Definition is_finite_max (n m : t) *)
  (*   : is_finite (max n m) <-> is_finite n \/ is_finite m. *)
  (* Proof. *)
  (*   split. *)
  (*   - destruct n, m; cbn; intros k e; try discriminate. *)
  (*     apply some_inj, eq_max in e. *)
  (*     destruct e; left|right; eexists; f_equal; eassumption. *)
  (*     left; eexists; reflexivity. *)
  (*     right; eexists; reflexivity. *)
  (*   - intros H|H. *)
  (*     destruct H as n' e; rewrite e; cbn. *)
  (*     destruct m; eexists; reflexivity. *)
  (*     destruct H as m' e; rewrite e; cbn. *)
  (*     destruct n; eexists; reflexivity. *)
  (* Defined. *)
  (* Definition is_finite_add (n m : t) *)
  (*   : is_finite (n + m) <-> is_finite n /\ is_finite m. *)
  (* Proof. *)
  (*   split. *)
  (*   - destruct n, m; cbn; intros k e; try discriminate. *)
  (*     split; eexists; reflexivity. *)
  (*   - intros [n1 e1] [n2 e2]; rewrite e1, e2. *)
  (*     eexists; reflexivity. *)
  (* Defined. *)

  (* Definition is_pos (n : t) := Some 1 <= n. *)
  (* Definition is_pos_max (n m : t) *)
  (*   : is_pos (max n m) -> is_pos n \/ is_pos m. *)
  (* Proof. *)
  (*   destruct n, m; cbn; intuition. lia. *)
  (* Defined. *)
  (* Definition is_pos_add (n m : t) *)
  (*   : is_pos (n + m) -> is_pos n \/ is_pos m. *)
  (* Proof. *)
  (*   destruct n, m; cbn; intuition. lia. *)
  (* Defined. *)

  (* Definition is_pos_is_finite n : is_pos n -> is_finite n. *)
  (* Proof. *)
  (*   destruct n; cbn; |intuition. *)
  (*   destruct n. lia. intros _. eexists; reflexivity. *)
  (* Qed. *)
  Lemma add_finite z1 z2 : Some (z1 + z2)%Z = Some z1 + Some z2.
  Proof. reflexivity. Qed.

  Definition add_assoc n m p : n + (m + p) = n + m + p.
  Proof.
    destruct n, m, p; try reflexivity; cbn.
    now rewrite Z.add_assoc.
  Defined.

  Definition add_0_r n : (n + Some 0 = n)%nbar.
  Proof.
    destruct n; try reflexivity; cbn.
    now rewrite Z.add_0_r.
  Defined.

  Lemma add_0_l n : (Some 0 + n = n)%nbar.
  Proof. by case: n. Qed.

  Lemma sub_diag n : n - n = match n with None ⇒ None | Some _ ⇒ Some 0 end.
  Proof. destruct n; simpl. now rewrite Z.sub_diag. auto. Defined.

  Lemma max_None n : max n None = n.
  Proof. destruct n; simpl; auto. Qed.

  Definition max_lub n m p : n ≤ p → m ≤ p → max n m ≤ p.
  Proof.
    destruct n, m, p; cbn; intuition lia.
  Defined.

  Definition add_max_distr_r n m p : max (n + p) (m + p) = max n m + p.
  Proof.
    destruct n, m, p; try reflexivity; cbn.
    now rewrite Z.add_max_distr_r.
  Defined.

  Definition max_le' n m p : p ≤ n ∨ p ≤ m → p ≤ max n m.
  Proof.
    destruct n, m, p; cbn; intuition; lia.
  Defined.

  Definition plus_le_compat_l n m p : n ≤ m → p + n ≤ p + m.
  Proof.
    destruct n, m, p; cbn; intuition.
  Defined.

  Definition plus_le_compat n m p q : n ≤ m → p ≤ q → n + p ≤ m + q.
  Proof.
    destruct n, m, p, q; cbn; intuition.
  Defined.

  Definition max_idempotent n : max n n = n.
  Proof.
    destruct n; try reflexivity; cbn.
    now rewrite Z.max_idempotent.
  Defined.

  Lemma eq_max n m k (H : max n m = k) : n = k ∨ m = k.
  Proof.
    destruct n, m; simpl in ×.
    destruct (Z.max_spec z z0); intuition congruence.
    all:intuition.
  Qed.

  Lemma fold_max_In n m l (H : fold_left max l n = m)
    : n = m ∨ In m l.
  Proof.
    revert n H; induction l; cbn; intros n H.
    intuition.
    apply IHl in H.
    apply or_assoc. destruct H; [left|now right].
    now apply eq_max.
  Qed.

  Lemma fold_max_le n m l (H : n ≤ m ∨ Exists (le n) l)
    : n ≤ fold_left max l m.
  Proof.
    revert m H; induction l; cbn in *; intros m [H|H].
    assumption. inversion H.
    eapply IHl. left. apply max_le'; now left.
    eapply IHl. inversion_clear H.
    left. apply max_le'; now right.
    right; assumption.
  Qed.

  Lemma fold_max_le' n m l (H : In n (m :: l))
    : n ≤ fold_left max l m.
  Proof.
    apply fold_max_le. destruct H.
    left; subst; reflexivity.
    right. apply Exists_exists.
    eexists. split. eassumption. reflexivity.
  Qed.

  Lemma le_dec n m : {n ≤ m} + {¬ n ≤ m}.
  Proof.
    destruct n as [n|], m as [m|]; cbn.
    simpl. destruct (n ?= m) eqn:comp. left.
    destruct (Z.compare_spec n m); subst; auto; try lia. discriminate.
    eapply (proj1 (Z.compare_lt_iff _ _)) in comp. left; lia.
    eapply (proj1 (Z.compare_gt_iff _ _)) in comp. right; lia.
    all: intuition.
  Defined.

  Lemma le_lt_dec n m : ({n ≤ m} + {m < n})%nbar.
  Proof.
    destruct n as [n|], m as [m|]; cbn.
    simpl. destruct (n ?= m) eqn:comp. left.
    destruct (Z.compare_spec n m); subst; auto; try lia. discriminate.
    eapply (proj1 (Z.compare_lt_iff _ _)) in comp. left; lia.
    eapply (proj1 (Z.compare_gt_iff _ _)) in comp. right; lia.

    all: (right; constructor) || (left; constructor).
  Defined.

  Lemma le_plus_r n m : (0 ≤ n)%Z → m ≤ Some n + m.
  Proof.
    destruct m; cbn; lia.
  Qed.

  Lemma le_antisymm {n m} : n ≤ m → m ≤ n → n = m.
  Proof.
    destruct n, m; cbn; try easy.
  Qed.

End Nbar.

Import Nbar.

From Stdlib Require Import MSetDecide MSetInterface.

Module WeightedGraph (V : UsualOrderedType) (VSet : MSetInterface.S with Module E := V).
  Module VSetFact := WFactsOn V VSet.
  Module VSetProp := WPropertiesOn V VSet.
  Module VSetDecide := WDecide (VSet).
  Ltac sets := VSetDecide.fsetdec.

  Lemma VSet_add_remove x y p :
    x ≠ y →
    VSet.Equal (VSet.add x (VSet.remove y p)) (VSet.remove y (VSet.add x p)).
  Proof. now sets. Qed.

  Lemma VSet_remove_add x p :
    ¬ VSet.In x p →
    VSet.Equal (VSet.remove x (VSet.add x p)) p.
  Proof. now sets. Qed.

  Lemma VSet_add_add x y p :
    VSet.Equal (VSet.add x (VSet.add y p)) (VSet.add y (VSet.add x p)).
  Proof. now sets. Qed.

  Lemma VSet_add_add_same x p :
    VSet.Equal (VSet.add x (VSet.add x p)) (VSet.add x p).
  Proof. now sets. Qed.

  Definition Disjoint s s' :=
    VSet.Empty (VSet.inter s s').

  Definition DisjointAdd x s s' := VSetProp.Add x s s' ∧ ¬ VSet.In x s.

  Lemma DisjointAdd_add1 {s0 s1 s2 x y}
        (H1 : DisjointAdd x s0 s1) (H2 : DisjointAdd y s1 s2)
    : DisjointAdd x (VSet.add y s0) s2.
  Proof.
    split.
    intro z; split; intro Hz. 2: destruct Hz as [Hz|Hz].
    - apply H2 in Hz. destruct Hz as [Hz|Hz]; [right|].
      now apply VSetFact.add_1.
      apply H1 in Hz. destruct Hz as [Hz|Hz]; [left; assumption|right].
      now apply VSetFact.add_2.
    - apply H2. right; apply H1. now left.
    - apply H2. apply VSet.add_spec in Hz.
      destruct Hz as [Hz|Hz]; [now left|right].
      apply H1. now right.
    - intro Hx. apply VSet.add_spec in Hx.
      destruct Hx as [Hx|Hx].
      subst. apply H2. apply H1. now left.
      now apply H1.
  Qed.

  Lemma DisjointAdd_add2 {s x} (H : ¬ VSet.In x s)
    : DisjointAdd x s (VSet.add x s).
  Proof.
    split. apply VSetProp.Add_add.
    assumption.
  Qed.

  Lemma DisjointAdd_add3 {s0 s1 s2 x y}
        (H1 : DisjointAdd x s0 s1) (H2 : DisjointAdd y s1 s2)
    : DisjointAdd y s0 (VSet.add y s0).
  Proof.
    apply DisjointAdd_add2. intro H.
    unfold DisjointAdd in ×.
    apply H2. apply H1. now right.
  Qed.

  Lemma DisjointAdd_remove {s s' x y} (H : DisjointAdd x s s') (H' : x ≠ y)
    : DisjointAdd x (VSet.remove y s) (VSet.remove y s').
  Proof.
    repeat split. 2: intros [H0|H0].
    - intro H0. apply VSet.remove_spec in H0.
      destruct H0 as [H0 H1].
      pose proof ((H.p1 y0).p1 H0) as H2.
      destruct H2; [now left|right].
      apply VSetFact.remove_2; intuition.
    - subst. apply VSet.remove_spec. split; [|assumption].
      apply H.p1. left; reflexivity.
    - apply VSet.remove_spec in H0; destruct H0 as [H0 H1].
      apply VSet.remove_spec; split; [|assumption].
      apply H.p1. right; assumption.
    - intro H0. apply VSet.remove_spec in H0; destruct H0 as [H0 _].
      apply H; assumption.
  Qed.

  Lemma DisjointAdd_Subset {x s s'}
    : DisjointAdd x s s' → VSet.Subset s s'.
  Proof.
    intros [H _] z Hz. apply H; intuition.
  Qed.

  Lemma DisjointAdd_union {s s' s'' x} (H : DisjointAdd x s s')
    : ¬ VSet.In x s'' → DisjointAdd x (VSet.union s s'') (VSet.union s' s'').
  Proof.
    destruct H as [hadd hin].
    split.
    now eapply VSetProp.union_Add. sets.
  Qed.

  Lemma DisjointAdd_remove1 {s x} (H : VSet.In x s)
    : DisjointAdd x (VSet.remove x s) s.
  Proof.
    split.
    - intro z; split; intro Hz. 2: destruct Hz as [Hz|Hz].
      + destruct (V.eq_dec x z). now left.
        right. now apply VSetFact.remove_2.
      + now subst.
      + eapply VSetFact.remove_3; eassumption.
    - now apply VSetFact.remove_1.
  Qed.

  Global Instance Add_Proper : Proper (eq ==> VSet.Equal ==> VSet.Equal ==> iff) VSetProp.Add.
  Proof.
    intros x y → s0 s1 eq s0' s1' eq'.
    unfold VSetProp.Add. now setoid_rewrite eq; setoid_rewrite eq'.
  Qed.

  Global Instance DisjointAdd_Proper : Proper (eq ==> VSet.Equal ==> VSet.Equal ==> iff) DisjointAdd.
  Proof.
    intros x y → s0 s1 eq s0' s1' eq'.
    unfold DisjointAdd.
    now rewrite eq eq'.
  Qed.

  Lemma Add_In {s x} (H : VSet.In x s)
    : VSetProp.Add x s s.
  Proof.
    split. intuition.
    intros []; try subst; assumption.
  Qed.

  Lemma Add_Add {s s' x} (H : VSetProp.Add x s s')
    : VSetProp.Add x s' s'.
  Proof.
    apply Add_In, H. left; reflexivity.
  Qed.

  Lemma Disjoint_DisjointAdd x s s' s'' :
    DisjointAdd x s s' →
    Disjoint s' s'' →
    Disjoint s s''.
  Proof.
    intros da; unfold Disjoint.
    intros disj i. specialize (disj i).
    intros ininter; apply disj.
    eapply DisjointAdd_Subset in da.
    sets.
  Qed.

  Lemma DisjointAdd_remove_add {x s} :
    DisjointAdd x (VSet.remove x s) (VSet.add x s).
  Proof. split; [intro|]; sets. Qed.

  Lemma DisjointAdd_Equal x s s' s'' : DisjointAdd x s s' → VSet.Equal s' s'' → DisjointAdd x s s''.
  Proof. now intros d <-. Qed.

  Lemma DisjointAdd_Equal_l x s s' s'' : DisjointAdd x s s' → VSet.Equal s s'' → DisjointAdd x s'' s'.
  Proof. now intros d <-. Qed.

  Lemma DisjointAdd_remove_inv {x s s' z} : DisjointAdd x s (VSet.remove z s') →
    VSet.Equal s (VSet.remove z s).
  Proof.
    intros [].
    intros i. rewrite VSet.remove_spec.
    intuition auto. red in H2; subst.
    specialize (proj2 (H z) (or_intror H1)).
    rewrite VSet.remove_spec.
    intuition.
  Qed.

  Module Edge.
    Definition t := (V.t × Z × V.t)%type.
    Definition eq : t → t → Prop := eq.
    Definition eq_equiv : RelationClasses.Equivalence eq := _.

    Definition lt : t → t → Prop :=
      fun '(x, n, y) '(x', n', y') ⇒ (V.lt x x') ∨ (V.eq x x' ∧ n < n')
                                   ∨ (V.eq x x' ∧ n = n' ∧ V.lt y y').
    Definition lt_strorder : StrictOrder lt.
      split.
      - intros [[x n] y] H; cbn in H. intuition.
        all: eapply V.lt_strorder; eassumption.
      - intros [[x1 n1] y1] [[x2 n2] y2] [[x3 n3] y3] H1 H2; cbn in ×.
        pose proof (StrictOrder_Transitive x1 x2 x3) as T1.
        pose proof (StrictOrder_Transitive y1 y2 y3) as T2.
        pose proof (@eq_trans _ n1 n2 n3) as T3.
        unfold VSet.E.lt in ×. unfold V.eq in ×.
        destruct H1 as [H1|[[H1 H1']|[H1 [H1' H1'']]]];
          destruct H2 as [H2|[[H2 H2']|[H2 [H2' H2'']]]]; subst; intuition.
    Qed.
    Definition lt_compat : Proper (Logic.eq ==> Logic.eq ==> iff) lt.
      intros x x' H1 y y' H2. now subst.
    Qed.
    Definition compare : t → t → comparison
      := fun '(x, n, y) '(x', n', y') ⇒ match V.compare x x' with
                                      | Lt ⇒ Lt
                                      | Gt ⇒ Gt
                                      | Eq ⇒ match Z.compare n n' with
                                             | Lt ⇒ Lt
                                             | Gt ⇒ Gt
                                             | Eq ⇒ V.compare y y'
                                             end
                                      end.
    Definition compare_spec :
      ∀ x y : t, CompareSpec (x = y) (lt x y) (lt y x) (compare x y).
      intros [[x1 n1] y1] [[x2 n2] y2]; cbn.
      pose proof (V.compare_spec x1 x2) as H1.
      destruct (V.compare x1 x2); cbn in *; inversion_clear H1.
      2-3: constructor; intuition.
      subst. pose proof (Z.compare_spec n1 n2) as H2.
      destruct (n1 ?= n2); cbn in *; inversion_clear H2.
      2-3: constructor; intuition.
      subst. pose proof (V.compare_spec y1 y2) as H3.
      destruct (V.compare y1 y2); cbn in *; inversion_clear H3;
        constructor; subst; intuition.
    Defined.

    Definition eq_dec : ∀ x y : t, {x = y} + {x ≠ y}.
      unfold eq. decide equality. apply V.eq_dec.
      decide equality. apply Z.eq_dec. apply V.eq_dec.
    Defined.
    Definition eqb : t → t → bool := fun x y ⇒ match compare x y with
                                          | Eq ⇒ true
                                          | _ ⇒ false
                                          end.

    Definition eq_leibniz : ∀ x y, eq x y → x = y := fun x y eq ⇒ eq.

  End Edge.
  Module EdgeSet:= MSetAVL.Make Edge.
  Module EdgeSetFact := WFactsOn Edge EdgeSet.
  Module EdgeSetProp := WPropertiesOn Edge EdgeSet.
  Module EdgeSetDecide := WDecide (EdgeSet).
  Ltac esets := EdgeSetDecide.fsetdec.

  Definition t := (VSet.t × EdgeSet.t × V.t)%type.

  Local Definition V (G : t) := fst (fst G).
  Local Definition E (G : t) := snd (fst G).
  Local Definition s (G : t) := snd G.

  Definition e_source : Edge.t → V.t := fst ∘ fst.
  Definition e_target : Edge.t → V.t := snd.
  Definition e_weight : Edge.t → Z := snd ∘ fst.
  Notation "x ..s" := (e_source x) (at level 3, format "x '..s'").
  Notation "x ..t" := (e_target x) (at level 3, format "x '..t'").
  Notation "x ..w" := (e_weight x) (at level 3, format "x '..w'").

  Definition opp_edge (e : Edge.t) : Edge.t :=
    (e..t, - e..w, e..s).

  Definition labelling := V.t → nat.

  Section graph.
    Context (G : t).

    Definition add_node x : t :=
      (VSet.add x (V G), (E G), (s G)).

    Definition add_edge e : t :=
      (VSet.add e..s (VSet.add e..t (V G)),
      EdgeSet.add e (E G), (s G)).

    Definition EdgeOf x y := ∑ n, EdgeSet.In (x, n, y) (E G).

    Inductive PathOf : V.t → V.t → Type :=
    | pathOf_refl x : PathOf x x
    | pathOf_step x y z : EdgeOf x y → PathOf y z → PathOf x z.

    Arguments pathOf_step {x y z} e p.

    Fixpoint weight {x y} (p : PathOf x y) :=
      match p with
      | pathOf_refl x ⇒ 0
      | pathOf_step e p ⇒ e.π1 + weight p
      end.

    Fixpoint nodes {x y} (p : PathOf x y) : VSet.t :=
      match p with
      | pathOf_refl x ⇒ VSet.empty
      | pathOf_step e p ⇒ VSet.add x (nodes p)
      end.

    Fixpoint concat {x y z} (p : PathOf x y) : PathOf y z → PathOf x z :=
      match p with
      | pathOf_refl _ ⇒ fun q ⇒ q
      | pathOf_step e p ⇒ fun q ⇒ pathOf_step e (concat p q)
      end.

    Fixpoint length {x y} (p : PathOf x y) :=
      match p with
      | pathOf_refl x ⇒ 0
      | pathOf_step e p ⇒ Z.succ (length p)
      end.

    Class invariants := mk_invariant
      { edges_vertices : (* E ⊆ V × V *)
         (∀ e, EdgeSet.In e (E G) → VSet.In e..s (V G) ∧ VSet.In e..t (V G));
        (* s ∈ V *)
        source_vertex : VSet.In (s G) (V G);
        (* s is a source that is lower than any other node *)
        source_pathOf : ∀ x, VSet.In x (V G) → ∥ ∑ p : PathOf (s G) x, ∥ 0 ≤ weight p ∥ ∥ }.

    Definition PosPathOf x y := ∃ p : PathOf x y, weight p > 0.

    Class acyclic_no_loop
      := Build_acyclic_no_loop : ∀ x (p : PathOf x x), weight p ≤ 0.

    Definition acyclic_no_loop' := ∀ x, ¬ (PosPathOf x x).

    Fact acyclic_no_loop_loop' : acyclic_no_loop ↔ acyclic_no_loop'.
    Proof using Type.
      unfold acyclic_no_loop, acyclic_no_loop', PosPathOf.
      split.
      - intros H x [p HH]. specialize (H x p). lia.
      - intros H x p. firstorder.
    Qed.

    Definition correct_labelling (l : labelling) :=
      l (s G) = 0%nat ∧
      ∀ e, EdgeSet.In e (E G) → Z.of_nat (l e..s) + e..w ≤ Z.of_nat (l e..t).

    Definition leq_vertices n x y := ∀ l, correct_labelling l → Z.of_nat (l x) + n ≤ Z.of_nat (l y).

    Inductive SPath : VSet.t → V.t → V.t → Type :=
    | spath_refl s x : SPath s x x
    | spath_step s s' x y z : DisjointAdd x s s' → EdgeOf x y
                               → SPath s y z → SPath s' x z.

    Arguments spath_step {s s' x y z} H e p.
    Derive Signature NoConfusion for SPath.

    (* Global Instance SPath_refl s : CRelationClasses.Reflexive (SPath s) *)
    (*   := spath_refl s. *)

    Fixpoint to_pathOf {s x y} (p : SPath s x y) : PathOf x y :=
      match p with
      | spath_refl _ x ⇒ pathOf_refl x
      | spath_step _ e p ⇒ pathOf_step e (to_pathOf p)
      end.

    Fixpoint sweight {s x y} (p : SPath s x y) :=
      match p with
      | spath_refl _ _ ⇒ 0
      | spath_step _ e p ⇒ e.π1 + sweight p
      end.

    Lemma sweight_weight {s x y} (p : SPath s x y)
      : sweight p = weight (to_pathOf p).
    Proof using Type.
      induction p; cbn; lia.
    Qed.

    Fixpoint is_simple {x y} (p : PathOf x y) :=
      match p with
      | pathOf_refl x ⇒ true
      | @pathOf_step x y z e p ⇒ negb (VSet.mem x (nodes p)) && is_simple p
      end.

    Program Definition to_simple : ∀ {x y} (p : PathOf x y),
        is_simple p = true → SPath (nodes p) x y
      := fix to_simple {x y} p (Hp : is_simple p = true) {struct p} :=
           match
             p in PathOf t t0
             return is_simple p = true → SPath (nodes p) t t0
           with
           | pathOf_refl x ⇒
             fun _ ⇒ spath_refl (nodes (pathOf_refl x)) x
           | @pathOf_step x y z e p0 ⇒
             fun Hp0 ⇒ spath_step _ e (to_simple p0 _)
           end Hp.
    Next Obligation.
      split.
      - eapply VSetProp.Add_add.
      - apply andb_andI in Hp0 as [h1 h2].
        apply negb_true_iff in h1. apply VSetFact.not_mem_iff in h1.
        assumption.
    Defined.

    Lemma weight_concat {x y z} (p : PathOf x y) (q : PathOf y z)
      : weight (concat p q) = weight p + weight q.
    Proof using Type.
      revert q; induction p; intro q; cbn.
      reflexivity. specialize (IHp q); intuition.
    Qed.

    Fixpoint add_end {s x y} (p : SPath s x y)
      : ∀ {z} (e : EdgeOf y z) {s'} (Hs : DisjointAdd y s s'), SPath s' x z
      := match p with
         | spath_refl s x ⇒ fun z e s' Hs ⇒ spath_step Hs e (spath_refl _ _)
         | spath_step H e p
           ⇒ fun z e' s' Hs ⇒ spath_step (DisjointAdd_add1 H Hs) e
                                        (add_end p e' (DisjointAdd_add3 H Hs))
         end.

    Lemma weight_add_end {s x y} (p : SPath s x y) {z e s'} Hs
      : sweight (@add_end s x y p z e s' Hs) = sweight p + e.π1.
    Proof using Type.
      revert z e s' Hs. induction p.
      - intros; cbn; lia.
      - intros; cbn. rewrite IHp; lia.
    Qed.

   (* Fixpoint split {s x y} (p : SPath s x y) *)
   (*   : SPath (VSet.remove y s) x y * ∑ s', SPath s' y y := *)
   (*    match p with *)
   (*    | spath_refl s x => (spath_refl _ x, (VSet.empty; spath_refl _ x)) *)
   (*    | spath_step s s' x0 y0 z0 H e p0 *)
   (*      => match V.eq_dec x0 z0 with *)
   (*        | left pp => (eq_rect _ (SPath _ _) (spath_refl _ _) _ pp, *)
   (*                     (s'; eq_rect _ (fun x => SPath _ x _) *)
   (*                                  (spath_step H e p0) _ pp)) *)
   (*        | right pp => (spath_step (DisjointAdd_remove H pp) e (split p0).1, *)
   (*                      (split p0).2) *)
   (*        end *)
   (*    end. *)

    Definition SPath_sub {s s' x y}
      : VSet.Subset s s' → SPath s x y → SPath s' x y.
    Proof.
      intros Hs p; revert s' Hs; induction p.
      - constructor.
      - intros s'0 Hs. unshelve econstructor.
        exact (VSet.remove x s'0).
        3: eassumption. 2: eapply IHp.
        + split. apply VSetProp.Add_remove.
          apply Hs, d; intuition.
          now apply VSetProp.FM.remove_1.
        + intros u Hu. apply VSetFact.remove_2.
          intro X. apply d. subst; assumption.
          apply Hs, d; intuition.
    Defined.

    Definition weight_SPath_sub {s s' x y} Hs p
      : sweight (@SPath_sub s s' x y Hs p) = sweight p.
    Proof using Type.
      revert s' Hs; induction p; simpl. reflexivity.
      intros s'0 Hs. now rewrite IHp.
    Qed.

    Obligation Tactic := Program.Tactics.program_simpl.
    Program Fixpoint sconcat {s s' x y z} (p : SPath s x y) : Disjoint s s' →
      SPath s' y z → SPath (VSet.union s s') x z :=
      match p in SPath s x y return Disjoint s s' → SPath s' y z → SPath (VSet.union s s') x z with
      | spath_refl _ _ ⇒ fun hin q ⇒ SPath_sub _ q
      | @spath_step s s0 x y z' da e p ⇒ fun hin q ⇒
        @spath_step (VSet.union s s') _ x y z _ e (@sconcat _ _ _ _ _ p _ q)
      end.
    Next Obligation. sets. Qed.
    Next Obligation.
      eapply DisjointAdd_union; eauto.
      destruct da. unfold Disjoint in hin.
      intros inxs'. apply (hin x).
      destruct (H x). specialize (H2 (or_introl eq_refl)).
      now eapply VSet.inter_spec.
    Qed.
    Next Obligation.
      eapply Disjoint_DisjointAdd in hin; eauto.
    Qed.

    Lemma sweight_sconcat {s s' x y z} (p : SPath s x y) (ss' : Disjoint s s')
          (q : SPath s' y z) :
      sweight (sconcat p ss' q) = sweight p + sweight q.
    Proof using Type.
     induction p; cbn.
     1: by apply: weight_SPath_sub.
     rewrite IHp; lia.
    Qed.

    Fixpoint snodes {s x y} (p : SPath s x y) : VSet.t :=
      match p with
      | spath_refl s x ⇒ VSet.empty
      | spath_step H e p ⇒ VSet.add x (snodes p)
      end.

    Definition split {s x y} (p : SPath s x y)
      : ∀ u, {VSet.In u (snodes p)} + {u = y} →
        SPath (VSet.remove u s) x u × SPath s u y.
    Proof.
      induction p; intros u Hu; cbn in ×.
      - induction Hu. eapply False_rect, VSet.empty_spec; eassumption.
        subst. split; constructor.
      - induction (V.eq_dec x u) as [Hx|Hx].
        + split. subst; constructor.
          econstructor; try eassumption; subst; eassumption.
        + assert (Hu' : {VSet.In u (snodes p)} + {u = z}). {
            induction Hu as [Hu|Hu].
            apply (VSetFact.add_3 Hx) in Hu. now left.
            now right. }
          specialize (IHp _ Hu'). split.
          × econstructor. 2: eassumption. 2: exact IHp.1.
            now apply DisjointAdd_remove.
          × eapply SPath_sub. 2: exact IHp.2.
            eapply DisjointAdd_Subset; eassumption.
    Defined.

    Lemma weight_split {s x y} (p : SPath s x y) {u Hu}
      : sweight (split p u Hu).1 + sweight (split p u Hu).2 = sweight p.
    Proof using Type.
      induction p.
      - destruct Hu as [Hu|Hu]. simpl in Hu.
        now exfalso; eapply VSetFact.empty_iff in Hu.
        destruct Hu; reflexivity.
      - simpl. destruct (V.eq_dec x u) as [X|X]; simpl.
        + destruct X; reflexivity.
        + rewrite weight_SPath_sub.
          rewrite <- Z.add_assoc.
          now rewrite IHp.
    Qed.

   (* Fixpoint split {s x y} (p : SPath s x y) *)
   (*   : SPath (VSet.remove y s) x y * SPath s y y := *)
   (*    match p with *)
   (*    | spath_refl s x => (spath_refl _ x, spath_refl _ x) *)
   (*    | spath_step s s' x0 y0 z0 H e p0 *)
   (*      => match V.eq_dec x0 z0 with *)
   (*        | left pp => (eq_rect _ (SPath _ _) (spath_refl _ _) _ pp, *)
   (*                     eq_rect _ (fun x => SPath _ x _) (spath_step H e p0) _ pp) *)
   (*        | right pp => (spath_step (DisjointAdd_remove H pp) e (split p0).1, *)
   (*                      SPath_sub (DisjointAdd_Subset H) (split p0).2) *)
   (*        end *)
   (*    end. *)

   (*  Lemma weight_split {s x y} (p : SPath s x y) *)
   (*    : sweight (split p).1 + sweight (split p).2 = sweight p. *)
   (*  Proof. *)
   (*    induction p. *)
   (*    - reflexivity. *)
   (*    - simpl. destruct (V.eq_dec x z). *)
   (*      + destruct e0; cbn. reflexivity. *)
   (*      + cbn. rewrite weight_SPath_sub; lia. *)
   (*  Qed. *)

    Definition split' {s x y} (p : SPath s x y)
      : SPath (VSet.remove y s) x y × SPath s y y
      := split p y (right eq_refl).

    Lemma weight_split' {s x y} (p : SPath s x y)
      : sweight (split' p).1 + sweight (split' p).2 = sweight p.
    Proof.
      unfold split'; apply weight_split.
    Defined.

    Definition spath_one {s x y k} (Hx : VSet.In x s) (Hk : EdgeSet.In (x, k, y) (E G))
      : SPath s x y.
    Proof.
      econstructor. 3: constructor. now apply DisjointAdd_remove1.
      ∃ k. assumption.
    Defined.

    Lemma simplify_aux1 {s0 s1 s2} (H : VSet.Equal (VSet.union s0 s1) s2)
      : VSet.Subset s0 s2.
    Proof using Type.
      intros x Hx. apply H.
      now apply VSetFact.union_2.
    Qed.

    Lemma simplify_aux2 {s0 x} (Hx : VSet.mem x s0 = true)
          {s1 s2}
          (Hs : VSet.Equal (VSet.union s0 (VSet.add x s1)) s2)
      : VSet.Equal (VSet.union s0 s1) s2.
    Proof using Type.
      apply VSet.mem_spec in Hx.
      etransitivity; [|eassumption].
      intro y; split; intro Hy; apply VSet.union_spec;
        apply VSet.union_spec in Hy; destruct Hy as [Hy|Hy].
      left; assumption.
      right; now apply VSetFact.add_2.
      left; assumption.
      apply VSet.add_spec in Hy; destruct Hy as [Hy|Hy].
      left; red in Hy; subst; assumption.
      right; assumption.
    Qed.

    Lemma simplify_aux3 {s0 s1 s2 x}
          (Hs : VSet.Equal (VSet.union s0 (VSet.add x s1)) s2)
      : VSet.Equal (VSet.union (VSet.add x s0) s1) s2.
    Proof using Type.
      etransitivity; [|eassumption].
      etransitivity. eapply VSetProp.union_add.
      symmetry. etransitivity. apply VSetProp.union_sym.
      etransitivity. eapply VSetProp.union_add.
      apply VSetFact.add_m. reflexivity.
      apply VSetProp.union_sym.
    Qed.

    Fixpoint simplify {s x y} (q : PathOf y x)
      : ∀ (p : SPath s x y) {s'},
        VSet.Equal (VSet.union s (nodes q)) s' → ∑ x', SPath s' x' x' :=
      match q with
      | pathOf_refl x ⇒ fun p s' Hs ⇒ (x; SPath_sub (simplify_aux1 Hs) p)
      | @pathOf_step y y' _ e q ⇒
        fun p s' Hs ⇒ match VSet.mem y s as X return VSet.mem y s = X → _ with
              | true ⇒ fun XX ⇒ let '(p1, p2) := split' p in
                       if 0 <? sweight p2
                       then (y; SPath_sub (simplify_aux1 Hs) p2)
                       else (simplify q (add_end p1 e
                                          (DisjointAdd_remove1 (VSetFact.mem_2 XX)))
                                      (simplify_aux2 XX Hs))
              | false ⇒ fun XX ⇒ (simplify q (add_end p e
                            (DisjointAdd_add2 ((VSetFact.not_mem_iff _ _).p2 XX)))
                                         (simplify_aux3 Hs))
              end eq_refl
      end.

    Lemma weight_simplify {s x y} q (p : SPath s x y)
      : ∀ {s'} Hs, (0 < weight q + sweight p)
        → 0 < sweight (simplify q p (s':=s') Hs).π2.
    Proof using Type.
      revert s p; induction q.
      - cbn; intros. intuition. now rewrite weight_SPath_sub.
      - intros s p s' Hs H; cbn in H. simpl.
        set (F0 := proj2 (VSetFact.not_mem_iff s x)); clearbody F0.
        set (F1 := @VSetFact.mem_2 s x); clearbody F1.
        set (F2 := @simplify_aux2 s x); clearbody F2.
        destruct (VSet.mem x s).
        + case_eq (split' p); intros p1 p2 Hp.
          case_eq (0 <? sweight p2); intro eq.
          × cbn. apply Z.ltb_lt in eq.
            rewrite weight_SPath_sub; lia.
          × eapply IHq. rewrite weight_add_end.
            pose proof (weight_split' p) as X; rewrite Hp in X; cbn in X.
            apply Z.ltb_ge in eq. rewrite <- X in H. lia.
        + eapply IHq. rewrite weight_add_end. lia.
    Qed.

    Definition succs (x : V.t) : list (Z × V.t)
      := let l := List.filter (fun e ⇒ V.eq_dec e..s x) (EdgeSet.elements (E G)) in
         List.map (fun e ⇒ (e..w, e..t)) l.

    (* lsp = longest simple path *)
    (* l is the list of authorized intermediate nodes *)
    (* lsp0 (a::l) x y = max (lsp0 l x y) (lsp0 l x a + lsp0 l a y) *)

    Fixpoint lsp00 fuel (s : VSet.t) (x z : V.t) : Nbar.t :=
      let base := if V.eq_dec x z then Some 0 else None in
      match fuel with
      | 0%nat ⇒ base
      | Datatypes.S fuel ⇒
        match VSet.mem x s with
        | true ⇒
          let ds := List.map
                      (fun '(n, y) ⇒ Some n + lsp00 fuel (VSet.remove x s) y z)%nbar
                      (succs x) in
          List.fold_left Nbar.max ds base
        | false ⇒ base end
      end.

    Definition lsp0 s := lsp00 (VSet.cardinal s) s.

    Lemma lsp0_eq s x z : lsp0 s x z =
      let base := if V.eq_dec x z then Some 0 else None in
      match VSet.mem x s with
      | true ⇒
        let ds := List.map (fun '(n, y) ⇒ Some n + lsp0 (VSet.remove x s) y z)%nbar
                           (succs x) in
        List.fold_left Nbar.max ds base
      | false ⇒ base end.
    Proof using Type.
      unfold lsp0. set (fuel := VSet.cardinal s).
      cut (VSet.cardinal s = fuel); [|reflexivity].
      clearbody fuel. revert s x. induction fuel.
      - intros s x H.
        apply VSetProp.cardinal_inv_1 in H.
        specialize (H x). apply VSetProp.FM.not_mem_iff in H.
        rewrite H. reflexivity.
      - intros s x H. simpl.
        case_eq (VSet.mem x s); [|reflexivity].
        intro HH. f_equal. apply List.map_ext.
        intros [n y].
        assert (H': VSet.cardinal (VSet.remove x s) = fuel);
          [|rewrite H'; reflexivity].
        apply VSet.mem_spec, VSetProp.remove_cardinal_1 in HH.
        lia.
    Qed.

  (* lsp = longest simple path *)
  (* l is the list of authorized intermediate nodes *)
  (* lsp0 (a::l) x y = max (lsp0 l x y) (lsp0 l x a + lsp0 l a y) *)

  Fixpoint lsp00_fast fuel (s : VSet.t) (x z : V.t) : Nbar.t :=
    let base := if V.eq_dec x z then Some 0 else None in
    match fuel with
    | 0%nat ⇒ base
    | Datatypes.S fuel ⇒
      match VSet.mem x s with
      | true ⇒
        let s := VSet.remove x s in
        EdgeSet.fold
          (fun '(src, w, tgt) acc ⇒
            if V.eq_dec src x then
              Nbar.max acc (Some w + lsp00_fast fuel s tgt z)
            else acc)%nbar
           (E G) base
      | false ⇒ base end
    end.

  Lemma fold_left_map {A B C} (f : A → B → A) (g : C → B) l acc : fold_left f (map g l) acc =
    fold_left (fun acc x ⇒ f acc (g x)) l acc.
  Proof using Type.
    induction l in acc |- *; cbn; auto.
  Qed.

  Lemma fold_left_filter {A B} (f : A → B → A) (g : B → bool) l acc : fold_left f (filter g l) acc =
    fold_left (fun acc x ⇒ if g x then f acc x else acc) l acc.
  Proof using Type.
    induction l in acc |- *; cbn; auto.
    destruct (g a) ⇒ //=.
  Qed.

  #[global] Instance fold_left_proper {A B} : Proper (`=2` ==> `=2`) (@fold_left A B).
  Proof using Type.
    intros f g hfg x acc.
    induction x in acc |- × ⇒ //.
    cbn. rewrite (hfg acc a). apply IHx.
  Qed.

  Lemma fold_left_equiv {A B C} (f : A → B → A) (g : A → C → A) (h : C → B) l l' acc :
    (∀ acc x, f acc (h x) = g acc x) →
    l = map h l' →
    fold_left f l acc = fold_left g l' acc.
  Proof using Type.
    intros hfg →.
    induction l' in acc |- *; cbn; auto.
    rewrite fold_left_map. rewrite hfg.
    apply fold_left_proper. exact hfg.
  Qed.

  Lemma lsp00_optim fuel s x z : lsp00_fast fuel s x z = lsp00 fuel s x z.
  Proof using Type.
    induction fuel in s, x, z |- *; auto. simpl.
    destruct VSet.mem ⇒ //.
    rewrite EdgeSet.fold_spec.
    rewrite fold_left_map.
    unfold succs. rewrite fold_left_map.
    rewrite fold_left_filter.
    eapply fold_left_proper ⇒ acc [[src w] tgt]; cbn.
    destruct is_left ⇒ //. f_equal. now rewrite IHfuel.
  Qed.

  Definition lsp_fast := lsp00_fast (VSet.cardinal (V G)) (V G).

    (* Equations lsp0 (s : VSet.t) (x z : V.t) : Nbar.t by wf (VSet.cardinal s) *)
    (*   := *)
    (*   lsp0 s x z := *)
    (*   let base := if V.eq_dec x z then Some 0 else None in *)
    (*   match VSet.mem x s as X return VSet.mem x s = X -> _ with *)
    (*   | true => fun XX => *)
    (*     let ds := List.map (fun '(n, y) => Some n + lsp0 (VSet.remove x s) y z)*)
    (*                        (succs x) in *)
    (*     List.fold_left Nbar.max ds base *)
    (*   | false => fun _ => base end eq_refl. *)
    (* Next Obligation. *)
    (*   apply VSet.mem_spec in XX. *)
    (*   pose proof (VSetProp.remove_cardinal_1 XX). *)
    (*   lia. *)
    (* Defined. *)

    Definition lsp := lsp0 (V G).

    Lemma lsp_optim x y : lsp_fast x y = lsp x y.
    Proof using Type.
      now rewrite /lsp /lsp_fast /lsp0 lsp00_optim.
    Qed.

    Lemma lsp0_VSet_Equal {s s' x y} :
      VSet.Equal s s' → lsp0 s x y = lsp0 s' x y.
    Proof using Type.
      intro H; unfold lsp0; rewrite (VSetProp.Equal_cardinal H).
      set (n := VSet.cardinal s'); clearbody n.
      revert x y s s' H. induction n.
      - reflexivity.
      - cbn. intros x y s s' H. erewrite map_ext.
        erewrite VSetFact.mem_m. 2: reflexivity. 2: eassumption.
        reflexivity.
        intros [m z]; cbn. erewrite IHn.
        reflexivity. now eapply VSetFact.remove_m.
    Qed.

    Lemma lsp0_spec_le {s x y} (p : SPath s x y)
      : (Some (sweight p) ≤ lsp0 s x y)%nbar.
    Proof using Type.
      induction p; rewrite lsp0_eq; simpl.
      - destruct (V.eq_dec x x); [|contradiction].
        destruct (VSet.mem x s0); [|cbn; reflexivity].
        match goal with
        | |- (_ ≤ fold_left ?F _ _)%nbar ⇒
          assert (XX: (∀ l acc, Some 0 ≤ acc → Some 0 ≤ fold_left F l acc)%nbar);
            [|apply XX; cbn; reflexivity]
        end.
        clear; induction l.
        + cbn; trivial.
        + intros acc H; simpl. apply IHl.
          apply max_le'; now left.
      - assert (ee: VSet.mem x s' = true). {
          apply VSet.mem_spec, d. left; reflexivity. }
        rewrite ee. etransitivity.
        eapply (plus_le_compat (Some e.π1) _ (Some (sweight p))).
        reflexivity. eassumption.
        apply Nbar.fold_max_le'.
        right.
        unfold succs. rewrite map_map_compose.
        apply in_map_iff. ∃ (x, e.π1, y). simpl.
        split.
        + cbn -[lsp0].
          assert (XX: VSet.Equal (VSet.remove x s') s0). {
            clear -d.
            intro a; split; intro Ha.
            × apply VSet.remove_spec in Ha. pose proof (d.p1 a).
              intuition. now symmetry in H2.
            × apply VSet.remove_spec. split.
              apply d. right; assumption.
              intro H. apply proj2 in d. apply d.
              red in H; subst; assumption. }
          rewrite (lsp0_VSet_Equal XX); reflexivity.
        + apply filter_In. split.
          apply InA_In_eq, EdgeSet.elements_spec1. exact e.π2.
          cbn. destruct (V.eq_dec x x); [reflexivity|contradiction].
    Qed.

    Lemma lsp0_spec_eq {s x y} n
      : lsp0 s x y = Some n → ∃ p : SPath s x y, sweight p = n.
    Proof using Type.
      set (c := VSet.cardinal s). assert (e: VSet.cardinal s = c) by reflexivity.
      clearbody c; revert s e x y n.
      induction c using Wf_nat.lt_wf_ind.
      rename H into IH.
      intros s e x y n H.
      rewrite lsp0_eq in H; cbn -[lsp0] in H.
      case_eq (VSet.mem x s); intro Hx; rewrite Hx in H.
      - apply fold_max_In in H. destruct H.
        + destruct (V.eq_dec x y); [|discriminate].
          apply some_inj in H; subst.
          unshelve eexists; constructor.
        + apply in_map_iff in H.
          destruct H as [[x' n'] [H1 H2]].
          case_eq (lsp0 (VSet.remove x s) n' y).
          2: intros ee; rewrite ee in H1; discriminate.
          intros nn ee; rewrite ee in H1.
          eapply IH in ee. 3: reflexivity.
          × destruct ee as [p1 Hp1].
            unfold succs in H2.
            apply in_map_iff in H2.
            destruct H2 as [[[x'' n''] y''] [H2 H2']]; cbn in H2.
            inversion H2; subst; clear H2.
            apply filter_In in H2'; destruct H2' as [H2 H2']; cbn in H2'.
            destruct (V.eq_dec x'' x); [subst|discriminate]; clear H2'.
            unshelve eexists. econstructor.
            3: eassumption.
            -- split. 2: apply VSetFact.remove_1; reflexivity.
               apply VSetProp.Add_remove.
               apply VSet.mem_spec; assumption.
            -- eexists.
               apply (EdgeSet.elements_spec1 _ _).p1, InA_In_eq; eassumption.
            -- cbn. now apply some_inj in H1.
          × subst. clear -Hx. apply VSet.mem_spec in Hx.
            apply VSetProp.remove_cardinal_1 in Hx. lia.
      - destruct (V.eq_dec x y); [|discriminate].
        apply some_inj in H; subst. unshelve eexists; constructor.
    Qed.

    Lemma lsp0_spec_eq0 {s x} n
      : lsp0 s x x = Some n → 0 ≤ n.
    Proof using Type.
      intros lspeq.
      generalize (lsp0_spec_le (spath_refl s x)).
      rewrite lspeq. simpl. auto.
    Qed.

    Lemma correct_labelling_PathOf l (Hl : correct_labelling l)
      : ∀ x y (p : PathOf x y), Z.of_nat (l x) + weight p ≤ Z.of_nat (l y).
    Proof using Type.
      induction p. cbn; lia.
      apply proj2 in Hl.
      specialize (Hl (x, e.π1, y) e.π2). cbn in *; lia.
    Qed.

    Lemma correct_labelling_lsp {x y n} (e : lsp x y = Some n) :
      ∀ l, correct_labelling l → Z.of_nat (l x) + n ≤ Z.of_nat (l y).
    Proof using Type.
      eapply lsp0_spec_eq in e as [p Hp].
      intros l Hl; eapply correct_labelling_PathOf with (p:= to_pathOf p) in Hl.
      now rewrite <- sweight_weight, Hp in Hl.
    Qed.

    Lemma acyclic_labelling l : correct_labelling l → acyclic_no_loop.
    Proof using Type.
      intros Hl x p.
      specialize (correct_labelling_PathOf l Hl x x p); lia.
    Qed.

    Lemma lsp0_triangle_inequality {HG : acyclic_no_loop} s x y1 y2 n
          (He : EdgeSet.In (y1, n, y2) (E G))
          (Hy : VSet.In y1 s)
      : (lsp0 s x y1 + Some n ≤ lsp0 s x y2)%nbar.
    Proof using Type.
      case_eq (lsp0 s x y1); [|cbn; trivial].
      intros m Hm.
      apply lsp0_spec_eq in Hm.
      destruct Hm as [p Hp].
      case_eq (split' p).
      intros p1 p2 Hp12.
      pose proof (weight_split' p) as H.
      rewrite Hp12 in H; cbn in H.
      etransitivity.
      2: unshelve eapply (lsp0_spec_le (add_end p1 (n; He) _)).
      subst; rewrite weight_add_end; cbn.
      pose proof (sweight_weight p2) as HH.
      red in HG. specialize (HG _ (to_pathOf p2)). lia.
      now apply DisjointAdd_remove1.
    Qed.

    Definition is_nonpos n :=
      match n with
      | Some z ⇒ (z <=? 0)
      | None ⇒ false
      end.

    Lemma is_nonpos_spec n : is_nonpos n ↔ ∃ z, n = Some z ∧ z ≤ 0.
    Proof using Type.
      unfold is_nonpos.
      split.
      - destruct n; try intuition congruence.
        intros le. eapply Z.leb_le in le. ∃ z; intuition eauto.
      - intros [z [-> le]]. now eapply Z.leb_le.
    Qed.

    Lemma is_nonpos_nbar n : is_nonpos n → (n ≤ Some 0)%nbar.
    Proof using Type.
      now intros [z [-> le]]%is_nonpos_spec.
    Qed.

    Definition lsp0_sub {s s' x y}
      : VSet.Subset s s' → (lsp0 s x y ≤ lsp0 s' x y)%nbar.
    Proof using Type.
      case_eq (lsp0 s x y); [|cbn; trivial].
      intros n Hn Hs.
      apply lsp0_spec_eq in Hn; destruct Hn as [p Hp]; subst.
      rewrite <- (weight_SPath_sub Hs p).
      apply lsp0_spec_le.
    Qed.

    Definition snodes_Subset {s x y} (p : SPath s x y)
      : VSet.Subset (snodes p) s.
    Proof using Type.
      induction p; cbn.
      - apply VSetProp.subset_empty.
      - apply VSetProp.subset_add_3.
        apply d. left; reflexivity.
        etransitivity. eassumption.
        eapply DisjointAdd_Subset; eassumption.
    Qed.

    Definition reduce {s x y} (p : SPath s x y)
      : SPath (snodes p) x y.
    Proof.
      induction p; cbn.
      - constructor.
      - econstructor; try eassumption.
        apply DisjointAdd_add2.
        intro Hx; apply d. eapply snodes_Subset.
        eassumption.
    Defined.

    Definition simplify2 {x z} (p : PathOf x z) : SPath (nodes p) x z.
    Proof.
      induction p; cbn.
      - constructor.
      - case_eq (VSet.mem x (snodes IHp)); intro Hx.
        + apply VSetFact.mem_2 in Hx.
          eapply SPath_sub. 2: exact (split _ _ (left Hx)).2.
          apply VSetProp.subset_add_2; reflexivity.
        + eapply SPath_sub. shelve.
          econstructor. 2: eassumption. 2: exact (reduce IHp).
          eapply DisjointAdd_add2. now apply VSetFact.not_mem_iff.
          Unshelve.
          apply VSetFact.add_s_m. reflexivity.
          apply snodes_Subset.
    Defined.

    Lemma weight_reduce {s x y} (p : SPath s x y)
      : sweight (reduce p) = sweight p.
    Proof using Type.
      induction p; simpl; intuition.
    Qed.

    Opaque split reduce SPath_sub.

    Lemma weight_simplify2 {HG : acyclic_no_loop} {x z} (p : PathOf x z)
      : weight p ≤ sweight (simplify2 p).
    Proof using Type.
      induction p.
      - reflexivity.
      - simpl.
        set (F0 := @VSetFact.mem_2 (snodes (simplify2 p)) x); clearbody F0.
        set (F1 := VSetFact.not_mem_iff (snodes (simplify2 p)) x); clearbody F1.
        destruct (VSet.mem x (snodes (simplify2 p))).
        + rewrite weight_SPath_sub.
          pose proof (@weight_split _ _ _ (simplify2 p))
               x (left (F0 (eq_refl))).
          set (q := split (simplify2 p) x (left (F0 (eq_refl)))) in ×.
          destruct q as [q1 q2]; cbn in ×.
          assert (sweight q1 + e.π1 ≤ 0); [|].
          specialize (HG _ (pathOf_step e (to_pathOf q1))). cbn in HG.
          rewrite <- sweight_weight in HG. lia.
          transitivity (e.π1 + sweight (simplify2 p)); [|lia]. rewrite <- H. lia.
        + rewrite weight_SPath_sub. cbn.
          rewrite weight_reduce; intuition.
    Qed.

    Context {HI : invariants}.

    Lemma nodes_subset {x y} (p : PathOf x y)
      : VSet.Subset (nodes p) (V G).
    Proof using HI.
      induction p; cbn.
      apply VSetProp.subset_empty.
      apply VSetProp.subset_add_3; [|assumption].
      apply (edges_vertices _ e.π2).
    Qed.

    Definition simplify2' {x z} (p : PathOf x z) : SPath (V G) x z.
    Proof using G HI.
      eapply SPath_sub. 2: exact (simplify2 p).
      apply nodes_subset.
    Defined.

    Lemma weight_simplify2' {HG : acyclic_no_loop} {x z} (p : PathOf x z)
      : weight p ≤ sweight (simplify2' p).
    Proof using Type.
      unfold simplify2'.
      unshelve erewrite weight_SPath_sub.
      eapply weight_simplify2.
    Qed.

    Lemma lsp_s {HG : acyclic_no_loop} x (Hx : VSet.In x (V G))
      : ∃ n, lsp (s G) x = Some n ∧ 0 ≤ n.
    Proof using G HI.
      case_eq (lsp (s G) x).
      - intros n H; eexists; split; [reflexivity|].
        destruct (source_pathOf _ Hx) as [[p [w]]].
        pose proof (lsp0_spec_le (simplify2' p)).
        unfold lsp in H. rewrite H in H0.
        simpl in H0.
        transitivity (weight p); auto.
        etransitivity; eauto. eapply weight_simplify2'.
      - intro e.
        destruct (source_pathOf x Hx) as [[p [w]]].
        pose proof (lsp0_spec_le (simplify2' p)) as X.
        unfold lsp in e; rewrite e in X. inversion X.
    Qed.

    Lemma SPath_In {s x y} (p : SPath s x y)
    : sweight p ≠ 0 → VSet.In x s.
    Proof using Type.
      destruct p. simpl. lia.
      intros _. apply d. left; reflexivity.
    Qed.

    Lemma SPath_In' {s x y} (p : SPath s x y) (H : VSet.In x (V G)) :
      VSet.In y (V G).
    Proof using G HI.
      induction p. simpl; auto.
      apply IHp. destruct e.
      now specialize (edges_vertices _ i).
    Qed.

    Lemma PathOf_In {x y} : VSet.In y (V G) → PathOf x y → VSet.In x (V G).
    Proof using G HI.
      intros hin p; induction p; auto.
      destruct e as [? ine].
      now eapply edges_vertices in ine.
    Qed.

    Lemma acyclic_lsp0_xx {HG : acyclic_no_loop} s x
      : lsp0 s x x = Some 0.
    Proof using Type.
      pose proof (lsp0_spec_le (spath_refl s x)) as H; cbn in H.
      case_eq (lsp0 s x x); [|intro e; rewrite e in H; cbn in H; lia].
      intros n Hn.
      pose proof (lsp0_spec_eq0 _ Hn).
      apply lsp0_spec_eq in Hn.
      destruct Hn as [p Hp]. rewrite sweight_weight in Hp.
      red in HG.
      specialize (HG _ (to_pathOf p)). subst n. f_equal. lia.
    Qed.

    (* We don't care about the default value here: lsp is defined everywhere starting from the source. *)
    Definition to_label (z : option Z) :=
      match z with
      | Some (Zpos p) ⇒ Pos.to_nat p
      | _ ⇒ 0%nat
      end.

    Lemma Z_of_to_label (z : Z) :
      Z.of_nat (to_label (Some z)) = if 0 <=? z then z else 0.
    Proof using Type.
      simpl. destruct z; auto. simpl.
      apply Z_of_pos_alt.
    Qed.

    Lemma Z_of_to_label_s {HG : acyclic_no_loop} x :
      VSet.In x (V G) →
      ∃ n, lsp (s G) x = Some n ∧
        0 ≤ n ∧ (Z.of_nat (to_label (lsp (s G) x))) = n.
    Proof using G HI.
      intros inx.
      destruct (lsp_s x inx) as [m [Hm Hpos]].
      rewrite Hm. eexists; split; auto. split; auto.
      rewrite Z_of_to_label.
      eapply Z.leb_le in Hpos. now rewrite Hpos.
    Qed.

    Lemma lsp_correctness {HG : acyclic_no_loop} :
        correct_labelling (fun x ⇒ to_label (lsp (s G) x)).
    Proof using G HI.
      split.
      - unfold lsp. now rewrite acyclic_lsp0_xx.
      - intros [[x n] y] He; cbn.
        simple refine (let H := lsp0_triangle_inequality
                                  (V G) (s G) x y n He _
                       in _); [|clearbody H].
        apply (edges_vertices _ He).
        fold lsp in H. revert H.
        destruct (Z_of_to_label_s x) as [xl [eq [pos ->]]]; rewrite ?eq.
        + apply (edges_vertices _ He).
        + destruct (Z_of_to_label_s y) as [yl [eq' [ylpos ->]]]; rewrite ?eq'.
          × apply (edges_vertices _ He).
          × now simpl.
    Qed.

    Lemma lsp_codistance {HG : acyclic_no_loop} x y z
      : (lsp x y + lsp y z ≤ lsp x z)%nbar.
    Proof using HI.
      case_eq (lsp x y); [|cbn; trivial]. intros n Hn.
      case_eq (lsp y z); [|cbn; trivial]. intros m Hm.
      destruct (lsp0_spec_eq _ Hn) as [p1 Hp1].
      destruct (lsp0_spec_eq _ Hm) as [p2 Hp2].
      pose proof (lsp0_spec_le (simplify2' (concat (to_pathOf p1) (to_pathOf p2))))
        as XX.
      epose proof (weight_simplify2' (concat (to_pathOf p1) (to_pathOf p2))).
      unshelve erewrite weight_concat, <- !sweight_weight in H;
        try assumption.
      cbn in H; erewrite Hp1, Hp2 in H.
      simpl. etransitivity; eauto. simpl. eauto.
    Qed.

    (* The two largest simple pathOf between nodes in both directions bound each other. *)
    Lemma lsp_sym {HG : acyclic_no_loop} {x y n} :
      lsp x y = Some n →
      (lsp y x ≤ Some (-n))%nbar.
    Proof using Type.
      intros Hn.
      destruct (lsp0_spec_eq _ Hn) as [p Hp].
      destruct (lsp y x) eqn:lspyx.
      2:simpl; auto.
      epose proof (lsp0_spec_eq _ lspyx) as [pi Hpi].
      clear Hn lspyx. rewrite -Hp -Hpi /=.
      epose proof (weight_simplify (to_pathOf pi) p (reflexivity _)).
      destruct simplify as [h loop].
      simpl in H.
      move: (HG _ (to_pathOf loop)).
      rewrite -sweight_weight.
      rewrite -sweight_weight Hp Hpi in H.
      rewrite Hp Hpi.
      destruct (Z.ltb 0 (z + n)) eqn:ltb.
      eapply Z.ltb_lt in ltb. specialize (H ltb). lia.
      eapply Z.ltb_nlt in ltb.
      intros wl.
      lia.
    Qed.

    Lemma le_Some_lsp {n x y} : (Some n ≤ lsp x y)%nbar →
      ∃ k, lsp x y = Some k ∧ n ≤ k.
    Proof using Type.
      destruct lsp eqn:xy.
      simpl. intros. eexists; split; eauto.
      simpl; now intros [].
    Qed.

    (* There can be no universe lower than the source: all pathOf to the source have null or
      negative weight. *)
    Lemma source_bottom {HG : acyclic_no_loop} {x} (p : PathOf x (s G)) : weight p ≤ 0.
    Proof using HI.
      unshelve epose proof (PathOf_In _ p).
      eapply source_vertex.
      destruct (lsp_s _ H) as [lx [lsx w]].
      etransitivity; [apply (weight_simplify2' p)|].
      set (sp := simplify2' p).
      epose proof (lsp0_spec_le sp).
      eapply le_Some_lsp in H0 as [xs [lxs wxs]].
      generalize (lsp_codistance x (s G) x).
      rewrite lxs lsx /lsp acyclic_lsp0_xx /=. lia.
    Qed.

    Lemma lsp_to_s {HG : acyclic_no_loop} {x} (Hx : VSet.In x (V G)) {n}
      : lsp x (s G) = Some n → n ≤ 0.
    Proof using HI.
      case_eq (lsp x (s G)).
      - intros z H [= <-].
        destruct (lsp0_spec_eq _ H).
        pose proof (source_bottom (to_pathOf x0)).
        rewrite <- sweight_weight in H1. congruence.
      - intro e. discriminate.
    Qed.

    Lemma lsp_xx_acyclic
      : VSet.For_all (fun x ⇒ lsp x x = Some 0) (V G) → acyclic_no_loop'.
    Proof using G HI.
      intros H. intros x [p Hp]. assert (hw: 0 < weight p + sweight ((spath_refl (V G) x))) by (simpl; lia).
      simple refine (let Hq := weight_simplify p (spath_refl (V G) _)
                                               _ hw
                     in _).
      + exact (V G).
      + etransitivity. apply VSetProp.union_sym.
        etransitivity. apply VSetProp.union_subset_equal.
        apply nodes_subset. reflexivity.
      + match goal with
        | _ : 0 < sweight ?qq.π2 |- _ ⇒ set (q := qq) in *; clearbody Hq
        end.
        destruct q as [x' q]; cbn in Hq.
        assert (Some (sweight q) ≤ Some 0)%nbar. {
          erewrite <- H. eapply lsp0_spec_le.
          eapply (SPath_In q). lia. }
        cbn in H0; lia.
    Defined.

    Lemma VSet_Forall_reflect P f (Hf : ∀ x, reflect (P x) (f x)) s
      : reflect (VSet.For_all P s) (VSet.for_all f s).
    Proof using G HI.
      apply iff_reflect. etransitivity.
      2: apply VSetFact.for_all_iff.
      2: intros x y []; reflexivity.
      apply iff_forall; intro x.
      apply iff_forall; intro Hx.
      now apply reflect_iff.
    Qed.

    Lemma reflect_logically_equiv {A B} (H : A ↔ B) f
      : reflect B f → reflect A f.
    Proof using Type.
      destruct 1; constructor; intuition.
    Qed.

    Definition is_acyclic := VSet.for_all (fun x ⇒ match lsp x x with
                                                 | Some 0 ⇒ true
                                                 | _ ⇒ false
                                                 end) (V G).