Types/functions for DAG?

Stream: new members

[aron]

I have a list of items that can reference other items by their index in the list, this effectively constitutes a directed graph. I need to ensure that this graph is acyclic though. Are there any modules or types in Mathlib that can help me do so? Either statically or at runtime?

Otherwise the way I would go about this is using an algorithm to find all strongly connected components of this graph and if all components have exactly one item in that would constitute a proof that the graph is acyclic. This is probably going to be quite tedious to create a proof out of.

[Marcus Rossel]

Could you post your current definition? My first thought would be to require that the edge relation's transitive closure is irreflexive, which is equivalent to being acyclic.

[aron]

Here's a simplified example of my code:

section Vec
inductive Vec (α : Type u) : (len : Nat) → Type u
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n+1)

def Vec.mem [DecidableEq α] (vec : Vec α n) (item : α) : Prop :=
  match vec with
  | .nil => False
  | .cons head tail => if head = item then True else mem tail item

instance [DecidableEq α] : Membership α (Vec α n) where mem := Vec.mem

@[reducible,simp] def Vec.get (vec : Vec α n) (index : Fin n) : α :=
  match vec, index with
  | .cons head tail, ⟨ 0, _ ⟩ => head
  | .cons head tail, ⟨ n+1, isLt ⟩ => by refine tail.get ⟨ n, ?_ ⟩; exact Nat.succ_lt_succ_iff.mp isLt

@[simp,reducible] instance : GetElem (Vec α n) (Fin n) α (valid := fun _ _ => True) where getElem as i _ := as.get i
end Vec



/-- Is either an `a`, `b`, a ref to one different node, or to two different nodes -/
inductive Node (n : Nat)
  | a : Node n
  | b : Node n
  | ref : Fin n → Node n
  | refTwo : Fin n → Fin n → Node n
  deriving DecidableEq

/-- The graph type -/
abbrev Graph len := Vec (Node len) len

/-- Proposition that a given node doesn't point to an index `i`, even across other nodes -/
inductive NodeDoesntPointTo (vec : Graph len) : Node len → (i : Fin len) → Prop
  | a : NodeDoesntPointTo vec .a i
  | b : NodeDoesntPointTo vec .b i
  | ref :
    (i j : Fin len) →
    i ≠ j →
    NodeDoesntPointTo vec vec[j] i →
    NodeDoesntPointTo vec (.ref j) i
  | refTwo :
    (i j k : Fin len) →
    i ≠ j →
    i ≠ k →
    NodeDoesntPointTo vec vec[j] i →
    NodeDoesntPointTo vec vec[k] i →
    NodeDoesntPointTo vec (.refTwo j k) i

/-- Prop that an entire graph is acyclic -/
def IsAcyclic {len} (vec : Graph len) :=
  ∀ node ∈ vec, ∀ i, NodeDoesntPointTo vec node i

[Johannes Tantow]

I have used the following definition for dags in one of my programs.

import Mathlib

abbrev OrderedGraph {A: Type} :=
  { arr : Array (A × List ℕ) // ∀ i : Fin arr.size, ∀ j ∈ arr[i].snd, j < i }

[Johannes Tantow]

But I only went through the graph once to check it (it was a proof graph). If you do more stuff, a hashmap might be better so that you find your elements faster.