Library MetaCoq.Checker.wGraph

Notation "p .1" := (fst p)
  (at level 2, left associativity, format "p .1") : pair_scope.
Notation "p .2" := (snd p)
  (at level 2, left associativity, format "p .2") : pair_scope.
Notation "p ..1" := (proj1 p)
  (at level 2, left associativity, format "p ..1") : pair_scope.
Notation "p ..2" := (proj2 p)
  (at level 2, left associativity, format "p ..2") : pair_scope.
Coercion is_left A B (u : {A} + {B}) := match u with left _ ⇒ true | _ ⇒ false end.

Definition fst_eq {A B} {x x' : A} {y y' : B}
  : (x, y) = (x', y') → x = x'.

Definition snd_eq {A B} {x x' : A} {y y' : B}
  : (x, y) = (x', y') → y = y'.

Lemma InAeq_In {A} (l : list A) x :
  InA eq x l ↔ In x l.

Lemma fold_max_In n m l (H : fold_left max l n = m)
  : n = m ∨ In m l.

Lemma fold_max_le n m l (H : n ≤ m ∨ Exists (Peano.le n) l)
  : n ≤ fold_left Nat.max l m.

Lemma fold_max_le' n m l (H : In n (m :: l))
  : n ≤ fold_left Nat.max l m.


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

Module Nbar.
  Definition t := option nat.
  Definition max (n m : t) : t :=
    match n, m with
    | Some n, Some m ⇒ Some (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 le (n m : t) : Prop :=
    match n, m with
    | Some n, Some m ⇒ n ≤ m
    | Some _, None ⇒ False
    | None, _ ⇒ True
    end.


  Infix "+" := add : nbar_scope.
  Infix "≤" := le : nbar_scope.


  Instance le_refl : Reflexive le.

  Instance le_trans : Transitive le.




  Definition add_assoc n m p : n + (m + p) = n + m + p.

  Definition add_0_r n : (n + Some 0 = n)%nbar.

  Definition max_lub n m p : n ≤ p → m ≤ p → max n m ≤ p.

  Definition add_max_distr_r n m p : max (n + p) (m + p) = max n m + p.

  Definition max_le' n m p : p ≤ n ∨ p ≤ m → p ≤ max n m.

  Definition plus_le_compat_l n m p : n ≤ m → p + n ≤ p + m.

  Definition plus_le_compat n m p q : n ≤ m → p ≤ q → n + p ≤ m + q.

  Definition max_idempotent n : max n n = n.

  Lemma eq_max n m k (H : max n m = k) : n = k ∨ m = k.

  Lemma fold_max_In n m l (H : fold_left max l n = m)
    : n = m ∨ In m l.

  Lemma fold_max_le n m l (H : n ≤ m ∨ Exists (le n) l)
    : n ≤ fold_left max l m.

  Lemma fold_max_le' n m l (H : In n (m :: l))
    : n ≤ fold_left max l m.

  Lemma le_dec n m : {n ≤ m} + {¬ n ≤ m}.

  Lemma le_plus_r n m : m ≤ Some n + m.

End Nbar.


Module WeightedGraph (V : UsualOrderedType).
  Module VSet := MSetList.Make V.
  Module VSetFact := WFactsOn V VSet.
  Module VSetProp := WPropertiesOn V VSet.
  Module Edge.
    Definition t := (V.t × nat × 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.
    Qed.
    Definition lt_compat : Proper (Logic.eq ==> Logic.eq ==> iff) lt.
    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 PeanoNat.Nat.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).
    Defined.

    Definition eq_dec : ∀ x y : t, {x = y} + {x ≠ y}.
    Defined.
    Definition eqb : t → t → bool := fun x y ⇒ match compare x y with
                                          | Eq ⇒ true
                                          | _ ⇒ false
                                          end.
  End Edge.
  Module EdgeSet:= MSets.MSetList.Make Edge.
  Module EdgeSetFact := WFactsOn Edge EdgeSet.
  Module EdgeSetProp := WPropertiesOn Edge EdgeSet.

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


  Definition e_source : Edge.t → V.t := fst ∘ fst.
  Definition e_target : Edge.t → V.t := snd.
  Definition e_weight : Edge.t → nat := 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 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 Edges x y := ∑ n, EdgeSet.In (x, n, y) (E G).

    Inductive Paths : V.t → V.t → Type :=
    | paths_refl x : Paths x x
    | paths_step x y z : Edges x y → Paths y z → Paths x z.


    Fixpoint weight {x y} (p : Paths x y) :=
      match p with
      | paths_refl x ⇒ 0
      | paths_step x y z e p ⇒ e.π1 + weight p
      end.

    Fixpoint nodes {x y} (p : Paths x y) : VSet.t :=
      match p with
      | paths_refl x ⇒ VSet.empty
      | paths_step x y z e p ⇒ VSet.add x (nodes p)
      end.

    Fixpoint concat {x y z} (p : Paths x y) : Paths y z → Paths x z :=
      match p with
      | paths_refl _ ⇒ fun q ⇒ q
      | paths_step _ _ _ e p ⇒ fun q ⇒ paths_step e (concat p q)
      end.

    Fixpoint length {x y} (p : Paths x y) :=
      match p with
      | paths_refl x ⇒ 0
      | paths_step x y z e p ⇒ S (length p)
      end.


    Class invariants := mk_invariant :
      
      (∀ e, EdgeSet.In e (E G) → VSet.In e..s (V G) ∧ VSet.In e..t (V G))
      
      ∧ VSet.In (s G) (V G)
      
      ∧ (∀ x, VSet.In x (V G) → ∥ Paths (s G) x ∥).

    Context {HI : invariants}.

    Definition PosPaths x y := ∃ p : Paths x y, weight p > 0.

    Definition acyclic_no_loop := ∀ x (p : Paths x x), weight p = 0.

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

    Fact acyclic_no_loop_loop' : acyclic_no_loop ↔ acyclic_no_loop'.

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

    Definition leq_vertices n x y := ∀ l, correct_labelling l → l x + n ≤ l y.

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

    Inductive SimplePaths : VSet.t → V.t → V.t → Type :=
    | spaths_refl s x : SimplePaths s x x
    | spaths_step s s' x y z : DisjointAdd x s s' → Edges x y
                               → SimplePaths s y z → SimplePaths s' x z.



    Fixpoint to_paths {s x y} (p : SimplePaths s x y) : Paths x y :=
      match p with
      | spaths_refl _ x ⇒ paths_refl x
      | spaths_step _ _ x y z _ e p ⇒ paths_step e (to_paths p)
      end.

    Fixpoint sweight {s x y} (p : SimplePaths s x y) :=
      match p with
      | spaths_refl _ _ ⇒ 0
      | spaths_step _ _ x y z _ e p ⇒ e.π1 + sweight p
      end.

    Lemma sweight_weight {s x y} (p : SimplePaths s x y)
      : sweight p = weight (to_paths p).

    Fixpoint is_simple {x y} (p : Paths x y) :=
      match p with
      | paths_refl x ⇒ true
      | paths_step x y z e p ⇒ negb (VSet.mem x (nodes p)) && is_simple p
      end.

    Program Fixpoint to_simple {x y} (p : Paths x y) (Hp : is_simple p = true)
            {struct p} : SimplePaths (nodes p) x y :=
      match p with
      | paths_refl x ⇒ spaths_refl _ _
      | paths_step x y z e p ⇒ spaths_step _ e (to_simple p _)
      end.

    Lemma weight_concat {x y z} (p : Paths x y) (q : Paths y z)
      : weight (concat p q) = weight p + weight q.


    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.

    Lemma DisjointAdd_add2 {s x} (H : ¬ VSet.In x s)
      : DisjointAdd x s (VSet.add x s).

    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).

    Fixpoint add_end {s x y} (p : SimplePaths s x y)
      : ∀ {z} (e : Edges y z) {s'} (Hs : DisjointAdd y s s'), SimplePaths s' x z
      := match p with
         | spaths_refl s x ⇒ fun z e s' Hs ⇒ spaths_step Hs e (spaths_refl _ _)
         | spaths_step s0 s x x0 y H e p
           ⇒ fun z e' s' Hs ⇒ spaths_step (DisjointAdd_add1 H Hs) e
                                        (add_end p e' (DisjointAdd_add3 H Hs))
         end.

    Lemma weight_add_end {s x y} (p : SimplePaths s x y) {z e s'} Hs
      : sweight (@add_end s x y p z e s' Hs) = sweight p + e.π1.

    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').


    Definition SimplePaths_sub {s s' x y}
      : VSet.Subset s s' → SimplePaths s x y → SimplePaths s' x y.

    Definition weight_SimplePaths_sub {s s' x y} Hs p
      : sweight (@SimplePaths_sub s s' x y Hs p) = sweight p.

    Lemma DisjointAdd_Subset {x s s'}
      : DisjointAdd x s s' → VSet.Subset s s'.

    Fixpoint snodes {s x y} (p : SimplePaths s x y) : VSet.t :=
      match p with
      | spaths_refl s x ⇒ VSet.empty
      | spaths_step s s' x y z H e p ⇒ VSet.add x (snodes p)
      end.

    Definition split {s x y} (p : SimplePaths s x y)
      : ∀ u, {VSet.In u (snodes p)} + {u = y}
             → SimplePaths (VSet.remove u s) x u × SimplePaths s u y.

    Lemma weight_split {s x y} (p : SimplePaths s x y) {u Hu}
      : sweight (split p u Hu).1 + sweight (split p u Hu).2 = sweight p.



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

    Lemma weight_split' {s x y} (p : SimplePaths s x y)
      : sweight (split' p).1 + sweight (split' p).2 = sweight p.

    Lemma DisjointAdd_remove1 {s x} (H : VSet.In x s)
      : DisjointAdd x (VSet.remove x s) s.

    Lemma Add_In {s x} (H : VSet.In x s)
      : VSetProp.Add x s s.

    Lemma Add_Add {s s' x} (H : VSetProp.Add x s s')
      : VSetProp.Add x s' s'.

    Lemma simplify_aux1 {s0 s1 s2} (H : VSet.Equal (VSet.union s0 s1) s2)
      : VSet.Subset s0 s2.

    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.

    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.

    Fixpoint simplify {s x y} (q : Paths y x)
      : ∀ (p : SimplePaths s x y) {s'},
        VSet.Equal (VSet.union s (nodes q)) s' → ∑ x', SimplePaths s' x' x' :=
      match q with
      | paths_refl x ⇒ fun p s' Hs ⇒ (x; SimplePaths_sub (simplify_aux1 Hs) p)
      | paths_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; SimplePaths_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 _ _)..2 XX)))
                                         (simplify_aux3 Hs))
              end eq_refl
      end.



    Lemma weight_simplify {s x y} q (p : SimplePaths s x y)
      : ∀ {s'} Hs, 0 < weight q ∨ 0 < sweight p
        → 0 < sweight (simplify q p (s':=s') Hs).π2.

    Definition succs (x : V.t) : list (nat × 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.


    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 ⇒ base
      | 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.



    Definition lsp := lsp0 (V G).

    Lemma lsp0_VSet_Equal {s s' x y} :
      VSet.Equal s s' → lsp0 s x y = lsp0 s' x y.

    Lemma lsp0_spec_le {s x y} (p : SimplePaths s x y)
      : (Some (sweight p) ≤ lsp0 s x y)%nbar.

    Lemma lsp0_spec_eq {s x y} n
      : lsp0 s x y = Some n → ∃ p : SimplePaths s x y, sweight p = n.

    Lemma correct_labelling_Paths l (Hl : correct_labelling l)
      : ∀ x y (p : Paths x y), l x + weight p ≤ l y.

    Lemma acyclic_labelling l : correct_labelling l → acyclic_no_loop.

    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.

    Lemma acyclic_lsp0_xx {HG : acyclic_no_loop} s x
      : lsp0 s x x = Some 0.

    Definition lsp0_sub {s s' x y}
      : VSet.Subset s s' → (lsp0 s x y ≤ lsp0 s' x y)%nbar.

    Definition snodes_Subset {s x y} (p : SimplePaths s x y)
      : VSet.Subset (snodes p) s.

    Definition reduce {s x y} (p : SimplePaths s x y)
      : SimplePaths (snodes p) x y.

    Definition simplify2 {x z} (p : Paths x z) : SimplePaths (nodes p) x z.

    Lemma weight_reduce {s x y} (p : SimplePaths s x y)
      : sweight (reduce p) = sweight p.

    Lemma weight_simplify2 {HG : acyclic_no_loop} {x z} (p : Paths x z)
      : sweight (simplify2 p) = weight p.

    Lemma nodes_subset {x y} (p : Paths x y)
      : VSet.Subset (nodes p) (V G).

    Definition simplify2' {x z} (p : Paths x z) : SimplePaths (V G) x z.

    Lemma weight_simplify2' {HG : acyclic_no_loop} {x z} (p : Paths x z)
      : sweight (simplify2' p) = weight p.

    Lemma lsp_s x (Hx : VSet.In x (V G))
      : ∃ n, lsp (s G) x = Some n.

    Lemma lsp_correctness {HG : acyclic_no_loop} :
        correct_labelling (fun x ⇒ option_get 0 (lsp (s G) x)).

    Lemma SimplePaths_In {s x y} (p : SimplePaths s x y)
      : sweight p > 0 → VSet.In x s.

    Lemma lsp_codistance {HG : acyclic_no_loop} x y z
      : (lsp x y + lsp y z ≤ lsp x z)%nbar.

    Lemma lsp_xx_acyclic
      : VSet.For_all (fun x ⇒ lsp x x = Some 0) (V G) → acyclic_no_loop'.

    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).

    Lemma reflect_logically_equiv {A B} (H : A ↔ B) f
      : reflect B f → reflect A f.

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

    Lemma acyclic_caract1
      : acyclic_no_loop ↔ ∃ l, correct_labelling l.

    Lemma acyclic_caract2 :
      acyclic_no_loop ↔ (VSet.For_all (fun x ⇒ lsp x x = Some 0) (V G)).


    Lemma is_acyclic_spec : is_acyclic ↔ acyclic_no_loop.

  End graph.

  Section graph2.
    Context (G : t) {HI : invariants G} {HG : acyclic_no_loop G}.

    Section subgraph.
      Context (n : nat) {x_0 y_0 : V.t} (Vx : VSet.In x_0 (V G))
              (Vy : VSet.In y_0 (V G)) (kx ky : nat)
              (Hkx : lsp G (s G) x_0 = Some kx)
              (Hky : lsp G (s G) y_0 = Some ky)
              (Hle : leq_vertices G n x_0 y_0)
              (p_0 : SimplePaths G (V G) (s G) y_0)
              (Hp_0 : lsp G (s G) y_0 = Some (sweight G p_0))
              (Hxs : lsp G x_0 (s G) = None)
              (Hx_0_0 : VSet.mem x_0 (snodes G p_0) = false).

      Definition K := Peano.max kx (S ky).

      Let G' : t
        := (V G, EdgeSet.add (s G, K, x_0) (E G), s G).

      Definition to_G' {u v} (q : Paths G u v) : Paths G' u v.


      Definition from_G' {S u v} (q : SimplePaths G' S u v)
        : SimplePaths G S u v + (SimplePaths G S u (s G) × SimplePaths G S x_0 v).


      Lemma from_G'_weight {S u v} (q : SimplePaths G' S u v)
        : sweight q = match from_G' q with
                      | inl q' ⇒ sweight q'
                      | inr (q1, q2) ⇒ sweight q1 + K + sweight q2
                      end.


      Lemma lsp_xy_le_n : (Some n ≤ lsp G x_0 y_0)%nbar.

    End subgraph.

    Lemma leq_vertices_caract0 {n x y} (Vy : VSet.In y (V G)) :
      leq_vertices G n x y ↔ (Some n ≤ lsp G x y)%nbar.

    Lemma leq_vertices_caract {n x y} :
      leq_vertices G n x y ↔ (if VSet.mem y (V G) then Some n ≤ lsp G x y
                             else n = 0 ∧ (x = y ∨ Some 0 ≤ lsp G x (s G)))%nbar.

    Definition leqb_vertices n x y : bool :=
      if VSet.mem y (V G) then le_dec (Some n) (lsp G x y)
      else Nat.eqb n 0 && (V.eq_dec x y || le_dec (Some 0) (lsp G x (s G))).

    Lemma leqb_vertices_correct n x y
      : leq_vertices G n x y ↔ leqb_vertices n x y.

  End graph2.
End WeightedGraph.